awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.EraseLead (goal)
Goal:
R : Type u_1
inst : Semiring R
n : ℕ
hn :
  ∀ {f : R[X]},
    #f.support = n →
      ∃ (k : Fin n → ℕ) (x : Fin n → R) (_ : StrictMono k) (_ : ∀ (i : Fin n), x i ≠ 0),
        f = ∑ i : Fin n, HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (x i) : R[X]) (HPow.hPow (α := R[X]) X (k i))
f : R[X]
h : #f.support = n + 1
k : Fin n → ℕ
x : Fin n → R
hk : StrictMono k
hx : ∀ (i : Fin n), x i ≠ 0
hf :
  f.eraseLead = ∑ i : Fin n, HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (x i) : R[X]) (HPow.hPow (α := R[X]) X (k i))
H : ¬∃ (k : Fin n), k.castSucc = Fin.last n
j : Fin (n + 1)
i : Fin n
hij : i.castSucc < j
hj : ¬∃ (j₀ : Fin n), j₀.castSucc = j
⊢ k i < Function.extend Fin.castSucc k (fun (x : Fin (n + 1)) ↦ f.natDegree) j
have neg : k i < f.natDegree
Tactic: rw [Function.extend_apply' _ _ _ hj]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.EraseLead (goal)
Goal:
R : Type u_1
inst : Semiring R
n : ℕ
hn :
  ∀ {f : R[X]},
    #f.support = n →
      ∃ (k : Fin n → ℕ) (x : Fin n → R) (_ : StrictMono k) (_ : ∀ (i : Fin n), x i ≠ 0),
        f = ∑ i : Fin n, HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (x i) : R[X]) (HPow.hPow (α := R[X]) X (k i))
f : R[X]
h : #f.support = n + 1
k : Fin n → ℕ
x : Fin n → R
hk : StrictMono k
hx : ∀ (i : Fin n), x i ≠ 0
hf :
  f.eraseLead = ∑ i : Fin n, HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (x i) : R[X]) (HPow.hPow (α := R[X]) X (k i))
H : ¬∃ (k : Fin n), k.castSucc = Fin.last n
j : Fin (n + 1)
i : Fin n
hij : i.castSucc < j
hj : ¬∃ (j₀ : Fin n), j₀.castSucc = j
⊢ k i < f.natDegree
have neg : k i ∈ f.eraseLead.support
Tactic: apply lt_natDegree_of_mem_eraseLead_support
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.EraseLead (goal)
Goal:
R : Type u_1
inst : Semiring R
n : ℕ
hn :
  ∀ {f : R[X]},
    #f.support = n →
      ∃ (k : Fin n → ℕ) (x : Fin n → R) (_ : StrictMono k) (_ : ∀ (i : Fin n), x i ≠ 0),
        f = ∑ i : Fin n, HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (x i) : R[X]) (HPow.hPow (α := R[X]) X (k i))
f : R[X]
h : #f.support = n + 1
k : Fin n → ℕ
x : Fin n → R
hk : StrictMono k
hx : ∀ (i : Fin n), x i ≠ 0
hf :
  f.eraseLead = ∑ i : Fin n, HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (x i) : R[X]) (HPow.hPow (α := R[X]) X (k i))
H : ¬∃ (k : Fin n), k.castSucc = Fin.last n
j : Fin (n + 1)
i : Fin n
hij : i.castSucc < j
hj : ¬∃ (j₀ : Fin n), j₀.castSucc = j
⊢ k i ∈ f.eraseLead.support
have neg : Ne.{u_1 + 1} (α := R)
  (∑ b : Fin n, (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (x b) : R[X]) (HPow.hPow (α := R[X]) X (k b))).coeff (k i))
  0
Tactic: rw [mem_support_iff, hf, finsetSum_coeff]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.EraseLead (goal)
Goal:
R : Type u_1
inst : Semiring R
n : ℕ
hn :
  ∀ {f : R[X]},
    #f.support = n →
      ∃ (k : Fin n → ℕ) (x : Fin n → R) (_ : StrictMono k) (_ : ∀ (i : Fin n), x i ≠ 0),
        f = ∑ i : Fin n, HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (x i) : R[X]) (HPow.hPow (α := R[X]) X (k i))
f : R[X]
h : #f.support = n + 1
k : Fin n → ℕ
x : Fin n → R
hk : StrictMono k
hx : ∀ (i : Fin n), x i ≠ 0
hf :
  f.eraseLead = ∑ i : Fin n, HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (x i) : R[X]) (HPow.hPow (α := R[X]) X (k i))
H : ¬∃ (k : Fin n), k.castSucc = Fin.last n
j : Fin (n + 1)
i : Fin n
hij : i.castSucc < j
hj : ¬∃ (j₀ : Fin n), j₀.castSucc = j
⊢ Ne.{u_1 + 1} (α := R)
    (∑ b : Fin n,
      (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (x b) : R[X]) (HPow.hPow (α := R[X]) X (k b))).coeff (k i))
    0
have neg : x i ≠ 0
Tactic: rw [sum_eq_single, coeff_C_mul, coeff_X_pow_self, mul_one]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.EraseLead (goal)
Goal:
R : Type u_1
inst : Semiring R
n : ℕ
hn :
  ∀ {f : R[X]},
    #f.support = n →
      ∃ (k : Fin n → ℕ) (x : Fin n → R) (_ : StrictMono k) (_ : ∀ (i : Fin n), x i ≠ 0),
        f = ∑ i : Fin n, HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (x i) : R[X]) (HPow.hPow (α := R[X]) X (k i))
f : R[X]
h : #f.support = n + 1
k : Fin n → ℕ
x : Fin n → R
hk : StrictMono k
hx : ∀ (i : Fin n), x i ≠ 0
hf :
  f.eraseLead = ∑ i : Fin n, HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (x i) : R[X]) (HPow.hPow (α := R[X]) X (k i))
H : ¬∃ (k : Fin n), k.castSucc = Fin.last n
j : Fin (n + 1)
i : Fin n
hij : i.castSucc < j
hj : ¬∃ (j₀ : Fin n), j₀.castSucc = j
neg : x i ≠ 0
⊢ Ne.{u_1 + 1} (α := R)
    (∑ b : Fin n,
      (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (x b) : R[X]) (HPow.hPow (α := R[X]) X (k b))).coeff (k i))
    0
have neg₁ : ∀ (b : Fin n),
  Membership.mem (γ := Finset (Fin n)) univ b →
    b ≠ i → (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (x b) : R[X]) (HPow.hPow (α := R[X]) X (k b))).coeff (k i) = 0
Tactic: rw [sum_eq_single, coeff_C_mul, coeff_X_pow_self, mul_one]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.EraseLead (goal)
Goal:
R : Type u_1
inst : Semiring R
n : ℕ
hn :
  ∀ {f : R[X]},
    #f.support = n →
      ∃ (k : Fin n → ℕ) (x : Fin n → R) (_ : StrictMono k) (_ : ∀ (i : Fin n), x i ≠ 0),
        f = ∑ i : Fin n, HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (x i) : R[X]) (HPow.hPow (α := R[X]) X (k i))
f : R[X]
h : #f.support = n + 1
k : Fin n → ℕ
x : Fin n → R
hk : StrictMono k
hx : ∀ (i : Fin n), x i ≠ 0
hf :
  f.eraseLead = ∑ i : Fin n, HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (x i) : R[X]) (HPow.hPow (α := R[X]) X (k i))
H : ¬∃ (k : Fin n), k.castSucc = Fin.last n
j : Fin (n + 1)
i : Fin n
hij : i.castSucc < j
hj : ¬∃ (j₀ : Fin n), j₀.castSucc = j
neg : x i ≠ 0
neg₁ :
  ∀ (b : Fin n),
    Membership.mem (γ := Finset (Fin n)) univ b →
      b ≠ i →
        (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (x b) : R[X]) (HPow.hPow (α := R[X]) X (k b))).coeff (k i) = 0
⊢ Ne.{u_1 + 1} (α := R)
    (∑ b : Fin n,
      (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (x b) : R[X]) (HPow.hPow (α := R[X]) X (k b))).coeff (k i))
    0
have neg₂ : i ∉ univ → (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (x i) : R[X]) (HPow.hPow (α := R[X]) X (k i))).coeff (k i) = 0
Tactic: rw [sum_eq_single, coeff_C_mul, coeff_X_pow_self, mul_one]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.EraseLead (goal)
Goal:
R : Type u_1
inst : Semiring R
n : ℕ
hn :
  ∀ {f : R[X]},
    #f.support = n →
      ∃ (k : Fin n → ℕ) (x : Fin n → R) (_ : StrictMono k) (_ : ∀ (i : Fin n), x i ≠ 0),
        f = ∑ i : Fin n, HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (x i) : R[X]) (HPow.hPow (α := R[X]) X (k i))
f : R[X]
h : #f.support = n + 1
k : Fin n → ℕ
x : Fin n → R
hk : StrictMono k
hx : ∀ (i : Fin n), x i ≠ 0
hf :
  f.eraseLead = ∑ i : Fin n, HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (x i) : R[X]) (HPow.hPow (α := R[X]) X (k i))
H : ¬∃ (k : Fin n), k.castSucc = Fin.last n
j_1 : Fin (n + 1)
i : Fin n
hij : i.castSucc < j_1
hj : ¬∃ (j₀ : Fin n), j₀.castSucc = j_1
j : Fin n
h_1 : Membership.mem (γ := Finset (Fin n)) univ j
hji : j ≠ i
⊢ (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (x j) : R[X]) (HPow.hPow (α := R[X]) X (k j))).coeff (k i) = 0
have neg : x j * (HPow.hPow (α := R[X]) X (k j)).coeff (k i) = 0
Tactic: rw [coeff_C_mul, coeff_X_pow, if_neg (hk.injective.ne hji.symm), mul_zero]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.EraseLead (goal)
Goal:
R : Type u_1
inst : Semiring R
n : ℕ
hn :
  ∀ {f : R[X]},
    #f.support = n →
      ∃ (k : Fin n → ℕ) (x : Fin n → R) (_ : StrictMono k) (_ : ∀ (i : Fin n), x i ≠ 0),
        f = ∑ i : Fin n, HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (x i) : R[X]) (HPow.hPow (α := R[X]) X (k i))
f : R[X]
h : #f.support = n + 1
k : Fin n → ℕ
x : Fin n → R
hk : StrictMono k
hx : ∀ (i : Fin n), x i ≠ 0
hf :
  f.eraseLead = ∑ i : Fin n, HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (x i) : R[X]) (HPow.hPow (α := R[X]) X (k i))
H : ¬∃ (k : Fin n), k.castSucc = Fin.last n
j_1 : Fin (n + 1)
i : Fin n
hij : i.castSucc < j_1
hj : ¬∃ (j₀ : Fin n), j₀.castSucc = j_1
j : Fin n
h_1 : Membership.mem (γ := Finset (Fin n)) univ j
hji : j ≠ i
neg : x j * (HPow.hPow (α := R[X]) X (k j)).coeff (k i) = 0
⊢ (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (x j) : R[X]) (HPow.hPow (α := R[X]) X (k j))).coeff (k i) = 0
have neg₁ : (x j * if k i = k j then 1 else 0) = 0
Tactic: rw [coeff_C_mul, coeff_X_pow, if_neg (hk.injective.ne hji.symm), mul_zero]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.EraseLead (goal)
Goal:
R : Type u_1
inst : Semiring R
n : ℕ
hn :
  ∀ {f : R[X]},
    #f.support = n →
      ∃ (k : Fin n → ℕ) (x : Fin n → R) (_ : StrictMono k) (_ : ∀ (i : Fin n), x i ≠ 0),
        f = ∑ i : Fin n, HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (x i) : R[X]) (HPow.hPow (α := R[X]) X (k i))
f : R[X]
h : #f.support = n + 1
k : Fin n → ℕ
x : Fin n → R
hk : StrictMono k
hx : ∀ (i : Fin n), x i ≠ 0
hf :
  f.eraseLead = ∑ i : Fin n, HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (x i) : R[X]) (HPow.hPow (α := R[X]) X (k i))
H : ¬∃ (k : Fin n), k.castSucc = Fin.last n
j_1 : Fin (n + 1)
i : Fin n
hij : i.castSucc < j_1
hj : ¬∃ (j₀ : Fin n), j₀.castSucc = j_1
j : Fin n
h_1 : Membership.mem (γ := Finset (Fin n)) univ j
hji : j ≠ i
neg : x j * (HPow.hPow (α := R[X]) X (k j)).coeff (k i) = 0
neg₁ : (x j * if k i = k j then 1 else 0) = 0
⊢ (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (x j) : R[X]) (HPow.hPow (α := R[X]) X (k j))).coeff (k i) = 0
have neg₂ : x j * 0 = 0
Tactic: rw [coeff_C_mul, coeff_X_pow, if_neg (hk.injective.ne hji.symm), mul_zero]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.EraseLead (goal)
Goal:
R : Type u_1
inst : Semiring R
n : ℕ
hn :
  ∀ {f : R[X]},
    #f.support = n →
      ∃ (k : Fin n → ℕ) (x : Fin n → R) (_ : StrictMono k) (_ : ∀ (i : Fin n), x i ≠ 0),
        f = ∑ i : Fin n, HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (x i) : R[X]) (HPow.hPow (α := R[X]) X (k i))
f : R[X]
h : #f.support = n + 1
k : Fin n → ℕ
x : Fin n → R
hk : StrictMono k
hx : ∀ (i : Fin n), x i ≠ 0
hf :
  f.eraseLead = ∑ i : Fin n, HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (x i) : R[X]) (HPow.hPow (α := R[X]) X (k i))
H : ¬∃ (k : Fin n), k.castSucc = Fin.last n
j_1 : Fin (n + 1)
i : Fin n
hij : i.castSucc < j_1
hj : ¬∃ (j₀ : Fin n), j₀.castSucc = j_1
j : Fin n
h_1 : Membership.mem (γ := Finset (Fin n)) univ j
hji : j ≠ i
neg : x j * (HPow.hPow (α := R[X]) X (k j)).coeff (k i) = 0
neg₁ : (x j * if k i = k j then 1 else 0) = 0
neg₂ : x j * 0 = 0
⊢ (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (x j) : R[X]) (HPow.hPow (α := R[X]) X (k j))).coeff (k i) = 0
have neg₃ : Eq.{u_1 + 1} (α := R) 0 0
Tactic: rw [coeff_C_mul, coeff_X_pow, if_neg (hk.injective.ne hji.symm), mul_zero]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.EraseLead (goal)
Goal:
R : Type u_1
inst : Semiring R
n : ℕ
hn :
  ∀ {f : R[X]},
    #f.support = n →
      ∃ (k : Fin n → ℕ) (x : Fin n → R) (_ : StrictMono k) (_ : ∀ (i : Fin n), x i ≠ 0),
        f = ∑ i : Fin n, HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (x i) : R[X]) (HPow.hPow (α := R[X]) X (k i))
f : R[X]
h : #f.support = n + 1
k : Fin n → ℕ
x : Fin n → R
hk : StrictMono k
hx : ∀ (i : Fin n), x i ≠ 0
hf :
  f.eraseLead = ∑ i : Fin n, HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (x i) : R[X]) (HPow.hPow (α := R[X]) X (k i))
H : ¬∃ (k : Fin n), k.castSucc = Fin.last n
i : Fin (n + 1)
⊢ Function.extend Fin.castSucc x (fun (x : Fin (n + 1)) ↦ f.leadingCoeff) i ≠ 0
have pos : ∀ (hi : ∃ (i₀ : Fin n), i₀.castSucc = i), Function.extend Fin.castSucc x (fun (x : Fin (n + 1)) ↦ f.leadingCoeff) i ≠ 0
Tactic: by_cases hi : ∃ i₀, Fin.castSucc i₀ = i
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.EraseLead (goal)
Goal:
R : Type u_1
inst : Semiring R
n : ℕ
hn :
  ∀ {f : R[X]},
    #f.support = n →
      ∃ (k : Fin n → ℕ) (x : Fin n → R) (_ : StrictMono k) (_ : ∀ (i : Fin n), x i ≠ 0),
        f = ∑ i : Fin n, HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (x i) : R[X]) (HPow.hPow (α := R[X]) X (k i))
f : R[X]
h : #f.support = n + 1
k : Fin n → ℕ
x : Fin n → R
hk : StrictMono k
hx : ∀ (i : Fin n), x i ≠ 0
hf :
  f.eraseLead = ∑ i : Fin n, HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (x i) : R[X]) (HPow.hPow (α := R[X]) X (k i))
H : ¬∃ (k : Fin n), k.castSucc = Fin.last n
i : Fin (n + 1)
pos :
  ∀ (hi : ∃ (i₀ : Fin n), i₀.castSucc = i),
    Function.extend Fin.castSucc x (fun (x : Fin (n + 1)) ↦ f.leadingCoeff) i ≠ 0
⊢ Function.extend Fin.castSucc x (fun (x : Fin (n + 1)) ↦ f.leadingCoeff) i ≠ 0
have neg : ∀ (hi : ¬∃ (i₀ : Fin n), i₀.castSucc = i), Function.extend Fin.castSucc x (fun (x : Fin (n + 1)) ↦ f.leadingCoeff) i ≠ 0
Tactic: by_cases hi : ∃ i₀, Fin.castSucc i₀ = i
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.EraseLead (goal)
Goal:
R : Type u_1
inst : Semiring R
n : ℕ
hn :
  ∀ {f : R[X]},
    #f.support = n →
      ∃ (k : Fin n → ℕ) (x : Fin n → R) (_ : StrictMono k) (_ : ∀ (i : Fin n), x i ≠ 0),
        f = ∑ i : Fin n, HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (x i) : R[X]) (HPow.hPow (α := R[X]) X (k i))
f : R[X]
h : #f.support = n + 1
k : Fin n → ℕ
x : Fin n → R
hk : StrictMono k
hx : ∀ (i : Fin n), x i ≠ 0
hf :
  f.eraseLead = ∑ i : Fin n, HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (x i) : R[X]) (HPow.hPow (α := R[X]) X (k i))
H : ¬∃ (k : Fin n), k.castSucc = Fin.last n
i : Fin (n + 1)
hi : ∃ (i₀ : Fin n), i₀.castSucc = i
⊢ Function.extend Fin.castSucc x (fun (x : Fin (n + 1)) ↦ f.leadingCoeff) i ≠ 0
have pos : ∀ (i : Fin n), Function.extend Fin.castSucc x (fun (x : Fin (n + 1)) ↦ f.leadingCoeff) i.castSucc ≠ 0
Tactic: obtain ⟨i, rfl⟩ := hi
Cleared hypotheses: i, hi
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.EraseLead (goal)
Goal:
R : Type u_1
inst : Semiring R
n : ℕ
hn :
  ∀ {f : R[X]},
    #f.support = n →
      ∃ (k : Fin n → ℕ) (x : Fin n → R) (_ : StrictMono k) (_ : ∀ (i : Fin n), x i ≠ 0),
        f = ∑ i : Fin n, HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (x i) : R[X]) (HPow.hPow (α := R[X]) X (k i))
f : R[X]
h : #f.support = n + 1
k : Fin n → ℕ
x : Fin n → R
hk : StrictMono k
hx : ∀ (i : Fin n), x i ≠ 0
hf :
  f.eraseLead = ∑ i : Fin n, HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (x i) : R[X]) (HPow.hPow (α := R[X]) X (k i))
H : ¬∃ (k : Fin n), k.castSucc = Fin.last n
i : Fin n
⊢ Function.extend Fin.castSucc x (fun (x : Fin (n + 1)) ↦ f.leadingCoeff) i.castSucc ≠ 0
have pos : x i ≠ 0
Tactic: rw [Fin.strictMono_castSucc.injective.extend_apply]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.EraseLead (goal)
Goal:
R : Type u_1
inst : Semiring R
n : ℕ
hn :
  ∀ {f : R[X]},
    #f.support = n →
      ∃ (k : Fin n → ℕ) (x : Fin n → R) (_ : StrictMono k) (_ : ∀ (i : Fin n), x i ≠ 0),
        f = ∑ i : Fin n, HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (x i) : R[X]) (HPow.hPow (α := R[X]) X (k i))
f : R[X]
h : #f.support = n + 1
k : Fin n → ℕ
x : Fin n → R
hk : StrictMono k
hx : ∀ (i : Fin n), x i ≠ 0
hf :
  f.eraseLead = ∑ i : Fin n, HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (x i) : R[X]) (HPow.hPow (α := R[X]) X (k i))
H : ¬∃ (k : Fin n), k.castSucc = Fin.last n
i : Fin (n + 1)
hi : ¬∃ (i₀ : Fin n), i₀.castSucc = i
⊢ Function.extend Fin.castSucc x (fun (x : Fin (n + 1)) ↦ f.leadingCoeff) i ≠ 0
have neg : ¬n + 1 = 0
Tactic: rw [Function.extend_apply' _ _ _ hi, Ne, leadingCoeff_eq_zero, ← card_support_eq_zero, h]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.EraseLead (goal)
Goal:
R : Type u_1
inst : Semiring R
n : ℕ
hn :
  ∀ {f : R[X]},
    #f.support = n →
      ∃ (k : Fin n → ℕ) (x : Fin n → R) (_ : StrictMono k) (_ : ∀ (i : Fin n), x i ≠ 0),
        f = ∑ i : Fin n, HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (x i) : R[X]) (HPow.hPow (α := R[X]) X (k i))
f : R[X]
h : #f.support = n + 1
k : Fin n → ℕ
x : Fin n → R
hk : StrictMono k
hx : ∀ (i : Fin n), x i ≠ 0
hf :
  f.eraseLead = ∑ i : Fin n, HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (x i) : R[X]) (HPow.hPow (α := R[X]) X (k i))
H : ¬∃ (k : Fin n), k.castSucc = Fin.last n
⊢ f =
    ∑ i : Fin (n + 1),
      HMul.hMul (α := R[X])
        ((C : (a : R) → R[X]) (Function.extend Fin.castSucc x (fun (x : Fin (n + 1)) ↦ f.leadingCoeff) i) : R[X])
        (HPow.hPow (α := R[X]) X (Function.extend Fin.castSucc k (fun (x : Fin (n + 1)) ↦ f.natDegree) i))
have succ : f =
  ∑ i : Fin n,
      HMul.hMul (α := R[X])
        ((C : (a : R) → R[X]) (Function.extend Fin.castSucc x (fun (x : Fin (n + 1)) ↦ f.leadingCoeff) i.castSucc) :
          R[X])
        (HPow.hPow (α := R[X]) X (Function.extend Fin.castSucc k (fun (x : Fin (n + 1)) ↦ f.natDegree) i.castSucc)) +
    HMul.hMul (α := R[X])
      ((C : (a : R) → R[X]) (Function.extend Fin.castSucc x (fun (x : Fin (n + 1)) ↦ f.leadingCoeff) (Fin.last n)) :
        R[X])
      (HPow.hPow (α := R[X]) X (Function.extend Fin.castSucc k (fun (x : Fin (n + 1)) ↦ f.natDegree) (Fin.last n)))
Tactic: rw [Fin.sum_univ_castSucc]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.EraseLead (goal)
Goal:
R : Type u_1
inst : Semiring R
n : ℕ
hn :
  ∀ {f : R[X]},
    #f.support = n →
      ∃ (k : Fin n → ℕ) (x : Fin n → R) (_ : StrictMono k) (_ : ∀ (i : Fin n), x i ≠ 0),
        f = ∑ i : Fin n, HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (x i) : R[X]) (HPow.hPow (α := R[X]) X (k i))
f : R[X]
h : #f.support = n + 1
k : Fin n → ℕ
x : Fin n → R
hk : StrictMono k
hx : ∀ (i : Fin n), x i ≠ 0
hf :
  f.eraseLead = ∑ i : Fin n, HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (x i) : R[X]) (HPow.hPow (α := R[X]) X (k i))
H : ¬∃ (k : Fin n), k.castSucc = Fin.last n
⊢ f =
    ∑ i : Fin n,
        HMul.hMul (α := R[X])
          ((C : (a : R) → R[X]) (Function.extend Fin.castSucc x (fun (x : Fin (n + 1)) ↦ f.leadingCoeff) i.castSucc) :
            R[X])
          (HPow.hPow (α := R[X]) X (Function.extend Fin.castSucc k (fun (x : Fin (n + 1)) ↦ f.natDegree) i.castSucc)) +
      HMul.hMul (α := R[X])
        ((C : (a : R) → R[X]) (Function.extend Fin.castSucc x (fun (x : Fin (n + 1)) ↦ f.leadingCoeff) (Fin.last n)) :
          R[X])
        (HPow.hPow (α := R[X]) X (Function.extend Fin.castSucc k (fun (x : Fin (n + 1)) ↦ f.natDegree) (Fin.last n)))
have succ : f =
  ∑ x_1 : Fin n, HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (x x_1) : R[X]) (HPow.hPow (α := R[X]) X (k x_1)) +
    HMul.hMul (α := R[X])
      ((C : (a : R) → R[X]) (Function.extend Fin.castSucc x (fun (x : Fin (n + 1)) ↦ f.leadingCoeff) (Fin.last n)) :
        R[X])
      (HPow.hPow (α := R[X]) X (Function.extend Fin.castSucc k (fun (x : Fin (n + 1)) ↦ f.natDegree) (Fin.last n)))
Tactic: simp only [Fin.strictMono_castSucc.injective.extend_apply]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.EraseLead (goal)
Goal:
R : Type u_1
inst : Semiring R
f : R[X]
n : ℕ
⊢ #f.support = n →
    ∃ (k : Fin n → ℕ) (x : Fin n → R) (_ : StrictMono k) (_ : ∀ (i : Fin n), x i ≠ 0),
      f = ∑ i : Fin n, HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (x i) : R[X]) (HPow.hPow (α := R[X]) X (k i))
have zero : ∀ {f : R[X]},
  #f.support = 0 →
    ∃ (k : Fin 0 → ℕ) (x : Fin 0 → R) (_ : StrictMono k) (_ : ∀ (i : Fin 0), x i ≠ 0),
      f = ∑ i : Fin 0, HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (x i) : R[X]) (HPow.hPow (α := R[X]) X (k i))
Tactic: induction n generalizing f with
  | zero => exact fun hf => ⟨0, 0, fun x => x.elim0, fun x => x.elim0, card_support_eq_zero.mp hf⟩
  | succ n hn =>
    intro h
    obtain ⟨k, x, hk, hx, hf⟩ := hn (card_support_eraseLead' h)
    have H : ¬∃ k : Fin n, Fin.castSucc k = Fin.last n := by
      rintro ⟨i, hi⟩
      exact i.castSucc_lt_last.ne hi
    refine
      ⟨Function.extend Fin.castSucc k fun _ => f.natDegree,
        Function.extend Fin.castSucc x fun _ => f.leadingCoeff, ?_, ?_, ?_⟩
    · intro i j hij
      have hi : i ∈ Set.range (Fin.castSucc : Fin n → Fin (n + 1)) := by
        simp only [Fin.range_castSucc, Nat.succ_eq_add_one, Set.mem_setOf_eq]
        exact lt_of_lt_of_le hij (Nat.lt_succ_iff.mp j.2)
      obtain ⟨i, rfl⟩ := hi
      rw [Fin.strictMono_castSucc.injective.extend_apply]
      by_cases hj : ∃ j₀, Fin.castSucc j₀ = j
      · obtain ⟨j, rfl⟩ := hj
        rwa [Fin.strictMono_castSucc.injective.extend_apply, hk.lt_iff_lt,
          ← Fin.castSucc_lt_castSucc_iff]
      · rw [Function.extend_apply' _ _ _ hj]
        apply lt_natDegree_of_mem_eraseLead_support
        rw [mem_support_iff, hf, finsetSum_coeff]
        rw [sum_eq_single, coeff_C_mul, coeff_X_pow_self, mul_one]
        · exact hx i
        · intro j _ hji
          rw [coeff_C_mul, coeff_X_pow, if_neg (hk.injective.ne hji.symm), mul_zero]
        · exact fun hi => (hi (mem_univ i)).elim
    · intro i
      by_cases hi : ∃ i₀, Fin.castSucc i₀ = i
      · obtain ⟨i, rfl⟩ := hi
        rw [Fin.strictMono_castSucc.injective.extend_apply]
        exact hx i
      · rw [Function.extend_apply' _ _ _ hi, Ne, leadingCoeff_eq_zero, ← card_support_eq_zero, h]
        exact n.succ_ne_zero
    · rw [Fin.sum_univ_castSucc]
      simp only [Fin.strictMono_castSucc.injective.extend_apply]
      rw [← hf, Function.extend_apply', Function.extend_apply', eraseLead_add_C_mul_X_pow]
      all_goals exact H
Cleared hypotheses: f, n
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.EraseLead (goal)
Goal:
R : Type u_1
inst : Semiring R
f : R[X]
n : ℕ
zero :
  ∀ {f : R[X]},
    #f.support = 0 →
      ∃ (k : Fin 0 → ℕ) (x : Fin 0 → R) (_ : StrictMono k) (_ : ∀ (i : Fin 0), x i ≠ 0),
        f = ∑ i : Fin 0, HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (x i) : R[X]) (HPow.hPow (α := R[X]) X (k i))
⊢ #f.support = n →
    ∃ (k : Fin n → ℕ) (x : Fin n → R) (_ : StrictMono k) (_ : ∀ (i : Fin n), x i ≠ 0),
      f = ∑ i : Fin n, HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (x i) : R[X]) (HPow.hPow (α := R[X]) X (k i))
have succ : ∀ (n : ℕ)
  (hn :
    ∀ {f : R[X]},
      #f.support = n →
        ∃ (k : Fin n → ℕ) (x : Fin n → R) (_ : StrictMono k) (_ : ∀ (i : Fin n), x i ≠ 0),
          f = ∑ i : Fin n, HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (x i) : R[X]) (HPow.hPow (α := R[X]) X (k i)))
  {f : R[X]},
  #f.support = n + 1 →
    ∃ (k : Fin (n + 1) → ℕ) (x : Fin (n + 1) → R) (_ : StrictMono k) (_ : ∀ (i : Fin (n + 1)), x i ≠ 0),
      f = ∑ i : Fin (n + 1), HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (x i) : R[X]) (HPow.hPow (α := R[X]) X (k i))
Tactic: induction n generalizing f with
  | zero => exact fun hf => ⟨0, 0, fun x => x.elim0, fun x => x.elim0, card_support_eq_zero.mp hf⟩
  | succ n hn =>
    intro h
    obtain ⟨k, x, hk, hx, hf⟩ := hn (card_support_eraseLead' h)
    have H : ¬∃ k : Fin n, Fin.castSucc k = Fin.last n := by
      rintro ⟨i, hi⟩
      exact i.castSucc_lt_last.ne hi
    refine
      ⟨Function.extend Fin.castSucc k fun _ => f.natDegree,
        Function.extend Fin.castSucc x fun _ => f.leadingCoeff, ?_, ?_, ?_⟩
    · intro i j hij
      have hi : i ∈ Set.range (Fin.castSucc : Fin n → Fin (n + 1)) := by
        simp only [Fin.range_castSucc, Nat.succ_eq_add_one, Set.mem_setOf_eq]
        exact lt_of_lt_of_le hij (Nat.lt_succ_iff.mp j.2)
      obtain ⟨i, rfl⟩ := hi
      rw [Fin.strictMono_castSucc.injective.extend_apply]
      by_cases hj : ∃ j₀, Fin.castSucc j₀ = j
      · obtain ⟨j, rfl⟩ := hj
        rwa [Fin.strictMono_castSucc.injective.extend_apply, hk.lt_iff_lt,
          ← Fin.castSucc_lt_castSucc_iff]
      · rw [Function.extend_apply' _ _ _ hj]
        apply lt_natDegree_of_mem_eraseLead_support
        rw [mem_support_iff, hf, finsetSum_coeff]
        rw [sum_eq_single, coeff_C_mul, coeff_X_pow_self, mul_one]
        · exact hx i
        · intro j _ hji
          rw [coeff_C_mul, coeff_X_pow, if_neg (hk.injective.ne hji.symm), mul_zero]
        · exact fun hi => (hi (mem_univ i)).elim
    · intro i
      by_cases hi : ∃ i₀, Fin.castSucc i₀ = i
      · obtain ⟨i, rfl⟩ := hi
        rw [Fin.strictMono_castSucc.injective.extend_apply]
        exact hx i
      · rw [Function.extend_apply' _ _ _ hi, Ne, leadingCoeff_eq_zero, ← card_support_eq_zero, h]
        exact n.succ_ne_zero
    · rw [Fin.sum_univ_castSucc]
      simp only [Fin.strictMono_castSucc.injective.extend_apply]
      rw [← hf, Function.extend_apply', Function.extend_apply', eraseLead_add_C_mul_X_pow]
      all_goals exact H
Cleared hypotheses: f, n
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.EraseLead (goal)
Goal:
R : Type u_1
inst : Semiring R
f : R[X]
⊢ #f.support = 1 ↔
    ∃ (k : ℕ) (x : R) (_ : x ≠ 0), f = HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) x : R[X]) (HPow.hPow (α := R[X]) X k)
have refine_1 : ∀ (h : #f.support = 1),
  ∃ (k : ℕ) (x : R) (_ : x ≠ 0), f = HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) x : R[X]) (HPow.hPow (α := R[X]) X k)
Tactic: refine ⟨fun h => ?_, ?_⟩