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

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
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
induction' cf with cf hcf
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

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
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
induction' cg with cg hcg
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
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
intro N O f g Cf Cg Nf Og
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)
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
rw [← C_mul_X_pow_eq_self Cf, ← C_mul_X_pow_eq_self Cg]
no goals
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)
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]
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
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
intro N O f g Cf Cg Nf Og
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

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
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
by_cases g0 : g = 0
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

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

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

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
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
rw [← eraseLead_add_C_mul_X_pow g, mul_add, reflect_add, reflect_add, mul_add, hcg, hcg] <;>
  try assumption
no goals
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
rw [g0, reflect_zero, mul_zero, mul_zero, reflect_zero]
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
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
assumption
no goals
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
exact le_add_left card_support_C_mul_X_pow_le_one
no goals
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
exact le_trans (natDegree_C_mul_X_pow_le g.leadingCoeff g.natDegree) Og
no goals
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
exact Nat.lt_succ_iff.mp (gt_of_ge_of_gt Cg (eraseLead_support_card_lt g0))
no goals
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
exact le_trans eraseLead_natDegree_le_aux Og
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
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
intro N O f g Cf Cg Nf Og
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

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
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
by_cases f0 : f = 0
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

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

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

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
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
rw [← eraseLead_add_C_mul_X_pow f, add_mul, reflect_add, reflect_add, add_mul, hcf, hcf] <;>
  try assumption
no goals
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
rw [f0, reflect_zero, zero_mul, zero_mul, reflect_zero]
no goals
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
assumption
no goals
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
exact le_add_left card_support_C_mul_X_pow_le_one
no goals
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
exact le_trans (natDegree_C_mul_X_pow_le f.leadingCoeff f.natDegree) Nf
no goals
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
exact Nat.lt_succ_iff.mp (gt_of_ge_of_gt Cf (eraseLead_support_card_lt f0))
no goals
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
exact le_trans eraseLead_natDegree_le_aux Nf