[GOAL]
R : Type u
inst✝¹ : CommSemiring R
S : Type v
inst✝ : CommSemiring S
p q : ℕ
f : R[X]
⊢ ↑(expand R p) f = sum f fun e a => ↑C a * (X ^ p) ^ e
[PROOFSTEP]
simp [expand, eval₂]
[GOAL]
R : Type u
inst✝¹ : CommSemiring R
S : Type v
inst✝ : CommSemiring S
p q : ℕ
r : R
⊢ ↑(expand R p) (↑(monomial q) r) = ↑(monomial (q * p)) r
[PROOFSTEP]
simp_rw [← smul_X_eq_monomial, AlgHom.map_smul, AlgHom.map_pow, expand_X, mul_comm, pow_mul]
[GOAL]
R : Type u
inst✝¹ : CommSemiring R
S : Type v
inst✝ : CommSemiring S
p q : ℕ
f : R[X]
r : R
⊢ ↑(expand R p) (↑(expand R q) (↑C r)) = ↑(expand R (p * q)) (↑C r)
[PROOFSTEP]
simp_rw [expand_C]
[GOAL]
R : Type u
inst✝¹ : CommSemiring R
S : Type v
inst✝ : CommSemiring S
p q : ℕ
f✝ f g : R[X]
ihf : ↑(expand R p) (↑(expand R q) f) = ↑(expand R (p * q)) f
ihg : ↑(expand R p) (↑(expand R q) g) = ↑(expand R (p * q)) g
⊢ ↑(expand R p) (↑(expand R q) (f + g)) = ↑(expand R (p * q)) (f + g)
[PROOFSTEP]
simp_rw [AlgHom.map_add, ihf, ihg]
[GOAL]
R : Type u
inst✝¹ : CommSemiring R
S : Type v
inst✝ : CommSemiring S
p q : ℕ
f : R[X]
n : ℕ
r : R
x✝ : ↑(expand R p) (↑(expand R q) (↑C r * X ^ n)) = ↑(expand R (p * q)) (↑C r * X ^ n)
⊢ ↑(expand R p) (↑(expand R q) (↑C r * X ^ (n + 1))) = ↑(expand R (p * q)) (↑C r * X ^ (n + 1))
[PROOFSTEP]
simp_rw [AlgHom.map_mul, expand_C, AlgHom.map_pow, expand_X, AlgHom.map_pow, expand_X, pow_mul]
[GOAL]
R : Type u
inst✝¹ : CommSemiring R
S : Type v
inst✝ : CommSemiring S
p q : ℕ
f : R[X]
⊢ ↑(expand R 0) f = ↑C (eval 1 f)
[PROOFSTEP]
simp [expand]
[GOAL]
R : Type u
inst✝¹ : CommSemiring R
S : Type v
inst✝ : CommSemiring S
p q : ℕ
f : R[X]
r : R
⊢ ↑(expand R 1) (↑C r) = ↑C r
[PROOFSTEP]
rw [expand_C]
[GOAL]
R : Type u
inst✝¹ : CommSemiring R
S : Type v
inst✝ : CommSemiring S
p q : ℕ
f✝ f g : R[X]
ihf : ↑(expand R 1) f = f
ihg : ↑(expand R 1) g = g
⊢ ↑(expand R 1) (f + g) = f + g
[PROOFSTEP]
rw [AlgHom.map_add, ihf, ihg]
[GOAL]
R : Type u
inst✝¹ : CommSemiring R
S : Type v
inst✝ : CommSemiring S
p q : ℕ
f : R[X]
n : ℕ
r : R
x✝ : ↑(expand R 1) (↑C r * X ^ n) = ↑C r * X ^ n
⊢ ↑(expand R 1) (↑C r * X ^ (n + 1)) = ↑C r * X ^ (n + 1)
[PROOFSTEP]
rw [AlgHom.map_mul, expand_C, AlgHom.map_pow, expand_X, pow_one]
[GOAL]
R : Type u
inst✝¹ : CommSemiring R
S : Type v
inst✝ : CommSemiring S
p q : ℕ
f : R[X]
⊢ ↑(expand R (p ^ Nat.zero)) f = (↑(expand R p))^[Nat.zero] f
[PROOFSTEP]
rw [pow_zero, expand_one, Function.iterate_zero, id]
[GOAL]
R : Type u
inst✝¹ : CommSemiring R
S : Type v
inst✝ : CommSemiring S
p q : ℕ
f : R[X]
n : ℕ
ih : ↑(expand R (p ^ n)) f = (↑(expand R p))^[n] f
⊢ ↑(expand R (p ^ Nat.succ n)) f = (↑(expand R p))^[Nat.succ n] f
[PROOFSTEP]
rw [Function.iterate_succ_apply', pow_succ, expand_mul, ih]
[GOAL]
R : Type u
inst✝¹ : CommSemiring R
S : Type v
inst✝ : CommSemiring S
p q : ℕ
f : R[X]
⊢ ↑derivative (↑(expand R p) f) = ↑(expand R p) (↑derivative f) * (↑p * X ^ (p - 1))
[PROOFSTEP]
rw [coe_expand, derivative_eval₂_C, derivative_pow, C_eq_nat_cast, derivative_X, mul_one]
[GOAL]
R : Type u
inst✝¹ : CommSemiring R
S : Type v
inst✝ : CommSemiring S
p✝ q p : ℕ
hp : 0 < p
f : R[X]
n : ℕ
⊢ coeff (↑(expand R p) f) n = if p ∣ n then coeff f (n / p) else 0
[PROOFSTEP]
simp only [expand_eq_sum]
[GOAL]
R : Type u
inst✝¹ : CommSemiring R
S : Type v
inst✝ : CommSemiring S
p✝ q p : ℕ
hp : 0 < p
f : R[X]
n : ℕ
⊢ coeff (sum f fun e a => ↑C a * (X ^ p) ^ e) n = if p ∣ n then coeff f (n / p) else 0
[PROOFSTEP]
simp_rw [coeff_sum, ← pow_mul, C_mul_X_pow_eq_monomial, coeff_monomial, sum]
[GOAL]
R : Type u
inst✝¹ : CommSemiring R
S : Type v
inst✝ : CommSemiring S
p✝ q p : ℕ
hp : 0 < p
f : R[X]
n : ℕ
⊢ (∑ x in support f, if p * x = n then coeff f x else 0) = if p ∣ n then coeff f (n / p) else 0
[PROOFSTEP]
split_ifs with h
[GOAL]
case pos
R : Type u
inst✝¹ : CommSemiring R
S : Type v
inst✝ : CommSemiring S
p✝ q p : ℕ
hp : 0 < p
f : R[X]
n : ℕ
h : p ∣ n
⊢ (∑ x in support f, if p * x = n then coeff f x else 0) = coeff f (n / p)
[PROOFSTEP]
rw [Finset.sum_eq_single (n / p), Nat.mul_div_cancel' h, if_pos rfl]
[GOAL]
case pos.h₀
R : Type u
inst✝¹ : CommSemiring R
S : Type v
inst✝ : CommSemiring S
p✝ q p : ℕ
hp : 0 < p
f : R[X]
n : ℕ
h : p ∣ n
⊢ ∀ (b : ℕ), b ∈ support f → b ≠ n / p → (if p * b = n then coeff f b else 0) = 0
[PROOFSTEP]
intro b _ hb2
[GOAL]
case pos.h₀
R : Type u
inst✝¹ : CommSemiring R
S : Type v
inst✝ : CommSemiring S
p✝ q p : ℕ
hp : 0 < p
f : R[X]
n : ℕ
h : p ∣ n
b : ℕ
a✝ : b ∈ support f
hb2 : b ≠ n / p
⊢ (if p * b = n then coeff f b else 0) = 0
[PROOFSTEP]
rw [if_neg]
[GOAL]
case pos.h₀.hnc
R : Type u
inst✝¹ : CommSemiring R
S : Type v
inst✝ : CommSemiring S
p✝ q p : ℕ
hp : 0 < p
f : R[X]
n : ℕ
h : p ∣ n
b : ℕ
a✝ : b ∈ support f
hb2 : b ≠ n / p
⊢ ¬p * b = n
[PROOFSTEP]
intro hb3
[GOAL]
case pos.h₀.hnc
R : Type u
inst✝¹ : CommSemiring R
S : Type v
inst✝ : CommSemiring S
p✝ q p : ℕ
hp : 0 < p
f : R[X]
n : ℕ
h : p ∣ n
b : ℕ
a✝ : b ∈ support f
hb2 : b ≠ n / p
hb3 : p * b = n
⊢ False
[PROOFSTEP]
apply hb2
[GOAL]
case pos.h₀.hnc
R : Type u
inst✝¹ : CommSemiring R
S : Type v
inst✝ : CommSemiring S
p✝ q p : ℕ
hp : 0 < p
f : R[X]
n : ℕ
h : p ∣ n
b : ℕ
a✝ : b ∈ support f
hb2 : b ≠ n / p
hb3 : p * b = n
⊢ b = n / p
[PROOFSTEP]
rw [← hb3, Nat.mul_div_cancel_left b hp]
[GOAL]
case pos.h₁
R : Type u
inst✝¹ : CommSemiring R
S : Type v
inst✝ : CommSemiring S
p✝ q p : ℕ
hp : 0 < p
f : R[X]
n : ℕ
h : p ∣ n
⊢ ¬n / p ∈ support f → (if p * (n / p) = n then coeff f (n / p) else 0) = 0
[PROOFSTEP]
intro hn
[GOAL]
case pos.h₁
R : Type u
inst✝¹ : CommSemiring R
S : Type v
inst✝ : CommSemiring S
p✝ q p : ℕ
hp : 0 < p
f : R[X]
n : ℕ
h : p ∣ n
hn : ¬n / p ∈ support f
⊢ (if p * (n / p) = n then coeff f (n / p) else 0) = 0
[PROOFSTEP]
rw [not_mem_support_iff.1 hn]
[GOAL]
case pos.h₁
R : Type u
inst✝¹ : CommSemiring R
S : Type v
inst✝ : CommSemiring S
p✝ q p : ℕ
hp : 0 < p
f : R[X]
n : ℕ
h : p ∣ n
hn : ¬n / p ∈ support f
⊢ (if p * (n / p) = n then 0 else 0) = 0
[PROOFSTEP]
split_ifs
[GOAL]
case pos
R : Type u
inst✝¹ : CommSemiring R
S : Type v
inst✝ : CommSemiring S
p✝ q p : ℕ
hp : 0 < p
f : R[X]
n : ℕ
h : p ∣ n
hn : ¬n / p ∈ support f
h✝ : p * (n / p) = n
⊢ 0 = 0
[PROOFSTEP]
rfl
[GOAL]
case neg
R : Type u
inst✝¹ : CommSemiring R
S : Type v
inst✝ : CommSemiring S
p✝ q p : ℕ
hp : 0 < p
f : R[X]
n : ℕ
h : p ∣ n
hn : ¬n / p ∈ support f
h✝ : ¬p * (n / p) = n
⊢ 0 = 0
[PROOFSTEP]
rfl
[GOAL]
case neg
R : Type u
inst✝¹ : CommSemiring R
S : Type v
inst✝ : CommSemiring S
p✝ q p : ℕ
hp : 0 < p
f : R[X]
n : ℕ
h : ¬p ∣ n
⊢ (∑ x in support f, if p * x = n then coeff f x else 0) = 0
[PROOFSTEP]
rw [Finset.sum_eq_zero]
[GOAL]
case neg
R : Type u
inst✝¹ : CommSemiring R
S : Type v
inst✝ : CommSemiring S
p✝ q p : ℕ
hp : 0 < p
f : R[X]
n : ℕ
h : ¬p ∣ n
⊢ ∀ (x : ℕ), x ∈ support f → (if p * x = n then coeff f x else 0) = 0
[PROOFSTEP]
intro k _
[GOAL]
case neg
R : Type u
inst✝¹ : CommSemiring R
S : Type v
inst✝ : CommSemiring S
p✝ q p : ℕ
hp : 0 < p
f : R[X]
n : ℕ
h : ¬p ∣ n
k : ℕ
a✝ : k ∈ support f
⊢ (if p * k = n then coeff f k else 0) = 0
[PROOFSTEP]
rw [if_neg]
[GOAL]
case neg.hnc
R : Type u
inst✝¹ : CommSemiring R
S : Type v
inst✝ : CommSemiring S
p✝ q p : ℕ
hp : 0 < p
f : R[X]
n : ℕ
h : ¬p ∣ n
k : ℕ
a✝ : k ∈ support f
⊢ ¬p * k = n
[PROOFSTEP]
exact fun hkn => h ⟨k, hkn.symm⟩
[GOAL]
R : Type u
inst✝¹ : CommSemiring R
S : Type v
inst✝ : CommSemiring S
p✝ q p : ℕ
hp : 0 < p
f : R[X]
n : ℕ
⊢ coeff (↑(expand R p) f) (n * p) = coeff f n
[PROOFSTEP]
rw [coeff_expand hp, if_pos (dvd_mul_left _ _), Nat.mul_div_cancel _ hp]
[GOAL]
R : Type u
inst✝¹ : CommSemiring R
S : Type v
inst✝ : CommSemiring S
p✝ q p : ℕ
hp : 0 < p
f : R[X]
n : ℕ
⊢ coeff (↑(expand R p) f) (p * n) = coeff f n
[PROOFSTEP]
rw [mul_comm, coeff_expand_mul hp]
[GOAL]
R : Type u
inst✝¹ : CommSemiring R
S : Type v
inst✝ : CommSemiring S
p q n : ℕ
hn : 0 < n
g g' : R[X]
H : ↑(expand R n) g = ↑(expand R n) g'
k : ℕ
⊢ coeff g k = coeff g' k
[PROOFSTEP]
rw [← coeff_expand_mul hn, H, coeff_expand_mul hn]
[GOAL]
R : Type u
inst✝¹ : CommSemiring R
S : Type v
inst✝ : CommSemiring S
p✝ q p : ℕ
hp : 0 < p
f : R[X]
r : R
⊢ ↑(expand R p) f = ↑C r ↔ f = ↑C r
[PROOFSTEP]
rw [← expand_C, expand_inj hp, expand_C]
[GOAL]
R : Type u
inst✝¹ : CommSemiring R
S : Type v
inst✝ : CommSemiring S
p✝ q p : ℕ
f : R[X]
⊢ natDegree (↑(expand R p) f) = natDegree f * p
[PROOFSTEP]
cases' p.eq_zero_or_pos with hp hp
[GOAL]
case inl
R : Type u
inst✝¹ : CommSemiring R
S : Type v
inst✝ : CommSemiring S
p✝ q p : ℕ
f : R[X]
hp : p = 0
⊢ natDegree (↑(expand R p) f) = natDegree f * p
[PROOFSTEP]
rw [hp, coe_expand, pow_zero, mul_zero, ← C_1, eval₂_hom, natDegree_C]
[GOAL]
case inr
R : Type u
inst✝¹ : CommSemiring R
S : Type v
inst✝ : CommSemiring S
p✝ q p : ℕ
f : R[X]
hp : p > 0
⊢ natDegree (↑(expand R p) f) = natDegree f * p
[PROOFSTEP]
by_cases hf : f = 0
[GOAL]
case pos
R : Type u
inst✝¹ : CommSemiring R
S : Type v
inst✝ : CommSemiring S
p✝ q p : ℕ
f : R[X]
hp : p > 0
hf : f = 0
⊢ natDegree (↑(expand R p) f) = natDegree f * p
[PROOFSTEP]
rw [hf, AlgHom.map_zero, natDegree_zero, zero_mul]
[GOAL]
case neg
R : Type u
inst✝¹ : CommSemiring R
S : Type v
inst✝ : CommSemiring S
p✝ q p : ℕ
f : R[X]
hp : p > 0
hf : ¬f = 0
⊢ natDegree (↑(expand R p) f) = natDegree f * p
[PROOFSTEP]
have hf1 : expand R p f ≠ 0 := mt (expand_eq_zero hp).1 hf
[GOAL]
case neg
R : Type u
inst✝¹ : CommSemiring R
S : Type v
inst✝ : CommSemiring S
p✝ q p : ℕ
f : R[X]
hp : p > 0
hf : ¬f = 0
hf1 : ↑(expand R p) f ≠ 0
⊢ natDegree (↑(expand R p) f) = natDegree f * p
[PROOFSTEP]
rw [← WithBot.coe_eq_coe]
[GOAL]
case neg
R : Type u
inst✝¹ : CommSemiring R
S : Type v
inst✝ : CommSemiring S
p✝ q p : ℕ
f : R[X]
hp : p > 0
hf : ¬f = 0
hf1 : ↑(expand R p) f ≠ 0
⊢ ↑(natDegree (↑(expand R p) f)) = ↑(natDegree f * p)
[PROOFSTEP]
convert (degree_eq_natDegree hf1).symm
[GOAL]
case h.e'_3
R : Type u
inst✝¹ : CommSemiring R
S : Type v
inst✝ : CommSemiring S
p✝ q p : ℕ
f : R[X]
hp : p > 0
hf : ¬f = 0
hf1 : ↑(expand R p) f ≠ 0
⊢ ↑(natDegree f * p) = degree (↑(expand R p) f)
[PROOFSTEP]
symm
[GOAL]
case h.e'_3
R : Type u
inst✝¹ : CommSemiring R
S : Type v
inst✝ : CommSemiring S
p✝ q p : ℕ
f : R[X]
hp : p > 0
hf : ¬f = 0
hf1 : ↑(expand R p) f ≠ 0
⊢ degree (↑(expand R p) f) = ↑(natDegree f * p)
[PROOFSTEP]
refine' le_antisymm ((degree_le_iff_coeff_zero _ _).2 fun n hn => _) _
[GOAL]
case h.e'_3.refine'_1
R : Type u
inst✝¹ : CommSemiring R
S : Type v
inst✝ : CommSemiring S
p✝ q p : ℕ
f : R[X]
hp : p > 0
hf : ¬f = 0
hf1 : ↑(expand R p) f ≠ 0
n : ℕ
hn : ↑(natDegree f * p) < ↑n
⊢ coeff (↑(expand R p) f) n = 0
[PROOFSTEP]
rw [coeff_expand hp]
[GOAL]
case h.e'_3.refine'_1
R : Type u
inst✝¹ : CommSemiring R
S : Type v
inst✝ : CommSemiring S
p✝ q p : ℕ
f : R[X]
hp : p > 0
hf : ¬f = 0
hf1 : ↑(expand R p) f ≠ 0
n : ℕ
hn : ↑(natDegree f * p) < ↑n
⊢ (if p ∣ n then coeff f (n / p) else 0) = 0
[PROOFSTEP]
split_ifs with hpn
[GOAL]
case pos
R : Type u
inst✝¹ : CommSemiring R
S : Type v
inst✝ : CommSemiring S
p✝ q p : ℕ
f : R[X]
hp : p > 0
hf : ¬f = 0
hf1 : ↑(expand R p) f ≠ 0
n : ℕ
hn : ↑(natDegree f * p) < ↑n
hpn : p ∣ n
⊢ coeff f (n / p) = 0
[PROOFSTEP]
rw [coeff_eq_zero_of_natDegree_lt]
[GOAL]
case pos
R : Type u
inst✝¹ : CommSemiring R
S : Type v
inst✝ : CommSemiring S
p✝ q p : ℕ
f : R[X]
hp : p > 0
hf : ¬f = 0
hf1 : ↑(expand R p) f ≠ 0
n : ℕ
hn : ↑(natDegree f * p) < ↑n
hpn : p ∣ n
⊢ natDegree f < n / p
[PROOFSTEP]
contrapose! hn
[GOAL]
case pos
R : Type u
inst✝¹ : CommSemiring R
S : Type v
inst✝ : CommSemiring S
p✝ q p : ℕ
f : R[X]
hp : p > 0
hf : ¬f = 0
hf1 : ↑(expand R p) f ≠ 0
n : ℕ
hpn : p ∣ n
hn : n / p ≤ natDegree f
⊢ ↑n ≤ ↑(natDegree f * p)
[PROOFSTEP]
erw [WithBot.coe_le_coe, ← Nat.div_mul_cancel hpn]
[GOAL]
case pos
R : Type u
inst✝¹ : CommSemiring R
S : Type v
inst✝ : CommSemiring S
p✝ q p : ℕ
f : R[X]
hp : p > 0
hf : ¬f = 0
hf1 : ↑(expand R p) f ≠ 0
n : ℕ
hpn : p ∣ n
hn : n / p ≤ natDegree f
⊢ ↑(n / p * p) ≤ natDegree f * p
[PROOFSTEP]
exact Nat.mul_le_mul_right p hn
[GOAL]
case neg
R : Type u
inst✝¹ : CommSemiring R
S : Type v
inst✝ : CommSemiring S
p✝ q p : ℕ
f : R[X]
hp : p > 0
hf : ¬f = 0
hf1 : ↑(expand R p) f ≠ 0
n : ℕ
hn : ↑(natDegree f * p) < ↑n
hpn : ¬p ∣ n
⊢ 0 = 0
[PROOFSTEP]
rfl
[GOAL]
case h.e'_3.refine'_2
R : Type u
inst✝¹ : CommSemiring R
S : Type v
inst✝ : CommSemiring S
p✝ q p : ℕ
f : R[X]
hp : p > 0
hf : ¬f = 0
hf1 : ↑(expand R p) f ≠ 0
⊢ ↑(natDegree f * p) ≤ degree (↑(expand R p) f)
[PROOFSTEP]
refine' le_degree_of_ne_zero _
[GOAL]
case h.e'_3.refine'_2
R : Type u
inst✝¹ : CommSemiring R
S : Type v
inst✝ : CommSemiring S
p✝ q p : ℕ
f : R[X]
hp : p > 0
hf : ¬f = 0
hf1 : ↑(expand R p) f ≠ 0
⊢ coeff (↑(expand R p) f) (Mul.mul (natDegree f) p) ≠ 0
[PROOFSTEP]
erw [coeff_expand_mul hp, ← leadingCoeff]
[GOAL]
case h.e'_3.refine'_2
R : Type u
inst✝¹ : CommSemiring R
S : Type v
inst✝ : CommSemiring S
p✝ q p : ℕ
f : R[X]
hp : p > 0
hf : ¬f = 0
hf1 : ↑(expand R p) f ≠ 0
⊢ leadingCoeff f ≠ 0
[PROOFSTEP]
exact mt leadingCoeff_eq_zero.1 hf
[GOAL]
R : Type u
inst✝¹ : CommSemiring R
S : Type v
inst✝ : CommSemiring S
p✝ q p : ℕ
f : R[X]
hp : 0 < p
h : Monic f
⊢ Monic (↑(Polynomial.expand R p) f)
[PROOFSTEP]
rw [Monic.def, Polynomial.leadingCoeff, natDegree_expand, coeff_expand hp]
[GOAL]
R : Type u
inst✝¹ : CommSemiring R
S : Type v
inst✝ : CommSemiring S
p✝ q p : ℕ
f : R[X]
hp : 0 < p
h : Monic f
⊢ (if p ∣ natDegree f * p then coeff f (natDegree f * p / p) else 0) = 1
[PROOFSTEP]
simp [hp, h]
[GOAL]
R : Type u
inst✝¹ : CommSemiring R
S : Type v
inst✝ : CommSemiring S
p✝ q✝ p : ℕ
f : R →+* S
q : R[X]
⊢ map f (↑(expand R p) q) = ↑(expand S p) (map f q)
[PROOFSTEP]
by_cases hp : p = 0
[GOAL]
case pos
R : Type u
inst✝¹ : CommSemiring R
S : Type v
inst✝ : CommSemiring S
p✝ q✝ p : ℕ
f : R →+* S
q : R[X]
hp : p = 0
⊢ map f (↑(expand R p) q) = ↑(expand S p) (map f q)
[PROOFSTEP]
simp [hp]
[GOAL]
case neg
R : Type u
inst✝¹ : CommSemiring R
S : Type v
inst✝ : CommSemiring S
p✝ q✝ p : ℕ
f : R →+* S
q : R[X]
hp : ¬p = 0
⊢ map f (↑(expand R p) q) = ↑(expand S p) (map f q)
[PROOFSTEP]
ext
[GOAL]
case neg.a
R : Type u
inst✝¹ : CommSemiring R
S : Type v
inst✝ : CommSemiring S
p✝ q✝ p : ℕ
f : R →+* S
q : R[X]
hp : ¬p = 0
n✝ : ℕ
⊢ coeff (map f (↑(expand R p) q)) n✝ = coeff (↑(expand S p) (map f q)) n✝
[PROOFSTEP]
rw [coeff_map, coeff_expand (Nat.pos_of_ne_zero hp), coeff_expand (Nat.pos_of_ne_zero hp)]
[GOAL]
case neg.a
R : Type u
inst✝¹ : CommSemiring R
S : Type v
inst✝ : CommSemiring S
p✝ q✝ p : ℕ
f : R →+* S
q : R[X]
hp : ¬p = 0
n✝ : ℕ
⊢ ↑f (if p ∣ n✝ then coeff q (n✝ / p) else 0) = if p ∣ n✝ then coeff (map f q) (n✝ / p) else 0
[PROOFSTEP]
split_ifs
[GOAL]
case pos
R : Type u
inst✝¹ : CommSemiring R
S : Type v
inst✝ : CommSemiring S
p✝ q✝ p : ℕ
f : R →+* S
q : R[X]
hp : ¬p = 0
n✝ : ℕ
h✝ : p ∣ n✝
⊢ ↑f (if p ∣ n✝ then coeff q (n✝ / p) else 0) = coeff (map f q) (n✝ / p)
[PROOFSTEP]
simp_all
[GOAL]
case neg
R : Type u
inst✝¹ : CommSemiring R
S : Type v
inst✝ : CommSemiring S
p✝ q✝ p : ℕ
f : R →+* S
q : R[X]
hp : ¬p = 0
n✝ : ℕ
h✝ : ¬p ∣ n✝
⊢ ↑f (if p ∣ n✝ then coeff q (n✝ / p) else 0) = 0
[PROOFSTEP]
simp_all
[GOAL]
R : Type u
inst✝¹ : CommSemiring R
S : Type v
inst✝ : CommSemiring S
p✝ q p : ℕ
P : R[X]
r : R
⊢ eval r (↑(expand R p) P) = eval (r ^ p) P
[PROOFSTEP]
refine' Polynomial.induction_on P (fun a => by simp) (fun f g hf hg => _) fun n a _ => by simp
[GOAL]
R : Type u
inst✝¹ : CommSemiring R
S : Type v
inst✝ : CommSemiring S
p✝ q p : ℕ
P : R[X]
r a : R
⊢ eval r (↑(expand R p) (↑C a)) = eval (r ^ p) (↑C a)
[PROOFSTEP]
simp
[GOAL]
R : Type u
inst✝¹ : CommSemiring R
S : Type v
inst✝ : CommSemiring S
p✝ q p : ℕ
P : R[X]
r : R
n : ℕ
a : R
x✝ : eval r (↑(expand R p) (↑C a * X ^ n)) = eval (r ^ p) (↑C a * X ^ n)
⊢ eval r (↑(expand R p) (↑C a * X ^ (n + 1))) = eval (r ^ p) (↑C a * X ^ (n + 1))
[PROOFSTEP]
simp
[GOAL]
R : Type u
inst✝¹ : CommSemiring R
S : Type v
inst✝ : CommSemiring S
p✝ q p : ℕ
P : R[X]
r : R
f g : R[X]
hf : eval r (↑(expand R p) f) = eval (r ^ p) f
hg : eval r (↑(expand R p) g) = eval (r ^ p) g
⊢ eval r (↑(expand R p) (f + g)) = eval (r ^ p) (f + g)
[PROOFSTEP]
rw [AlgHom.map_add, eval_add, eval_add, hf, hg]
[GOAL]
R : Type u
inst✝³ : CommSemiring R
S : Type v
inst✝² : CommSemiring S
p✝ q : ℕ
A : Type u_1
inst✝¹ : Semiring A
inst✝ : Algebra R A
p : ℕ
P : R[X]
r : A
⊢ ↑(aeval r) (↑(expand R p) P) = ↑(aeval (r ^ p)) P
[PROOFSTEP]
refine' Polynomial.induction_on P (fun a => by simp) (fun f g hf hg => _) fun n a _ => by simp
[GOAL]
R : Type u
inst✝³ : CommSemiring R
S : Type v
inst✝² : CommSemiring S
p✝ q : ℕ
A : Type u_1
inst✝¹ : Semiring A
inst✝ : Algebra R A
p : ℕ
P : R[X]
r : A
a : R
⊢ ↑(aeval r) (↑(expand R p) (↑C a)) = ↑(aeval (r ^ p)) (↑C a)
[PROOFSTEP]
simp
[GOAL]
R : Type u
inst✝³ : CommSemiring R
S : Type v
inst✝² : CommSemiring S
p✝ q : ℕ
A : Type u_1
inst✝¹ : Semiring A
inst✝ : Algebra R A
p : ℕ
P : R[X]
r : A
n : ℕ
a : R
x✝ : ↑(aeval r) (↑(expand R p) (↑C a * X ^ n)) = ↑(aeval (r ^ p)) (↑C a * X ^ n)
⊢ ↑(aeval r) (↑(expand R p) (↑C a * X ^ (n + 1))) = ↑(aeval (r ^ p)) (↑C a * X ^ (n + 1))
[PROOFSTEP]
simp
[GOAL]
R : Type u
inst✝³ : CommSemiring R
S : Type v
inst✝² : CommSemiring S
p✝ q : ℕ
A : Type u_1
inst✝¹ : Semiring A
inst✝ : Algebra R A
p : ℕ
P : R[X]
r : A
f g : R[X]
hf : ↑(aeval r) (↑(expand R p) f) = ↑(aeval (r ^ p)) f
hg : ↑(aeval r) (↑(expand R p) g) = ↑(aeval (r ^ p)) g
⊢ ↑(aeval r) (↑(expand R p) (f + g)) = ↑(aeval (r ^ p)) (f + g)
[PROOFSTEP]
rw [AlgHom.map_add, aeval_add, aeval_add, hf, hg]
[GOAL]
R : Type u
inst✝¹ : CommSemiring R
S : Type v
inst✝ : CommSemiring S
p✝ q p : ℕ
hp : p ≠ 0
f : R[X]
n : ℕ
⊢ coeff (contract p f) n = coeff f (n * p)
[PROOFSTEP]
simp only [contract, coeff_monomial, sum_ite_eq', finset_sum_coeff, mem_range, not_lt, ite_eq_left_iff]
[GOAL]
R : Type u
inst✝¹ : CommSemiring R
S : Type v
inst✝ : CommSemiring S
p✝ q p : ℕ
hp : p ≠ 0
f : R[X]
n : ℕ
⊢ natDegree f + 1 ≤ n → 0 = coeff f (n * p)
[PROOFSTEP]
intro hn
[GOAL]
R : Type u
inst✝¹ : CommSemiring R
S : Type v
inst✝ : CommSemiring S
p✝ q p : ℕ
hp : p ≠ 0
f : R[X]
n : ℕ
hn : natDegree f + 1 ≤ n
⊢ 0 = coeff f (n * p)
[PROOFSTEP]
apply (coeff_eq_zero_of_natDegree_lt _).symm
[GOAL]
R : Type u
inst✝¹ : CommSemiring R
S : Type v
inst✝ : CommSemiring S
p✝ q p : ℕ
hp : p ≠ 0
f : R[X]
n : ℕ
hn : natDegree f + 1 ≤ n
⊢ natDegree f < n * p
[PROOFSTEP]
calc
  f.natDegree < f.natDegree + 1 := Nat.lt_succ_self _
  _ ≤ n * 1 := by simpa only [mul_one] using hn
  _ ≤ n * p := mul_le_mul_of_nonneg_left (show 1 ≤ p from hp.bot_lt) (zero_le n)
[GOAL]
R : Type u
inst✝¹ : CommSemiring R
S : Type v
inst✝ : CommSemiring S
p✝ q p : ℕ
hp : p ≠ 0
f : R[X]
n : ℕ
hn : natDegree f + 1 ≤ n
⊢ natDegree f + 1 ≤ n * 1
[PROOFSTEP]
simpa only [mul_one] using hn
[GOAL]
R : Type u
inst✝¹ : CommSemiring R
S : Type v
inst✝ : CommSemiring S
p q : ℕ
f : R[X]
hp : p ≠ 0
⊢ contract p (↑(expand R p) f) = f
[PROOFSTEP]
ext
[GOAL]
case a
R : Type u
inst✝¹ : CommSemiring R
S : Type v
inst✝ : CommSemiring S
p q : ℕ
f : R[X]
hp : p ≠ 0
n✝ : ℕ
⊢ coeff (contract p (↑(expand R p) f)) n✝ = coeff f n✝
[PROOFSTEP]
simp [coeff_contract hp, coeff_expand hp.bot_lt, Nat.mul_div_cancel _ hp.bot_lt]
[GOAL]
R : Type u
inst✝³ : CommSemiring R
S : Type v
inst✝² : CommSemiring S
p q : ℕ
inst✝¹ : CharP R p
inst✝ : NoZeroDivisors R
f : R[X]
hf : ↑derivative f = 0
hp : p ≠ 0
⊢ ↑(expand R p) (contract p f) = f
[PROOFSTEP]
ext n
[GOAL]
case a
R : Type u
inst✝³ : CommSemiring R
S : Type v
inst✝² : CommSemiring S
p q : ℕ
inst✝¹ : CharP R p
inst✝ : NoZeroDivisors R
f : R[X]
hf : ↑derivative f = 0
hp : p ≠ 0
n : ℕ
⊢ coeff (↑(expand R p) (contract p f)) n = coeff f n
[PROOFSTEP]
rw [coeff_expand hp.bot_lt, coeff_contract hp]
[GOAL]
case a
R : Type u
inst✝³ : CommSemiring R
S : Type v
inst✝² : CommSemiring S
p q : ℕ
inst✝¹ : CharP R p
inst✝ : NoZeroDivisors R
f : R[X]
hf : ↑derivative f = 0
hp : p ≠ 0
n : ℕ
⊢ (if p ∣ n then coeff f (n / p * p) else 0) = coeff f n
[PROOFSTEP]
split_ifs with h
[GOAL]
case pos
R : Type u
inst✝³ : CommSemiring R
S : Type v
inst✝² : CommSemiring S
p q : ℕ
inst✝¹ : CharP R p
inst✝ : NoZeroDivisors R
f : R[X]
hf : ↑derivative f = 0
hp : p ≠ 0
n : ℕ
h : p ∣ n
⊢ coeff f (n / p * p) = coeff f n
[PROOFSTEP]
rw [Nat.div_mul_cancel h]
[GOAL]
case neg
R : Type u
inst✝³ : CommSemiring R
S : Type v
inst✝² : CommSemiring S
p q : ℕ
inst✝¹ : CharP R p
inst✝ : NoZeroDivisors R
f : R[X]
hf : ↑derivative f = 0
hp : p ≠ 0
n : ℕ
h : ¬p ∣ n
⊢ 0 = coeff f n
[PROOFSTEP]
cases' n with n
[GOAL]
case neg.zero
R : Type u
inst✝³ : CommSemiring R
S : Type v
inst✝² : CommSemiring S
p q : ℕ
inst✝¹ : CharP R p
inst✝ : NoZeroDivisors R
f : R[X]
hf : ↑derivative f = 0
hp : p ≠ 0
h : ¬p ∣ Nat.zero
⊢ 0 = coeff f Nat.zero
[PROOFSTEP]
exact absurd (dvd_zero p) h
[GOAL]
case neg.succ
R : Type u
inst✝³ : CommSemiring R
S : Type v
inst✝² : CommSemiring S
p q : ℕ
inst✝¹ : CharP R p
inst✝ : NoZeroDivisors R
f : R[X]
hf : ↑derivative f = 0
hp : p ≠ 0
n : ℕ
h : ¬p ∣ Nat.succ n
⊢ 0 = coeff f (Nat.succ n)
[PROOFSTEP]
have := coeff_derivative f n
[GOAL]
case neg.succ
R : Type u
inst✝³ : CommSemiring R
S : Type v
inst✝² : CommSemiring S
p q : ℕ
inst✝¹ : CharP R p
inst✝ : NoZeroDivisors R
f : R[X]
hf : ↑derivative f = 0
hp : p ≠ 0
n : ℕ
h : ¬p ∣ Nat.succ n
this : coeff (↑derivative f) n = coeff f (n + 1) * (↑n + 1)
⊢ 0 = coeff f (Nat.succ n)
[PROOFSTEP]
rw [hf, coeff_zero, zero_eq_mul] at this
[GOAL]
case neg.succ
R : Type u
inst✝³ : CommSemiring R
S : Type v
inst✝² : CommSemiring S
p q : ℕ
inst✝¹ : CharP R p
inst✝ : NoZeroDivisors R
f : R[X]
hf : ↑derivative f = 0
hp : p ≠ 0
n : ℕ
h : ¬p ∣ Nat.succ n
this : coeff f (n + 1) = 0 ∨ ↑n + 1 = 0
⊢ 0 = coeff f (Nat.succ n)
[PROOFSTEP]
cases' this with h'
[GOAL]
case neg.succ.inl
R : Type u
inst✝³ : CommSemiring R
S : Type v
inst✝² : CommSemiring S
p q : ℕ
inst✝¹ : CharP R p
inst✝ : NoZeroDivisors R
f : R[X]
hf : ↑derivative f = 0
hp : p ≠ 0
n : ℕ
h : ¬p ∣ Nat.succ n
h' : coeff f (n + 1) = 0
⊢ 0 = coeff f (Nat.succ n)
[PROOFSTEP]
rw [h']
[GOAL]
case neg.succ.inr
R : Type u
inst✝³ : CommSemiring R
S : Type v
inst✝² : CommSemiring S
p q : ℕ
inst✝¹ : CharP R p
inst✝ : NoZeroDivisors R
f : R[X]
hf : ↑derivative f = 0
hp : p ≠ 0
n : ℕ
h : ¬p ∣ Nat.succ n
h✝ : ↑n + 1 = 0
⊢ 0 = coeff f (Nat.succ n)
[PROOFSTEP]
rename_i _ _ _ _ h'
[GOAL]
case neg.succ.inr
R : Type u
inst✝³ : CommSemiring R
S : Type v
inst✝² : CommSemiring S
p q : ℕ
inst✝¹ : CharP R p
inst✝ : NoZeroDivisors R
f : R[X]
hf : ↑derivative f = 0
hp : p ≠ 0
n : ℕ
h : ¬p ∣ Nat.succ n
h' : ↑n + 1 = 0
⊢ 0 = coeff f (Nat.succ n)
[PROOFSTEP]
rw [← Nat.cast_succ, CharP.cast_eq_zero_iff R p] at h'
[GOAL]
case neg.succ.inr
R : Type u
inst✝³ : CommSemiring R
S : Type v
inst✝² : CommSemiring S
p q : ℕ
inst✝¹ : CharP R p
inst✝ : NoZeroDivisors R
f : R[X]
hf : ↑derivative f = 0
hp : p ≠ 0
n : ℕ
h : ¬p ∣ Nat.succ n
h' : p ∣ Nat.succ n
⊢ 0 = coeff f (Nat.succ n)
[PROOFSTEP]
exact absurd h' h
[GOAL]
R : Type u
inst✝² : CommSemiring R
S : Type v
inst✝¹ : CommSemiring S
p q : ℕ
inst✝ : CharP R p
hp : Fact (Nat.Prime p)
f : R[X]
⊢ map (frobenius R p) (↑(expand R p) f) = f ^ p
[PROOFSTEP]
refine' f.induction_on' (fun a b ha hb => _) fun n a => _
[GOAL]
case refine'_1
R : Type u
inst✝² : CommSemiring R
S : Type v
inst✝¹ : CommSemiring S
p q : ℕ
inst✝ : CharP R p
hp : Fact (Nat.Prime p)
f a b : R[X]
ha : map (frobenius R p) (↑(expand R p) a) = a ^ p
hb : map (frobenius R p) (↑(expand R p) b) = b ^ p
⊢ map (frobenius R p) (↑(expand R p) (a + b)) = (a + b) ^ p
[PROOFSTEP]
rw [AlgHom.map_add, Polynomial.map_add, ha, hb, add_pow_char]
[GOAL]
case refine'_2
R : Type u
inst✝² : CommSemiring R
S : Type v
inst✝¹ : CommSemiring S
p q : ℕ
inst✝ : CharP R p
hp : Fact (Nat.Prime p)
f : R[X]
n : ℕ
a : R
⊢ map (frobenius R p) (↑(expand R p) (↑(monomial n) a)) = ↑(monomial n) a ^ p
[PROOFSTEP]
rw [expand_monomial, map_monomial, ← C_mul_X_pow_eq_monomial, ← C_mul_X_pow_eq_monomial, mul_pow, ← C.map_pow,
  frobenius_def]
[GOAL]
case refine'_2
R : Type u
inst✝² : CommSemiring R
S : Type v
inst✝¹ : CommSemiring S
p q : ℕ
inst✝ : CharP R p
hp : Fact (Nat.Prime p)
f : R[X]
n : ℕ
a : R
⊢ ↑C (a ^ p) * X ^ (n * p) = ↑C (a ^ p) * (X ^ n) ^ p
[PROOFSTEP]
ring
[GOAL]
R : Type u
inst✝² : CommSemiring R
S : Type v
inst✝¹ : CommSemiring S
p q : ℕ
inst✝ : CharP R p
hp : Fact (Nat.Prime p)
f : R[X]
n : ℕ
⊢ map (frobenius R p ^ n) (↑(expand R (p ^ n)) f) = f ^ p ^ n
[PROOFSTEP]
induction' n with _ n_ih
[GOAL]
case zero
R : Type u
inst✝² : CommSemiring R
S : Type v
inst✝¹ : CommSemiring S
p q : ℕ
inst✝ : CharP R p
hp : Fact (Nat.Prime p)
f : R[X]
⊢ map (frobenius R p ^ Nat.zero) (↑(expand R (p ^ Nat.zero)) f) = f ^ p ^ Nat.zero
[PROOFSTEP]
simp [RingHom.one_def]
[GOAL]
case succ
R : Type u
inst✝² : CommSemiring R
S : Type v
inst✝¹ : CommSemiring S
p q : ℕ
inst✝ : CharP R p
hp : Fact (Nat.Prime p)
f : R[X]
n✝ : ℕ
n_ih : map (frobenius R p ^ n✝) (↑(expand R (p ^ n✝)) f) = f ^ p ^ n✝
⊢ map (frobenius R p ^ Nat.succ n✝) (↑(expand R (p ^ Nat.succ n✝)) f) = f ^ p ^ Nat.succ n✝
[PROOFSTEP]
symm
[GOAL]
case succ
R : Type u
inst✝² : CommSemiring R
S : Type v
inst✝¹ : CommSemiring S
p q : ℕ
inst✝ : CharP R p
hp : Fact (Nat.Prime p)
f : R[X]
n✝ : ℕ
n_ih : map (frobenius R p ^ n✝) (↑(expand R (p ^ n✝)) f) = f ^ p ^ n✝
⊢ f ^ p ^ Nat.succ n✝ = map (frobenius R p ^ Nat.succ n✝) (↑(expand R (p ^ Nat.succ n✝)) f)
[PROOFSTEP]
rw [pow_succ', pow_mul, ← n_ih, ← expand_char, pow_succ, RingHom.mul_def, ← map_map, mul_comm, expand_mul, ← map_expand]
[GOAL]
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : ℕ
hp : 0 < p
⊢ IsLocalRingHom ↑(expand R p)
[PROOFSTEP]
refine' ⟨fun f hf1 => _⟩
[GOAL]
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : ℕ
hp : 0 < p
f : R[X]
hf1 : IsUnit (↑↑(expand R p) f)
⊢ IsUnit f
[PROOFSTEP]
norm_cast at hf1
[GOAL]
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : ℕ
hp : 0 < p
f : R[X]
hf1 : IsUnit (↑(expand R p) f)
⊢ IsUnit f
[PROOFSTEP]
have hf2 := eq_C_of_degree_eq_zero (degree_eq_zero_of_isUnit hf1)
[GOAL]
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : ℕ
hp : 0 < p
f : R[X]
hf1 : IsUnit (↑(expand R p) f)
hf2 : ↑(expand R p) f = ↑C (coeff (↑(expand R p) f) 0)
⊢ IsUnit f
[PROOFSTEP]
rw [coeff_expand hp, if_pos (dvd_zero _), p.zero_div] at hf2
[GOAL]
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : ℕ
hp : 0 < p
f : R[X]
hf1 : IsUnit (↑(expand R p) f)
hf2 : ↑(expand R p) f = ↑C (coeff f 0)
⊢ IsUnit f
[PROOFSTEP]
rw [hf2, isUnit_C] at hf1
[GOAL]
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : ℕ
hp : 0 < p
f : R[X]
hf1 : IsUnit (coeff f 0)
hf2 : ↑(expand R p) f = ↑C (coeff f 0)
⊢ IsUnit f
[PROOFSTEP]
rw [expand_eq_C hp] at hf2
[GOAL]
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : ℕ
hp : 0 < p
f : R[X]
hf1 : IsUnit (coeff f 0)
hf2 : f = ↑C (coeff f 0)
⊢ IsUnit f
[PROOFSTEP]
rwa [hf2, isUnit_C]
[GOAL]
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : ℕ
hp : p ≠ 0
f : R[X]
n : ℕ
hf : Irreducible (↑(expand R (p ^ Nat.zero)) f)
⊢ Irreducible f
[PROOFSTEP]
rwa [pow_zero, expand_one] at hf
[GOAL]
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : ℕ
hp : p ≠ 0
f : R[X]
n✝ n : ℕ
ih : Irreducible (↑(expand R (p ^ n)) f) → Irreducible f
hf : Irreducible (↑(expand R (p ^ Nat.succ n)) f)
⊢ Irreducible (↑(expand R p) (↑(expand R (p ^ n)) f))
[PROOFSTEP]
rw [pow_succ] at hf
[GOAL]
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : ℕ
hp : p ≠ 0
f : R[X]
n✝ n : ℕ
ih : Irreducible (↑(expand R (p ^ n)) f) → Irreducible f
hf : Irreducible (↑(expand R (p * p ^ n)) f)
⊢ Irreducible (↑(expand R p) (↑(expand R (p ^ n)) f))
[PROOFSTEP]
rwa [expand_expand]


[GOAL]
R : Type u_1
A : Type u_2
inst✝ : CommSemiring R
f g : R[X]
⊢ ↑{
          toAddHom :=
            { toFun := ↑derivative,
              map_add' := (_ : ∀ (x x_1 : R[X]), ↑derivative (x + x_1) = ↑derivative x + ↑derivative x_1) },
          map_smul' := (_ : ∀ (s : R) (p : R[X]), ↑derivative (s • p) = s • ↑derivative p) }
      (f * g) =
    f •
        ↑{
              toAddHom :=
                { toFun := ↑derivative,
                  map_add' := (_ : ∀ (x x_1 : R[X]), ↑derivative (x + x_1) = ↑derivative x + ↑derivative x_1) },
              map_smul' := (_ : ∀ (s : R) (p : R[X]), ↑derivative (s • p) = s • ↑derivative p) }
          g +
      g •
        ↑{
              toAddHom :=
                { toFun := ↑derivative,
                  map_add' := (_ : ∀ (x x_1 : R[X]), ↑derivative (x + x_1) = ↑derivative x + ↑derivative x_1) },
              map_smul' := (_ : ∀ (s : R) (p : R[X]), ↑derivative (s • p) = s • ↑derivative p) }
          f
[PROOFSTEP]
simp [mul_comm, add_comm, derivative_mul]
[GOAL]
R : Type u_1
A : Type u_2
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid A
inst✝¹ : Module R A
inst✝ : Module R[X] A
D : Derivation R R[X] A
a : R
f : R[X]
⊢ ↑C a • ↑D f = a • ↑D f
[PROOFSTEP]
have : C a • D f = D (C a * f) := by simp
[GOAL]
R : Type u_1
A : Type u_2
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid A
inst✝¹ : Module R A
inst✝ : Module R[X] A
D : Derivation R R[X] A
a : R
f : R[X]
⊢ ↑C a • ↑D f = ↑D (↑C a * f)
[PROOFSTEP]
simp
[GOAL]
R : Type u_1
A : Type u_2
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid A
inst✝¹ : Module R A
inst✝ : Module R[X] A
D : Derivation R R[X] A
a : R
f : R[X]
this : ↑C a • ↑D f = ↑D (↑C a * f)
⊢ ↑C a • ↑D f = a • ↑D f
[PROOFSTEP]
rw [this, C_mul', D.map_smul]
[GOAL]
R : Type u_1
A : Type u_2
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid A
inst✝¹ : Module R A
inst✝ : Module R[X] A
D₁ D₂ : Derivation R R[X] A
h : ↑D₁ X = ↑D₂ X
f : R[X]
⊢ f ∈ ↑(Algebra.adjoin R {X})
[PROOFSTEP]
simp only [adjoin_X, Algebra.coe_top, Set.mem_univ]
[GOAL]
R : Type u_1
A : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid A
inst✝² : Module R A
inst✝¹ : Module R[X] A
inst✝ : IsScalarTower R R[X] A
a b : A
⊢ (fun a => ↑(LinearMap.compDer (LinearMap.toSpanSingleton R[X] A a)) derivative') (a + b) =
    (fun a => ↑(LinearMap.compDer (LinearMap.toSpanSingleton R[X] A a)) derivative') a +
      (fun a => ↑(LinearMap.compDer (LinearMap.toSpanSingleton R[X] A a)) derivative') b
[PROOFSTEP]
ext
[GOAL]
case h
R : Type u_1
A : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid A
inst✝² : Module R A
inst✝¹ : Module R[X] A
inst✝ : IsScalarTower R R[X] A
a b : A
⊢ ↑((fun a => ↑(LinearMap.compDer (LinearMap.toSpanSingleton R[X] A a)) derivative') (a + b)) X =
    ↑((fun a => ↑(LinearMap.compDer (LinearMap.toSpanSingleton R[X] A a)) derivative') a +
          (fun a => ↑(LinearMap.compDer (LinearMap.toSpanSingleton R[X] A a)) derivative') b)
      X
[PROOFSTEP]
simp
[GOAL]
R : Type u_1
A : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid A
inst✝² : Module R A
inst✝¹ : Module R[X] A
inst✝ : IsScalarTower R R[X] A
t : R
a : A
⊢ AddHom.toFun
      { toFun := fun a => ↑(LinearMap.compDer (LinearMap.toSpanSingleton R[X] A a)) derivative',
        map_add' :=
          (_ :
            ∀ (a b : A),
              (fun a => ↑(LinearMap.compDer (LinearMap.toSpanSingleton R[X] A a)) derivative') (a + b) =
                (fun a => ↑(LinearMap.compDer (LinearMap.toSpanSingleton R[X] A a)) derivative') a +
                  (fun a => ↑(LinearMap.compDer (LinearMap.toSpanSingleton R[X] A a)) derivative') b) }
      (t • a) =
    ↑(RingHom.id R) t •
      AddHom.toFun
        { toFun := fun a => ↑(LinearMap.compDer (LinearMap.toSpanSingleton R[X] A a)) derivative',
          map_add' :=
            (_ :
              ∀ (a b : A),
                (fun a => ↑(LinearMap.compDer (LinearMap.toSpanSingleton R[X] A a)) derivative') (a + b) =
                  (fun a => ↑(LinearMap.compDer (LinearMap.toSpanSingleton R[X] A a)) derivative') a +
                    (fun a => ↑(LinearMap.compDer (LinearMap.toSpanSingleton R[X] A a)) derivative') b) }
        a
[PROOFSTEP]
ext
[GOAL]
case h
R : Type u_1
A : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid A
inst✝² : Module R A
inst✝¹ : Module R[X] A
inst✝ : IsScalarTower R R[X] A
t : R
a : A
⊢ ↑(AddHom.toFun
          { toFun := fun a => ↑(LinearMap.compDer (LinearMap.toSpanSingleton R[X] A a)) derivative',
            map_add' :=
              (_ :
                ∀ (a b : A),
                  (fun a => ↑(LinearMap.compDer (LinearMap.toSpanSingleton R[X] A a)) derivative') (a + b) =
                    (fun a => ↑(LinearMap.compDer (LinearMap.toSpanSingleton R[X] A a)) derivative') a +
                      (fun a => ↑(LinearMap.compDer (LinearMap.toSpanSingleton R[X] A a)) derivative') b) }
          (t • a))
      X =
    ↑(↑(RingHom.id R) t •
          AddHom.toFun
            { toFun := fun a => ↑(LinearMap.compDer (LinearMap.toSpanSingleton R[X] A a)) derivative',
              map_add' :=
                (_ :
                  ∀ (a b : A),
                    (fun a => ↑(LinearMap.compDer (LinearMap.toSpanSingleton R[X] A a)) derivative') (a + b) =
                      (fun a => ↑(LinearMap.compDer (LinearMap.toSpanSingleton R[X] A a)) derivative') a +
                        (fun a => ↑(LinearMap.compDer (LinearMap.toSpanSingleton R[X] A a)) derivative') b) }
            a)
      X
[PROOFSTEP]
simp
[GOAL]
R : Type u_1
A : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid A
inst✝² : Module R A
inst✝¹ : Module R[X] A
inst✝ : IsScalarTower R R[X] A
a : A
f : R[X]
⊢ ↑(↑(mkDerivation R) a) f = ↑derivative f • a
[PROOFSTEP]
rfl
[GOAL]
R : Type u_1
A : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid A
inst✝² : Module R A
inst✝¹ : Module R[X] A
inst✝ : IsScalarTower R R[X] A
a : A
⊢ ↑(↑(mkDerivation R) a) X = a
[PROOFSTEP]
simp [mkDerivation_apply]
[GOAL]
R : Type u_1
A : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid A
inst✝² : Module R A
inst✝¹ : Module R[X] A
inst✝ : IsScalarTower R R[X] A
⊢ ↑(mkDerivation R) 1 = derivative'
[PROOFSTEP]
ext : 1
[GOAL]
case h
R : Type u_1
A : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid A
inst✝² : Module R A
inst✝¹ : Module R[X] A
inst✝ : IsScalarTower R R[X] A
⊢ ↑(↑(mkDerivation R) 1) X = ↑derivative' X
[PROOFSTEP]
simp [derivative']
[GOAL]
R : Type u_1
A : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid A
inst✝² : Module R A
inst✝¹ : Module R[X] A
inst✝ : IsScalarTower R R[X] A
f : R[X]
⊢ ↑(↑(mkDerivation R) 1) f = ↑derivative f
[PROOFSTEP]
rw [mkDerivation_one_eq_derivative']
[GOAL]
R : Type u_1
A : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid A
inst✝² : Module R A
inst✝¹ : Module R[X] A
inst✝ : IsScalarTower R R[X] A
f : R[X]
⊢ ↑derivative' f = ↑derivative f
[PROOFSTEP]
rfl
[GOAL]
R : Type u_1
A : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid A
inst✝² : Module R A
inst✝¹ : Module R[X] A
inst✝ : IsScalarTower R R[X] A
a : A
⊢ ↑(mkDerivationEquiv R) a = ↑(mkDerivation R) a
[PROOFSTEP]
rfl


[GOAL]
R : Type u_1
inst✝ : Semiring R
f : R[X]
N i : ℕ
⊢ revAtFun N (revAtFun N i) = i
[PROOFSTEP]
unfold revAtFun
[GOAL]
R : Type u_1
inst✝ : Semiring R
f : R[X]
N i : ℕ
⊢ (if (if i ≤ N then N - i else i) ≤ N then N - if i ≤ N then N - i else i else if i ≤ N then N - i else i) = i
[PROOFSTEP]
split_ifs with h j
[GOAL]
case pos
R : Type u_1
inst✝ : Semiring R
f : R[X]
N i : ℕ
h : i ≤ N
j : N - i ≤ N
⊢ N - (N - i) = i
[PROOFSTEP]
exact tsub_tsub_cancel_of_le h
[GOAL]
case neg
R : Type u_1
inst✝ : Semiring R
f : R[X]
N i : ℕ
h : i ≤ N
j : ¬N - i ≤ N
⊢ N - i = i
[PROOFSTEP]
exfalso
[GOAL]
case neg.h
R : Type u_1
inst✝ : Semiring R
f : R[X]
N i : ℕ
h : i ≤ N
j : ¬N - i ≤ N
⊢ False
[PROOFSTEP]
apply j
[GOAL]
case neg.h
R : Type u_1
inst✝ : Semiring R
f : R[X]
N i : ℕ
h : i ≤ N
j : ¬N - i ≤ N
⊢ N - i ≤ N
[PROOFSTEP]
exact Nat.sub_le N i
[GOAL]
case neg
R : Type u_1
inst✝ : Semiring R
f : R[X]
N i : ℕ
h : ¬i ≤ N
⊢ i = i
[PROOFSTEP]
rfl
[GOAL]
R : Type u_1
inst✝ : Semiring R
f : R[X]
N : ℕ
⊢ Function.Injective (revAtFun N)
[PROOFSTEP]
intro a b hab
[GOAL]
R : Type u_1
inst✝ : Semiring R
f : R[X]
N a b : ℕ
hab : revAtFun N a = revAtFun N b
⊢ a = b
[PROOFSTEP]
rw [← @revAtFun_invol N a, hab, revAtFun_invol]
[GOAL]
R : Type u_1
inst✝ : Semiring R
f : R[X]
N i : ℕ
h : N < i
⊢ ↑(revAt N) i = i
[PROOFSTEP]
simp [revAt, Nat.not_le.mpr h]
[GOAL]
R : Type u_1
inst✝ : Semiring R
f : R[X]
N O n o : ℕ
hn : n ≤ N
ho : o ≤ O
⊢ ↑(revAt (N + O)) (n + o) = ↑(revAt N) n + ↑(revAt O) o
[PROOFSTEP]
rcases Nat.le.dest hn with ⟨n', rfl⟩
[GOAL]
case intro
R : Type u_1
inst✝ : Semiring R
f : R[X]
O n o : ℕ
ho : o ≤ O
n' : ℕ
hn : n ≤ n + n'
⊢ ↑(revAt (n + n' + O)) (n + o) = ↑(revAt (n + n')) n + ↑(revAt O) o
[PROOFSTEP]
rcases Nat.le.dest ho with ⟨o', rfl⟩
[GOAL]
case intro.intro
R : Type u_1
inst✝ : Semiring R
f : R[X]
n o n' : ℕ
hn : n ≤ n + n'
o' : ℕ
ho : o ≤ o + o'
⊢ ↑(revAt (n + n' + (o + o'))) (n + o) = ↑(revAt (n + n')) n + ↑(revAt (o + o')) o
[PROOFSTEP]
repeat' rw [revAt_le (le_add_right rfl.le)]
[GOAL]
case intro.intro
R : Type u_1
inst✝ : Semiring R
f : R[X]
n o n' : ℕ
hn : n ≤ n + n'
o' : ℕ
ho : o ≤ o + o'
⊢ ↑(revAt (n + n' + (o + o'))) (n + o) = ↑(revAt (n + n')) n + ↑(revAt (o + o')) o
[PROOFSTEP]
rw [revAt_le (le_add_right rfl.le)]
[GOAL]
case intro.intro
R : Type u_1
inst✝ : Semiring R
f : R[X]
n o n' : ℕ
hn : n ≤ n + n'
o' : ℕ
ho : o ≤ o + o'
⊢ ↑(revAt (n + n' + (o + o'))) (n + o) = n + n' - n + ↑(revAt (o + o')) o
[PROOFSTEP]
rw [revAt_le (le_add_right rfl.le)]
[GOAL]
case intro.intro
R : Type u_1
inst✝ : Semiring R
f : R[X]
n o n' : ℕ
hn : n ≤ n + n'
o' : ℕ
ho : o ≤ o + o'
⊢ ↑(revAt (n + n' + (o + o'))) (n + o) = n + n' - n + (o + o' - o)
[PROOFSTEP]
rw [revAt_le (le_add_right rfl.le)]
[GOAL]
case intro.intro
R : Type u_1
inst✝ : Semiring R
f : R[X]
n o n' : ℕ
hn : n ≤ n + n'
o' : ℕ
ho : o ≤ o + o'
⊢ ↑(revAt (n + n' + (o + o'))) (n + o) = n + n' - n + (o + o' - o)
[PROOFSTEP]
rw [add_assoc, add_left_comm n' o, ← add_assoc, revAt_le (le_add_right rfl.le)]
[GOAL]
case intro.intro
R : Type u_1
inst✝ : Semiring R
f : R[X]
n o n' : ℕ
hn : n ≤ n + n'
o' : ℕ
ho : o ≤ o + o'
⊢ n + o + (n' + o') - (n + o) = n + n' - n + (o + o' - o)
[PROOFSTEP]
repeat' rw [add_tsub_cancel_left]
[GOAL]
case intro.intro
R : Type u_1
inst✝ : Semiring R
f : R[X]
n o n' : ℕ
hn : n ≤ n + n'
o' : ℕ
ho : o ≤ o + o'
⊢ n + o + (n' + o') - (n + o) = n + n' - n + (o + o' - o)
[PROOFSTEP]
rw [add_tsub_cancel_left]
[GOAL]
case intro.intro
R : Type u_1
inst✝ : Semiring R
f : R[X]
n o n' : ℕ
hn : n ≤ n + n'
o' : ℕ
ho : o ≤ o + o'
⊢ n' + o' = n + n' - n + (o + o' - o)
[PROOFSTEP]
rw [add_tsub_cancel_left]
[GOAL]
case intro.intro
R : Type u_1
inst✝ : Semiring R
f : R[X]
n o n' : ℕ
hn : n ≤ n + n'
o' : ℕ
ho : o ≤ o + o'
⊢ n' + o' = n' + (o + o' - o)
[PROOFSTEP]
rw [add_tsub_cancel_left]
[GOAL]
R : Type u_1
inst✝ : Semiring R
f : R[X]
N : ℕ
⊢ ↑(revAt N) 0 = N
[PROOFSTEP]
simp
[GOAL]
R : Type u_1
inst✝ : Semiring R
f✝ : R[X]
N : ℕ
f : R[X]
⊢ support (reflect N f) = image (↑(revAt N)) (support f)
[PROOFSTEP]
rcases f with ⟨⟩
[GOAL]
case ofFinsupp
R : Type u_1
inst✝ : Semiring R
f : R[X]
N : ℕ
toFinsupp✝ : AddMonoidAlgebra R ℕ
⊢ support (reflect N { toFinsupp := toFinsupp✝ }) = image (↑(revAt N)) (support { toFinsupp := toFinsupp✝ })
[PROOFSTEP]
ext1
[GOAL]
case ofFinsupp.a
R : Type u_1
inst✝ : Semiring R
f : R[X]
N : ℕ
toFinsupp✝ : AddMonoidAlgebra R ℕ
a✝ : ℕ
⊢ a✝ ∈ support (reflect N { toFinsupp := toFinsupp✝ }) ↔ a✝ ∈ image (↑(revAt N)) (support { toFinsupp := toFinsupp✝ })
[PROOFSTEP]
simp only [reflect, support_ofFinsupp, support_embDomain, Finset.mem_map, Finset.mem_image]
[GOAL]
R : Type u_1
inst✝ : Semiring R
f✝ : R[X]
N : ℕ
f : R[X]
i : ℕ
⊢ coeff (reflect N f) i = coeff f (↑(revAt N) i)
[PROOFSTEP]
rcases f with ⟨f⟩
[GOAL]
case ofFinsupp
R : Type u_1
inst✝ : Semiring R
f✝ : R[X]
N i : ℕ
f : AddMonoidAlgebra R ℕ
⊢ coeff (reflect N { toFinsupp := f }) i = coeff { toFinsupp := f } (↑(revAt N) i)
[PROOFSTEP]
simp only [reflect, coeff]
[GOAL]
case ofFinsupp
R : Type u_1
inst✝ : Semiring R
f✝ : R[X]
N i : ℕ
f : AddMonoidAlgebra R ℕ
⊢ ↑(embDomain (revAt N) f) i = ↑f (↑(revAt N) i)
[PROOFSTEP]
calc
  Finsupp.embDomain (revAt N) f i = Finsupp.embDomain (revAt N) f (revAt N (revAt N i)) := by rw [revAt_invol]
  _ = f (revAt N i) := Finsupp.embDomain_apply _ _ _
[GOAL]
R : Type u_1
inst✝ : Semiring R
f✝ : R[X]
N i : ℕ
f : AddMonoidAlgebra R ℕ
⊢ ↑(embDomain (revAt N) f) i = ↑(embDomain (revAt N) f) (↑(revAt N) (↑(revAt N) i))
[PROOFSTEP]
rw [revAt_invol]
[GOAL]
R : Type u_1
inst✝ : Semiring R
f✝ : R[X]
N : ℕ
f : R[X]
⊢ reflect N f = 0 ↔ f = 0
[PROOFSTEP]
rw [ofFinsupp_eq_zero, reflect, embDomain_eq_zero, ofFinsupp_eq_zero]
[GOAL]
R : Type u_1
inst✝ : Semiring R
f✝ f g : R[X]
N : ℕ
⊢ reflect N (f + g) = reflect N f + reflect N g
[PROOFSTEP]
ext
[GOAL]
case a
R : Type u_1
inst✝ : Semiring R
f✝ f g : R[X]
N n✝ : ℕ
⊢ coeff (reflect N (f + g)) n✝ = coeff (reflect N f + reflect N g) n✝
[PROOFSTEP]
simp only [coeff_add, coeff_reflect]
[GOAL]
R : Type u_1
inst✝ : Semiring R
f✝ f : R[X]
r : R
N : ℕ
⊢ reflect N (↑C r * f) = ↑C r * reflect N f
[PROOFSTEP]
ext
[GOAL]
case a
R : Type u_1
inst✝ : Semiring R
f✝ f : R[X]
r : R
N n✝ : ℕ
⊢ coeff (reflect N (↑C r * f)) n✝ = coeff (↑C r * reflect N f) n✝
[PROOFSTEP]
simp only [coeff_reflect, coeff_C_mul]
[GOAL]
R : Type u_1
inst✝ : Semiring R
f : R[X]
N n : ℕ
c : R
⊢ reflect N (↑C c * X ^ n) = ↑C c * X ^ ↑(revAt N) n
[PROOFSTEP]
ext
[GOAL]
case a
R : Type u_1
inst✝ : Semiring R
f : R[X]
N n : ℕ
c : R
n✝ : ℕ
⊢ coeff (reflect N (↑C c * X ^ n)) n✝ = coeff (↑C c * X ^ ↑(revAt N) n) n✝
[PROOFSTEP]
rw [reflect_C_mul, coeff_C_mul, coeff_C_mul, coeff_X_pow, coeff_reflect]
[GOAL]
case a
R : Type u_1
inst✝ : Semiring R
f : R[X]
N n : ℕ
c : R
n✝ : ℕ
⊢ c * coeff (X ^ n) (↑(revAt N) n✝) = c * if n✝ = ↑(revAt N) n then 1 else 0
[PROOFSTEP]
split_ifs with h
[GOAL]
case pos
R : Type u_1
inst✝ : Semiring R
f : R[X]
N n : ℕ
c : R
n✝ : ℕ
h : n✝ = ↑(revAt N) n
⊢ c * coeff (X ^ n) (↑(revAt N) n✝) = c * 1
[PROOFSTEP]
rw [h, revAt_invol, coeff_X_pow_self]
[GOAL]
case neg
R : Type u_1
inst✝ : Semiring R
f : R[X]
N n : ℕ
c : R
n✝ : ℕ
h : ¬n✝ = ↑(revAt N) n
⊢ c * coeff (X ^ n) (↑(revAt N) n✝) = c * 0
[PROOFSTEP]
rw [not_mem_support_iff.mp]
[GOAL]
case neg
R : Type u_1
inst✝ : Semiring R
f : R[X]
N n : ℕ
c : R
n✝ : ℕ
h : ¬n✝ = ↑(revAt N) n
⊢ ¬↑(revAt N) n✝ ∈ support (X ^ n)
[PROOFSTEP]
intro a
[GOAL]
case neg
R : Type u_1
inst✝ : Semiring R
f : R[X]
N n : ℕ
c : R
n✝ : ℕ
h : ¬n✝ = ↑(revAt N) n
a : ↑(revAt N) n✝ ∈ support (X ^ n)
⊢ False
[PROOFSTEP]
rw [← one_mul (X ^ n), ← C_1] at a
[GOAL]
case neg
R : Type u_1
inst✝ : Semiring R
f : R[X]
N n : ℕ
c : R
n✝ : ℕ
h : ¬n✝ = ↑(revAt N) n
a : ↑(revAt N) n✝ ∈ support (↑C 1 * X ^ n)
⊢ False
[PROOFSTEP]
apply h
[GOAL]
case neg
R : Type u_1
inst✝ : Semiring R
f : R[X]
N n : ℕ
c : R
n✝ : ℕ
h : ¬n✝ = ↑(revAt N) n
a : ↑(revAt N) n✝ ∈ support (↑C 1 * X ^ n)
⊢ n✝ = ↑(revAt N) n
[PROOFSTEP]
rw [← mem_support_C_mul_X_pow a, revAt_invol]
[GOAL]
R : Type u_1
inst✝ : Semiring R
f : R[X]
r : R
N : ℕ
⊢ reflect N (↑C r) = ↑C r * X ^ N
[PROOFSTEP]
conv_lhs => rw [← mul_one (C r), ← pow_zero X, reflect_C_mul_X_pow, revAt_zero]
[GOAL]
R : Type u_1
inst✝ : Semiring R
f : R[X]
r : R
N : ℕ
| reflect N (↑C r)
[PROOFSTEP]
rw [← mul_one (C r), ← pow_zero X, reflect_C_mul_X_pow, revAt_zero]
[GOAL]
R : Type u_1
inst✝ : Semiring R
f : R[X]
r : R
N : ℕ
| reflect N (↑C r)
[PROOFSTEP]
rw [← mul_one (C r), ← pow_zero X, reflect_C_mul_X_pow, revAt_zero]
[GOAL]
R : Type u_1
inst✝ : Semiring R
f : R[X]
r : R
N : ℕ
| reflect N (↑C r)
[PROOFSTEP]
rw [← mul_one (C r), ← pow_zero X, reflect_C_mul_X_pow, revAt_zero]
[GOAL]
R : Type u_1
inst✝ : Semiring R
f : R[X]
N n : ℕ
⊢ reflect N (X ^ n) = X ^ ↑(revAt N) n
[PROOFSTEP]
rw [← one_mul (X ^ n), ← one_mul (X ^ revAt N n), ← C_1, reflect_C_mul_X_pow]
[GOAL]
R : Type u_1
inst✝ : Semiring R
f : R[X]
cf cg : ℕ
⊢ ∀ (N O : ℕ) (f g : R[X]),
    card (support f) ≤ Nat.succ cf →
      card (support g) ≤ Nat.succ cg →
        natDegree f ≤ N → natDegree g ≤ O → reflect (N + O) (f * g) = reflect N f * reflect O g
[PROOFSTEP]
induction' cf with cf hcf
[GOAL]
case zero
R : Type u_1
inst✝ : Semiring R
f : R[X]
cg : ℕ
⊢ ∀ (N O : ℕ) (f g : R[X]),
    card (support f) ≤ Nat.succ Nat.zero →
      card (support g) ≤ Nat.succ cg →
        natDegree f ≤ N → natDegree g ≤ O → reflect (N + O) (f * g) = reflect N f * reflect O g
[PROOFSTEP]
induction' cg with cg hcg
[GOAL]
case zero.zero
R : Type u_1
inst✝ : Semiring R
f : R[X]
⊢ ∀ (N O : ℕ) (f g : R[X]),
    card (support f) ≤ Nat.succ Nat.zero →
      card (support g) ≤ Nat.succ Nat.zero →
        natDegree f ≤ N → natDegree g ≤ O → reflect (N + O) (f * g) = reflect N f * reflect O g
[PROOFSTEP]
intro N O f g Cf Cg Nf Og
[GOAL]
case zero.zero
R : Type u_1
inst✝ : Semiring R
f✝ : R[X]
N O : ℕ
f g : R[X]
Cf : card (support f) ≤ Nat.succ Nat.zero
Cg : card (support g) ≤ Nat.succ Nat.zero
Nf : natDegree f ≤ N
Og : natDegree g ≤ O
⊢ reflect (N + O) (f * g) = reflect N f * reflect O g
[PROOFSTEP]
rw [← C_mul_X_pow_eq_self Cf, ← C_mul_X_pow_eq_self Cg]
[GOAL]
case zero.zero
R : Type u_1
inst✝ : Semiring R
f✝ : R[X]
N O : ℕ
f g : R[X]
Cf : card (support f) ≤ Nat.succ Nat.zero
Cg : card (support g) ≤ Nat.succ Nat.zero
Nf : natDegree f ≤ N
Og : natDegree g ≤ O
⊢ reflect (N + O) (↑C (leadingCoeff f) * X ^ natDegree f * (↑C (leadingCoeff g) * X ^ natDegree g)) =
    reflect N (↑C (leadingCoeff f) * X ^ natDegree f) * reflect O (↑C (leadingCoeff g) * X ^ natDegree g)
[PROOFSTEP]
simp_rw [mul_assoc, X_pow_mul, mul_assoc, ← pow_add (X : R[X]), reflect_C_mul, reflect_monomial, add_comm,
  revAt_add Nf Og, mul_assoc, X_pow_mul, mul_assoc, ← pow_add (X : R[X]), add_comm]
  -- second induction (right): induction step
[GOAL]
case zero.succ
R : Type u_1
inst✝ : Semiring R
f : R[X]
cg : ℕ
hcg :
  ∀ (N O : ℕ) (f g : R[X]),
    card (support f) ≤ Nat.succ Nat.zero →
      card (support g) ≤ Nat.succ cg →
        natDegree f ≤ N → natDegree g ≤ O → reflect (N + O) (f * g) = reflect N f * reflect O g
⊢ ∀ (N O : ℕ) (f g : R[X]),
    card (support f) ≤ Nat.succ Nat.zero →
      card (support g) ≤ Nat.succ (Nat.succ cg) →
        natDegree f ≤ N → natDegree g ≤ O → reflect (N + O) (f * g) = reflect N f * reflect O g
[PROOFSTEP]
intro N O f g Cf Cg Nf Og
[GOAL]
case zero.succ
R : Type u_1
inst✝ : Semiring R
f✝ : R[X]
cg : ℕ
hcg :
  ∀ (N O : ℕ) (f g : R[X]),
    card (support f) ≤ Nat.succ Nat.zero →
      card (support g) ≤ Nat.succ cg →
        natDegree f ≤ N → natDegree g ≤ O → reflect (N + O) (f * g) = reflect N f * reflect O g
N O : ℕ
f g : R[X]
Cf : card (support f) ≤ Nat.succ Nat.zero
Cg : card (support g) ≤ Nat.succ (Nat.succ cg)
Nf : natDegree f ≤ N
Og : natDegree g ≤ O
⊢ reflect (N + O) (f * g) = reflect N f * reflect O g
[PROOFSTEP]
by_cases g0 : g = 0
[GOAL]
case pos
R : Type u_1
inst✝ : Semiring R
f✝ : R[X]
cg : ℕ
hcg :
  ∀ (N O : ℕ) (f g : R[X]),
    card (support f) ≤ Nat.succ Nat.zero →
      card (support g) ≤ Nat.succ cg →
        natDegree f ≤ N → natDegree g ≤ O → reflect (N + O) (f * g) = reflect N f * reflect O g
N O : ℕ
f g : R[X]
Cf : card (support f) ≤ Nat.succ Nat.zero
Cg : card (support g) ≤ Nat.succ (Nat.succ cg)
Nf : natDegree f ≤ N
Og : natDegree g ≤ O
g0 : g = 0
⊢ reflect (N + O) (f * g) = reflect N f * reflect O g
[PROOFSTEP]
rw [g0, reflect_zero, mul_zero, mul_zero, reflect_zero]
[GOAL]
case neg
R : Type u_1
inst✝ : Semiring R
f✝ : R[X]
cg : ℕ
hcg :
  ∀ (N O : ℕ) (f g : R[X]),
    card (support f) ≤ Nat.succ Nat.zero →
      card (support g) ≤ Nat.succ cg →
        natDegree f ≤ N → natDegree g ≤ O → reflect (N + O) (f * g) = reflect N f * reflect O g
N O : ℕ
f g : R[X]
Cf : card (support f) ≤ Nat.succ Nat.zero
Cg : card (support g) ≤ Nat.succ (Nat.succ cg)
Nf : natDegree f ≤ N
Og : natDegree g ≤ O
g0 : ¬g = 0
⊢ reflect (N + O) (f * g) = reflect N f * reflect O g
[PROOFSTEP]
rw [← eraseLead_add_C_mul_X_pow g, mul_add, reflect_add, reflect_add, mul_add, hcg, hcg]
[GOAL]
case neg.a
R : Type u_1
inst✝ : Semiring R
f✝ : R[X]
cg : ℕ
hcg :
  ∀ (N O : ℕ) (f g : R[X]),
    card (support f) ≤ Nat.succ Nat.zero →
      card (support g) ≤ Nat.succ cg →
        natDegree f ≤ N → natDegree g ≤ O → reflect (N + O) (f * g) = reflect N f * reflect O g
N O : ℕ
f g : R[X]
Cf : card (support f) ≤ Nat.succ Nat.zero
Cg : card (support g) ≤ Nat.succ (Nat.succ cg)
Nf : natDegree f ≤ N
Og : natDegree g ≤ O
g0 : ¬g = 0
⊢ card (support f) ≤ Nat.succ Nat.zero
[PROOFSTEP]
try assumption
[GOAL]
case neg.a
R : Type u_1
inst✝ : Semiring R
f✝ : R[X]
cg : ℕ
hcg :
  ∀ (N O : ℕ) (f g : R[X]),
    card (support f) ≤ Nat.succ Nat.zero →
      card (support g) ≤ Nat.succ cg →
        natDegree f ≤ N → natDegree g ≤ O → reflect (N + O) (f * g) = reflect N f * reflect O g
N O : ℕ
f g : R[X]
Cf : card (support f) ≤ Nat.succ Nat.zero
Cg : card (support g) ≤ Nat.succ (Nat.succ cg)
Nf : natDegree f ≤ N
Og : natDegree g ≤ O
g0 : ¬g = 0
⊢ card (support f) ≤ Nat.succ Nat.zero
[PROOFSTEP]
assumption
[GOAL]
case neg.a
R : Type u_1
inst✝ : Semiring R
f✝ : R[X]
cg : ℕ
hcg :
  ∀ (N O : ℕ) (f g : R[X]),
    card (support f) ≤ Nat.succ Nat.zero →
      card (support g) ≤ Nat.succ cg →
        natDegree f ≤ N → natDegree g ≤ O → reflect (N + O) (f * g) = reflect N f * reflect O g
N O : ℕ
f g : R[X]
Cf : card (support f) ≤ Nat.succ Nat.zero
Cg : card (support g) ≤ Nat.succ (Nat.succ cg)
Nf : natDegree f ≤ N
Og : natDegree g ≤ O
g0 : ¬g = 0
⊢ card (support (↑C (leadingCoeff g) * X ^ natDegree g)) ≤ Nat.succ cg
[PROOFSTEP]
try assumption
[GOAL]
case neg.a
R : Type u_1
inst✝ : Semiring R
f✝ : R[X]
cg : ℕ
hcg :
  ∀ (N O : ℕ) (f g : R[X]),
    card (support f) ≤ Nat.succ Nat.zero →
      card (support g) ≤ Nat.succ cg →
        natDegree f ≤ N → natDegree g ≤ O → reflect (N + O) (f * g) = reflect N f * reflect O g
N O : ℕ
f g : R[X]
Cf : card (support f) ≤ Nat.succ Nat.zero
Cg : card (support g) ≤ Nat.succ (Nat.succ cg)
Nf : natDegree f ≤ N
Og : natDegree g ≤ O
g0 : ¬g = 0
⊢ card (support (↑C (leadingCoeff g) * X ^ natDegree g)) ≤ Nat.succ cg
[PROOFSTEP]
assumption
[GOAL]
case neg.a
R : Type u_1
inst✝ : Semiring R
f✝ : R[X]
cg : ℕ
hcg :
  ∀ (N O : ℕ) (f g : R[X]),
    card (support f) ≤ Nat.succ Nat.zero →
      card (support g) ≤ Nat.succ cg →
        natDegree f ≤ N → natDegree g ≤ O → reflect (N + O) (f * g) = reflect N f * reflect O g
N O : ℕ
f g : R[X]
Cf : card (support f) ≤ Nat.succ Nat.zero
Cg : card (support g) ≤ Nat.succ (Nat.succ cg)
Nf : natDegree f ≤ N
Og : natDegree g ≤ O
g0 : ¬g = 0
⊢ natDegree f ≤ N
[PROOFSTEP]
try assumption
[GOAL]
case neg.a
R : Type u_1
inst✝ : Semiring R
f✝ : R[X]
cg : ℕ
hcg :
  ∀ (N O : ℕ) (f g : R[X]),
    card (support f) ≤ Nat.succ Nat.zero →
      card (support g) ≤ Nat.succ cg →
        natDegree f ≤ N → natDegree g ≤ O → reflect (N + O) (f * g) = reflect N f * reflect O g
N O : ℕ
f g : R[X]
Cf : card (support f) ≤ Nat.succ Nat.zero
Cg : card (support g) ≤ Nat.succ (Nat.succ cg)
Nf : natDegree f ≤ N
Og : natDegree g ≤ O
g0 : ¬g = 0
⊢ natDegree f ≤ N
[PROOFSTEP]
assumption
[GOAL]
case neg.a
R : Type u_1
inst✝ : Semiring R
f✝ : R[X]
cg : ℕ
hcg :
  ∀ (N O : ℕ) (f g : R[X]),
    card (support f) ≤ Nat.succ Nat.zero →
      card (support g) ≤ Nat.succ cg →
        natDegree f ≤ N → natDegree g ≤ O → reflect (N + O) (f * g) = reflect N f * reflect O g
N O : ℕ
f g : R[X]
Cf : card (support f) ≤ Nat.succ Nat.zero
Cg : card (support g) ≤ Nat.succ (Nat.succ cg)
Nf : natDegree f ≤ N
Og : natDegree g ≤ O
g0 : ¬g = 0
⊢ natDegree (↑C (leadingCoeff g) * X ^ natDegree g) ≤ O
[PROOFSTEP]
try assumption
[GOAL]
case neg.a
R : Type u_1
inst✝ : Semiring R
f✝ : R[X]
cg : ℕ
hcg :
  ∀ (N O : ℕ) (f g : R[X]),
    card (support f) ≤ Nat.succ Nat.zero →
      card (support g) ≤ Nat.succ cg →
        natDegree f ≤ N → natDegree g ≤ O → reflect (N + O) (f * g) = reflect N f * reflect O g
N O : ℕ
f g : R[X]
Cf : card (support f) ≤ Nat.succ Nat.zero
Cg : card (support g) ≤ Nat.succ (Nat.succ cg)
Nf : natDegree f ≤ N
Og : natDegree g ≤ O
g0 : ¬g = 0
⊢ natDegree (↑C (leadingCoeff g) * X ^ natDegree g) ≤ O
[PROOFSTEP]
assumption
[GOAL]
case neg.a
R : Type u_1
inst✝ : Semiring R
f✝ : R[X]
cg : ℕ
hcg :
  ∀ (N O : ℕ) (f g : R[X]),
    card (support f) ≤ Nat.succ Nat.zero →
      card (support g) ≤ Nat.succ cg →
        natDegree f ≤ N → natDegree g ≤ O → reflect (N + O) (f * g) = reflect N f * reflect O g
N O : ℕ
f g : R[X]
Cf : card (support f) ≤ Nat.succ Nat.zero
Cg : card (support g) ≤ Nat.succ (Nat.succ cg)
Nf : natDegree f ≤ N
Og : natDegree g ≤ O
g0 : ¬g = 0
⊢ card (support f) ≤ Nat.succ Nat.zero
[PROOFSTEP]
try assumption
[GOAL]
case neg.a
R : Type u_1
inst✝ : Semiring R
f✝ : R[X]
cg : ℕ
hcg :
  ∀ (N O : ℕ) (f g : R[X]),
    card (support f) ≤ Nat.succ Nat.zero →
      card (support g) ≤ Nat.succ cg →
        natDegree f ≤ N → natDegree g ≤ O → reflect (N + O) (f * g) = reflect N f * reflect O g
N O : ℕ
f g : R[X]
Cf : card (support f) ≤ Nat.succ Nat.zero
Cg : card (support g) ≤ Nat.succ (Nat.succ cg)
Nf : natDegree f ≤ N
Og : natDegree g ≤ O
g0 : ¬g = 0
⊢ card (support f) ≤ Nat.succ Nat.zero
[PROOFSTEP]
assumption
[GOAL]
case neg.a
R : Type u_1
inst✝ : Semiring R
f✝ : R[X]
cg : ℕ
hcg :
  ∀ (N O : ℕ) (f g : R[X]),
    card (support f) ≤ Nat.succ Nat.zero →
      card (support g) ≤ Nat.succ cg →
        natDegree f ≤ N → natDegree g ≤ O → reflect (N + O) (f * g) = reflect N f * reflect O g
N O : ℕ
f g : R[X]
Cf : card (support f) ≤ Nat.succ Nat.zero
Cg : card (support g) ≤ Nat.succ (Nat.succ cg)
Nf : natDegree f ≤ N
Og : natDegree g ≤ O
g0 : ¬g = 0
⊢ card (support (eraseLead g)) ≤ Nat.succ cg
[PROOFSTEP]
try assumption
[GOAL]
case neg.a
R : Type u_1
inst✝ : Semiring R
f✝ : R[X]
cg : ℕ
hcg :
  ∀ (N O : ℕ) (f g : R[X]),
    card (support f) ≤ Nat.succ Nat.zero →
      card (support g) ≤ Nat.succ cg →
        natDegree f ≤ N → natDegree g ≤ O → reflect (N + O) (f * g) = reflect N f * reflect O g
N O : ℕ
f g : R[X]
Cf : card (support f) ≤ Nat.succ Nat.zero
Cg : card (support g) ≤ Nat.succ (Nat.succ cg)
Nf : natDegree f ≤ N
Og : natDegree g ≤ O
g0 : ¬g = 0
⊢ card (support (eraseLead g)) ≤ Nat.succ cg
[PROOFSTEP]
assumption
[GOAL]
case neg.a
R : Type u_1
inst✝ : Semiring R
f✝ : R[X]
cg : ℕ
hcg :
  ∀ (N O : ℕ) (f g : R[X]),
    card (support f) ≤ Nat.succ Nat.zero →
      card (support g) ≤ Nat.succ cg →
        natDegree f ≤ N → natDegree g ≤ O → reflect (N + O) (f * g) = reflect N f * reflect O g
N O : ℕ
f g : R[X]
Cf : card (support f) ≤ Nat.succ Nat.zero
Cg : card (support g) ≤ Nat.succ (Nat.succ cg)
Nf : natDegree f ≤ N
Og : natDegree g ≤ O
g0 : ¬g = 0
⊢ natDegree f ≤ N
[PROOFSTEP]
try assumption
[GOAL]
case neg.a
R : Type u_1
inst✝ : Semiring R
f✝ : R[X]
cg : ℕ
hcg :
  ∀ (N O : ℕ) (f g : R[X]),
    card (support f) ≤ Nat.succ Nat.zero →
      card (support g) ≤ Nat.succ cg →
        natDegree f ≤ N → natDegree g ≤ O → reflect (N + O) (f * g) = reflect N f * reflect O g
N O : ℕ
f g : R[X]
Cf : card (support f) ≤ Nat.succ Nat.zero
Cg : card (support g) ≤ Nat.succ (Nat.succ cg)
Nf : natDegree f ≤ N
Og : natDegree g ≤ O
g0 : ¬g = 0
⊢ natDegree f ≤ N
[PROOFSTEP]
assumption
[GOAL]
case neg.a
R : Type u_1
inst✝ : Semiring R
f✝ : R[X]
cg : ℕ
hcg :
  ∀ (N O : ℕ) (f g : R[X]),
    card (support f) ≤ Nat.succ Nat.zero →
      card (support g) ≤ Nat.succ cg →
        natDegree f ≤ N → natDegree g ≤ O → reflect (N + O) (f * g) = reflect N f * reflect O g
N O : ℕ
f g : R[X]
Cf : card (support f) ≤ Nat.succ Nat.zero
Cg : card (support g) ≤ Nat.succ (Nat.succ cg)
Nf : natDegree f ≤ N
Og : natDegree g ≤ O
g0 : ¬g = 0
⊢ natDegree (eraseLead g) ≤ O
[PROOFSTEP]
try assumption
[GOAL]
case neg.a
R : Type u_1
inst✝ : Semiring R
f✝ : R[X]
cg : ℕ
hcg :
  ∀ (N O : ℕ) (f g : R[X]),
    card (support f) ≤ Nat.succ Nat.zero →
      card (support g) ≤ Nat.succ cg →
        natDegree f ≤ N → natDegree g ≤ O → reflect (N + O) (f * g) = reflect N f * reflect O g
N O : ℕ
f g : R[X]
Cf : card (support f) ≤ Nat.succ Nat.zero
Cg : card (support g) ≤ Nat.succ (Nat.succ cg)
Nf : natDegree f ≤ N
Og : natDegree g ≤ O
g0 : ¬g = 0
⊢ natDegree (eraseLead g) ≤ O
[PROOFSTEP]
assumption
[GOAL]
case neg.a
R : Type u_1
inst✝ : Semiring R
f✝ : R[X]
cg : ℕ
hcg :
  ∀ (N O : ℕ) (f g : R[X]),
    card (support f) ≤ Nat.succ Nat.zero →
      card (support g) ≤ Nat.succ cg →
        natDegree f ≤ N → natDegree g ≤ O → reflect (N + O) (f * g) = reflect N f * reflect O g
N O : ℕ
f g : R[X]
Cf : card (support f) ≤ Nat.succ Nat.zero
Cg : card (support g) ≤ Nat.succ (Nat.succ cg)
Nf : natDegree f ≤ N
Og : natDegree g ≤ O
g0 : ¬g = 0
⊢ card (support (↑C (leadingCoeff g) * X ^ natDegree g)) ≤ Nat.succ cg
[PROOFSTEP]
exact le_add_left card_support_C_mul_X_pow_le_one
[GOAL]
case neg.a
R : Type u_1
inst✝ : Semiring R
f✝ : R[X]
cg : ℕ
hcg :
  ∀ (N O : ℕ) (f g : R[X]),
    card (support f) ≤ Nat.succ Nat.zero →
      card (support g) ≤ Nat.succ cg →
        natDegree f ≤ N → natDegree g ≤ O → reflect (N + O) (f * g) = reflect N f * reflect O g
N O : ℕ
f g : R[X]
Cf : card (support f) ≤ Nat.succ Nat.zero
Cg : card (support g) ≤ Nat.succ (Nat.succ cg)
Nf : natDegree f ≤ N
Og : natDegree g ≤ O
g0 : ¬g = 0
⊢ natDegree (↑C (leadingCoeff g) * X ^ natDegree g) ≤ O
[PROOFSTEP]
exact le_trans (natDegree_C_mul_X_pow_le g.leadingCoeff g.natDegree) Og
[GOAL]
case neg.a
R : Type u_1
inst✝ : Semiring R
f✝ : R[X]
cg : ℕ
hcg :
  ∀ (N O : ℕ) (f g : R[X]),
    card (support f) ≤ Nat.succ Nat.zero →
      card (support g) ≤ Nat.succ cg →
        natDegree f ≤ N → natDegree g ≤ O → reflect (N + O) (f * g) = reflect N f * reflect O g
N O : ℕ
f g : R[X]
Cf : card (support f) ≤ Nat.succ Nat.zero
Cg : card (support g) ≤ Nat.succ (Nat.succ cg)
Nf : natDegree f ≤ N
Og : natDegree g ≤ O
g0 : ¬g = 0
⊢ card (support (eraseLead g)) ≤ Nat.succ cg
[PROOFSTEP]
exact Nat.lt_succ_iff.mp (gt_of_ge_of_gt Cg (eraseLead_support_card_lt g0))
[GOAL]
case neg.a
R : Type u_1
inst✝ : Semiring R
f✝ : R[X]
cg : ℕ
hcg :
  ∀ (N O : ℕ) (f g : R[X]),
    card (support f) ≤ Nat.succ Nat.zero →
      card (support g) ≤ Nat.succ cg →
        natDegree f ≤ N → natDegree g ≤ O → reflect (N + O) (f * g) = reflect N f * reflect O g
N O : ℕ
f g : R[X]
Cf : card (support f) ≤ Nat.succ Nat.zero
Cg : card (support g) ≤ Nat.succ (Nat.succ cg)
Nf : natDegree f ≤ N
Og : natDegree g ≤ O
g0 : ¬g = 0
⊢ natDegree (eraseLead g) ≤ O
[PROOFSTEP]
exact le_trans eraseLead_natDegree_le_aux Og
[GOAL]
case succ
R : Type u_1
inst✝ : Semiring R
f : R[X]
cg cf : ℕ
hcf :
  ∀ (N O : ℕ) (f g : R[X]),
    card (support f) ≤ Nat.succ cf →
      card (support g) ≤ Nat.succ cg →
        natDegree f ≤ N → natDegree g ≤ O → reflect (N + O) (f * g) = reflect N f * reflect O g
⊢ ∀ (N O : ℕ) (f g : R[X]),
    card (support f) ≤ Nat.succ (Nat.succ cf) →
      card (support g) ≤ Nat.succ cg →
        natDegree f ≤ N → natDegree g ≤ O → reflect (N + O) (f * g) = reflect N f * reflect O g
[PROOFSTEP]
intro N O f g Cf Cg Nf Og
[GOAL]
case succ
R : Type u_1
inst✝ : Semiring R
f✝ : R[X]
cg cf : ℕ
hcf :
  ∀ (N O : ℕ) (f g : R[X]),
    card (support f) ≤ Nat.succ cf →
      card (support g) ≤ Nat.succ cg →
        natDegree f ≤ N → natDegree g ≤ O → reflect (N + O) (f * g) = reflect N f * reflect O g
N O : ℕ
f g : R[X]
Cf : card (support f) ≤ Nat.succ (Nat.succ cf)
Cg : card (support g) ≤ Nat.succ cg
Nf : natDegree f ≤ N
Og : natDegree g ≤ O
⊢ reflect (N + O) (f * g) = reflect N f * reflect O g
[PROOFSTEP]
by_cases f0 : f = 0
[GOAL]
case pos
R : Type u_1
inst✝ : Semiring R
f✝ : R[X]
cg cf : ℕ
hcf :
  ∀ (N O : ℕ) (f g : R[X]),
    card (support f) ≤ Nat.succ cf →
      card (support g) ≤ Nat.succ cg →
        natDegree f ≤ N → natDegree g ≤ O → reflect (N + O) (f * g) = reflect N f * reflect O g
N O : ℕ
f g : R[X]
Cf : card (support f) ≤ Nat.succ (Nat.succ cf)
Cg : card (support g) ≤ Nat.succ cg
Nf : natDegree f ≤ N
Og : natDegree g ≤ O
f0 : f = 0
⊢ reflect (N + O) (f * g) = reflect N f * reflect O g
[PROOFSTEP]
rw [f0, reflect_zero, zero_mul, zero_mul, reflect_zero]
[GOAL]
case neg
R : Type u_1
inst✝ : Semiring R
f✝ : R[X]
cg cf : ℕ
hcf :
  ∀ (N O : ℕ) (f g : R[X]),
    card (support f) ≤ Nat.succ cf →
      card (support g) ≤ Nat.succ cg →
        natDegree f ≤ N → natDegree g ≤ O → reflect (N + O) (f * g) = reflect N f * reflect O g
N O : ℕ
f g : R[X]
Cf : card (support f) ≤ Nat.succ (Nat.succ cf)
Cg : card (support g) ≤ Nat.succ cg
Nf : natDegree f ≤ N
Og : natDegree g ≤ O
f0 : ¬f = 0
⊢ reflect (N + O) (f * g) = reflect N f * reflect O g
[PROOFSTEP]
rw [← eraseLead_add_C_mul_X_pow f, add_mul, reflect_add, reflect_add, add_mul, hcf, hcf]
[GOAL]
case neg.a
R : Type u_1
inst✝ : Semiring R
f✝ : R[X]
cg cf : ℕ
hcf :
  ∀ (N O : ℕ) (f g : R[X]),
    card (support f) ≤ Nat.succ cf →
      card (support g) ≤ Nat.succ cg →
        natDegree f ≤ N → natDegree g ≤ O → reflect (N + O) (f * g) = reflect N f * reflect O g
N O : ℕ
f g : R[X]
Cf : card (support f) ≤ Nat.succ (Nat.succ cf)
Cg : card (support g) ≤ Nat.succ cg
Nf : natDegree f ≤ N
Og : natDegree g ≤ O
f0 : ¬f = 0
⊢ card (support (↑C (leadingCoeff f) * X ^ natDegree f)) ≤ Nat.succ cf
[PROOFSTEP]
try assumption
[GOAL]
case neg.a
R : Type u_1
inst✝ : Semiring R
f✝ : R[X]
cg cf : ℕ
hcf :
  ∀ (N O : ℕ) (f g : R[X]),
    card (support f) ≤ Nat.succ cf →
      card (support g) ≤ Nat.succ cg →
        natDegree f ≤ N → natDegree g ≤ O → reflect (N + O) (f * g) = reflect N f * reflect O g
N O : ℕ
f g : R[X]
Cf : card (support f) ≤ Nat.succ (Nat.succ cf)
Cg : card (support g) ≤ Nat.succ cg
Nf : natDegree f ≤ N
Og : natDegree g ≤ O
f0 : ¬f = 0
⊢ card (support (↑C (leadingCoeff f) * X ^ natDegree f)) ≤ Nat.succ cf
[PROOFSTEP]
assumption
[GOAL]
case neg.a
R : Type u_1
inst✝ : Semiring R
f✝ : R[X]
cg cf : ℕ
hcf :
  ∀ (N O : ℕ) (f g : R[X]),
    card (support f) ≤ Nat.succ cf →
      card (support g) ≤ Nat.succ cg →
        natDegree f ≤ N → natDegree g ≤ O → reflect (N + O) (f * g) = reflect N f * reflect O g
N O : ℕ
f g : R[X]
Cf : card (support f) ≤ Nat.succ (Nat.succ cf)
Cg : card (support g) ≤ Nat.succ cg
Nf : natDegree f ≤ N
Og : natDegree g ≤ O
f0 : ¬f = 0
⊢ card (support g) ≤ Nat.succ cg
[PROOFSTEP]
try assumption
[GOAL]
case neg.a
R : Type u_1
inst✝ : Semiring R
f✝ : R[X]
cg cf : ℕ
hcf :
  ∀ (N O : ℕ) (f g : R[X]),
    card (support f) ≤ Nat.succ cf →
      card (support g) ≤ Nat.succ cg →
        natDegree f ≤ N → natDegree g ≤ O → reflect (N + O) (f * g) = reflect N f * reflect O g
N O : ℕ
f g : R[X]
Cf : card (support f) ≤ Nat.succ (Nat.succ cf)
Cg : card (support g) ≤ Nat.succ cg
Nf : natDegree f ≤ N
Og : natDegree g ≤ O
f0 : ¬f = 0
⊢ card (support g) ≤ Nat.succ cg
[PROOFSTEP]
assumption
[GOAL]
case neg.a
R : Type u_1
inst✝ : Semiring R
f✝ : R[X]
cg cf : ℕ
hcf :
  ∀ (N O : ℕ) (f g : R[X]),
    card (support f) ≤ Nat.succ cf →
      card (support g) ≤ Nat.succ cg →
        natDegree f ≤ N → natDegree g ≤ O → reflect (N + O) (f * g) = reflect N f * reflect O g
N O : ℕ
f g : R[X]
Cf : card (support f) ≤ Nat.succ (Nat.succ cf)
Cg : card (support g) ≤ Nat.succ cg
Nf : natDegree f ≤ N
Og : natDegree g ≤ O
f0 : ¬f = 0
⊢ natDegree (↑C (leadingCoeff f) * X ^ natDegree f) ≤ N
[PROOFSTEP]
try assumption
[GOAL]
case neg.a
R : Type u_1
inst✝ : Semiring R
f✝ : R[X]
cg cf : ℕ
hcf :
  ∀ (N O : ℕ) (f g : R[X]),
    card (support f) ≤ Nat.succ cf →
      card (support g) ≤ Nat.succ cg →
        natDegree f ≤ N → natDegree g ≤ O → reflect (N + O) (f * g) = reflect N f * reflect O g
N O : ℕ
f g : R[X]
Cf : card (support f) ≤ Nat.succ (Nat.succ cf)
Cg : card (support g) ≤ Nat.succ cg
Nf : natDegree f ≤ N
Og : natDegree g ≤ O
f0 : ¬f = 0
⊢ natDegree (↑C (leadingCoeff f) * X ^ natDegree f) ≤ N
[PROOFSTEP]
assumption
[GOAL]
case neg.a
R : Type u_1
inst✝ : Semiring R
f✝ : R[X]
cg cf : ℕ
hcf :
  ∀ (N O : ℕ) (f g : R[X]),
    card (support f) ≤ Nat.succ cf →
      card (support g) ≤ Nat.succ cg →
        natDegree f ≤ N → natDegree g ≤ O → reflect (N + O) (f * g) = reflect N f * reflect O g
N O : ℕ
f g : R[X]
Cf : card (support f) ≤ Nat.succ (Nat.succ cf)
Cg : card (support g) ≤ Nat.succ cg
Nf : natDegree f ≤ N
Og : natDegree g ≤ O
f0 : ¬f = 0
⊢ natDegree g ≤ O
[PROOFSTEP]
try assumption
[GOAL]
case neg.a
R : Type u_1
inst✝ : Semiring R
f✝ : R[X]
cg cf : ℕ
hcf :
  ∀ (N O : ℕ) (f g : R[X]),
    card (support f) ≤ Nat.succ cf →
      card (support g) ≤ Nat.succ cg →
        natDegree f ≤ N → natDegree g ≤ O → reflect (N + O) (f * g) = reflect N f * reflect O g
N O : ℕ
f g : R[X]
Cf : card (support f) ≤ Nat.succ (Nat.succ cf)
Cg : card (support g) ≤ Nat.succ cg
Nf : natDegree f ≤ N
Og : natDegree g ≤ O
f0 : ¬f = 0
⊢ natDegree g ≤ O
[PROOFSTEP]
assumption
[GOAL]
case neg.a
R : Type u_1
inst✝ : Semiring R
f✝ : R[X]
cg cf : ℕ
hcf :
  ∀ (N O : ℕ) (f g : R[X]),
    card (support f) ≤ Nat.succ cf →
      card (support g) ≤ Nat.succ cg →
        natDegree f ≤ N → natDegree g ≤ O → reflect (N + O) (f * g) = reflect N f * reflect O g
N O : ℕ
f g : R[X]
Cf : card (support f) ≤ Nat.succ (Nat.succ cf)
Cg : card (support g) ≤ Nat.succ cg
Nf : natDegree f ≤ N
Og : natDegree g ≤ O
f0 : ¬f = 0
⊢ card (support (eraseLead f)) ≤ Nat.succ cf
[PROOFSTEP]
try assumption
[GOAL]
case neg.a
R : Type u_1
inst✝ : Semiring R
f✝ : R[X]
cg cf : ℕ
hcf :
  ∀ (N O : ℕ) (f g : R[X]),
    card (support f) ≤ Nat.succ cf →
      card (support g) ≤ Nat.succ cg →
        natDegree f ≤ N → natDegree g ≤ O → reflect (N + O) (f * g) = reflect N f * reflect O g
N O : ℕ
f g : R[X]
Cf : card (support f) ≤ Nat.succ (Nat.succ cf)
Cg : card (support g) ≤ Nat.succ cg
Nf : natDegree f ≤ N
Og : natDegree g ≤ O
f0 : ¬f = 0
⊢ card (support (eraseLead f)) ≤ Nat.succ cf
[PROOFSTEP]
assumption
[GOAL]
case neg.a
R : Type u_1
inst✝ : Semiring R
f✝ : R[X]
cg cf : ℕ
hcf :
  ∀ (N O : ℕ) (f g : R[X]),
    card (support f) ≤ Nat.succ cf →
      card (support g) ≤ Nat.succ cg →
        natDegree f ≤ N → natDegree g ≤ O → reflect (N + O) (f * g) = reflect N f * reflect O g
N O : ℕ
f g : R[X]
Cf : card (support f) ≤ Nat.succ (Nat.succ cf)
Cg : card (support g) ≤ Nat.succ cg
Nf : natDegree f ≤ N
Og : natDegree g ≤ O
f0 : ¬f = 0
⊢ card (support g) ≤ Nat.succ cg
[PROOFSTEP]
try assumption
[GOAL]
case neg.a
R : Type u_1
inst✝ : Semiring R
f✝ : R[X]
cg cf : ℕ
hcf :
  ∀ (N O : ℕ) (f g : R[X]),
    card (support f) ≤ Nat.succ cf →
      card (support g) ≤ Nat.succ cg →
        natDegree f ≤ N → natDegree g ≤ O → reflect (N + O) (f * g) = reflect N f * reflect O g
N O : ℕ
f g : R[X]
Cf : card (support f) ≤ Nat.succ (Nat.succ cf)
Cg : card (support g) ≤ Nat.succ cg
Nf : natDegree f ≤ N
Og : natDegree g ≤ O
f0 : ¬f = 0
⊢ card (support g) ≤ Nat.succ cg
[PROOFSTEP]
assumption
[GOAL]
case neg.a
R : Type u_1
inst✝ : Semiring R
f✝ : R[X]
cg cf : ℕ
hcf :
  ∀ (N O : ℕ) (f g : R[X]),
    card (support f) ≤ Nat.succ cf →
      card (support g) ≤ Nat.succ cg →
        natDegree f ≤ N → natDegree g ≤ O → reflect (N + O) (f * g) = reflect N f * reflect O g
N O : ℕ
f g : R[X]
Cf : card (support f) ≤ Nat.succ (Nat.succ cf)
Cg : card (support g) ≤ Nat.succ cg
Nf : natDegree f ≤ N
Og : natDegree g ≤ O
f0 : ¬f = 0
⊢ natDegree (eraseLead f) ≤ N
[PROOFSTEP]
try assumption
[GOAL]
case neg.a
R : Type u_1
inst✝ : Semiring R
f✝ : R[X]
cg cf : ℕ
hcf :
  ∀ (N O : ℕ) (f g : R[X]),
    card (support f) ≤ Nat.succ cf →
      card (support g) ≤ Nat.succ cg →
        natDegree f ≤ N → natDegree g ≤ O → reflect (N + O) (f * g) = reflect N f * reflect O g
N O : ℕ
f g : R[X]
Cf : card (support f) ≤ Nat.succ (Nat.succ cf)
Cg : card (support g) ≤ Nat.succ cg
Nf : natDegree f ≤ N
Og : natDegree g ≤ O
f0 : ¬f = 0
⊢ natDegree (eraseLead f) ≤ N
[PROOFSTEP]
assumption
[GOAL]
case neg.a
R : Type u_1
inst✝ : Semiring R
f✝ : R[X]
cg cf : ℕ
hcf :
  ∀ (N O : ℕ) (f g : R[X]),
    card (support f) ≤ Nat.succ cf →
      card (support g) ≤ Nat.succ cg →
        natDegree f ≤ N → natDegree g ≤ O → reflect (N + O) (f * g) = reflect N f * reflect O g
N O : ℕ
f g : R[X]
Cf : card (support f) ≤ Nat.succ (Nat.succ cf)
Cg : card (support g) ≤ Nat.succ cg
Nf : natDegree f ≤ N
Og : natDegree g ≤ O
f0 : ¬f = 0
⊢ natDegree g ≤ O
[PROOFSTEP]
try assumption
[GOAL]
case neg.a
R : Type u_1
inst✝ : Semiring R
f✝ : R[X]
cg cf : ℕ
hcf :
  ∀ (N O : ℕ) (f g : R[X]),
    card (support f) ≤ Nat.succ cf →
      card (support g) ≤ Nat.succ cg →
        natDegree f ≤ N → natDegree g ≤ O → reflect (N + O) (f * g) = reflect N f * reflect O g
N O : ℕ
f g : R[X]
Cf : card (support f) ≤ Nat.succ (Nat.succ cf)
Cg : card (support g) ≤ Nat.succ cg
Nf : natDegree f ≤ N
Og : natDegree g ≤ O
f0 : ¬f = 0
⊢ natDegree g ≤ O
[PROOFSTEP]
assumption
[GOAL]
case neg.a
R : Type u_1
inst✝ : Semiring R
f✝ : R[X]
cg cf : ℕ
hcf :
  ∀ (N O : ℕ) (f g : R[X]),
    card (support f) ≤ Nat.succ cf →
      card (support g) ≤ Nat.succ cg →
        natDegree f ≤ N → natDegree g ≤ O → reflect (N + O) (f * g) = reflect N f * reflect O g
N O : ℕ
f g : R[X]
Cf : card (support f) ≤ Nat.succ (Nat.succ cf)
Cg : card (support g) ≤ Nat.succ cg
Nf : natDegree f ≤ N
Og : natDegree g ≤ O
f0 : ¬f = 0
⊢ card (support (↑C (leadingCoeff f) * X ^ natDegree f)) ≤ Nat.succ cf
[PROOFSTEP]
exact le_add_left card_support_C_mul_X_pow_le_one
[GOAL]
case neg.a
R : Type u_1
inst✝ : Semiring R
f✝ : R[X]
cg cf : ℕ
hcf :
  ∀ (N O : ℕ) (f g : R[X]),
    card (support f) ≤ Nat.succ cf →
      card (support g) ≤ Nat.succ cg →
        natDegree f ≤ N → natDegree g ≤ O → reflect (N + O) (f * g) = reflect N f * reflect O g
N O : ℕ
f g : R[X]
Cf : card (support f) ≤ Nat.succ (Nat.succ cf)
Cg : card (support g) ≤ Nat.succ cg
Nf : natDegree f ≤ N
Og : natDegree g ≤ O
f0 : ¬f = 0
⊢ natDegree (↑C (leadingCoeff f) * X ^ natDegree f) ≤ N
[PROOFSTEP]
exact le_trans (natDegree_C_mul_X_pow_le f.leadingCoeff f.natDegree) Nf
[GOAL]
case neg.a
R : Type u_1
inst✝ : Semiring R
f✝ : R[X]
cg cf : ℕ
hcf :
  ∀ (N O : ℕ) (f g : R[X]),
    card (support f) ≤ Nat.succ cf →
      card (support g) ≤ Nat.succ cg →
        natDegree f ≤ N → natDegree g ≤ O → reflect (N + O) (f * g) = reflect N f * reflect O g
N O : ℕ
f g : R[X]
Cf : card (support f) ≤ Nat.succ (Nat.succ cf)
Cg : card (support g) ≤ Nat.succ cg
Nf : natDegree f ≤ N
Og : natDegree g ≤ O
f0 : ¬f = 0
⊢ card (support (eraseLead f)) ≤ Nat.succ cf
[PROOFSTEP]
exact Nat.lt_succ_iff.mp (gt_of_ge_of_gt Cf (eraseLead_support_card_lt f0))
[GOAL]
case neg.a
R : Type u_1
inst✝ : Semiring R
f✝ : R[X]
cg cf : ℕ
hcf :
  ∀ (N O : ℕ) (f g : R[X]),
    card (support f) ≤ Nat.succ cf →
      card (support g) ≤ Nat.succ cg →
        natDegree f ≤ N → natDegree g ≤ O → reflect (N + O) (f * g) = reflect N f * reflect O g
N O : ℕ
f g : R[X]
Cf : card (support f) ≤ Nat.succ (Nat.succ cf)
Cg : card (support g) ≤ Nat.succ cg
Nf : natDegree f ≤ N
Og : natDegree g ≤ O
f0 : ¬f = 0
⊢ natDegree (eraseLead f) ≤ N
[PROOFSTEP]
exact le_trans eraseLead_natDegree_le_aux Nf
[GOAL]
R : Type u_1
inst✝² : Semiring R
f✝ : R[X]
S : Type u_2
inst✝¹ : CommSemiring S
i : R →+* S
x : S
inst✝ : Invertible x
N : ℕ
f : R[X]
hf : natDegree f ≤ N
⊢ eval₂ i (⅟x) (reflect N f) * x ^ N = eval₂ i x f
[PROOFSTEP]
refine' induction_with_natDegree_le (fun f => eval₂ i (⅟x) (reflect N f) * x ^ N = eval₂ i x f) _ _ _ _ f hf
[GOAL]
case refine'_1
R : Type u_1
inst✝² : Semiring R
f✝ : R[X]
S : Type u_2
inst✝¹ : CommSemiring S
i : R →+* S
x : S
inst✝ : Invertible x
N : ℕ
f : R[X]
hf : natDegree f ≤ N
⊢ (fun f => eval₂ i (⅟x) (reflect N f) * x ^ N = eval₂ i x f) 0
[PROOFSTEP]
simp
[GOAL]
case refine'_2
R : Type u_1
inst✝² : Semiring R
f✝ : R[X]
S : Type u_2
inst✝¹ : CommSemiring S
i : R →+* S
x : S
inst✝ : Invertible x
N : ℕ
f : R[X]
hf : natDegree f ≤ N
⊢ ∀ (n : ℕ) (r : R), r ≠ 0 → n ≤ N → (fun f => eval₂ i (⅟x) (reflect N f) * x ^ N = eval₂ i x f) (↑C r * X ^ n)
[PROOFSTEP]
intro n r _ hnN
[GOAL]
case refine'_2
R : Type u_1
inst✝² : Semiring R
f✝ : R[X]
S : Type u_2
inst✝¹ : CommSemiring S
i : R →+* S
x : S
inst✝ : Invertible x
N : ℕ
f : R[X]
hf : natDegree f ≤ N
n : ℕ
r : R
a✝ : r ≠ 0
hnN : n ≤ N
⊢ eval₂ i (⅟x) (reflect N (↑C r * X ^ n)) * x ^ N = eval₂ i x (↑C r * X ^ n)
[PROOFSTEP]
simp only [revAt_le hnN, reflect_C_mul_X_pow, eval₂_X_pow, eval₂_C, eval₂_mul]
[GOAL]
case refine'_2
R : Type u_1
inst✝² : Semiring R
f✝ : R[X]
S : Type u_2
inst✝¹ : CommSemiring S
i : R →+* S
x : S
inst✝ : Invertible x
N : ℕ
f : R[X]
hf : natDegree f ≤ N
n : ℕ
r : R
a✝ : r ≠ 0
hnN : n ≤ N
⊢ ↑i r * ⅟x ^ (N - n) * x ^ N = ↑i r * x ^ n
[PROOFSTEP]
conv in x ^ N => rw [← Nat.sub_add_cancel hnN]
[GOAL]
R : Type u_1
inst✝² : Semiring R
f✝ : R[X]
S : Type u_2
inst✝¹ : CommSemiring S
i : R →+* S
x : S
inst✝ : Invertible x
N : ℕ
f : R[X]
hf : natDegree f ≤ N
n : ℕ
r : R
a✝ : r ≠ 0
hnN : n ≤ N
| x ^ N
[PROOFSTEP]
rw [← Nat.sub_add_cancel hnN]
[GOAL]
R : Type u_1
inst✝² : Semiring R
f✝ : R[X]
S : Type u_2
inst✝¹ : CommSemiring S
i : R →+* S
x : S
inst✝ : Invertible x
N : ℕ
f : R[X]
hf : natDegree f ≤ N
n : ℕ
r : R
a✝ : r ≠ 0
hnN : n ≤ N
| x ^ N
[PROOFSTEP]
rw [← Nat.sub_add_cancel hnN]
[GOAL]
R : Type u_1
inst✝² : Semiring R
f✝ : R[X]
S : Type u_2
inst✝¹ : CommSemiring S
i : R →+* S
x : S
inst✝ : Invertible x
N : ℕ
f : R[X]
hf : natDegree f ≤ N
n : ℕ
r : R
a✝ : r ≠ 0
hnN : n ≤ N
| x ^ N
[PROOFSTEP]
rw [← Nat.sub_add_cancel hnN]
[GOAL]
case refine'_2
R : Type u_1
inst✝² : Semiring R
f✝ : R[X]
S : Type u_2
inst✝¹ : CommSemiring S
i : R →+* S
x : S
inst✝ : Invertible x
N : ℕ
f : R[X]
hf : natDegree f ≤ N
n : ℕ
r : R
a✝ : r ≠ 0
hnN : n ≤ N
⊢ ↑i r * ⅟x ^ (N - n) * x ^ (N - n + n) = ↑i r * x ^ n
[PROOFSTEP]
rw [pow_add, ← mul_assoc, mul_assoc (i r), ← mul_pow, invOf_mul_self, one_pow, mul_one]
[GOAL]
case refine'_3
R : Type u_1
inst✝² : Semiring R
f✝ : R[X]
S : Type u_2
inst✝¹ : CommSemiring S
i : R →+* S
x : S
inst✝ : Invertible x
N : ℕ
f : R[X]
hf : natDegree f ≤ N
⊢ ∀ (f g : R[X]),
    natDegree f < natDegree g →
      natDegree g ≤ N →
        (fun f => eval₂ i (⅟x) (reflect N f) * x ^ N = eval₂ i x f) f →
          (fun f => eval₂ i (⅟x) (reflect N f) * x ^ N = eval₂ i x f) g →
            (fun f => eval₂ i (⅟x) (reflect N f) * x ^ N = eval₂ i x f) (f + g)
[PROOFSTEP]
intros
[GOAL]
case refine'_3
R : Type u_1
inst✝² : Semiring R
f✝¹ : R[X]
S : Type u_2
inst✝¹ : CommSemiring S
i : R →+* S
x : S
inst✝ : Invertible x
N : ℕ
f : R[X]
hf : natDegree f ≤ N
f✝ g✝ : R[X]
a✝³ : natDegree f✝ < natDegree g✝
a✝² : natDegree g✝ ≤ N
a✝¹ : eval₂ i (⅟x) (reflect N f✝) * x ^ N = eval₂ i x f✝
a✝ : eval₂ i (⅟x) (reflect N g✝) * x ^ N = eval₂ i x g✝
⊢ eval₂ i (⅟x) (reflect N (f✝ + g✝)) * x ^ N = eval₂ i x (f✝ + g✝)
[PROOFSTEP]
simp [*, add_mul]
[GOAL]
R : Type u_1
inst✝² : Semiring R
f✝ : R[X]
S : Type u_2
inst✝¹ : CommSemiring S
i : R →+* S
x : S
inst✝ : Invertible x
N : ℕ
f : R[X]
hf : natDegree f ≤ N
⊢ eval₂ i (⅟x) (reflect N f) = 0 ↔ eval₂ i x f = 0
[PROOFSTEP]
conv_rhs => rw [← eval₂_reflect_mul_pow i x N f hf]
[GOAL]
R : Type u_1
inst✝² : Semiring R
f✝ : R[X]
S : Type u_2
inst✝¹ : CommSemiring S
i : R →+* S
x : S
inst✝ : Invertible x
N : ℕ
f : R[X]
hf : natDegree f ≤ N
| eval₂ i x f = 0
[PROOFSTEP]
rw [← eval₂_reflect_mul_pow i x N f hf]
[GOAL]
R : Type u_1
inst✝² : Semiring R
f✝ : R[X]
S : Type u_2
inst✝¹ : CommSemiring S
i : R →+* S
x : S
inst✝ : Invertible x
N : ℕ
f : R[X]
hf : natDegree f ≤ N
| eval₂ i x f = 0
[PROOFSTEP]
rw [← eval₂_reflect_mul_pow i x N f hf]
[GOAL]
R : Type u_1
inst✝² : Semiring R
f✝ : R[X]
S : Type u_2
inst✝¹ : CommSemiring S
i : R →+* S
x : S
inst✝ : Invertible x
N : ℕ
f : R[X]
hf : natDegree f ≤ N
| eval₂ i x f = 0
[PROOFSTEP]
rw [← eval₂_reflect_mul_pow i x N f hf]
[GOAL]
R : Type u_1
inst✝² : Semiring R
f✝ : R[X]
S : Type u_2
inst✝¹ : CommSemiring S
i : R →+* S
x : S
inst✝ : Invertible x
N : ℕ
f : R[X]
hf : natDegree f ≤ N
⊢ eval₂ i (⅟x) (reflect N f) = 0 ↔ eval₂ i (⅟x) (reflect N f) * x ^ N = 0
[PROOFSTEP]
constructor
[GOAL]
case mp
R : Type u_1
inst✝² : Semiring R
f✝ : R[X]
S : Type u_2
inst✝¹ : CommSemiring S
i : R →+* S
x : S
inst✝ : Invertible x
N : ℕ
f : R[X]
hf : natDegree f ≤ N
⊢ eval₂ i (⅟x) (reflect N f) = 0 → eval₂ i (⅟x) (reflect N f) * x ^ N = 0
[PROOFSTEP]
intro h
[GOAL]
case mp
R : Type u_1
inst✝² : Semiring R
f✝ : R[X]
S : Type u_2
inst✝¹ : CommSemiring S
i : R →+* S
x : S
inst✝ : Invertible x
N : ℕ
f : R[X]
hf : natDegree f ≤ N
h : eval₂ i (⅟x) (reflect N f) = 0
⊢ eval₂ i (⅟x) (reflect N f) * x ^ N = 0
[PROOFSTEP]
rw [h, zero_mul]
[GOAL]
case mpr
R : Type u_1
inst✝² : Semiring R
f✝ : R[X]
S : Type u_2
inst✝¹ : CommSemiring S
i : R →+* S
x : S
inst✝ : Invertible x
N : ℕ
f : R[X]
hf : natDegree f ≤ N
⊢ eval₂ i (⅟x) (reflect N f) * x ^ N = 0 → eval₂ i (⅟x) (reflect N f) = 0
[PROOFSTEP]
intro h
[GOAL]
case mpr
R : Type u_1
inst✝² : Semiring R
f✝ : R[X]
S : Type u_2
inst✝¹ : CommSemiring S
i : R →+* S
x : S
inst✝ : Invertible x
N : ℕ
f : R[X]
hf : natDegree f ≤ N
h : eval₂ i (⅟x) (reflect N f) * x ^ N = 0
⊢ eval₂ i (⅟x) (reflect N f) = 0
[PROOFSTEP]
rw [← mul_one (eval₂ i (⅟x) _), ← one_pow N, ← mul_invOf_self x, mul_pow, ← mul_assoc, h, zero_mul]
[GOAL]
R : Type u_1
inst✝ : Semiring R
f✝ f : R[X]
n : ℕ
⊢ coeff (reverse f) n = coeff f (↑(revAt (natDegree f)) n)
[PROOFSTEP]
rw [reverse, coeff_reflect]
[GOAL]
R : Type u_1
inst✝ : Semiring R
f✝ f : R[X]
⊢ coeff (reverse f) 0 = leadingCoeff f
[PROOFSTEP]
rw [coeff_reverse, revAt_le (zero_le f.natDegree), tsub_zero, leadingCoeff]
[GOAL]
R : Type u_1
inst✝ : Semiring R
f : R[X]
⊢ reverse f = 0 ↔ f = 0
[PROOFSTEP]
simp [reverse]
[GOAL]
R : Type u_1
inst✝ : Semiring R
f✝ f : R[X]
⊢ natDegree (reverse f) ≤ natDegree f
[PROOFSTEP]
rw [natDegree_le_iff_degree_le, degree_le_iff_coeff_zero]
[GOAL]
R : Type u_1
inst✝ : Semiring R
f✝ f : R[X]
⊢ ∀ (m : ℕ), ↑(natDegree f) < ↑m → coeff (reverse f) m = 0
[PROOFSTEP]
intro n hn
[GOAL]
R : Type u_1
inst✝ : Semiring R
f✝ f : R[X]
n : ℕ
hn : ↑(natDegree f) < ↑n
⊢ coeff (reverse f) n = 0
[PROOFSTEP]
rw [Nat.cast_withBot, Nat.cast_withBot, WithBot.coe_lt_coe] at hn
[GOAL]
R : Type u_1
inst✝ : Semiring R
f✝ f : R[X]
n : ℕ
hn : natDegree f < n
⊢ coeff (reverse f) n = 0
[PROOFSTEP]
rw [coeff_reverse, revAt, Function.Embedding.coeFn_mk, if_neg (not_le_of_gt hn), coeff_eq_zero_of_natDegree_lt hn]
[GOAL]
R : Type u_1
inst✝ : Semiring R
f✝ f : R[X]
⊢ natDegree f = natDegree (reverse f) + natTrailingDegree f
[PROOFSTEP]
by_cases hf : f = 0
[GOAL]
case pos
R : Type u_1
inst✝ : Semiring R
f✝ f : R[X]
hf : f = 0
⊢ natDegree f = natDegree (reverse f) + natTrailingDegree f
[PROOFSTEP]
rw [hf, reverse_zero, natDegree_zero, natTrailingDegree_zero]
[GOAL]
case neg
R : Type u_1
inst✝ : Semiring R
f✝ f : R[X]
hf : ¬f = 0
⊢ natDegree f = natDegree (reverse f) + natTrailingDegree f
[PROOFSTEP]
apply le_antisymm
[GOAL]
case neg.a
R : Type u_1
inst✝ : Semiring R
f✝ f : R[X]
hf : ¬f = 0
⊢ natDegree f ≤ natDegree (reverse f) + natTrailingDegree f
[PROOFSTEP]
refine' tsub_le_iff_right.mp _
[GOAL]
case neg.a
R : Type u_1
inst✝ : Semiring R
f✝ f : R[X]
hf : ¬f = 0
⊢ natDegree f - natTrailingDegree f ≤ natDegree (reverse f)
[PROOFSTEP]
apply le_natDegree_of_ne_zero
[GOAL]
case neg.a.h
R : Type u_1
inst✝ : Semiring R
f✝ f : R[X]
hf : ¬f = 0
⊢ coeff (reverse f) (natDegree f - natTrailingDegree f) ≠ 0
[PROOFSTEP]
rw [reverse, coeff_reflect, ← revAt_le f.natTrailingDegree_le_natDegree, revAt_invol]
[GOAL]
case neg.a.h
R : Type u_1
inst✝ : Semiring R
f✝ f : R[X]
hf : ¬f = 0
⊢ coeff f (natTrailingDegree f) ≠ 0
[PROOFSTEP]
exact trailingCoeff_nonzero_iff_nonzero.mpr hf
[GOAL]
case neg.a
R : Type u_1
inst✝ : Semiring R
f✝ f : R[X]
hf : ¬f = 0
⊢ natDegree (reverse f) + natTrailingDegree f ≤ natDegree f
[PROOFSTEP]
rw [← le_tsub_iff_left f.reverse_natDegree_le]
[GOAL]
case neg.a
R : Type u_1
inst✝ : Semiring R
f✝ f : R[X]
hf : ¬f = 0
⊢ natTrailingDegree f ≤ natDegree f - natDegree (reverse f)
[PROOFSTEP]
apply natTrailingDegree_le_of_ne_zero
[GOAL]
case neg.a.h
R : Type u_1
inst✝ : Semiring R
f✝ f : R[X]
hf : ¬f = 0
⊢ coeff f (natDegree f - natDegree (reverse f)) ≠ 0
[PROOFSTEP]
have key := mt leadingCoeff_eq_zero.mp (mt reverse_eq_zero.mp hf)
[GOAL]
case neg.a.h
R : Type u_1
inst✝ : Semiring R
f✝ f : R[X]
hf : ¬f = 0
key : ¬leadingCoeff (reverse f) = 0
⊢ coeff f (natDegree f - natDegree (reverse f)) ≠ 0
[PROOFSTEP]
rwa [leadingCoeff, coeff_reverse, revAt_le f.reverse_natDegree_le] at key
[GOAL]
R : Type u_1
inst✝ : Semiring R
f✝ f : R[X]
⊢ natDegree (reverse f) = natDegree f - natTrailingDegree f
[PROOFSTEP]
rw [f.natDegree_eq_reverse_natDegree_add_natTrailingDegree, add_tsub_cancel_right]
[GOAL]
R : Type u_1
inst✝ : Semiring R
f✝ f : R[X]
⊢ leadingCoeff (reverse f) = trailingCoeff f
[PROOFSTEP]
rw [leadingCoeff, reverse_natDegree, ← revAt_le f.natTrailingDegree_le_natDegree, coeff_reverse, revAt_invol,
  trailingCoeff]
[GOAL]
R : Type u_1
inst✝ : Semiring R
f✝ f : R[X]
⊢ natTrailingDegree (reverse f) = 0
[PROOFSTEP]
by_cases hf : f = 0
[GOAL]
case pos
R : Type u_1
inst✝ : Semiring R
f✝ f : R[X]
hf : f = 0
⊢ natTrailingDegree (reverse f) = 0
[PROOFSTEP]
rw [hf, reverse_zero, natTrailingDegree_zero]
[GOAL]
case neg
R : Type u_1
inst✝ : Semiring R
f✝ f : R[X]
hf : ¬f = 0
⊢ natTrailingDegree (reverse f) = 0
[PROOFSTEP]
rw [← le_zero_iff]
[GOAL]
case neg
R : Type u_1
inst✝ : Semiring R
f✝ f : R[X]
hf : ¬f = 0
⊢ natTrailingDegree (reverse f) ≤ 0
[PROOFSTEP]
apply natTrailingDegree_le_of_ne_zero
[GOAL]
case neg.h
R : Type u_1
inst✝ : Semiring R
f✝ f : R[X]
hf : ¬f = 0
⊢ coeff (reverse f) 0 ≠ 0
[PROOFSTEP]
rw [coeff_zero_reverse]
[GOAL]
case neg.h
R : Type u_1
inst✝ : Semiring R
f✝ f : R[X]
hf : ¬f = 0
⊢ leadingCoeff f ≠ 0
[PROOFSTEP]
exact mt leadingCoeff_eq_zero.mp hf
[GOAL]
R : Type u_1
inst✝ : Semiring R
f✝ f : R[X]
⊢ trailingCoeff (reverse f) = leadingCoeff f
[PROOFSTEP]
rw [trailingCoeff, reverse_natTrailingDegree, coeff_zero_reverse]
[GOAL]
R : Type u_1
inst✝ : Semiring R
f✝ f g : R[X]
fg : leadingCoeff f * leadingCoeff g ≠ 0
⊢ reverse (f * g) = reverse f * reverse g
[PROOFSTEP]
unfold reverse
[GOAL]
R : Type u_1
inst✝ : Semiring R
f✝ f g : R[X]
fg : leadingCoeff f * leadingCoeff g ≠ 0
⊢ reflect (natDegree (f * g)) (f * g) = reflect (natDegree f) f * reflect (natDegree g) g
[PROOFSTEP]
rw [natDegree_mul' fg, reflect_mul f g rfl.le rfl.le]
[GOAL]
R✝ : Type u_1
inst✝² : Semiring R✝
f✝ : R✝[X]
R : Type u_2
inst✝¹ : Ring R
inst✝ : NoZeroDivisors R
f g : R[X]
⊢ reverse (f * g) = reverse f * reverse g
[PROOFSTEP]
by_cases f0 : f = 0
[GOAL]
case pos
R✝ : Type u_1
inst✝² : Semiring R✝
f✝ : R✝[X]
R : Type u_2
inst✝¹ : Ring R
inst✝ : NoZeroDivisors R
f g : R[X]
f0 : f = 0
⊢ reverse (f * g) = reverse f * reverse g
[PROOFSTEP]
simp only [f0, zero_mul, reverse_zero]
[GOAL]
case neg
R✝ : Type u_1
inst✝² : Semiring R✝
f✝ : R✝[X]
R : Type u_2
inst✝¹ : Ring R
inst✝ : NoZeroDivisors R
f g : R[X]
f0 : ¬f = 0
⊢ reverse (f * g) = reverse f * reverse g
[PROOFSTEP]
by_cases g0 : g = 0
[GOAL]
case pos
R✝ : Type u_1
inst✝² : Semiring R✝
f✝ : R✝[X]
R : Type u_2
inst✝¹ : Ring R
inst✝ : NoZeroDivisors R
f g : R[X]
f0 : ¬f = 0
g0 : g = 0
⊢ reverse (f * g) = reverse f * reverse g
[PROOFSTEP]
rw [g0, mul_zero, reverse_zero, mul_zero]
[GOAL]
case neg
R✝ : Type u_1
inst✝² : Semiring R✝
f✝ : R✝[X]
R : Type u_2
inst✝¹ : Ring R
inst✝ : NoZeroDivisors R
f g : R[X]
f0 : ¬f = 0
g0 : ¬g = 0
⊢ reverse (f * g) = reverse f * reverse g
[PROOFSTEP]
simp [reverse_mul, *]
[GOAL]
R✝ : Type u_1
inst✝² : Semiring R✝
f : R✝[X]
R : Type u_2
inst✝¹ : Ring R
inst✝ : NoZeroDivisors R
p q : R[X]
⊢ trailingCoeff (p * q) = trailingCoeff p * trailingCoeff q
[PROOFSTEP]
rw [← reverse_leadingCoeff, reverse_mul_of_domain, leadingCoeff_mul, reverse_leadingCoeff, reverse_leadingCoeff]
[GOAL]
R : Type u_1
inst✝ : Semiring R
f✝ f : R[X]
⊢ coeff (reverse f) 1 = nextCoeff f
[PROOFSTEP]
rw [coeff_reverse, nextCoeff]
[GOAL]
R : Type u_1
inst✝ : Semiring R
f✝ f : R[X]
⊢ coeff f (↑(revAt (natDegree f)) 1) = if natDegree f = 0 then 0 else coeff f (natDegree f - 1)
[PROOFSTEP]
split_ifs with hf
[GOAL]
case pos
R : Type u_1
inst✝ : Semiring R
f✝ f : R[X]
hf : natDegree f = 0
⊢ coeff f (↑(revAt (natDegree f)) 1) = 0
[PROOFSTEP]
have : coeff f 1 = 0 := coeff_eq_zero_of_natDegree_lt (by simp only [hf, zero_lt_one])
[GOAL]
R : Type u_1
inst✝ : Semiring R
f✝ f : R[X]
hf : natDegree f = 0
⊢ natDegree f < 1
[PROOFSTEP]
simp only [hf, zero_lt_one]
[GOAL]
case pos
R : Type u_1
inst✝ : Semiring R
f✝ f : R[X]
hf : natDegree f = 0
this : coeff f 1 = 0
⊢ coeff f (↑(revAt (natDegree f)) 1) = 0
[PROOFSTEP]
simp [*, revAt]
[GOAL]
case neg
R : Type u_1
inst✝ : Semiring R
f✝ f : R[X]
hf : ¬natDegree f = 0
⊢ coeff f (↑(revAt (natDegree f)) 1) = coeff f (natDegree f - 1)
[PROOFSTEP]
rw [revAt_le]
[GOAL]
case neg
R : Type u_1
inst✝ : Semiring R
f✝ f : R[X]
hf : ¬natDegree f = 0
⊢ 1 ≤ natDegree f
[PROOFSTEP]
exact Nat.succ_le_iff.2 (pos_iff_ne_zero.2 hf)
[GOAL]
R : Type u_1
inst✝ : Ring R
f : R[X]
N : ℕ
⊢ reflect N (-f) = -reflect N f
[PROOFSTEP]
rw [neg_eq_neg_one_mul, ← C_1, ← C_neg, reflect_C_mul, C_neg, C_1, ← neg_eq_neg_one_mul]
[GOAL]
R : Type u_1
inst✝ : Ring R
f g : R[X]
N : ℕ
⊢ reflect N (f - g) = reflect N f - reflect N g
[PROOFSTEP]
rw [sub_eq_add_neg, sub_eq_add_neg, reflect_add, reflect_neg]
[GOAL]
R : Type u_1
inst✝ : Ring R
f : R[X]
⊢ reverse (-f) = -reverse f
[PROOFSTEP]
rw [reverse, reverse, reflect_neg, natDegree_neg]


[GOAL]
R : Type u
a b : R
m n : ℕ
inst✝¹ : Semiring R
p q r : R[X]
inst✝ : Nontrivial R
i j : ℕ
⊢ ↑(monomial i) 1 = ↑(monomial j) 1 ↔ i = j
[PROOFSTEP]
simp_rw [← ofFinsupp_single, ofFinsupp.injEq]
[GOAL]
R : Type u
a b : R
m n : ℕ
inst✝¹ : Semiring R
p q r : R[X]
inst✝ : Nontrivial R
i j : ℕ
⊢ Finsupp.single i 1 = Finsupp.single j 1 ↔ i = j
[PROOFSTEP]
exact AddMonoidAlgebra.of_injective.eq_iff
[GOAL]
R : Type u
a b : R
m✝ n✝ : ℕ
inst✝¹ : Semiring R
p q r : R[X]
inst✝ : Nontrivial R
m n : ℕ
h : (fun i => ↑(monomial i) 1) m = (fun i => ↑(monomial i) 1) n
⊢ m = n
[PROOFSTEP]
simpa [monomial_one_eq_iff] using h
[GOAL]
R : Type u
a b : R
m n : ℕ
inst✝ : Semiring R
p q r f : R[X]
⊢ Finset.card (support f) ≤ 1 ↔ ∃ n a, f = ↑(monomial n) a
[PROOFSTEP]
constructor
[GOAL]
case mp
R : Type u
a b : R
m n : ℕ
inst✝ : Semiring R
p q r f : R[X]
⊢ Finset.card (support f) ≤ 1 → ∃ n a, f = ↑(monomial n) a
[PROOFSTEP]
intro H
[GOAL]
case mp
R : Type u
a b : R
m n : ℕ
inst✝ : Semiring R
p q r f : R[X]
H : Finset.card (support f) ≤ 1
⊢ ∃ n a, f = ↑(monomial n) a
[PROOFSTEP]
rw [Finset.card_le_one_iff_subset_singleton] at H
[GOAL]
case mp
R : Type u
a b : R
m n : ℕ
inst✝ : Semiring R
p q r f : R[X]
H : ∃ x, support f ⊆ {x}
⊢ ∃ n a, f = ↑(monomial n) a
[PROOFSTEP]
rcases H with ⟨n, hn⟩
[GOAL]
case mp.intro
R : Type u
a b : R
m n✝ : ℕ
inst✝ : Semiring R
p q r f : R[X]
n : ℕ
hn : support f ⊆ {n}
⊢ ∃ n a, f = ↑(monomial n) a
[PROOFSTEP]
refine' ⟨n, f.coeff n, _⟩
[GOAL]
case mp.intro
R : Type u
a b : R
m n✝ : ℕ
inst✝ : Semiring R
p q r f : R[X]
n : ℕ
hn : support f ⊆ {n}
⊢ f = ↑(monomial n) (coeff f n)
[PROOFSTEP]
ext i
[GOAL]
case mp.intro.a
R : Type u
a b : R
m n✝ : ℕ
inst✝ : Semiring R
p q r f : R[X]
n : ℕ
hn : support f ⊆ {n}
i : ℕ
⊢ coeff f i = coeff (↑(monomial n) (coeff f n)) i
[PROOFSTEP]
by_cases hi : i = n
[GOAL]
case pos
R : Type u
a b : R
m n✝ : ℕ
inst✝ : Semiring R
p q r f : R[X]
n : ℕ
hn : support f ⊆ {n}
i : ℕ
hi : i = n
⊢ coeff f i = coeff (↑(monomial n) (coeff f n)) i
[PROOFSTEP]
simp [hi, coeff_monomial]
[GOAL]
case neg
R : Type u
a b : R
m n✝ : ℕ
inst✝ : Semiring R
p q r f : R[X]
n : ℕ
hn : support f ⊆ {n}
i : ℕ
hi : ¬i = n
⊢ coeff f i = coeff (↑(monomial n) (coeff f n)) i
[PROOFSTEP]
have : f.coeff i = 0 := by
  rw [← not_mem_support_iff]
  exact fun hi' => hi (Finset.mem_singleton.1 (hn hi'))
[GOAL]
R : Type u
a b : R
m n✝ : ℕ
inst✝ : Semiring R
p q r f : R[X]
n : ℕ
hn : support f ⊆ {n}
i : ℕ
hi : ¬i = n
⊢ coeff f i = 0
[PROOFSTEP]
rw [← not_mem_support_iff]
[GOAL]
R : Type u
a b : R
m n✝ : ℕ
inst✝ : Semiring R
p q r f : R[X]
n : ℕ
hn : support f ⊆ {n}
i : ℕ
hi : ¬i = n
⊢ ¬i ∈ support f
[PROOFSTEP]
exact fun hi' => hi (Finset.mem_singleton.1 (hn hi'))
[GOAL]
case neg
R : Type u
a b : R
m n✝ : ℕ
inst✝ : Semiring R
p q r f : R[X]
n : ℕ
hn : support f ⊆ {n}
i : ℕ
hi : ¬i = n
this : coeff f i = 0
⊢ coeff f i = coeff (↑(monomial n) (coeff f n)) i
[PROOFSTEP]
simp [this, Ne.symm hi, coeff_monomial]
[GOAL]
case mpr
R : Type u
a b : R
m n : ℕ
inst✝ : Semiring R
p q r f : R[X]
⊢ (∃ n a, f = ↑(monomial n) a) → Finset.card (support f) ≤ 1
[PROOFSTEP]
rintro ⟨n, a, rfl⟩
[GOAL]
case mpr.intro.intro
R : Type u
a✝ b : R
m n✝ : ℕ
inst✝ : Semiring R
p q r : R[X]
n : ℕ
a : R
⊢ Finset.card (support (↑(monomial n) a)) ≤ 1
[PROOFSTEP]
rw [← Finset.card_singleton n]
[GOAL]
case mpr.intro.intro
R : Type u
a✝ b : R
m n✝ : ℕ
inst✝ : Semiring R
p q r : R[X]
n : ℕ
a : R
⊢ Finset.card (support (↑(monomial n) a)) ≤ Finset.card {n}
[PROOFSTEP]
apply Finset.card_le_of_subset
[GOAL]
case mpr.intro.intro.a
R : Type u
a✝ b : R
m n✝ : ℕ
inst✝ : Semiring R
p q r : R[X]
n : ℕ
a : R
⊢ support (↑(monomial n) a) ⊆ {n}
[PROOFSTEP]
exact support_monomial' _ _
[GOAL]
R : Type u
a b : R
m n : ℕ
inst✝¹ : Semiring R
p q r : R[X]
S : Type u_1
inst✝ : Semiring S
f g : R[X] →+* S
h₁ : ∀ (a : R), ↑f (↑C a) = ↑g (↑C a)
h₂ : ↑f X = ↑g X
⊢ f = g
[PROOFSTEP]
set f' := f.comp (toFinsuppIso R).symm.toRingHom with hf'
[GOAL]
R : Type u
a b : R
m n : ℕ
inst✝¹ : Semiring R
p q r : R[X]
S : Type u_1
inst✝ : Semiring S
f g : R[X] →+* S
h₁ : ∀ (a : R), ↑f (↑C a) = ↑g (↑C a)
h₂ : ↑f X = ↑g X
f' : AddMonoidAlgebra R ℕ →+* S := RingHom.comp f (RingEquiv.toRingHom (RingEquiv.symm (toFinsuppIso R)))
hf' : f' = RingHom.comp f (RingEquiv.toRingHom (RingEquiv.symm (toFinsuppIso R)))
⊢ f = g
[PROOFSTEP]
set g' := g.comp (toFinsuppIso R).symm.toRingHom with hg'
[GOAL]
R : Type u
a b : R
m n : ℕ
inst✝¹ : Semiring R
p q r : R[X]
S : Type u_1
inst✝ : Semiring S
f g : R[X] →+* S
h₁ : ∀ (a : R), ↑f (↑C a) = ↑g (↑C a)
h₂ : ↑f X = ↑g X
f' : AddMonoidAlgebra R ℕ →+* S := RingHom.comp f (RingEquiv.toRingHom (RingEquiv.symm (toFinsuppIso R)))
hf' : f' = RingHom.comp f (RingEquiv.toRingHom (RingEquiv.symm (toFinsuppIso R)))
g' : AddMonoidAlgebra R ℕ →+* S := RingHom.comp g (RingEquiv.toRingHom (RingEquiv.symm (toFinsuppIso R)))
hg' : g' = RingHom.comp g (RingEquiv.toRingHom (RingEquiv.symm (toFinsuppIso R)))
⊢ f = g
[PROOFSTEP]
have A : f' = g' := by
  -- Porting note: Was `ext; simp [..]; simpa [..] using h₂`.
  ext : 1
  · ext
    simp [h₁, RingEquiv.toRingHom_eq_coe]
  · refine MonoidHom.ext_mnat ?_
    simpa [RingEquiv.toRingHom_eq_coe] using h₂
[GOAL]
R : Type u
a b : R
m n : ℕ
inst✝¹ : Semiring R
p q r : R[X]
S : Type u_1
inst✝ : Semiring S
f g : R[X] →+* S
h₁ : ∀ (a : R), ↑f (↑C a) = ↑g (↑C a)
h₂ : ↑f X = ↑g X
f' : AddMonoidAlgebra R ℕ →+* S := RingHom.comp f (RingEquiv.toRingHom (RingEquiv.symm (toFinsuppIso R)))
hf' : f' = RingHom.comp f (RingEquiv.toRingHom (RingEquiv.symm (toFinsuppIso R)))
g' : AddMonoidAlgebra R ℕ →+* S := RingHom.comp g (RingEquiv.toRingHom (RingEquiv.symm (toFinsuppIso R)))
hg' : g' = RingHom.comp g (RingEquiv.toRingHom (RingEquiv.symm (toFinsuppIso R)))
⊢ f' = g'
[PROOFSTEP]
ext : 1
[GOAL]
case h₁
R : Type u
a b : R
m n : ℕ
inst✝¹ : Semiring R
p q r : R[X]
S : Type u_1
inst✝ : Semiring S
f g : R[X] →+* S
h₁ : ∀ (a : R), ↑f (↑C a) = ↑g (↑C a)
h₂ : ↑f X = ↑g X
f' : AddMonoidAlgebra R ℕ →+* S := RingHom.comp f (RingEquiv.toRingHom (RingEquiv.symm (toFinsuppIso R)))
hf' : f' = RingHom.comp f (RingEquiv.toRingHom (RingEquiv.symm (toFinsuppIso R)))
g' : AddMonoidAlgebra R ℕ →+* S := RingHom.comp g (RingEquiv.toRingHom (RingEquiv.symm (toFinsuppIso R)))
hg' : g' = RingHom.comp g (RingEquiv.toRingHom (RingEquiv.symm (toFinsuppIso R)))
⊢ RingHom.comp f' AddMonoidAlgebra.singleZeroRingHom = RingHom.comp g' AddMonoidAlgebra.singleZeroRingHom
[PROOFSTEP]
ext
[GOAL]
case h₁.a
R : Type u
a b : R
m n : ℕ
inst✝¹ : Semiring R
p q r : R[X]
S : Type u_1
inst✝ : Semiring S
f g : R[X] →+* S
h₁ : ∀ (a : R), ↑f (↑C a) = ↑g (↑C a)
h₂ : ↑f X = ↑g X
f' : AddMonoidAlgebra R ℕ →+* S := RingHom.comp f (RingEquiv.toRingHom (RingEquiv.symm (toFinsuppIso R)))
hf' : f' = RingHom.comp f (RingEquiv.toRingHom (RingEquiv.symm (toFinsuppIso R)))
g' : AddMonoidAlgebra R ℕ →+* S := RingHom.comp g (RingEquiv.toRingHom (RingEquiv.symm (toFinsuppIso R)))
hg' : g' = RingHom.comp g (RingEquiv.toRingHom (RingEquiv.symm (toFinsuppIso R)))
x✝ : R
⊢ ↑(RingHom.comp f' AddMonoidAlgebra.singleZeroRingHom) x✝ = ↑(RingHom.comp g' AddMonoidAlgebra.singleZeroRingHom) x✝
[PROOFSTEP]
simp [h₁, RingEquiv.toRingHom_eq_coe]
[GOAL]
case h_of
R : Type u
a b : R
m n : ℕ
inst✝¹ : Semiring R
p q r : R[X]
S : Type u_1
inst✝ : Semiring S
f g : R[X] →+* S
h₁ : ∀ (a : R), ↑f (↑C a) = ↑g (↑C a)
h₂ : ↑f X = ↑g X
f' : AddMonoidAlgebra R ℕ →+* S := RingHom.comp f (RingEquiv.toRingHom (RingEquiv.symm (toFinsuppIso R)))
hf' : f' = RingHom.comp f (RingEquiv.toRingHom (RingEquiv.symm (toFinsuppIso R)))
g' : AddMonoidAlgebra R ℕ →+* S := RingHom.comp g (RingEquiv.toRingHom (RingEquiv.symm (toFinsuppIso R)))
hg' : g' = RingHom.comp g (RingEquiv.toRingHom (RingEquiv.symm (toFinsuppIso R)))
⊢ MonoidHom.comp (↑f') (AddMonoidAlgebra.of R ℕ) = MonoidHom.comp (↑g') (AddMonoidAlgebra.of R ℕ)
[PROOFSTEP]
refine MonoidHom.ext_mnat ?_
[GOAL]
case h_of
R : Type u
a b : R
m n : ℕ
inst✝¹ : Semiring R
p q r : R[X]
S : Type u_1
inst✝ : Semiring S
f g : R[X] →+* S
h₁ : ∀ (a : R), ↑f (↑C a) = ↑g (↑C a)
h₂ : ↑f X = ↑g X
f' : AddMonoidAlgebra R ℕ →+* S := RingHom.comp f (RingEquiv.toRingHom (RingEquiv.symm (toFinsuppIso R)))
hf' : f' = RingHom.comp f (RingEquiv.toRingHom (RingEquiv.symm (toFinsuppIso R)))
g' : AddMonoidAlgebra R ℕ →+* S := RingHom.comp g (RingEquiv.toRingHom (RingEquiv.symm (toFinsuppIso R)))
hg' : g' = RingHom.comp g (RingEquiv.toRingHom (RingEquiv.symm (toFinsuppIso R)))
⊢ ↑(MonoidHom.comp (↑f') (AddMonoidAlgebra.of R ℕ)) (↑Multiplicative.ofAdd 1) =
    ↑(MonoidHom.comp (↑g') (AddMonoidAlgebra.of R ℕ)) (↑Multiplicative.ofAdd 1)
[PROOFSTEP]
simpa [RingEquiv.toRingHom_eq_coe] using h₂
[GOAL]
R : Type u
a b : R
m n : ℕ
inst✝¹ : Semiring R
p q r : R[X]
S : Type u_1
inst✝ : Semiring S
f g : R[X] →+* S
h₁ : ∀ (a : R), ↑f (↑C a) = ↑g (↑C a)
h₂ : ↑f X = ↑g X
f' : AddMonoidAlgebra R ℕ →+* S := RingHom.comp f (RingEquiv.toRingHom (RingEquiv.symm (toFinsuppIso R)))
hf' : f' = RingHom.comp f (RingEquiv.toRingHom (RingEquiv.symm (toFinsuppIso R)))
g' : AddMonoidAlgebra R ℕ →+* S := RingHom.comp g (RingEquiv.toRingHom (RingEquiv.symm (toFinsuppIso R)))
hg' : g' = RingHom.comp g (RingEquiv.toRingHom (RingEquiv.symm (toFinsuppIso R)))
A : f' = g'
⊢ f = g
[PROOFSTEP]
have B : f = f'.comp (toFinsuppIso R) := by
  rw [hf', RingHom.comp_assoc]
  ext x
  simp only [RingEquiv.toRingHom_eq_coe, RingEquiv.symm_apply_apply, Function.comp_apply, RingHom.coe_comp,
    RingEquiv.coe_toRingHom]
[GOAL]
R : Type u
a b : R
m n : ℕ
inst✝¹ : Semiring R
p q r : R[X]
S : Type u_1
inst✝ : Semiring S
f g : R[X] →+* S
h₁ : ∀ (a : R), ↑f (↑C a) = ↑g (↑C a)
h₂ : ↑f X = ↑g X
f' : AddMonoidAlgebra R ℕ →+* S := RingHom.comp f (RingEquiv.toRingHom (RingEquiv.symm (toFinsuppIso R)))
hf' : f' = RingHom.comp f (RingEquiv.toRingHom (RingEquiv.symm (toFinsuppIso R)))
g' : AddMonoidAlgebra R ℕ →+* S := RingHom.comp g (RingEquiv.toRingHom (RingEquiv.symm (toFinsuppIso R)))
hg' : g' = RingHom.comp g (RingEquiv.toRingHom (RingEquiv.symm (toFinsuppIso R)))
A : f' = g'
⊢ f = RingHom.comp f' ↑(toFinsuppIso R)
[PROOFSTEP]
rw [hf', RingHom.comp_assoc]
[GOAL]
R : Type u
a b : R
m n : ℕ
inst✝¹ : Semiring R
p q r : R[X]
S : Type u_1
inst✝ : Semiring S
f g : R[X] →+* S
h₁ : ∀ (a : R), ↑f (↑C a) = ↑g (↑C a)
h₂ : ↑f X = ↑g X
f' : AddMonoidAlgebra R ℕ →+* S := RingHom.comp f (RingEquiv.toRingHom (RingEquiv.symm (toFinsuppIso R)))
hf' : f' = RingHom.comp f (RingEquiv.toRingHom (RingEquiv.symm (toFinsuppIso R)))
g' : AddMonoidAlgebra R ℕ →+* S := RingHom.comp g (RingEquiv.toRingHom (RingEquiv.symm (toFinsuppIso R)))
hg' : g' = RingHom.comp g (RingEquiv.toRingHom (RingEquiv.symm (toFinsuppIso R)))
A : f' = g'
⊢ f = RingHom.comp f (RingHom.comp (RingEquiv.toRingHom (RingEquiv.symm (toFinsuppIso R))) ↑(toFinsuppIso R))
[PROOFSTEP]
ext x
[GOAL]
case a
R : Type u
a b : R
m n : ℕ
inst✝¹ : Semiring R
p q r : R[X]
S : Type u_1
inst✝ : Semiring S
f g : R[X] →+* S
h₁ : ∀ (a : R), ↑f (↑C a) = ↑g (↑C a)
h₂ : ↑f X = ↑g X
f' : AddMonoidAlgebra R ℕ →+* S := RingHom.comp f (RingEquiv.toRingHom (RingEquiv.symm (toFinsuppIso R)))
hf' : f' = RingHom.comp f (RingEquiv.toRingHom (RingEquiv.symm (toFinsuppIso R)))
g' : AddMonoidAlgebra R ℕ →+* S := RingHom.comp g (RingEquiv.toRingHom (RingEquiv.symm (toFinsuppIso R)))
hg' : g' = RingHom.comp g (RingEquiv.toRingHom (RingEquiv.symm (toFinsuppIso R)))
A : f' = g'
x : R[X]
⊢ ↑f x = ↑(RingHom.comp f (RingHom.comp (RingEquiv.toRingHom (RingEquiv.symm (toFinsuppIso R))) ↑(toFinsuppIso R))) x
[PROOFSTEP]
simp only [RingEquiv.toRingHom_eq_coe, RingEquiv.symm_apply_apply, Function.comp_apply, RingHom.coe_comp,
  RingEquiv.coe_toRingHom]
[GOAL]
R : Type u
a b : R
m n : ℕ
inst✝¹ : Semiring R
p q r : R[X]
S : Type u_1
inst✝ : Semiring S
f g : R[X] →+* S
h₁ : ∀ (a : R), ↑f (↑C a) = ↑g (↑C a)
h₂ : ↑f X = ↑g X
f' : AddMonoidAlgebra R ℕ →+* S := RingHom.comp f (RingEquiv.toRingHom (RingEquiv.symm (toFinsuppIso R)))
hf' : f' = RingHom.comp f (RingEquiv.toRingHom (RingEquiv.symm (toFinsuppIso R)))
g' : AddMonoidAlgebra R ℕ →+* S := RingHom.comp g (RingEquiv.toRingHom (RingEquiv.symm (toFinsuppIso R)))
hg' : g' = RingHom.comp g (RingEquiv.toRingHom (RingEquiv.symm (toFinsuppIso R)))
A : f' = g'
B : f = RingHom.comp f' ↑(toFinsuppIso R)
⊢ f = g
[PROOFSTEP]
have C' : g = g'.comp (toFinsuppIso R) := by
  rw [hg', RingHom.comp_assoc]
  ext x
  simp only [RingEquiv.toRingHom_eq_coe, RingEquiv.symm_apply_apply, Function.comp_apply, RingHom.coe_comp,
    RingEquiv.coe_toRingHom]
[GOAL]
R : Type u
a b : R
m n : ℕ
inst✝¹ : Semiring R
p q r : R[X]
S : Type u_1
inst✝ : Semiring S
f g : R[X] →+* S
h₁ : ∀ (a : R), ↑f (↑C a) = ↑g (↑C a)
h₂ : ↑f X = ↑g X
f' : AddMonoidAlgebra R ℕ →+* S := RingHom.comp f (RingEquiv.toRingHom (RingEquiv.symm (toFinsuppIso R)))
hf' : f' = RingHom.comp f (RingEquiv.toRingHom (RingEquiv.symm (toFinsuppIso R)))
g' : AddMonoidAlgebra R ℕ →+* S := RingHom.comp g (RingEquiv.toRingHom (RingEquiv.symm (toFinsuppIso R)))
hg' : g' = RingHom.comp g (RingEquiv.toRingHom (RingEquiv.symm (toFinsuppIso R)))
A : f' = g'
B : f = RingHom.comp f' ↑(toFinsuppIso R)
⊢ g = RingHom.comp g' ↑(toFinsuppIso R)
[PROOFSTEP]
rw [hg', RingHom.comp_assoc]
[GOAL]
R : Type u
a b : R
m n : ℕ
inst✝¹ : Semiring R
p q r : R[X]
S : Type u_1
inst✝ : Semiring S
f g : R[X] →+* S
h₁ : ∀ (a : R), ↑f (↑C a) = ↑g (↑C a)
h₂ : ↑f X = ↑g X
f' : AddMonoidAlgebra R ℕ →+* S := RingHom.comp f (RingEquiv.toRingHom (RingEquiv.symm (toFinsuppIso R)))
hf' : f' = RingHom.comp f (RingEquiv.toRingHom (RingEquiv.symm (toFinsuppIso R)))
g' : AddMonoidAlgebra R ℕ →+* S := RingHom.comp g (RingEquiv.toRingHom (RingEquiv.symm (toFinsuppIso R)))
hg' : g' = RingHom.comp g (RingEquiv.toRingHom (RingEquiv.symm (toFinsuppIso R)))
A : f' = g'
B : f = RingHom.comp f' ↑(toFinsuppIso R)
⊢ g = RingHom.comp g (RingHom.comp (RingEquiv.toRingHom (RingEquiv.symm (toFinsuppIso R))) ↑(toFinsuppIso R))
[PROOFSTEP]
ext x
[GOAL]
case a
R : Type u
a b : R
m n : ℕ
inst✝¹ : Semiring R
p q r : R[X]
S : Type u_1
inst✝ : Semiring S
f g : R[X] →+* S
h₁ : ∀ (a : R), ↑f (↑C a) = ↑g (↑C a)
h₂ : ↑f X = ↑g X
f' : AddMonoidAlgebra R ℕ →+* S := RingHom.comp f (RingEquiv.toRingHom (RingEquiv.symm (toFinsuppIso R)))
hf' : f' = RingHom.comp f (RingEquiv.toRingHom (RingEquiv.symm (toFinsuppIso R)))
g' : AddMonoidAlgebra R ℕ →+* S := RingHom.comp g (RingEquiv.toRingHom (RingEquiv.symm (toFinsuppIso R)))
hg' : g' = RingHom.comp g (RingEquiv.toRingHom (RingEquiv.symm (toFinsuppIso R)))
A : f' = g'
B : f = RingHom.comp f' ↑(toFinsuppIso R)
x : R[X]
⊢ ↑g x = ↑(RingHom.comp g (RingHom.comp (RingEquiv.toRingHom (RingEquiv.symm (toFinsuppIso R))) ↑(toFinsuppIso R))) x
[PROOFSTEP]
simp only [RingEquiv.toRingHom_eq_coe, RingEquiv.symm_apply_apply, Function.comp_apply, RingHom.coe_comp,
  RingEquiv.coe_toRingHom]
[GOAL]
R : Type u
a b : R
m n : ℕ
inst✝¹ : Semiring R
p q r : R[X]
S : Type u_1
inst✝ : Semiring S
f g : R[X] →+* S
h₁ : ∀ (a : R), ↑f (↑C a) = ↑g (↑C a)
h₂ : ↑f X = ↑g X
f' : AddMonoidAlgebra R ℕ →+* S := RingHom.comp f (RingEquiv.toRingHom (RingEquiv.symm (toFinsuppIso R)))
hf' : f' = RingHom.comp f (RingEquiv.toRingHom (RingEquiv.symm (toFinsuppIso R)))
g' : AddMonoidAlgebra R ℕ →+* S := RingHom.comp g (RingEquiv.toRingHom (RingEquiv.symm (toFinsuppIso R)))
hg' : g' = RingHom.comp g (RingEquiv.toRingHom (RingEquiv.symm (toFinsuppIso R)))
A : f' = g'
B : f = RingHom.comp f' ↑(toFinsuppIso R)
C' : g = RingHom.comp g' ↑(toFinsuppIso R)
⊢ f = g
[PROOFSTEP]
rw [B, C', A]