awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Polynomial.EraseLead
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
pos :
  ∀ (j : Fin n) (hij : i.castSucc < j.castSucc),
    k i < Function.extend Fin.castSucc k (fun (x : Fin (n + 1)) ↦ f.natDegree) j.castSucc
⊢ k i < Function.extend Fin.castSucc k (fun (x : Fin (n + 1)) ↦ f.natDegree) j

Tactic:
obtain ⟨j, rfl⟩ := hj

Premises used: rfl
-- Module: Mathlib.Algebra.Polynomial.EraseLead
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 j : Fin n
hij : i.castSucc < j.castSucc
pos : k i < k j
pos₁ : i < j
pos₂ pos₃ pos₄ pos₅ : i.castSucc < j.castSucc
⊢ k i < Function.extend Fin.castSucc k (fun (x : Fin (n + 1)) ↦ f.natDegree) j.castSucc

Tactic:
rwa [Fin.strictMono_castSucc.injective.extend_apply, hk.lt_iff_lt,
          ← Fin.castSucc_lt_castSucc_iff]

Premises used: Fin.castSucc_lt_castSucc_iff, StrictMono.lt_iff_lt, Function.Injective.extend_apply, StrictMono.injective, Fin.strictMono_castSucc
-- Module: Mathlib.Algebra.Polynomial.EraseLead
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 : k i < f.natDegree
⊢ k i < Function.extend Fin.castSucc k (fun (x : Fin (n + 1)) ↦ f.natDegree) j

Tactic:
rw [Function.extend_apply' _ _ _ hj]

Premises used: Function.extend_apply'
-- Module: Mathlib.Algebra.Polynomial.EraseLead
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 : k i ∈ f.eraseLead.support
⊢ k i < f.natDegree

Tactic:
apply lt_natDegree_of_mem_eraseLead_support

Premises used: Polynomial.lt_natDegree_of_mem_eraseLead_support
-- Module: Mathlib.Algebra.Polynomial.EraseLead
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 :
  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
⊢ k i ∈ f.eraseLead.support

Tactic:
rw [mem_support_iff, hf, finsetSum_coeff]

Premises used: Polynomial.mem_support_iff, Polynomial.finsetSum_coeff
-- Module: Mathlib.Algebra.Polynomial.EraseLead
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
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
⊢ 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 [sum_eq_single, coeff_C_mul, coeff_X_pow_self, mul_one]

Premises used: Polynomial.coeff_C_mul, Finset.sum_eq_single, Polynomial.coeff_X_pow_self, mul_one
-- Module: Mathlib.Algebra.Polynomial.EraseLead
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
⊢ x i ≠ 0

Tactic:
hx i
-- Module: Mathlib.Algebra.Polynomial.EraseLead
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
⊢ x i ≠ 0

Tactic:
exact hx i
-- Module: Mathlib.Algebra.Polynomial.EraseLead
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
neg :
  Membership.mem (γ := Finset (Fin n)) univ j →
    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
⊢ Membership.mem (γ := Finset (Fin n)) univ j →
    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

Tactic:
_
-- Module: Mathlib.Algebra.Polynomial.EraseLead
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
neg₃ neg₄ : Eq.{u_1 + 1} (α := R) 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

Tactic:
rw [coeff_C_mul, coeff_X_pow, if_neg (hk.injective.ne hji.symm), mul_zero]

Premises used: Polynomial.coeff_X_pow, Function.Injective.ne, Polynomial.coeff_C_mul, Ne.symm, MulZeroClass.mul_zero, StrictMono.injective, if_neg
-- Module: Mathlib.Algebra.Polynomial.EraseLead
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
⊢ 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:
fun hi => (hi (mem_univ i)).elim

Premises used: Finset.mem_univ, False.elim
-- Module: Mathlib.Algebra.Polynomial.EraseLead
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
⊢ 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:
exact fun hi => (hi (mem_univ i)).elim
-- Module: Mathlib.Algebra.Polynomial.EraseLead
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
neg :
  ∀ (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

Tactic:
by_cases hi : ∃ i₀, Fin.castSucc i₀ = i
-- Module: Mathlib.Algebra.Polynomial.EraseLead
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
pos : ∀ (i : Fin n), Function.extend Fin.castSucc x (fun (x : Fin (n + 1)) ↦ f.leadingCoeff) i.castSucc ≠ 0
⊢ Function.extend Fin.castSucc x (fun (x : Fin (n + 1)) ↦ f.leadingCoeff) i ≠ 0

Tactic:
obtain ⟨i, rfl⟩ := hi

Premises used: rfl
-- Module: Mathlib.Algebra.Polynomial.EraseLead
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
pos : x i ≠ 0
⊢ Function.extend Fin.castSucc x (fun (x : Fin (n + 1)) ↦ f.leadingCoeff) i.castSucc ≠ 0

Tactic:
rw [Fin.strictMono_castSucc.injective.extend_apply]

Premises used: Function.Injective.extend_apply, StrictMono.injective, Fin.strictMono_castSucc
-- Module: Mathlib.Algebra.Polynomial.EraseLead
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
⊢ x i ≠ 0

Tactic:
hx i
-- Module: Mathlib.Algebra.Polynomial.EraseLead
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
⊢ x i ≠ 0

Tactic:
exact hx i
-- Module: Mathlib.Algebra.Polynomial.EraseLead
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
neg : ¬n + 1 = 0
⊢ Function.extend Fin.castSucc x (fun (x : Fin (n + 1)) ↦ f.leadingCoeff) i ≠ 0

Tactic:
rw [Function.extend_apply' _ _ _ hi, Ne, leadingCoeff_eq_zero, ← card_support_eq_zero, h]

Premises used: Ne, Polynomial.card_support_eq_zero, Function.extend_apply', Polynomial.leadingCoeff_eq_zero
-- Module: Mathlib.Algebra.Polynomial.EraseLead
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
⊢ ¬n + 1 = 0

Tactic:
n.succ_ne_zero

Premises used: Nat.succ_ne_zero
-- Module: Mathlib.Algebra.Polynomial.EraseLead
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
⊢ ¬n + 1 = 0

Tactic:
exact n.succ_ne_zero

Premises used: Nat.succ_ne_zero
-- Module: Mathlib.Algebra.Polynomial.EraseLead
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
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)))
⊢ 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))

Tactic:
rw [Fin.sum_univ_castSucc]

Premises used: Fin.sum_univ_castSucc
-- Module: Mathlib.Algebra.Polynomial.EraseLead
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
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)))
⊢ 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:
simp only [Fin.strictMono_castSucc.injective.extend_apply]

Premises used: Function.Injective.extend_apply, StrictMono.injective, Fin.strictMono_castSucc
-- Module: Mathlib.Algebra.Polynomial.EraseLead
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 succ succ₁ : ¬∃ (a : Fin n), a.castSucc = Fin.last n
⊢ 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:
rw [← hf, Function.extend_apply', Function.extend_apply', eraseLead_add_C_mul_X_pow]

Premises used: Polynomial.eraseLead_add_C_mul_X_pow, Function.extend_apply'
-- Module: Mathlib.Algebra.Polynomial.EraseLead
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
⊢ ¬∃ (a : Fin n), a.castSucc = Fin.last n

Tactic:
H
-- Module: Mathlib.Algebra.Polynomial.EraseLead
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
⊢ ¬∃ (a : Fin n), a.castSucc = Fin.last n

Tactic:
exact H
-- Module: Mathlib.Algebra.Polynomial.EraseLead
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)

Tactic:
⟨fun h => ?_, ?_⟩

Premises used: Iff.intro