-- Mathlib/Algebra/Polynomial/Reverse.lean
theorem reflect_mul_induction (cf cg : ℕ) :
    ∀ N O : ℕ,
      ∀ f g : R[X],
        #f.support ≤ cf.succ →
          #g.support ≤ cg.succ →
            f.natDegree ≤ N →
              g.natDegree ≤ O → reflect (N + O) (f * g) = reflect N f * reflect O g

Proof state:
case neg
R : Type u_1
inst✝ : Semiring R
cg cf : ℕ
hcf :
  ∀ (N O : ℕ) (f g : R[X]),
    #f.support ≤ cf.succ →
      #g.support ≤ cg.succ → f.natDegree ≤ N → g.natDegree ≤ O → reflect (N + O) (f * g) = reflect N f * reflect O g
N O : ℕ
f g : R[X]
Cf : #f.support ≤ (cf + 1).succ
Cg : #g.support ≤ cg.succ
Nf : f.natDegree ≤ N
Og : g.natDegree ≤ O
f0 : ¬f = 0
⊢ reflect (N + O) (f * g) = reflect N f * reflect O g

Tactic:
rw [← eraseLead_add_C_mul_X_pow f, add_mul, reflect_add, reflect_add, add_mul, hcf, hcf] <;>
  try assumption

Result:
case neg.a
R : Type u_1
inst✝ : Semiring R
cg cf : ℕ
hcf :
  ∀ (N O : ℕ) (f g : R[X]),
    #f.support ≤ cf.succ →
      #g.support ≤ cg.succ → f.natDegree ≤ N → g.natDegree ≤ O → reflect (N + O) (f * g) = reflect N f * reflect O g
N O : ℕ
f g : R[X]
Cf : #f.support ≤ (cf + 1).succ
Cg : #g.support ≤ cg.succ
Nf : f.natDegree ≤ N
Og : g.natDegree ≤ O
f0 : ¬f = 0
⊢ #(C f.leadingCoeff * X ^ f.natDegree).support ≤ cf.succ

case neg.a
R : Type u_1
inst✝ : Semiring R
cg cf : ℕ
hcf :
  ∀ (N O : ℕ) (f g : R[X]),
    #f.support ≤ cf.succ →
      #g.support ≤ cg.succ → f.natDegree ≤ N → g.natDegree ≤ O → reflect (N + O) (f * g) = reflect N f * reflect O g
N O : ℕ
f g : R[X]
Cf : #f.support ≤ (cf + 1).succ
Cg : #g.support ≤ cg.succ
Nf : f.natDegree ≤ N
Og : g.natDegree ≤ O
f0 : ¬f = 0
⊢ (C f.leadingCoeff * X ^ f.natDegree).natDegree ≤ N

case neg.a
R : Type u_1
inst✝ : Semiring R
cg cf : ℕ
hcf :
  ∀ (N O : ℕ) (f g : R[X]),
    #f.support ≤ cf.succ →
      #g.support ≤ cg.succ → f.natDegree ≤ N → g.natDegree ≤ O → reflect (N + O) (f * g) = reflect N f * reflect O g
N O : ℕ
f g : R[X]
Cf : #f.support ≤ (cf + 1).succ
Cg : #g.support ≤ cg.succ
Nf : f.natDegree ≤ N
Og : g.natDegree ≤ O
f0 : ¬f = 0
⊢ #f.eraseLead.support ≤ cf.succ

case neg.a
R : Type u_1
inst✝ : Semiring R
cg cf : ℕ
hcf :
  ∀ (N O : ℕ) (f g : R[X]),
    #f.support ≤ cf.succ →
      #g.support ≤ cg.succ → f.natDegree ≤ N → g.natDegree ≤ O → reflect (N + O) (f * g) = reflect N f * reflect O g
N O : ℕ
f g : R[X]
Cf : #f.support ≤ (cf + 1).succ
Cg : #g.support ≤ cg.succ
Nf : f.natDegree ≤ N
Og : g.natDegree ≤ O
f0 : ¬f = 0
⊢ f.eraseLead.natDegree ≤ N

Proof state:
case neg.a
R : Type u_1
inst✝ : Semiring R
cg cf : ℕ
hcf :
  ∀ (N O : ℕ) (f g : R[X]),
    #f.support ≤ cf.succ →
      #g.support ≤ cg.succ → f.natDegree ≤ N → g.natDegree ≤ O → reflect (N + O) (f * g) = reflect N f * reflect O g
N O : ℕ
f g : R[X]
Cf : #f.support ≤ (cf + 1).succ
Cg : #g.support ≤ cg.succ
Nf : f.natDegree ≤ N
Og : g.natDegree ≤ O
f0 : ¬f = 0
⊢ (C f.leadingCoeff * X ^ f.natDegree).natDegree ≤ N

Tactic:
exact le_trans (natDegree_C_mul_X_pow_le f.leadingCoeff f.natDegree) Nf

Result:
no goals

Proof state:
case pos
R : Type u_1
inst✝ : Semiring R
cg cf : ℕ
hcf :
  ∀ (N O : ℕ) (f g : R[X]),
    #f.support ≤ cf.succ →
      #g.support ≤ cg.succ → f.natDegree ≤ N → g.natDegree ≤ O → reflect (N + O) (f * g) = reflect N f * reflect O g
N O : ℕ
f g : R[X]
Cf : #f.support ≤ (cf + 1).succ
Cg : #g.support ≤ cg.succ
Nf : f.natDegree ≤ N
Og : g.natDegree ≤ O
f0 : f = 0
⊢ reflect (N + O) (f * g) = reflect N f * reflect O g

Tactic:
rw [f0, reflect_zero, zero_mul, zero_mul, reflect_zero]

Result:
no goals

Proof state:
case succ
R : Type u_1
inst✝ : Semiring R
cg cf : ℕ
hcf :
  ∀ (N O : ℕ) (f g : R[X]),
    #f.support ≤ cf.succ →
      #g.support ≤ cg.succ → f.natDegree ≤ N → g.natDegree ≤ O → reflect (N + O) (f * g) = reflect N f * reflect O g
⊢ ∀ (N O : ℕ) (f g : R[X]),
    #f.support ≤ (cf + 1).succ →
      #g.support ≤ cg.succ → f.natDegree ≤ N → g.natDegree ≤ O → reflect (N + O) (f * g) = reflect N f * reflect O g

Tactic:
intro N O f g Cf Cg Nf Og

Result:
case succ
R : Type u_1
inst✝ : Semiring R
cg cf : ℕ
hcf :
  ∀ (N O : ℕ) (f g : R[X]),
    #f.support ≤ cf.succ →
      #g.support ≤ cg.succ → f.natDegree ≤ N → g.natDegree ≤ O → reflect (N + O) (f * g) = reflect N f * reflect O g
N O : ℕ
f g : R[X]
Cf : #f.support ≤ (cf + 1).succ
Cg : #g.support ≤ cg.succ
Nf : f.natDegree ≤ N
Og : g.natDegree ≤ O
⊢ reflect (N + O) (f * g) = reflect N f * reflect O g

Proof state:
case neg
R : Type u_1
inst✝ : Semiring R
cg : ℕ
hcg :
  ∀ (N O : ℕ) (f g : R[X]),
    #f.support ≤ Nat.succ 0 →
      #g.support ≤ cg.succ → f.natDegree ≤ N → g.natDegree ≤ O → reflect (N + O) (f * g) = reflect N f * reflect O g
N O : ℕ
f g : R[X]
Cf : #f.support ≤ Nat.succ 0
Cg : #g.support ≤ (cg + 1).succ
Nf : f.natDegree ≤ N
Og : g.natDegree ≤ O
g0 : ¬g = 0
⊢ reflect (N + O) (f * g) = reflect N f * reflect O g

Tactic:
rw [← eraseLead_add_C_mul_X_pow g, mul_add, reflect_add, reflect_add, mul_add, hcg, hcg] <;>
  try assumption

Result:
case neg.a
R : Type u_1
inst✝ : Semiring R
cg : ℕ
hcg :
  ∀ (N O : ℕ) (f g : R[X]),
    #f.support ≤ Nat.succ 0 →
      #g.support ≤ cg.succ → f.natDegree ≤ N → g.natDegree ≤ O → reflect (N + O) (f * g) = reflect N f * reflect O g
N O : ℕ
f g : R[X]
Cf : #f.support ≤ Nat.succ 0
Cg : #g.support ≤ (cg + 1).succ
Nf : f.natDegree ≤ N
Og : g.natDegree ≤ O
g0 : ¬g = 0
⊢ #(C g.leadingCoeff * X ^ g.natDegree).support ≤ cg.succ

case neg.a
R : Type u_1
inst✝ : Semiring R
cg : ℕ
hcg :
  ∀ (N O : ℕ) (f g : R[X]),
    #f.support ≤ Nat.succ 0 →
      #g.support ≤ cg.succ → f.natDegree ≤ N → g.natDegree ≤ O → reflect (N + O) (f * g) = reflect N f * reflect O g
N O : ℕ
f g : R[X]
Cf : #f.support ≤ Nat.succ 0
Cg : #g.support ≤ (cg + 1).succ
Nf : f.natDegree ≤ N
Og : g.natDegree ≤ O
g0 : ¬g = 0
⊢ (C g.leadingCoeff * X ^ g.natDegree).natDegree ≤ O

case neg.a
R : Type u_1
inst✝ : Semiring R
cg : ℕ
hcg :
  ∀ (N O : ℕ) (f g : R[X]),
    #f.support ≤ Nat.succ 0 →
      #g.support ≤ cg.succ → f.natDegree ≤ N → g.natDegree ≤ O → reflect (N + O) (f * g) = reflect N f * reflect O g
N O : ℕ
f g : R[X]
Cf : #f.support ≤ Nat.succ 0
Cg : #g.support ≤ (cg + 1).succ
Nf : f.natDegree ≤ N
Og : g.natDegree ≤ O
g0 : ¬g = 0
⊢ #g.eraseLead.support ≤ cg.succ

case neg.a
R : Type u_1
inst✝ : Semiring R
cg : ℕ
hcg :
  ∀ (N O : ℕ) (f g : R[X]),
    #f.support ≤ Nat.succ 0 →
      #g.support ≤ cg.succ → f.natDegree ≤ N → g.natDegree ≤ O → reflect (N + O) (f * g) = reflect N f * reflect O g
N O : ℕ
f g : R[X]
Cf : #f.support ≤ Nat.succ 0
Cg : #g.support ≤ (cg + 1).succ
Nf : f.natDegree ≤ N
Og : g.natDegree ≤ O
g0 : ¬g = 0
⊢ g.eraseLead.natDegree ≤ O

Proof state:
case zero.succ
R : Type u_1
inst✝ : Semiring R
cg : ℕ
hcg :
  ∀ (N O : ℕ) (f g : R[X]),
    #f.support ≤ Nat.succ 0 →
      #g.support ≤ cg.succ → f.natDegree ≤ N → g.natDegree ≤ O → reflect (N + O) (f * g) = reflect N f * reflect O g
N O : ℕ
f g : R[X]
Cf : #f.support ≤ Nat.succ 0
Cg : #g.support ≤ (cg + 1).succ
Nf : f.natDegree ≤ N
Og : g.natDegree ≤ O
⊢ reflect (N + O) (f * g) = reflect N f * reflect O g

Tactic:
by_cases g0 : g = 0

Result:
case pos
R : Type u_1
inst✝ : Semiring R
cg : ℕ
hcg :
  ∀ (N O : ℕ) (f g : R[X]),
    #f.support ≤ Nat.succ 0 →
      #g.support ≤ cg.succ → f.natDegree ≤ N → g.natDegree ≤ O → reflect (N + O) (f * g) = reflect N f * reflect O g
N O : ℕ
f g : R[X]
Cf : #f.support ≤ Nat.succ 0
Cg : #g.support ≤ (cg + 1).succ
Nf : f.natDegree ≤ N
Og : g.natDegree ≤ O
g0 : g = 0
⊢ reflect (N + O) (f * g) = reflect N f * reflect O g

case neg
R : Type u_1
inst✝ : Semiring R
cg : ℕ
hcg :
  ∀ (N O : ℕ) (f g : R[X]),
    #f.support ≤ Nat.succ 0 →
      #g.support ≤ cg.succ → f.natDegree ≤ N → g.natDegree ≤ O → reflect (N + O) (f * g) = reflect N f * reflect O g
N O : ℕ
f g : R[X]
Cf : #f.support ≤ Nat.succ 0
Cg : #g.support ≤ (cg + 1).succ
Nf : f.natDegree ≤ N
Og : g.natDegree ≤ O
g0 : ¬g = 0
⊢ reflect (N + O) (f * g) = reflect N f * reflect O g