awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.EraseLead (goal)
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
neg :
  ∀ (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
⊢ (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 =
    0
have neg₁ : ∀ (n_1 : ℕ) (hn₂ : n = n_1 + 1),
  (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: rcases hn₂ : n
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.EraseLead (goal)
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
⊢ (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
have 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
Tactic: rw [coeff_X_sub_C_mul, coeff_monomial, coeff_monomial, if_neg (by lia),
        if_neg (by lia), mul_zero, sub_zero]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.EraseLead (goal)
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
⊢ (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
have 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
Tactic: rw [coeff_X_sub_C_mul, coeff_monomial, coeff_monomial, if_neg (by lia),
        if_neg (by lia), mul_zero, sub_zero]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.EraseLead (goal)
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
⊢ (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
have neg₂ : ((if P.natDegree = n_1 then P.leadingCoeff else 0) - x * if P.natDegree = n_1 + 1 then P.leadingCoeff else 0) = 0
Tactic: rw [coeff_X_sub_C_mul, coeff_monomial, coeff_monomial, if_neg (by lia),
        if_neg (by lia), mul_zero, sub_zero]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.EraseLead (goal)
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
⊢ (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
have neg₃ : (0 - x * if P.natDegree = n_1 + 1 then P.leadingCoeff else 0) = 0
Tactic: rw [coeff_X_sub_C_mul, coeff_monomial, coeff_monomial, if_neg (by lia),
        if_neg (by lia), mul_zero, sub_zero]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.EraseLead (goal)
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
⊢ (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
have neg₄ : 0 - x * 0 = 0
Tactic: rw [coeff_X_sub_C_mul, coeff_monomial, coeff_monomial, if_neg (by lia),
        if_neg (by lia), mul_zero, sub_zero]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.EraseLead (goal)
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
⊢ (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
have neg₅ : HSub.hSub (α := R) 0 0 = 0
Tactic: rw [coeff_X_sub_C_mul, coeff_monomial, coeff_monomial, if_neg (by lia),
        if_neg (by lia), mul_zero, sub_zero]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.EraseLead (goal)
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
⊢ (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
have neg₆ : Eq.{u_2 + 1} (α := R) 0 0
Tactic: rw [coeff_X_sub_C_mul, coeff_monomial, coeff_monomial, if_neg (by lia),
        if_neg (by lia), mul_zero, sub_zero]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.EraseLead (goal)
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).eraseLead.eraseLead.coeff n =
    (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X]) * P.eraseLead).coeff n
have trans : (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X]) * P).eraseLead.eraseLead.coeff n = 0
Tactic: trans 0
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.EraseLead (goal)
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
⊢ (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
have trans₁ : 0 = (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X]) * P.eraseLead).coeff n
Tactic: trans 0
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.EraseLead (goal)
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).eraseLead.eraseLead.coeff n = 0
have rw : (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X]) * P).eraseLead.eraseLead.natDegree < n
Tactic: rw [coeff_eq_zero_of_natDegree_lt]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.EraseLead (goal)
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
⊢ 0 = (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X]) * P.eraseLead).coeff n
have rw : (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X]) * P.eraseLead).natDegree < n
Tactic: rw [coeff_eq_zero_of_natDegree_lt]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.EraseLead (goal)
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).eraseLead.eraseLead.natDegree < n
have grw : (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X]) * P).natDegree - 1 - 1 < n
Tactic: grw [eraseLead_natDegree_le, eraseLead_natDegree_le]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.EraseLead (goal)
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.eraseLead).natDegree < n
have grw : (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])).natDegree + (P.natDegree - 2) < n
Tactic: grw [natDegree_mul (X_sub_C_ne_zero x) he, natDegree_eraseLead_le_of_nextCoeff_eq_zero h]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.EraseLead (goal)
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 f
have h : f = 0
Tactic: convert! zero
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.EraseLead (goal)
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
⊢ motive f
have succ : motive
  (f.eraseLead +
    HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) f.leadingCoeff : R[X]) (HPow.hPow (α := R[X]) X f.natDegree))
Tactic: rw [← eraseLead_add_C_mul_X_pow f]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.EraseLead (goal)
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
⊢ motive
    (f.eraseLead +
      HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) f.leadingCoeff : R[X]) (HPow.hPow (α := R[X]) X f.natDegree))
have 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))
Tactic: cases c
Cleared hypotheses: c, hc, hf
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.EraseLead (goal)
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))
⊢ motive
    (f.eraseLead +
      HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) f.leadingCoeff : R[X]) (HPow.hPow (α := R[X]) X f.natDegree))
have 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))
Tactic: cases c
Cleared hypotheses: c, hc, hf
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.EraseLead (goal)
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
    (f.eraseLead +
      HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) f.leadingCoeff : R[X]) (HPow.hPow (α := R[X]) X f.natDegree))
have 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)
Tactic: convert! C_mul_pow f.natDegree f.leadingCoeff ?_ df using 1
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.EraseLead (goal)
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)
⊢ motive
    (f.eraseLead +
      HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) f.leadingCoeff : R[X]) (HPow.hPow (α := R[X]) X f.natDegree))
have succ : f.leadingCoeff ≠ 0
Tactic: convert! C_mul_pow f.natDegree f.leadingCoeff ?_ df using 1
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.EraseLead (goal)
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
⊢ 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)
have h : f.eraseLead = 0
Tactic: convert! zero_add (C (leadingCoeff f) * X ^ f.natDegree)
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.EraseLead (goal)
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
⊢ f.eraseLead = 0
have h : #f.eraseLead.support = 0
Tactic: rw [← card_support_eq_zero, card_support_eraseLead' hf]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.EraseLead (goal)
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
⊢ f.eraseLead = 0
have h₁ : Eq (α := ℕ) 0 0
Tactic: rw [← card_support_eq_zero, card_support_eraseLead' hf]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.EraseLead (goal)
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
⊢ f.leadingCoeff ≠ 0
have succ : ¬HAdd.hAdd (α := ℕ) 0 1 = 0
Tactic: rw [leadingCoeff_ne_zero, Ne, ← card_support_eq_zero, hf]