-- 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.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

Tactic:
exact Nat.lt_succ_iff.mp (gt_of_ge_of_gt Cf (eraseLead_support_card_lt f0))

Result:
no goals

Proof state:
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

Tactic:
exact le_trans eraseLead_natDegree_le_aux Og

Result:
no goals

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
⊢ f.eraseLead.natDegree ≤ N

Tactic:
exact le_trans eraseLead_natDegree_le_aux Nf

Result:
no goals

Proof state:
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

Tactic:
exact Nat.lt_succ_iff.mp (gt_of_ge_of_gt Cg (eraseLead_support_card_lt g0))

Result:
no goals

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
⊢ g.natDegree ≤ O

Tactic:
assumption

Result:
no goals

Proof state:
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

Tactic:
rw [g0, reflect_zero, mul_zero, mul_zero, reflect_zero]

Result:
no goals

Proof state:
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
⊢ f.natDegree ≤ N

Tactic:
assumption

Result:
no goals

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]),
    #f.support ≤ Nat.succ 0 →
      #g.support ≤ (cg + 1).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 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