-- 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:
R : Type u_1
inst✝ : Semiring R
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

Tactic:
induction' cf with cf hcf

Result:
case zero
R : Type u_1
inst✝ : Semiring R
cg : ℕ
⊢ ∀ (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

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

Proof state:
case zero
R : Type u_1
inst✝ : Semiring R
cg : ℕ
⊢ ∀ (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

Tactic:
induction' cg with cg hcg

Result:
case zero.zero
R : Type u_1
inst✝ : Semiring R
⊢ ∀ (N O : ℕ) (f g : R[X]),
    #f.support ≤ Nat.succ 0 →
      #g.support ≤ Nat.succ 0 → f.natDegree ≤ N → g.natDegree ≤ O → reflect (N + O) (f * g) = reflect N f * reflect O g

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

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
⊢ #(C g.leadingCoeff * X ^ g.natDegree).support ≤ cg.succ

Tactic:
exact le_add_left card_support_C_mul_X_pow_le_one

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

Tactic:
by_cases f0 : f = 0

Result:
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

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

Proof state:
case zero.zero
R : Type u_1
inst✝ : Semiring R
⊢ ∀ (N O : ℕ) (f g : R[X]),
    #f.support ≤ Nat.succ 0 →
      #g.support ≤ Nat.succ 0 → 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.zero
R : Type u_1
inst✝ : Semiring R
N O : ℕ
f g : R[X]
Cf : #f.support ≤ Nat.succ 0
Cg : #g.support ≤ Nat.succ 0
Nf : f.natDegree ≤ N
Og : 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 : ℕ
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

Tactic:
exact le_trans (natDegree_C_mul_X_pow_le g.leadingCoeff g.natDegree) Og

Result:
no goals

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

Tactic:
rw [← C_mul_X_pow_eq_self Cf, ← C_mul_X_pow_eq_self Cg]

Result:
case zero.zero
R : Type u_1
inst✝ : Semiring R
N O : ℕ
f g : R[X]
Cf : #f.support ≤ Nat.succ 0
Cg : #g.support ≤ Nat.succ 0
Nf : f.natDegree ≤ N
Og : g.natDegree ≤ O
⊢ reflect (N + O) (C f.leadingCoeff * X ^ f.natDegree * (C g.leadingCoeff * X ^ g.natDegree)) =
    reflect N (C f.leadingCoeff * X ^ f.natDegree) * reflect O (C g.leadingCoeff * X ^ g.natDegree)

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).support ≤ cf.succ

Tactic:
exact le_add_left card_support_C_mul_X_pow_le_one

Result:
no goals

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

Tactic:
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]

Result:
no goals