[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]
