awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Polynomial.EraseLead
Goal:
R : Type u_2
inst : Ring R
inst_1 : NoZeroDivisors R
inst_2 : Nontrivial R
x : R
P : R[X]
hx : x ≠ 0
h : P.nextCoeff = 0
hp : ¬P = 0
he : ¬P.eraseLead = 0
h₁ : (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X]) * P).natDegree = P.natDegree + 1
dP : ℕ
hdP : P.natDegree = dP + 2
h₂ : (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X]) * P).nextCoeff ≠ 0
n : ℕ
hn : n < P.natDegree
hd₁ : n < (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X]) * P).eraseLead.natDegree
hn₂ : n = 0
⊢ (HMul.hMul (β := R[X]) (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X]))
          ((monomial P.natDegree : (a : R) → R[X]) P.leadingCoeff : R[X])).coeff
      0 =
    0

Tactic:
simpa [coeff_monomial, hp] using fun _ ↦ by lia

Premises used: Polynomial.coeff_monomial
-- Module: Mathlib.Algebra.Polynomial.EraseLead
Goal:
R : Type u_2
inst : Ring R
inst_1 : NoZeroDivisors R
inst_2 : Nontrivial R
x : R
P : R[X]
hx : x ≠ 0
h : P.nextCoeff = 0
hp : ¬P = 0
he : ¬P.eraseLead = 0
h₁ : (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X]) * P).natDegree = P.natDegree + 1
dP : ℕ
hdP : P.natDegree = dP + 2
h₂ : (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X]) * P).nextCoeff ≠ 0
n : ℕ
hn : n < P.natDegree
hd₁ : n < (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X]) * P).eraseLead.natDegree
n_1 : ℕ
hn₂ : n = n_1 + 1
⊢ ¬P.natDegree = n_1

Tactic:
lia
-- Module: Mathlib.Algebra.Polynomial.EraseLead
Goal:
R : Type u_2
inst : Ring R
inst_1 : NoZeroDivisors R
inst_2 : Nontrivial R
x : R
P : R[X]
hx : x ≠ 0
h : P.nextCoeff = 0
hp : ¬P = 0
he : ¬P.eraseLead = 0
h₁ : (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X]) * P).natDegree = P.natDegree + 1
dP : ℕ
hdP : P.natDegree = dP + 2
h₂ : (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X]) * P).nextCoeff ≠ 0
n : ℕ
hn : n < P.natDegree
hd₁ : n < (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X]) * P).eraseLead.natDegree
n_1 : ℕ
hn₂ : n = n_1 + 1
⊢ ¬P.natDegree = n_1 + 1

Tactic:
lia
-- Module: Mathlib.Algebra.Polynomial.EraseLead
Goal:
R : Type u_2
inst : Ring R
inst_1 : NoZeroDivisors R
inst_2 : Nontrivial R
x : R
P : R[X]
hx : x ≠ 0
h : P.nextCoeff = 0
hp : ¬P = 0
he : ¬P.eraseLead = 0
h₁ : (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X]) * P).natDegree = P.natDegree + 1
dP : ℕ
hdP : P.natDegree = dP + 2
h₂ : (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X]) * P).nextCoeff ≠ 0
n : ℕ
hn : n < P.natDegree
hd₁ : n < (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X]) * P).eraseLead.natDegree
n_1 : ℕ
hn₂ : n = n_1 + 1
neg :
  coeff ((monomial P.natDegree : (a : R) → R[X]) P.leadingCoeff) n_1 -
      x * coeff ((monomial P.natDegree : (a : R) → R[X]) P.leadingCoeff) (n_1 + 1) =
    0
neg₁ :
  (if P.natDegree = n_1 then P.leadingCoeff else 0) -
      x * coeff ((monomial P.natDegree : (a : R) → R[X]) P.leadingCoeff) (n_1 + 1) =
    0
neg₂ : ((if P.natDegree = n_1 then P.leadingCoeff else 0) - x * if P.natDegree = n_1 + 1 then P.leadingCoeff else 0) = 0
neg₃ : (0 - x * if P.natDegree = n_1 + 1 then P.leadingCoeff else 0) = 0
neg₄ : 0 - x * 0 = 0
neg₅ : HSub.hSub (α := R) 0 0 = 0
neg₆ neg₇ : Eq.{u_2 + 1} (α := R) 0 0
⊢ (HMul.hMul (β := R[X]) (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X]))
          ((monomial P.natDegree : (a : R) → R[X]) P.leadingCoeff : R[X])).coeff
      (n_1 + 1) =
    0

Tactic:
rw [coeff_X_sub_C_mul, coeff_monomial, coeff_monomial, if_neg (by lia),
        if_neg (by lia), mul_zero, sub_zero]

Premises used: sub_zero, Polynomial.coeff_X_sub_C_mul, Polynomial.coeff_monomial, MulZeroClass.mul_zero, if_neg
-- Module: Mathlib.Algebra.Polynomial.EraseLead
Goal:
R : Type u_2
inst : Ring R
inst_1 : NoZeroDivisors R
inst_2 : Nontrivial R
x : R
P : R[X]
hx : x ≠ 0
h : P.nextCoeff = 0
hp : ¬P = 0
he : ¬P.eraseLead = 0
h₁ : (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X]) * P).natDegree = P.natDegree + 1
dP : ℕ
hdP : P.natDegree = dP + 2
h₂ : (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X]) * P).nextCoeff ≠ 0
n : ℕ
hn : n ≥ P.natDegree
trans : (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X]) * P).eraseLead.eraseLead.coeff n = 0
trans₁ : 0 = (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X]) * P.eraseLead).coeff n
⊢ (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X]) * P).eraseLead.eraseLead.coeff n =
    (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X]) * P.eraseLead).coeff n

Tactic:
trans 0
-- Module: Mathlib.Algebra.Polynomial.EraseLead
Goal:
R : Type u_2
inst : Ring R
inst_1 : NoZeroDivisors R
inst_2 : Nontrivial R
x : R
P : R[X]
hx : x ≠ 0
h : P.nextCoeff = 0
hp : ¬P = 0
he : ¬P.eraseLead = 0
h₁ : (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X]) * P).natDegree = P.natDegree + 1
dP : ℕ
hdP : P.natDegree = dP + 2
h₂ : (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X]) * P).nextCoeff ≠ 0
n : ℕ
hn : n ≥ P.natDegree
rw : (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X]) * P).eraseLead.eraseLead.natDegree < n
⊢ (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X]) * P).eraseLead.eraseLead.coeff n = 0

Tactic:
rw [coeff_eq_zero_of_natDegree_lt]

Premises used: Polynomial.coeff_eq_zero_of_natDegree_lt
-- Module: Mathlib.Algebra.Polynomial.EraseLead
Goal:
R : Type u_2
inst : Ring R
inst_1 : NoZeroDivisors R
inst_2 : Nontrivial R
x : R
P : R[X]
hx : x ≠ 0
h : P.nextCoeff = 0
hp : ¬P = 0
he : ¬P.eraseLead = 0
h₁ : (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X]) * P).natDegree = P.natDegree + 1
dP : ℕ
hdP : P.natDegree = dP + 2
h₂ : (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X]) * P).nextCoeff ≠ 0
n : ℕ
hn : n ≥ P.natDegree
rw : (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X]) * P.eraseLead).natDegree < n
⊢ 0 = (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X]) * P.eraseLead).coeff n

Tactic:
rw [coeff_eq_zero_of_natDegree_lt]

Premises used: Polynomial.coeff_eq_zero_of_natDegree_lt
-- Module: Mathlib.Algebra.Polynomial.EraseLead
Goal:
R : Type u_2
inst : Ring R
inst_1 : NoZeroDivisors R
inst_2 : Nontrivial R
x : R
P : R[X]
hx : x ≠ 0
h : P.nextCoeff = 0
hp : ¬P = 0
he : ¬P.eraseLead = 0
h₁ : (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X]) * P).natDegree = P.natDegree + 1
dP : ℕ
hdP : P.natDegree = dP + 2
h₂ : (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X]) * P).nextCoeff ≠ 0
n : ℕ
hn : n ≥ P.natDegree
grw : (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X]) * P).natDegree - 1 - 1 < n
⊢ (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X]) * P).eraseLead.eraseLead.natDegree < n

Tactic:
grw [eraseLead_natDegree_le, eraseLead_natDegree_le]

Premises used: Polynomial.eraseLead_natDegree_le
-- Module: Mathlib.Algebra.Polynomial.EraseLead
Goal:
R : Type u_2
inst : Ring R
inst_1 : NoZeroDivisors R
inst_2 : Nontrivial R
x : R
P : R[X]
hx : x ≠ 0
h : P.nextCoeff = 0
hp : ¬P = 0
he : ¬P.eraseLead = 0
h₁ : (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X]) * P).natDegree = P.natDegree + 1
dP : ℕ
hdP : P.natDegree = dP + 2
h₂ : (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X]) * P).nextCoeff ≠ 0
n : ℕ
hn : n ≥ P.natDegree
⊢ (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X]) * P).natDegree - 1 - 1 < n

Tactic:
simpa [h₁, hdP] using hn
-- Module: Mathlib.Algebra.Polynomial.EraseLead
Goal:
R : Type u_2
inst : Ring R
inst_1 : NoZeroDivisors R
inst_2 : Nontrivial R
x : R
P : R[X]
hx : x ≠ 0
h : P.nextCoeff = 0
hp : ¬P = 0
he : ¬P.eraseLead = 0
h₁ : (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X]) * P).natDegree = P.natDegree + 1
dP : ℕ
hdP : P.natDegree = dP + 2
h₂ : (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X]) * P).nextCoeff ≠ 0
n : ℕ
hn : n ≥ P.natDegree
grw : (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])).natDegree + (P.natDegree - 2) < n
⊢ (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X]) * P.eraseLead).natDegree < n

Tactic:
grw [natDegree_mul (X_sub_C_ne_zero x) he, natDegree_eraseLead_le_of_nextCoeff_eq_zero h]

Premises used: Polynomial.natDegree_mul, Polynomial.X_sub_C_ne_zero, Polynomial.natDegree_eraseLead_le_of_nextCoeff_eq_zero
-- Module: Mathlib.Algebra.Polynomial.EraseLead
Goal:
R : Type u_2
inst : Ring R
inst_1 : NoZeroDivisors R
inst_2 : Nontrivial R
x : R
P : R[X]
hx : x ≠ 0
h : P.nextCoeff = 0
hp : ¬P = 0
he : ¬P.eraseLead = 0
h₁ : (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X]) * P).natDegree = P.natDegree + 1
dP : ℕ
hdP : P.natDegree = dP + 2
h₂ : (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X]) * P).nextCoeff ≠ 0
n : ℕ
hn : n ≥ P.natDegree
⊢ (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])).natDegree + (P.natDegree - 2) < n

Tactic:
simpa [add_comm, hdP] using hn

Premises used: add_comm
-- Module: Mathlib.Algebra.Polynomial.EraseLead
Goal:
R : Type u_1
inst : Semiring R
motive : R[X] → Prop
N : ℕ
zero : motive 0
C_mul_pow :
  ∀ (n : ℕ) (r : R),
    r ≠ 0 → n ≤ N → motive (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) r : R[X]) (HPow.hPow (α := R[X]) X n))
add : ∀ (f g : R[X]), f.natDegree < g.natDegree → g.natDegree ≤ N → motive f → motive g → motive (f + g)
f : R[X]
df : f.natDegree ≤ N
hf : #f.support = 0
⊢ motive 0

Tactic:
zero
-- Module: Mathlib.Algebra.Polynomial.EraseLead
Goal:
R : Type u_1
inst : Semiring R
motive : R[X] → Prop
N : ℕ
zero : motive 0
C_mul_pow :
  ∀ (n : ℕ) (r : R),
    r ≠ 0 → n ≤ N → motive (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) r : R[X]) (HPow.hPow (α := R[X]) X n))
add : ∀ (f g : R[X]), f.natDegree < g.natDegree → g.natDegree ≤ N → motive f → motive g → motive (f + g)
f : R[X]
df : f.natDegree ≤ N
hf : #f.support = 0
h : f = 0
⊢ motive f

Tactic:
convert! zero
-- Module: Mathlib.Algebra.Polynomial.EraseLead
Goal:
R : Type u_1
inst : Semiring R
motive : R[X] → Prop
N : ℕ
zero : motive 0
C_mul_pow :
  ∀ (n : ℕ) (r : R),
    r ≠ 0 → n ≤ N → motive (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) r : R[X]) (HPow.hPow (α := R[X]) X n))
add : ∀ (f g : R[X]), f.natDegree < g.natDegree → g.natDegree ≤ N → motive f → motive g → motive (f + g)
f : R[X]
df : f.natDegree ≤ N
hf : #f.support = 0
⊢ f = 0

Tactic:
simpa [support_eq_empty, card_eq_zero] using hf

Premises used: Finset.card_eq_zero, Polynomial.support_eq_empty
-- Module: Mathlib.Algebra.Polynomial.EraseLead
Goal:
R : Type u_1
inst : Semiring R
motive : R[X] → Prop
N : ℕ
zero : motive 0
C_mul_pow :
  ∀ (n : ℕ) (r : R),
    r ≠ 0 → n ≤ N → motive (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) r : R[X]) (HPow.hPow (α := R[X]) X n))
add : ∀ (f g : R[X]), f.natDegree < g.natDegree → g.natDegree ≤ N → motive f → motive g → motive (f + g)
c : ℕ
hc : ∀ (f : R[X]) (df : f.natDegree ≤ N) (hf : #f.support = c), motive f
f : R[X]
df : f.natDegree ≤ N
hf : #f.support = c + 1
succ :
  motive
    (f.eraseLead +
      HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) f.leadingCoeff : R[X]) (HPow.hPow (α := R[X]) X f.natDegree))
⊢ motive f

Tactic:
rw [← eraseLead_add_C_mul_X_pow f]

Premises used: Polynomial.eraseLead_add_C_mul_X_pow
-- Module: Mathlib.Algebra.Polynomial.EraseLead
Goal:
R : Type u_1
inst : Semiring R
motive : R[X] → Prop
N : ℕ
zero : motive 0
C_mul_pow :
  ∀ (n : ℕ) (r : R),
    r ≠ 0 → n ≤ N → motive (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) r : R[X]) (HPow.hPow (α := R[X]) X n))
add : ∀ (f g : R[X]), f.natDegree < g.natDegree → g.natDegree ≤ N → motive f → motive g → motive (f + g)
c : ℕ
hc : ∀ (f : R[X]) (df : f.natDegree ≤ N) (hf : #f.support = c), motive f
f : R[X]
df : f.natDegree ≤ N
hf : #f.support = c + 1
succ :
  ∀ (hc : ∀ (f : R[X]) (df : f.natDegree ≤ N) (hf : #f.support = 0), motive f)
    (hf : #f.support = HAdd.hAdd (α := ℕ) 0 1),
    motive
      (f.eraseLead +
        HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) f.leadingCoeff : R[X]) (HPow.hPow (α := R[X]) X f.natDegree))
succ₁ :
  ∀ (n : ℕ) (hc : ∀ (f : R[X]) (df : f.natDegree ≤ N) (hf : #f.support = n + 1), motive f)
    (hf : #f.support = n + 1 + 1),
    motive
      (f.eraseLead +
        HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) f.leadingCoeff : R[X]) (HPow.hPow (α := R[X]) X f.natDegree))
⊢ motive
    (f.eraseLead +
      HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) f.leadingCoeff : R[X]) (HPow.hPow (α := R[X]) X f.natDegree))

Tactic:
cases c
-- Module: Mathlib.Algebra.Polynomial.EraseLead
Goal:
R : Type u_1
inst : Semiring R
motive : R[X] → Prop
N : ℕ
zero : motive 0
C_mul_pow :
  ∀ (n : ℕ) (r : R),
    r ≠ 0 → n ≤ N → motive (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) r : R[X]) (HPow.hPow (α := R[X]) X n))
add : ∀ (f g : R[X]), f.natDegree < g.natDegree → g.natDegree ≤ N → motive f → motive g → motive (f + g)
f : R[X]
df : f.natDegree ≤ N
hc : ∀ (f : R[X]) (df : f.natDegree ≤ N) (hf : #f.support = 0), motive f
hf : #f.support = HAdd.hAdd (α := ℕ) 0 1
⊢ motive (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) f.leadingCoeff : R[X]) (HPow.hPow (α := R[X]) X f.natDegree))

Tactic:
C_mul_pow f.natDegree f.leadingCoeff ?_ df

Premises used: Polynomial.leadingCoeff, Polynomial.natDegree
-- Module: Mathlib.Algebra.Polynomial.EraseLead
Goal:
R : Type u_1
inst : Semiring R
motive : R[X] → Prop
N : ℕ
zero : motive 0
C_mul_pow :
  ∀ (n : ℕ) (r : R),
    r ≠ 0 → n ≤ N → motive (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) r : R[X]) (HPow.hPow (α := R[X]) X n))
add : ∀ (f g : R[X]), f.natDegree < g.natDegree → g.natDegree ≤ N → motive f → motive g → motive (f + g)
f : R[X]
df : f.natDegree ≤ N
hc : ∀ (f : R[X]) (df : f.natDegree ≤ N) (hf : #f.support = 0), motive f
hf : #f.support = HAdd.hAdd (α := ℕ) 0 1
h :
  f.eraseLead +
      HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) f.leadingCoeff : R[X]) (HPow.hPow (α := R[X]) X f.natDegree) =
    HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) f.leadingCoeff : R[X]) (HPow.hPow (α := R[X]) X f.natDegree)
succ : f.leadingCoeff ≠ 0
⊢ motive
    (f.eraseLead +
      HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) f.leadingCoeff : R[X]) (HPow.hPow (α := R[X]) X f.natDegree))

Tactic:
convert! C_mul_pow f.natDegree f.leadingCoeff ?_ df using 1

Premises used: Polynomial.leadingCoeff, Polynomial.natDegree
-- Module: Mathlib.Algebra.Polynomial.EraseLead
Goal:
R : Type u_1
inst : Semiring R
motive : R[X] → Prop
N : ℕ
zero : motive 0
C_mul_pow :
  ∀ (n : ℕ) (r : R),
    r ≠ 0 → n ≤ N → motive (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) r : R[X]) (HPow.hPow (α := R[X]) X n))
add : ∀ (f g : R[X]), f.natDegree < g.natDegree → g.natDegree ≤ N → motive f → motive g → motive (f + g)
f : R[X]
df : f.natDegree ≤ N
hc : ∀ (f : R[X]) (df : f.natDegree ≤ N) (hf : #f.support = 0), motive f
hf : #f.support = HAdd.hAdd (α := ℕ) 0 1
⊢ 0 + HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) f.leadingCoeff : R[X]) (HPow.hPow (α := R[X]) X f.natDegree) =
    HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) f.leadingCoeff : R[X]) (HPow.hPow (α := R[X]) X f.natDegree)

Tactic:
zero_add (C (leadingCoeff f) * X ^ f.natDegree)

Premises used: Polynomial.C, HMul.hMul, Polynomial.leadingCoeff, zero_add, HPow.hPow, Polynomial.natDegree, Polynomial.X, DFunLike.coe
-- Module: Mathlib.Algebra.Polynomial.EraseLead
Goal:
R : Type u_1
inst : Semiring R
motive : R[X] → Prop
N : ℕ
zero : motive 0
C_mul_pow :
  ∀ (n : ℕ) (r : R),
    r ≠ 0 → n ≤ N → motive (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) r : R[X]) (HPow.hPow (α := R[X]) X n))
add : ∀ (f g : R[X]), f.natDegree < g.natDegree → g.natDegree ≤ N → motive f → motive g → motive (f + g)
f : R[X]
df : f.natDegree ≤ N
hc : ∀ (f : R[X]) (df : f.natDegree ≤ N) (hf : #f.support = 0), motive f
hf : #f.support = HAdd.hAdd (α := ℕ) 0 1
h : f.eraseLead = 0
⊢ f.eraseLead +
      HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) f.leadingCoeff : R[X]) (HPow.hPow (α := R[X]) X f.natDegree) =
    HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) f.leadingCoeff : R[X]) (HPow.hPow (α := R[X]) X f.natDegree)

Tactic:
convert! zero_add (C (leadingCoeff f) * X ^ f.natDegree)

Premises used: Polynomial.C, HMul.hMul, Polynomial.leadingCoeff, zero_add, HPow.hPow, Polynomial.natDegree, Polynomial.X, DFunLike.coe
-- Module: Mathlib.Algebra.Polynomial.EraseLead
Goal:
R : Type u_1
inst : Semiring R
motive : R[X] → Prop
N : ℕ
zero : motive 0
C_mul_pow :
  ∀ (n : ℕ) (r : R),
    r ≠ 0 → n ≤ N → motive (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) r : R[X]) (HPow.hPow (α := R[X]) X n))
add : ∀ (f g : R[X]), f.natDegree < g.natDegree → g.natDegree ≤ N → motive f → motive g → motive (f + g)
f : R[X]
df : f.natDegree ≤ N
hc : ∀ (f : R[X]) (df : f.natDegree ≤ N) (hf : #f.support = 0), motive f
hf : #f.support = HAdd.hAdd (α := ℕ) 0 1
h : #f.eraseLead.support = 0
h₁ h₂ : Eq (α := ℕ) 0 0
⊢ f.eraseLead = 0

Tactic:
rw [← card_support_eq_zero, card_support_eraseLead' hf]

Premises used: Polynomial.card_support_eraseLead', Polynomial.card_support_eq_zero
-- Module: Mathlib.Algebra.Polynomial.EraseLead
Goal:
R : Type u_1
inst : Semiring R
motive : R[X] → Prop
N : ℕ
zero : motive 0
C_mul_pow :
  ∀ (n : ℕ) (r : R),
    r ≠ 0 → n ≤ N → motive (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) r : R[X]) (HPow.hPow (α := R[X]) X n))
add : ∀ (f g : R[X]), f.natDegree < g.natDegree → g.natDegree ≤ N → motive f → motive g → motive (f + g)
f : R[X]
df : f.natDegree ≤ N
hc : ∀ (f : R[X]) (df : f.natDegree ≤ N) (hf : #f.support = 0), motive f
hf : #f.support = HAdd.hAdd (α := ℕ) 0 1
succ : ¬HAdd.hAdd (α := ℕ) 0 1 = 0
⊢ f.leadingCoeff ≠ 0

Tactic:
rw [leadingCoeff_ne_zero, Ne, ← card_support_eq_zero, hf]

Premises used: Ne, Polynomial.card_support_eq_zero, Polynomial.leadingCoeff_ne_zero
-- Module: Mathlib.Algebra.Polynomial.EraseLead
Goal:
R : Type u_1
inst : Semiring R
motive : R[X] → Prop
N : ℕ
zero : motive 0
C_mul_pow :
  ∀ (n : ℕ) (r : R),
    r ≠ 0 → n ≤ N → motive (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) r : R[X]) (HPow.hPow (α := R[X]) X n))
add : ∀ (f g : R[X]), f.natDegree < g.natDegree → g.natDegree ≤ N → motive f → motive g → motive (f + g)
f : R[X]
df : f.natDegree ≤ N
hc : ∀ (f : R[X]) (df : f.natDegree ≤ N) (hf : #f.support = 0), motive f
hf : #f.support = HAdd.hAdd (α := ℕ) 0 1
⊢ ¬HAdd.hAdd (α := ℕ) 0 1 = 0

Tactic:
zero_ne_one.symm

Premises used: zero_ne_one, Ne.symm
-- Module: Mathlib.Algebra.Polynomial.EraseLead
Goal:
R : Type u_1
inst : Semiring R
motive : R[X] → Prop
N : ℕ
zero : motive 0
C_mul_pow :
  ∀ (n : ℕ) (r : R),
    r ≠ 0 → n ≤ N → motive (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) r : R[X]) (HPow.hPow (α := R[X]) X n))
add : ∀ (f g : R[X]), f.natDegree < g.natDegree → g.natDegree ≤ N → motive f → motive g → motive (f + g)
f : R[X]
df : f.natDegree ≤ N
hc : ∀ (f : R[X]) (df : f.natDegree ≤ N) (hf : #f.support = 0), motive f
hf : #f.support = HAdd.hAdd (α := ℕ) 0 1
⊢ ¬HAdd.hAdd (α := ℕ) 0 1 = 0

Tactic:
exact zero_ne_one.symm

Premises used: zero_ne_one, Ne.symm
-- Module: Mathlib.Algebra.Polynomial.EraseLead
Goal:
R : Type u_1
inst : Semiring R
motive : R[X] → Prop
N : ℕ
zero : motive 0
C_mul_pow :
  ∀ (n : ℕ) (r : R),
    r ≠ 0 → n ≤ N → motive (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) r : R[X]) (HPow.hPow (α := R[X]) X n))
add : ∀ (f g : R[X]), f.natDegree < g.natDegree → g.natDegree ≤ N → motive f → motive g → motive (f + g)
f : R[X]
df : f.natDegree ≤ N
n : ℕ
hc : ∀ (f : R[X]) (df : f.natDegree ≤ N) (hf : #f.support = n + 1), motive f
hf : #f.support = n + 1 + 1
⊢ motive
    (f.eraseLead +
      HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) f.leadingCoeff : R[X]) (HPow.hPow (α := R[X]) X f.natDegree))

Tactic:
add f.eraseLead _ ?_ ?_ ?_ ?_

Premises used: Polynomial.eraseLead
-- Module: Mathlib.Algebra.Polynomial.EraseLead
Goal:
R : Type u_1
inst : Semiring R
motive : R[X] → Prop
N : ℕ
zero : motive 0
C_mul_pow :
  ∀ (n : ℕ) (r : R),
    r ≠ 0 → n ≤ N → motive (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) r : R[X]) (HPow.hPow (α := R[X]) X n))
add : ∀ (f g : R[X]), f.natDegree < g.natDegree → g.natDegree ≤ N → motive f → motive g → motive (f + g)
f : R[X]
df : f.natDegree ≤ N
n : ℕ
hc : ∀ (f : R[X]) (df : f.natDegree ≤ N) (hf : #f.support = n + 1), motive f
hf : #f.support = n + 1 + 1
succ :
  f.eraseLead.natDegree <
    (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) f.leadingCoeff : R[X]) (HPow.hPow (α := R[X]) X f.natDegree)).natDegree
succ₁ :
  (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) f.leadingCoeff : R[X]) (HPow.hPow (α := R[X]) X f.natDegree)).natDegree ≤
    N
succ₂ : motive f.eraseLead
succ₃ :
  motive (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) f.leadingCoeff : R[X]) (HPow.hPow (α := R[X]) X f.natDegree))
⊢ motive
    (f.eraseLead +
      HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) f.leadingCoeff : R[X]) (HPow.hPow (α := R[X]) X f.natDegree))

Tactic:
refine add f.eraseLead _ ?_ ?_ ?_ ?_

Premises used: Polynomial.eraseLead
-- Module: Mathlib.Algebra.Polynomial.EraseLead
Goal:
R : Type u_1
inst : Semiring R
motive : R[X] → Prop
N : ℕ
zero : motive 0
C_mul_pow :
  ∀ (n : ℕ) (r : R),
    r ≠ 0 → n ≤ N → motive (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) r : R[X]) (HPow.hPow (α := R[X]) X n))
add : ∀ (f g : R[X]), f.natDegree < g.natDegree → g.natDegree ≤ N → motive f → motive g → motive (f + g)
f : R[X]
df : f.natDegree ≤ N
n : ℕ
hc : ∀ (f : R[X]) (df : f.natDegree ≤ N) (hf : #f.support = n + 1), motive f
hf : #f.support = n + 1 + 1
⊢ f.eraseLead.natDegree <
    (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) f.leadingCoeff : R[X]) (HPow.hPow (α := R[X]) X f.natDegree)).natDegree

Tactic:
(eraseLead_natDegree_lt ?_).trans_le (le_of_eq ?_)

Premises used: LT.lt.trans_le, Polynomial.eraseLead_natDegree_lt, le_of_eq
-- Module: Mathlib.Algebra.Polynomial.EraseLead
Goal:
R : Type u_1
inst : Semiring R
motive : R[X] → Prop
N : ℕ
zero : motive 0
C_mul_pow :
  ∀ (n : ℕ) (r : R),
    r ≠ 0 → n ≤ N → motive (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) r : R[X]) (HPow.hPow (α := R[X]) X n))
add : ∀ (f g : R[X]), f.natDegree < g.natDegree → g.natDegree ≤ N → motive f → motive g → motive (f + g)
f : R[X]
df : f.natDegree ≤ N
n : ℕ
hc : ∀ (f : R[X]) (df : f.natDegree ≤ N) (hf : #f.support = n + 1), motive f
hf : #f.support = n + 1 + 1
succ : 2 ≤ #f.support
succ₁ :
  f.natDegree =
    (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) f.leadingCoeff : R[X]) (HPow.hPow (α := R[X]) X f.natDegree)).natDegree
⊢ f.eraseLead.natDegree <
    (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) f.leadingCoeff : R[X]) (HPow.hPow (α := R[X]) X f.natDegree)).natDegree

Tactic:
refine (eraseLead_natDegree_lt ?_).trans_le (le_of_eq ?_)

Premises used: LT.lt.trans_le, Polynomial.eraseLead_natDegree_lt, le_of_eq
-- Module: Mathlib.Algebra.Polynomial.EraseLead
Goal:
R : Type u_1
inst : Semiring R
motive : R[X] → Prop
N : ℕ
zero : motive 0
C_mul_pow :
  ∀ (n : ℕ) (r : R),
    r ≠ 0 → n ≤ N → motive (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) r : R[X]) (HPow.hPow (α := R[X]) X n))
add : ∀ (f g : R[X]), f.natDegree < g.natDegree → g.natDegree ≤ N → motive f → motive g → motive (f + g)
f : R[X]
df : f.natDegree ≤ N
n : ℕ
hc : ∀ (f : R[X]) (df : f.natDegree ≤ N) (hf : #f.support = n + 1), motive f
hf : #f.support = n + 1 + 1
⊢ 2 ≤ #f.support

Tactic:
(Nat.succ_le_succ (Nat.succ_le_succ (Nat.zero_le _))).trans hf.ge

Premises used: Nat.zero_le, Eq.ge, LE.le.trans, Nat.succ_le_succ
-- Module: Mathlib.Algebra.Polynomial.EraseLead
Goal:
R : Type u_1
inst : Semiring R
motive : R[X] → Prop
N : ℕ
zero : motive 0
C_mul_pow :
  ∀ (n : ℕ) (r : R),
    r ≠ 0 → n ≤ N → motive (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) r : R[X]) (HPow.hPow (α := R[X]) X n))
add : ∀ (f g : R[X]), f.natDegree < g.natDegree → g.natDegree ≤ N → motive f → motive g → motive (f + g)
f : R[X]
df : f.natDegree ≤ N
n : ℕ
hc : ∀ (f : R[X]) (df : f.natDegree ≤ N) (hf : #f.support = n + 1), motive f
hf : #f.support = n + 1 + 1
⊢ 2 ≤ #f.support

Tactic:
exact (Nat.succ_le_succ (Nat.succ_le_succ (Nat.zero_le _))).trans hf.ge

Premises used: Nat.zero_le, Eq.ge, LE.le.trans, Nat.succ_le_succ