awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Polynomial.Reverse
Goal:
R : Type u_1
inst : Semiring R
N O : ℕ
f : R[X]
Cf : #f.support ≤ Nat.succ 0
Nf : f.natDegree ≤ N
cg : ℕ
hcg :
  ∀ (g : R[X]) (Cg : #g.support ≤ cg.succ) (Og : g.natDegree ≤ O), reflect (N + O) (f * g) = reflect N f * reflect O g
g : R[X]
Cg : #g.support ≤ (cg + 1).succ
Og : g.natDegree ≤ O
g0 : ¬g = 0
neg :
  #(HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) g.leadingCoeff : R[X]) (HPow.hPow (α := R[X]) X g.natDegree)).support ≤
    cg.succ
neg₁ :
  (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) g.leadingCoeff : R[X]) (HPow.hPow (α := R[X]) X g.natDegree)).natDegree ≤
    O
neg₂ : #g.eraseLead.support ≤ cg.succ
neg₃ : g.eraseLead.natDegree ≤ O
⊢ 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]

Premises used: Polynomial.eraseLead_add_C_mul_X_pow, Polynomial.reflect_add, mul_add
-- Module: Mathlib.Algebra.Polynomial.Reverse
Goal:
R : Type u_1
inst : Semiring R
N O : ℕ
f : R[X]
Cf : #f.support ≤ Nat.succ 0
Nf : f.natDegree ≤ N
cg : ℕ
hcg :
  ∀ (g : R[X]) (Cg : #g.support ≤ cg.succ) (Og : g.natDegree ≤ O), reflect (N + O) (f * g) = reflect N f * reflect O g
g : R[X]
Cg : #g.support ≤ (cg + 1).succ
Og : g.natDegree ≤ O
g0 : ¬g = 0
⊢ #(HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) g.leadingCoeff : R[X]) (HPow.hPow (α := R[X]) X g.natDegree)).support ≤
    cg.succ

Tactic:
le_add_left card_support_C_mul_X_pow_le_one

Premises used: Polynomial.card_support_C_mul_X_pow_le_one, le_add_left
-- Module: Mathlib.Algebra.Polynomial.Reverse
Goal:
R : Type u_1
inst : Semiring R
N O : ℕ
f : R[X]
Cf : #f.support ≤ Nat.succ 0
Nf : f.natDegree ≤ N
cg : ℕ
hcg :
  ∀ (g : R[X]) (Cg : #g.support ≤ cg.succ) (Og : g.natDegree ≤ O), reflect (N + O) (f * g) = reflect N f * reflect O g
g : R[X]
Cg : #g.support ≤ (cg + 1).succ
Og : g.natDegree ≤ O
g0 : ¬g = 0
⊢ #(HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) g.leadingCoeff : R[X]) (HPow.hPow (α := R[X]) X g.natDegree)).support ≤
    cg.succ

Tactic:
exact le_add_left card_support_C_mul_X_pow_le_one

Premises used: Polynomial.card_support_C_mul_X_pow_le_one, le_add_left
-- Module: Mathlib.Algebra.Polynomial.Reverse
Goal:
R : Type u_1
inst : Semiring R
N O : ℕ
f : R[X]
Cf : #f.support ≤ Nat.succ 0
Nf : f.natDegree ≤ N
cg : ℕ
hcg :
  ∀ (g : R[X]) (Cg : #g.support ≤ cg.succ) (Og : g.natDegree ≤ O), reflect (N + O) (f * g) = reflect N f * reflect O g
g : R[X]
Cg : #g.support ≤ (cg + 1).succ
Og : g.natDegree ≤ O
g0 : ¬g = 0
⊢ (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) g.leadingCoeff : R[X]) (HPow.hPow (α := R[X]) X g.natDegree)).natDegree ≤
    O

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

Premises used: Polynomial.leadingCoeff, Polynomial.natDegree, Polynomial.natDegree_C_mul_X_pow_le, le_trans
-- Module: Mathlib.Algebra.Polynomial.Reverse
Goal:
R : Type u_1
inst : Semiring R
N O : ℕ
f : R[X]
Cf : #f.support ≤ Nat.succ 0
Nf : f.natDegree ≤ N
cg : ℕ
hcg :
  ∀ (g : R[X]) (Cg : #g.support ≤ cg.succ) (Og : g.natDegree ≤ O), reflect (N + O) (f * g) = reflect N f * reflect O g
g : R[X]
Cg : #g.support ≤ (cg + 1).succ
Og : g.natDegree ≤ O
g0 : ¬g = 0
⊢ (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) g.leadingCoeff : R[X]) (HPow.hPow (α := R[X]) X g.natDegree)).natDegree ≤
    O

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

Premises used: Polynomial.leadingCoeff, Polynomial.natDegree, Polynomial.natDegree_C_mul_X_pow_le, le_trans
-- Module: Mathlib.Algebra.Polynomial.Reverse
Goal:
R : Type u_1
inst : Semiring R
N O : ℕ
f : R[X]
Cf : #f.support ≤ Nat.succ 0
Nf : f.natDegree ≤ N
cg : ℕ
hcg :
  ∀ (g : R[X]) (Cg : #g.support ≤ cg.succ) (Og : g.natDegree ≤ O), reflect (N + O) (f * g) = reflect N f * reflect O g
g : R[X]
Cg : #g.support ≤ (cg + 1).succ
Og : g.natDegree ≤ O
g0 : ¬g = 0
⊢ #g.eraseLead.support ≤ cg.succ

Tactic:
Nat.lt_succ_iff.mp (lt_of_lt_of_le (eraseLead_support_card_lt g0) Cg)

Premises used: Nat.lt_succ_iff, Polynomial.eraseLead_support_card_lt, Iff.mp, lt_of_lt_of_le
-- Module: Mathlib.Algebra.Polynomial.Reverse
Goal:
R : Type u_1
inst : Semiring R
N O : ℕ
f : R[X]
Cf : #f.support ≤ Nat.succ 0
Nf : f.natDegree ≤ N
cg : ℕ
hcg :
  ∀ (g : R[X]) (Cg : #g.support ≤ cg.succ) (Og : g.natDegree ≤ O), reflect (N + O) (f * g) = reflect N f * reflect O g
g : R[X]
Cg : #g.support ≤ (cg + 1).succ
Og : g.natDegree ≤ O
g0 : ¬g = 0
⊢ #g.eraseLead.support ≤ cg.succ

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

Premises used: Nat.lt_succ_iff, Polynomial.eraseLead_support_card_lt, Iff.mp, lt_of_lt_of_le
-- Module: Mathlib.Algebra.Polynomial.Reverse
Goal:
R : Type u_1
inst : Semiring R
N O : ℕ
f : R[X]
Cf : #f.support ≤ Nat.succ 0
Nf : f.natDegree ≤ N
cg : ℕ
hcg :
  ∀ (g : R[X]) (Cg : #g.support ≤ cg.succ) (Og : g.natDegree ≤ O), reflect (N + O) (f * g) = reflect N f * reflect O g
g : R[X]
Cg : #g.support ≤ (cg + 1).succ
Og : g.natDegree ≤ O
g0 : ¬g = 0
⊢ g.eraseLead.natDegree ≤ O

Tactic:
le_trans eraseLead_natDegree_le_aux Og

Premises used: Polynomial.eraseLead_natDegree_le_aux, le_trans
-- Module: Mathlib.Algebra.Polynomial.Reverse
Goal:
R : Type u_1
inst : Semiring R
N O : ℕ
f : R[X]
Cf : #f.support ≤ Nat.succ 0
Nf : f.natDegree ≤ N
cg : ℕ
hcg :
  ∀ (g : R[X]) (Cg : #g.support ≤ cg.succ) (Og : g.natDegree ≤ O), reflect (N + O) (f * g) = reflect N f * reflect O g
g : R[X]
Cg : #g.support ≤ (cg + 1).succ
Og : g.natDegree ≤ O
g0 : ¬g = 0
⊢ g.eraseLead.natDegree ≤ O

Tactic:
exact le_trans eraseLead_natDegree_le_aux Og

Premises used: Polynomial.eraseLead_natDegree_le_aux, le_trans
-- Module: Mathlib.Algebra.Polynomial.Reverse
Goal:
R : Type u_1
inst : Semiring R
cg N O : ℕ
g : R[X]
Cg : #g.support ≤ cg.succ
Og : g.natDegree ≤ O
f : R[X]
Cf : #f.support ≤ Nat.succ 0
Nf : f.natDegree ≤ N
zero :
  ∀ (g : R[X]) (Cg : #g.support ≤ Nat.succ 0) (Og : g.natDegree ≤ O),
    reflect (N + O) (f * g) = reflect N f * reflect O g
zero₁ :
  ∀ (cg : ℕ)
    (hcg :
      ∀ (g : R[X]) (Cg : #g.support ≤ cg.succ) (Og : g.natDegree ≤ O),
        reflect (N + O) (f * g) = reflect N f * reflect O g)
    (g : R[X]) (Cg : #g.support ≤ (cg + 1).succ) (Og : g.natDegree ≤ O),
    reflect (N + O) (f * g) = reflect N f * reflect O g
⊢ reflect (N + O) (f * g) = reflect N f * reflect O g

Tactic:
induction cg generalizing g with
    | zero =>
      rw [← C_mul_X_pow_eq_self Cf, ← C_mul_X_pow_eq_self Cg]
      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]
    | succ cg hcg =>
      by_cases g0 : g = 0
      · rw [g0, reflect_zero, mul_zero, mul_zero, reflect_zero]
      rw [← eraseLead_add_C_mul_X_pow g, mul_add, reflect_add, reflect_add, mul_add, hcg, hcg] <;>
        try assumption
      · exact le_add_left card_support_C_mul_X_pow_le_one
      · exact le_trans (natDegree_C_mul_X_pow_le g.leadingCoeff g.natDegree) Og
      · exact Nat.lt_succ_iff.mp (lt_of_lt_of_le (eraseLead_support_card_lt g0) Cg)
      · exact le_trans eraseLead_natDegree_le_aux Og

Premises used: Polynomial.eraseLead_add_C_mul_X_pow, mul_assoc, pow_add, Polynomial.reflect_add, Polynomial.reflect_monomial, Polynomial.leadingCoeff, add_comm, Polynomial.reflect_zero, MulZeroClass.mul_zero, Polynomial.C_mul_X_pow_eq_self, Polynomial.card_support_C_mul_X_pow_le_one, Polynomial.reflect_C_mul, mul_add, Polynomial.natDegree, Polynomial.revAt_add, Polynomial.eraseLead_natDegree_le_aux, Polynomial.X, Polynomial.natDegree_C_mul_X_pow_le, le_trans, Polynomial.X_pow_mul, le_add_left
-- Module: Mathlib.Algebra.Polynomial.Reverse
Goal:
R : Type u_1
inst : Semiring R
cg N O : ℕ
g : R[X]
Cg : #g.support ≤ cg.succ
Og : g.natDegree ≤ O
cf : ℕ
hcf :
  ∀ (f : R[X]) (Cf : #f.support ≤ cf.succ) (Nf : f.natDegree ≤ N), reflect (N + O) (f * g) = reflect N f * reflect O g
f : R[X]
Cf : #f.support ≤ (cf + 1).succ
Nf : f.natDegree ≤ N
pos : ∀ (f0 : f = 0), reflect (N + O) (f * g) = reflect N f * reflect O g
neg : ∀ (f0 : ¬f = 0), reflect (N + O) (f * g) = reflect N f * reflect O g
⊢ reflect (N + O) (f * g) = reflect N f * reflect O g

Tactic:
by_cases f0 : f = 0
-- Module: Mathlib.Algebra.Polynomial.Reverse
Goal:
R : Type u_1
inst : Semiring R
cg N O : ℕ
g : R[X]
Cg : #g.support ≤ cg.succ
Og : g.natDegree ≤ O
cf : ℕ
hcf :
  ∀ (f : R[X]) (Cf : #f.support ≤ cf.succ) (Nf : f.natDegree ≤ N), reflect (N + O) (f * g) = reflect N f * reflect O g
f : R[X]
Cf : #f.support ≤ (cf + 1).succ
Nf : f.natDegree ≤ N
f0 : f = 0
pos : reflect (N + O) (0 * g) = reflect N 0 * reflect O g
pos₁ : reflect (N + O) (0 * g) = 0 * reflect O g
pos₂ : reflect (N + O) 0 = 0 * reflect O g
pos₃ : Eq.{u_1 + 1} (α := R[X]) (reflect (N + O) 0) 0
pos₄ pos₅ : Eq.{u_1 + 1} (α := R[X]) 0 0
⊢ reflect (N + O) (f * g) = reflect N f * reflect O g

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

Premises used: MulZeroClass.zero_mul, Polynomial.reflect_zero
-- Module: Mathlib.Algebra.Polynomial.Reverse
Goal:
R : Type u_1
inst : Semiring R
cg N O : ℕ
g : R[X]
Cg : #g.support ≤ cg.succ
Og : g.natDegree ≤ O
cf : ℕ
hcf :
  ∀ (f : R[X]) (Cf : #f.support ≤ cf.succ) (Nf : f.natDegree ≤ N), reflect (N + O) (f * g) = reflect N f * reflect O g
f : R[X]
Cf : #f.support ≤ (cf + 1).succ
Nf : f.natDegree ≤ N
f0 : ¬f = 0
neg :
  #(HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) f.leadingCoeff : R[X]) (HPow.hPow (α := R[X]) X f.natDegree)).support ≤
    cf.succ
neg₁ :
  (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) f.leadingCoeff : R[X]) (HPow.hPow (α := R[X]) X f.natDegree)).natDegree ≤
    N
neg₂ : #f.eraseLead.support ≤ cf.succ
neg₃ : f.eraseLead.natDegree ≤ N
⊢ 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]

Premises used: add_mul, Polynomial.eraseLead_add_C_mul_X_pow, Polynomial.reflect_add
-- Module: Mathlib.Algebra.Polynomial.Reverse
Goal:
R : Type u_1
inst : Semiring R
cg N O : ℕ
g : R[X]
Cg : #g.support ≤ cg.succ
Og : g.natDegree ≤ O
cf : ℕ
hcf :
  ∀ (f : R[X]) (Cf : #f.support ≤ cf.succ) (Nf : f.natDegree ≤ N), reflect (N + O) (f * g) = reflect N f * reflect O g
f : R[X]
Cf : #f.support ≤ (cf + 1).succ
Nf : f.natDegree ≤ N
f0 : ¬f = 0
⊢ #(HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) f.leadingCoeff : R[X]) (HPow.hPow (α := R[X]) X f.natDegree)).support ≤
    cf.succ

Tactic:
le_add_left card_support_C_mul_X_pow_le_one

Premises used: Polynomial.card_support_C_mul_X_pow_le_one, le_add_left
-- Module: Mathlib.Algebra.Polynomial.Reverse
Goal:
R : Type u_1
inst : Semiring R
cg N O : ℕ
g : R[X]
Cg : #g.support ≤ cg.succ
Og : g.natDegree ≤ O
cf : ℕ
hcf :
  ∀ (f : R[X]) (Cf : #f.support ≤ cf.succ) (Nf : f.natDegree ≤ N), reflect (N + O) (f * g) = reflect N f * reflect O g
f : R[X]
Cf : #f.support ≤ (cf + 1).succ
Nf : f.natDegree ≤ N
f0 : ¬f = 0
⊢ #(HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) f.leadingCoeff : R[X]) (HPow.hPow (α := R[X]) X f.natDegree)).support ≤
    cf.succ

Tactic:
exact le_add_left card_support_C_mul_X_pow_le_one

Premises used: Polynomial.card_support_C_mul_X_pow_le_one, le_add_left
-- Module: Mathlib.Algebra.Polynomial.Reverse
Goal:
R : Type u_1
inst : Semiring R
cg N O : ℕ
g : R[X]
Cg : #g.support ≤ cg.succ
Og : g.natDegree ≤ O
cf : ℕ
hcf :
  ∀ (f : R[X]) (Cf : #f.support ≤ cf.succ) (Nf : f.natDegree ≤ N), reflect (N + O) (f * g) = reflect N f * reflect O g
f : R[X]
Cf : #f.support ≤ (cf + 1).succ
Nf : f.natDegree ≤ N
f0 : ¬f = 0
⊢ (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) f.leadingCoeff : R[X]) (HPow.hPow (α := R[X]) X f.natDegree)).natDegree ≤
    N

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

Premises used: Polynomial.leadingCoeff, Polynomial.natDegree, Polynomial.natDegree_C_mul_X_pow_le, le_trans
-- Module: Mathlib.Algebra.Polynomial.Reverse
Goal:
R : Type u_1
inst : Semiring R
cg N O : ℕ
g : R[X]
Cg : #g.support ≤ cg.succ
Og : g.natDegree ≤ O
cf : ℕ
hcf :
  ∀ (f : R[X]) (Cf : #f.support ≤ cf.succ) (Nf : f.natDegree ≤ N), reflect (N + O) (f * g) = reflect N f * reflect O g
f : R[X]
Cf : #f.support ≤ (cf + 1).succ
Nf : f.natDegree ≤ N
f0 : ¬f = 0
⊢ (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) f.leadingCoeff : R[X]) (HPow.hPow (α := R[X]) X f.natDegree)).natDegree ≤
    N

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

Premises used: Polynomial.leadingCoeff, Polynomial.natDegree, Polynomial.natDegree_C_mul_X_pow_le, le_trans
-- Module: Mathlib.Algebra.Polynomial.Reverse
Goal:
R : Type u_1
inst : Semiring R
cg N O : ℕ
g : R[X]
Cg : #g.support ≤ cg.succ
Og : g.natDegree ≤ O
cf : ℕ
hcf :
  ∀ (f : R[X]) (Cf : #f.support ≤ cf.succ) (Nf : f.natDegree ≤ N), reflect (N + O) (f * g) = reflect N f * reflect O g
f : R[X]
Cf : #f.support ≤ (cf + 1).succ
Nf : f.natDegree ≤ N
f0 : ¬f = 0
⊢ #f.eraseLead.support ≤ cf.succ

Tactic:
Nat.lt_succ_iff.mp (lt_of_lt_of_le (eraseLead_support_card_lt f0) Cf)

Premises used: Nat.lt_succ_iff, Polynomial.eraseLead_support_card_lt, Iff.mp, lt_of_lt_of_le
-- Module: Mathlib.Algebra.Polynomial.Reverse
Goal:
R : Type u_1
inst : Semiring R
cg N O : ℕ
g : R[X]
Cg : #g.support ≤ cg.succ
Og : g.natDegree ≤ O
cf : ℕ
hcf :
  ∀ (f : R[X]) (Cf : #f.support ≤ cf.succ) (Nf : f.natDegree ≤ N), reflect (N + O) (f * g) = reflect N f * reflect O g
f : R[X]
Cf : #f.support ≤ (cf + 1).succ
Nf : f.natDegree ≤ N
f0 : ¬f = 0
⊢ #f.eraseLead.support ≤ cf.succ

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

Premises used: Nat.lt_succ_iff, Polynomial.eraseLead_support_card_lt, Iff.mp, lt_of_lt_of_le
-- Module: Mathlib.Algebra.Polynomial.Reverse
Goal:
R : Type u_1
inst : Semiring R
cg N O : ℕ
g : R[X]
Cg : #g.support ≤ cg.succ
Og : g.natDegree ≤ O
cf : ℕ
hcf :
  ∀ (f : R[X]) (Cf : #f.support ≤ cf.succ) (Nf : f.natDegree ≤ N), reflect (N + O) (f * g) = reflect N f * reflect O g
f : R[X]
Cf : #f.support ≤ (cf + 1).succ
Nf : f.natDegree ≤ N
f0 : ¬f = 0
⊢ f.eraseLead.natDegree ≤ N

Tactic:
le_trans eraseLead_natDegree_le_aux Nf

Premises used: Polynomial.eraseLead_natDegree_le_aux, le_trans
-- Module: Mathlib.Algebra.Polynomial.Reverse
Goal:
R : Type u_1
inst : Semiring R
cg N O : ℕ
g : R[X]
Cg : #g.support ≤ cg.succ
Og : g.natDegree ≤ O
cf : ℕ
hcf :
  ∀ (f : R[X]) (Cf : #f.support ≤ cf.succ) (Nf : f.natDegree ≤ N), reflect (N + O) (f * g) = reflect N f * reflect O g
f : R[X]
Cf : #f.support ≤ (cf + 1).succ
Nf : f.natDegree ≤ N
f0 : ¬f = 0
⊢ f.eraseLead.natDegree ≤ N

Tactic:
exact le_trans eraseLead_natDegree_le_aux Nf

Premises used: Polynomial.eraseLead_natDegree_le_aux, le_trans
-- Module: Mathlib.Algebra.Polynomial.Reverse
Goal:
R : Type u_1
inst : Semiring R
cf cg N O : ℕ
f g : R[X]
Cf : #f.support ≤ cf.succ
Cg : #g.support ≤ cg.succ
Nf : f.natDegree ≤ N
Og : g.natDegree ≤ O
zero :
  ∀ (f : R[X]) (Cf : #f.support ≤ Nat.succ 0) (Nf : f.natDegree ≤ N),
    reflect (N + O) (f * g) = reflect N f * reflect O g
succ :
  ∀ (cf : ℕ)
    (hcf :
      ∀ (f : R[X]) (Cf : #f.support ≤ cf.succ) (Nf : f.natDegree ≤ N),
        reflect (N + O) (f * g) = reflect N f * reflect O g)
    (f : R[X]) (Cf : #f.support ≤ (cf + 1).succ) (Nf : f.natDegree ≤ N),
    reflect (N + O) (f * g) = reflect N f * reflect O g
⊢ reflect (N + O) (f * g) = reflect N f * reflect O g

Tactic:
induction cf generalizing f with
  | zero =>
    induction cg generalizing g with
    | zero =>
      rw [← C_mul_X_pow_eq_self Cf, ← C_mul_X_pow_eq_self Cg]
      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]
    | succ cg hcg =>
      by_cases g0 : g = 0
      · rw [g0, reflect_zero, mul_zero, mul_zero, reflect_zero]
      rw [← eraseLead_add_C_mul_X_pow g, mul_add, reflect_add, reflect_add, mul_add, hcg, hcg] <;>
        try assumption
      · exact le_add_left card_support_C_mul_X_pow_le_one
      · exact le_trans (natDegree_C_mul_X_pow_le g.leadingCoeff g.natDegree) Og
      · exact Nat.lt_succ_iff.mp (lt_of_lt_of_le (eraseLead_support_card_lt g0) Cg)
      · exact le_trans eraseLead_natDegree_le_aux Og
  | succ cf hcf =>
    by_cases f0 : f = 0
    · rw [f0, reflect_zero, zero_mul, zero_mul, reflect_zero]
    rw [← eraseLead_add_C_mul_X_pow f, add_mul, reflect_add, reflect_add, add_mul, hcf, hcf] <;>
      try assumption
    · exact le_add_left card_support_C_mul_X_pow_le_one
    · exact le_trans (natDegree_C_mul_X_pow_le f.leadingCoeff f.natDegree) Nf
    · exact Nat.lt_succ_iff.mp (lt_of_lt_of_le (eraseLead_support_card_lt f0) Cf)
    · exact le_trans eraseLead_natDegree_le_aux Nf

Premises used: add_mul, Polynomial.eraseLead_add_C_mul_X_pow, MulZeroClass.zero_mul, mul_assoc, pow_add, Polynomial.reflect_add, Polynomial.reflect_monomial, Polynomial.leadingCoeff, add_comm, Polynomial.reflect_zero, MulZeroClass.mul_zero, Polynomial.C_mul_X_pow_eq_self, Polynomial.card_support_C_mul_X_pow_le_one, Polynomial.reflect_C_mul, mul_add, Polynomial.natDegree, Polynomial.revAt_add, Polynomial.eraseLead_natDegree_le_aux, Polynomial.X, Polynomial.natDegree_C_mul_X_pow_le, le_trans, Polynomial.X_pow_mul, le_add_left
-- Module: Mathlib.Algebra.Polynomial.Reverse
Goal:
R : Type u_1
inst : Semiring R
f g : R[X]
F G : ℕ
Ff : f.natDegree ≤ F
Gg : g.natDegree ≤ G
⊢ reflect (F + G) (f * g) = reflect F f * reflect G g

Tactic:
reflect_mul_induction _ _ F G f g f.support.card.le_succ g.support.card.le_succ Ff Gg

Premises used: Nat.le_succ, Finset.card, Polynomial.support, Polynomial.reflect_mul_induction
-- Module: Mathlib.Algebra.Polynomial.Reverse
Goal:
R : Type u_1
inst : Semiring R
N : ℕ
p : R[X]
⊢ (reflect N p).natDegree ≤ max N p.natDegree

Tactic:
simp +contextual [-le_sup_iff, natDegree_le_iff_coeff_eq_zero,
    revAt, not_le_of_gt, coeff_eq_zero_of_natDegree_lt]

Premises used: Polynomial.natDegree_le_iff_coeff_eq_zero, Polynomial.revAt, Polynomial.coeff_eq_zero_of_natDegree_lt, le_sup_iff, not_le_of_gt
-- Module: Mathlib.Algebra.Polynomial.Reverse
Goal:
R : Type u_1
inst : Semiring R
S : Type u_2
inst_1 : CommSemiring S
i : R →+* S
x : S
inst_2 : Invertible x
N : ℕ
f : R[X]
hf : f.natDegree ≤ N
⊢ eval₂ i (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne x _) (reflect N f) * x ^ N = eval₂ i x f

Tactic:
induction_with_natDegree_le (fun f => eval₂ i (⅟x) (reflect N f) * x ^ N = eval₂ i x f) _ ?_ ?_
      ?_ f hf

Premises used: HMul.hMul, Invertible.invOf, Polynomial.induction_with_natDegree_le, Polynomial.eval₂, HPow.hPow, Polynomial.reflect, Eq
-- Module: Mathlib.Algebra.Polynomial.Reverse
Goal:
R : Type u_1
inst : Semiring R
S : Type u_2
inst_1 : CommSemiring S
i : R →+* S
x : S
inst_2 : Invertible x
N : ℕ
f : R[X]
hf : f.natDegree ≤ N
refine_1 : eval₂ i (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne x _) (reflect N 0) * x ^ N = eval₂ i x 0
refine_2 :
  ∀ (n : ℕ) (r : R),
    r ≠ 0 →
      n ≤ N →
        (fun (f : R[X]) ↦
            eval₂ i (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne x _) (reflect N f) * x ^ N = eval₂ i x f)
          (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) r : R[X]) (HPow.hPow (α := R[X]) X n))
refine_3 :
  ∀ (f g : R[X]),
    f.natDegree < g.natDegree →
      g.natDegree ≤ N →
        (fun (f : R[X]) ↦
              eval₂ i (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne x _) (reflect N f) * x ^ N =
                eval₂ i x f)
            f →
          (fun (f : R[X]) ↦
                eval₂ i (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne x _) (reflect N f) * x ^ N =
                  eval₂ i x f)
              g →
            (fun (f : R[X]) ↦
                eval₂ i (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne x _) (reflect N f) * x ^ N =
                  eval₂ i x f)
              (f + g)
⊢ eval₂ i (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne x _) (reflect N f) * x ^ N = eval₂ i x f

Tactic:
refine
    induction_with_natDegree_le (fun f => eval₂ i (⅟x) (reflect N f) * x ^ N = eval₂ i x f) _ ?_ ?_
      ?_ f hf

Premises used: HMul.hMul, Invertible.invOf, Polynomial.induction_with_natDegree_le, Polynomial.eval₂, HPow.hPow, Polynomial.reflect, Eq
-- Module: Mathlib.Algebra.Polynomial.Reverse
Goal:
R : Type u_1
inst : Semiring R
S : Type u_2
inst_1 : CommSemiring S
i : R →+* S
x : S
inst_2 : Invertible x
N : ℕ
f : R[X]
hf : f.natDegree ≤ N
⊢ (fun (f : R[X]) ↦
      eval₂ i (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne x _) (reflect N f) * x ^ N = eval₂ i x f)
    0

Tactic:
simp
-- Module: Mathlib.Algebra.Polynomial.Reverse
Goal:
R : Type u_1
inst : Semiring R
S : Type u_2
inst_1 : CommSemiring S
i : R →+* S
x : S
inst_2 : Invertible x
N : ℕ
f : R[X]
hf : f.natDegree ≤ N
n : ℕ
r : R
refine_2 :
  r ≠ 0 →
    n ≤ N →
      (fun (f : R[X]) ↦
          eval₂ i (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne x _) (reflect N f) * x ^ N = eval₂ i x f)
        (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) r : R[X]) (HPow.hPow (α := R[X]) X n))
⊢ r ≠ 0 →
    n ≤ N →
      (fun (f : R[X]) ↦
          eval₂ i (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne x _) (reflect N f) * x ^ N = eval₂ i x f)
        (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) r : R[X]) (HPow.hPow (α := R[X]) X n))

Tactic:
_
-- Module: Mathlib.Algebra.Polynomial.Reverse
Goal:
R : Type u_1
inst : Semiring R
S : Type u_2
inst_1 : CommSemiring S
i : R →+* S
x : S
inst_2 : Invertible x
N : ℕ
f : R[X]
hf : f.natDegree ≤ N
n : ℕ
r : R
h : r ≠ 0
hnN : n ≤ N
refine_2 :
  HMul.hMul (α := S) ((i : (a : R) → S) r : S)
        (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne x _ ^ (N - n)) *
      x ^ N =
    HMul.hMul (α := S) ((i : (a : R) → S) r : S) (x ^ n)
⊢ eval₂ i (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne x _)
        (reflect N (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) r : R[X]) (HPow.hPow (α := R[X]) X n))) *
      x ^ N =
    eval₂ i x (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) r : R[X]) (HPow.hPow (α := R[X]) X n))

Tactic:
simp only [revAt_le hnN, reflect_C_mul_X_pow, eval₂_X_pow, eval₂_C, eval₂_mul]

Premises used: Polynomial.eval₂_X_pow, Polynomial.revAt_le, Polynomial.eval₂_mul, Polynomial.reflect_C_mul_X_pow, Polynomial.eval₂_C
-- Module: Mathlib.Algebra.Polynomial.Reverse
Goal:
R : Type u_1
inst : Semiring R
S : Type u_2
inst_1 : CommSemiring S
i : R →+* S
x : S
inst_2 : Invertible x
N : ℕ
f : R[X]
hf : f.natDegree ≤ N
n : ℕ
r : R
h : r ≠ 0
hnN : n ≤ N
rw : x ^ (N - n + n)
| x ^ N

Tactic:
rw [← Nat.sub_add_cancel hnN]

Premises used: Nat.sub_add_cancel
-- Module: Mathlib.Algebra.Polynomial.Reverse
Goal:
R : Type u_1
inst : Semiring R
S : Type u_2
inst_1 : CommSemiring S
i : R →+* S
x : S
inst_2 : Invertible x
N : ℕ
f : R[X]
hf : f.natDegree ≤ N
n : ℕ
r : R
h : r ≠ 0
hnN : n ≤ N
refine_2 :
  HMul.hMul (α := S) ((i : (a : R) → S) r : S)
        (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne x _ ^ (N - n)) *
      x ^ (N - n + n) =
    HMul.hMul (α := S) ((i : (a : R) → S) r : S) (x ^ n)
⊢ HMul.hMul (α := S) ((i : (a : R) → S) r : S)
        (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne x _ ^ (N - n)) *
      x ^ N =
    HMul.hMul (α := S) ((i : (a : R) → S) r : S) (x ^ n)

Tactic:
conv in x ^ N => rw [← Nat.sub_add_cancel hnN]

Premises used: Nat.sub_add_cancel