awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Polynomial.EraseLead
Goal:
R : Type u_1
inst : Semiring R
S : Type u_2
F : Type u_3
inst_1 : Semiring S
inst_2 : FunLike.{u_3 + 1, u_1 + 1, u_2 + 1} F R[X] S[X]
inst_3 : AddMonoidHomClass.{u_3, u_1, u_2} F R[X] S[X]
φ : F
p : R[X]
fu : ℕ → ℕ
φ_mon_nat :
  ∀ (n : ℕ) (c : R), c ≠ 0 → natDegree.{u_2} (R := S) ((φ : (a : R[X]) → S[X]) ((monomial n : (a : R) → R[X]) c)) = fu n
f g : R[X]
fg : f.natDegree < g.natDegree
h : g.natDegree ≤ p.natDegree
fk : natDegree.{u_2} (R := S) ((φ : (a : R[X]) → S[X]) f) = fu f.natDegree
gk : natDegree.{u_2} (R := S) ((φ : (a : R[X]) → S[X]) g) = fu g.natDegree
fu0 : ∀ {n : ℕ}, n ≤ 0 → fu n = 0
fc : ∀ {n m : ℕ}, 0 ≤ n → n < m → fu n < fu m
φ_k : ∀ {f : R[X]}, f.natDegree < 0 → Eq.{u_2 + 1} (α := S[X]) ((φ : (a : R[X]) → S[X]) f : S[X]) (0 : S[X])
FG : f.natDegree < 0
⊢ (HAdd.hAdd (α := S[X]) (β := S[X]) ((φ : (a : R[X]) → S[X]) f : S[X]) ((φ : (a : R[X]) → S[X]) g : S[X])).natDegree =
    fu g.natDegree

Tactic:
nomatch FG
-- Module: Mathlib.Algebra.Polynomial.EraseLead
Goal:
R : Type u_1
inst : Semiring R
S : Type u_2
F : Type u_3
inst_1 : Semiring S
inst_2 : FunLike.{u_3 + 1, u_1 + 1, u_2 + 1} F R[X] S[X]
inst_3 : AddMonoidHomClass.{u_3, u_1, u_2} F R[X] S[X]
φ : F
p : R[X]
fu : ℕ → ℕ
φ_mon_nat :
  ∀ (n : ℕ) (c : R), c ≠ 0 → natDegree.{u_2} (R := S) ((φ : (a : R[X]) → S[X]) ((monomial n : (a : R) → R[X]) c)) = fu n
f g : R[X]
fg : f.natDegree < g.natDegree
h : g.natDegree ≤ p.natDegree
fk : natDegree.{u_2} (R := S) ((φ : (a : R[X]) → S[X]) f) = fu f.natDegree
gk : natDegree.{u_2} (R := S) ((φ : (a : R[X]) → S[X]) g) = fu g.natDegree
n : ℕ
fu0 : ∀ {n_1 : ℕ}, n_1 ≤ n + 1 → fu n_1 = 0
fc : ∀ {n_1 m : ℕ}, n + 1 ≤ n_1 → n_1 < m → fu n_1 < fu m
φ_k : ∀ {f : R[X]}, f.natDegree < n + 1 → Eq.{u_2 + 1} (α := S[X]) ((φ : (a : R[X]) → S[X]) f : S[X]) (0 : S[X])
FG : f.natDegree < n + 1
neg : (HAdd.hAdd (α := S[X]) (β := S[X]) (0 : S[X]) ((φ : (a : R[X]) → S[X]) g : S[X])).natDegree = fu g.natDegree
neg₁ neg₂ neg₃ neg₄ : natDegree.{u_2} (R := S) ((φ : (a : R[X]) → S[X]) g) = fu g.natDegree
⊢ (HAdd.hAdd (α := S[X]) (β := S[X]) ((φ : (a : R[X]) → S[X]) f : S[X]) ((φ : (a : R[X]) → S[X]) g : S[X])).natDegree =
    fu g.natDegree

Tactic:
rwa [φ_k FG, zero_add]

Premises used: zero_add
-- Module: Mathlib.Algebra.Polynomial.EraseLead
Goal:
R : Type u_1
inst : Semiring R
S : Type u_2
F : Type u_3
inst_1 : Semiring S
inst_2 : FunLike.{u_3 + 1, u_1 + 1, u_2 + 1} F R[X] S[X]
inst_3 : AddMonoidHomClass.{u_3, u_1, u_2} F R[X] S[X]
φ : F
p : R[X]
k : ℕ
φ_k : ∀ (f : R[X]), f.natDegree < k → Eq.{u_2 + 1} (α := S[X]) ((φ : (a : R[X]) → S[X]) f : S[X]) (0 : S[X])
φ_mon :
  ∀ (n : ℕ) (c : R),
    c ≠ 0 → natDegree.{u_2} (R := S) ((φ : (a : R[X]) → S[X]) ((monomial n : (a : R) → R[X]) c)) = n - k
⊢ ∀ {n : ℕ}, n ≤ k → Eq (α := ℕ) ((fun (j : ℕ) ↦ j - k) n) 0

Tactic:
simp_all
-- Module: Mathlib.Algebra.Polynomial.EraseLead
Goal:
R : Type u_1
inst : Semiring R
S : Type u_2
F : Type u_3
inst_1 : Semiring S
inst_2 : FunLike.{u_3 + 1, u_1 + 1, u_2 + 1} F R[X] S[X]
inst_3 : AddMonoidHomClass.{u_3, u_1, u_2} F R[X] S[X]
φ : F
p : R[X]
φ_mon_nat :
  ∀ (n : ℕ) (c : R), c ≠ 0 → natDegree.{u_2} (R := S) ((φ : (a : R[X]) → S[X]) ((monomial n : (a : R) → R[X]) c)) = n
⊢ ∀ (n : ℕ) (c : R),
    c ≠ 0 → natDegree.{u_2} (R := S) ((φ : (a : R[X]) → S[X]) ((monomial n : (a : R) → R[X]) c)) = n - 0

Tactic:
simpa
-- Module: Mathlib.Algebra.Polynomial.EraseLead
Goal:
R : Type u_1
inst : Semiring R
n : ℕ
k : Fin n → ℕ
x : Fin n → R
hk : Function.Injective k
hx : ∀ (i : Fin n), x i ≠ 0
this :
  support.{u_1} (R := R)
      (∑ i : Fin n, HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (x i) : R[X]) (HPow.hPow (α := R[X]) X (k i))) =
    image k univ
rw : #(image k univ) = n
rw₁ : card (α := Fin n) univ = n
rw₂ rw₃ : n = n
⊢ #(support.{u_1} (R := R)
        (∑ i : Fin n, HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (x i) : R[X]) (HPow.hPow (α := R[X]) X (k i)))) =
    n

Tactic:
rw [this, univ.card_image_of_injective hk, card_fin]

Premises used: Finset.univ, Finset.card_image_of_injective, Finset.card_fin
-- Module: Mathlib.Algebra.Polynomial.EraseLead
Goal:
R : Type u_1
inst : Semiring R
n : ℕ
k : Fin n → ℕ
x : Fin n → R
hk : Function.Injective k
hx : ∀ (i : Fin n), x i ≠ 0
suffices :
  support.{u_1} (R := R)
      (∑ i : Fin n, HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (x i) : R[X]) (HPow.hPow (α := R[X]) X (k i))) =
    image k univ
⊢ #(support.{u_1} (R := R)
        (∑ i : Fin n, HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (x i) : R[X]) (HPow.hPow (α := R[X]) X (k i)))) =
    n

Tactic:
suffices (∑ i, C (x i) * X ^ k i).support = image k univ by
    rw [this, univ.card_image_of_injective hk, card_fin]
-- Module: Mathlib.Algebra.Polynomial.EraseLead
Goal:
R : Type u_1
inst : Semiring R
n : ℕ
k : Fin n → ℕ
x : Fin n → R
hk : Function.Injective k
hx : ∀ (i : Fin n), x i ≠ 0
simp_rw :
  ∀ (a : ℕ), Ne.{u_1 + 1} (α := R) (∑ x_1 : Fin n, if a = k x_1 then x x_1 else 0) 0 ↔ ∃ (a_1 : Fin n), k a_1 = a
⊢ support.{u_1} (R := R)
      (∑ i : Fin n, HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (x i) : R[X]) (HPow.hPow (α := R[X]) X (k i))) =
    image k univ

Tactic:
simp_rw [Finset.ext_iff, mem_support_iff, finsetSum_coeff, coeff_C_mul_X_pow, mem_image,
    mem_univ, true_and]

Premises used: Finset.mem_univ, Finset.mem_image, Polynomial.mem_support_iff, Polynomial.finsetSum_coeff, Finset.ext_iff, Polynomial.coeff_C_mul_X_pow, true_and
-- Module: Mathlib.Algebra.Polynomial.EraseLead
Goal:
R : Type u_1
inst : Semiring R
n : ℕ
k : Fin n → ℕ
x : Fin n → R
hk : Function.Injective k
hx : ∀ (i : Fin n), x i ≠ 0
⊢ ∀ (a : ℕ), Ne.{u_1 + 1} (α := R) (∑ x_1 : Fin n, if a = k x_1 then x x_1 else 0) 0 ↔ ∃ (a_1 : Fin n), k a_1 = a

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

Premises used: Iff.intro
-- Module: Mathlib.Algebra.Polynomial.EraseLead
Goal:
R : Type u_1
inst : Semiring R
n : ℕ
k : Fin n → ℕ
x : Fin n → R
hk : Function.Injective k
hx : ∀ (i : Fin n), x i ≠ 0
refine_1 :
  ∀ (i : ℕ) (h : Ne.{u_1 + 1} (α := R) (∑ x_1 : Fin n, if i = k x_1 then x x_1 else 0) 0), ∃ (a : Fin n), k a = i
refine_2 : ∀ (i : ℕ), (∃ (a : Fin n), k a = i) → Ne.{u_1 + 1} (α := R) (∑ x_1 : Fin n, if i = k x_1 then x x_1 else 0) 0
⊢ ∀ (a : ℕ), Ne.{u_1 + 1} (α := R) (∑ x_1 : Fin n, if a = k x_1 then x x_1 else 0) 0 ↔ ∃ (a_1 : Fin n), k a_1 = a

Tactic:
refine fun i => ⟨fun h => ?_, ?_⟩
-- Module: Mathlib.Algebra.Polynomial.EraseLead
Goal:
R : Type u_1
inst : Semiring R
n : ℕ
k : Fin n → ℕ
x : Fin n → R
hk : Function.Injective k
hx : ∀ (i : Fin n), x i ≠ 0
i : ℕ
h : Ne.{u_1 + 1} (α := R) (∑ x_1 : Fin n, if i = k x_1 then x x_1 else 0) 0
refine_1 :
  ∀ (j : Fin n),
    Membership.mem (γ := Finset (Fin n)) univ j → ∀ (h : (if i = k j then x j else 0) ≠ 0), ∃ (a : Fin n), k a = i
⊢ ∃ (a : Fin n), k a = i

Tactic:
obtain ⟨j, _, h⟩ := exists_ne_zero_of_sum_ne_zero h

Premises used: Finset.exists_ne_zero_of_sum_ne_zero
-- Module: Mathlib.Algebra.Polynomial.EraseLead
Goal:
R : Type u_1
inst : Semiring R
n : ℕ
k : Fin n → ℕ
x : Fin n → R
hk : Function.Injective k
hx : ∀ (i : Fin n), x i ≠ 0
i : ℕ
h_1 : Ne.{u_1 + 1} (α := R) (∑ x_1 : Fin n, if i = k x_1 then x x_1 else 0) 0
j : Fin n
left : Membership.mem (γ := Finset (Fin n)) univ j
h : (if i = k j then x j else 0) ≠ 0
⊢ ∃ (a : Fin n), k a = i

Tactic:
⟨j, (ite_ne_right_iff.mp h).1.symm⟩

Premises used: And.left, Exists.intro, Iff.mp, ite_ne_right_iff, Eq.symm
-- Module: Mathlib.Algebra.Polynomial.EraseLead
Goal:
R : Type u_1
inst : Semiring R
n : ℕ
k : Fin n → ℕ
x : Fin n → R
hk : Function.Injective k
hx : ∀ (i : Fin n), x i ≠ 0
i : ℕ
h_1 : Ne.{u_1 + 1} (α := R) (∑ x_1 : Fin n, if i = k x_1 then x x_1 else 0) 0
j : Fin n
left : Membership.mem (γ := Finset (Fin n)) univ j
h : (if i = k j then x j else 0) ≠ 0
⊢ ∃ (a : Fin n), k a = i

Tactic:
exact ⟨j, (ite_ne_right_iff.mp h).1.symm⟩
-- Module: Mathlib.Algebra.Polynomial.EraseLead
Goal:
R : Type u_1
inst : Semiring R
n : ℕ
k : Fin n → ℕ
x : Fin n → R
hk : Function.Injective k
hx : ∀ (i : Fin n), x i ≠ 0
j : Fin n
refine_2 : x j ≠ 0
refine_2₁ : ∀ (b : Fin n), Membership.mem (γ := Finset (Fin n)) univ b → b ≠ j → (if k j = k b then x b else 0) = 0
⊢ Ne.{u_1 + 1} (α := R) (∑ x_1 : Fin n, if k j = k x_1 then x x_1 else 0) 0

Tactic:
rw [sum_eq_single_of_mem j (mem_univ j), if_pos rfl]

Premises used: Finset.mem_univ, Finset.sum_eq_single_of_mem, if_pos, rfl
-- Module: Mathlib.Algebra.Polynomial.EraseLead
Goal:
R : Type u_1
inst : Semiring R
n : ℕ
k : Fin n → ℕ
x : Fin n → R
hk : Function.Injective k
hx : ∀ (i : Fin n), x i ≠ 0
j : Fin n
⊢ x j ≠ 0

Tactic:
hx j
-- Module: Mathlib.Algebra.Polynomial.EraseLead
Goal:
R : Type u_1
inst : Semiring R
n : ℕ
k : Fin n → ℕ
x : Fin n → R
hk : Function.Injective k
hx : ∀ (i : Fin n), x i ≠ 0
j : Fin n
⊢ x j ≠ 0

Tactic:
exact hx j
-- Module: Mathlib.Algebra.Polynomial.EraseLead
Goal:
R : Type u_1
inst : Semiring R
n : ℕ
k : Fin n → ℕ
x : Fin n → R
hk : Function.Injective k
hx : ∀ (i : Fin n), x i ≠ 0
j : Fin n
⊢ ∀ (b : Fin n), Membership.mem (γ := Finset (Fin n)) univ b → b ≠ j → (if k j = k b then x b else 0) = 0

Tactic:
fun m _ hmj => if_neg fun h => hmj.symm (hk h)

Premises used: Ne.symm, if_neg
-- Module: Mathlib.Algebra.Polynomial.EraseLead
Goal:
R : Type u_1
inst : Semiring R
n : ℕ
k : Fin n → ℕ
x : Fin n → R
hk : Function.Injective k
hx : ∀ (i : Fin n), x i ≠ 0
j : Fin n
⊢ ∀ (b : Fin n), Membership.mem (γ := Finset (Fin n)) univ b → b ≠ j → (if k j = k b then x b else 0) = 0

Tactic:
exact fun m _ hmj => if_neg fun h => hmj.symm (hk h)

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

Tactic:
⟨?_, fun ⟨k, x, hk, hx, hf⟩ => hf.symm ▸ card_support_eq' k x hk.injective hx⟩

Premises used: _private.0.Polynomial.card_support_eq.match_1, Eq.rec, Polynomial.card_support_eq', StrictMono.injective, Iff.intro, Finset.card, Eq.symm, Eq, Polynomial.support
-- Module: Mathlib.Algebra.Polynomial.EraseLead
Goal:
R : Type u_1
inst : Semiring R
f : R[X]
n : ℕ
refine :
  #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.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))

Tactic:
refine ⟨?_, fun ⟨k, x, hk, hx, hf⟩ => hf.symm ▸ card_support_eq' k x hk.injective hx⟩
-- Module: Mathlib.Algebra.Polynomial.EraseLead
Goal:
R : Type u_1
inst : Semiring R
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:
fun hf => ⟨0, 0, fun x => x.elim0, fun x => x.elim0, card_support_eq_zero.mp hf⟩

Premises used: Polynomial.card_support_eq_zero, Exists.intro, Iff.mp, OfNat.ofNat, Fin.elim0
-- Module: Mathlib.Algebra.Polynomial.EraseLead
Goal:
R : Type u_1
inst : Semiring R
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:
exact fun hf => ⟨0, 0, fun x => x.elim0, fun x => x.elim0, card_support_eq_zero.mp hf⟩
-- 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
succ :
  ∀ (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))),
    ∃ (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))
⊢ ∃ (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:
obtain ⟨k, x, hk, hx, hf⟩ := hn (card_support_eraseLead' h)

Premises used: Polynomial.card_support_eraseLead'
-- 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))
i : Fin n
hi : i.castSucc = Fin.last n
⊢ False

Tactic:
i.castSucc_lt_last.ne hi

Premises used: Fin.castSucc_lt_last, LT.lt.ne
-- 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))
i : Fin n
hi : i.castSucc = Fin.last n
⊢ False

Tactic:
exact i.castSucc_lt_last.ne hi

Premises used: Fin.castSucc_lt_last, LT.lt.ne
-- 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))
⊢ ¬∃ (k : Fin n), k.castSucc = Fin.last n

Tactic:
have H : ¬∃ k : Fin n, Fin.castSucc k = Fin.last n := by
      rintro ⟨i, hi⟩
      exact i.castSucc_lt_last.ne hi
-- 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
⊢ ∃ (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:
⟨Function.extend Fin.castSucc k fun _ => f.natDegree,
        Function.extend Fin.castSucc x fun _ => f.leadingCoeff, ?_, ?_, ?_⟩

Premises used: Polynomial.leadingCoeff, Function.extend, Exists.intro, Fin.castSucc, Polynomial.natDegree
-- 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 : StrictMono (Function.extend Fin.castSucc k fun (x : Fin (n + 1)) ↦ f.natDegree)
succ₁ : ∀ (i : Fin (n + 1)), Function.extend Fin.castSucc x (fun (x : Fin (n + 1)) ↦ f.leadingCoeff) i ≠ 0
succ₂ :
  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))
⊢ ∃ (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:
refine
      ⟨Function.extend Fin.castSucc k fun _ => f.natDegree,
        Function.extend Fin.castSucc x fun _ => f.leadingCoeff, ?_, ?_, ?_⟩
-- 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 + 1)
hij : i < j
simp : (↑i : ℕ) < n
⊢ Membership.mem (γ := Set (Fin (n + 1))) (Set.range Fin.castSucc) i

Tactic:
simp only [Fin.range_castSucc, Nat.succ_eq_add_one, Set.mem_setOf_eq]

Premises used: Nat.succ_eq_add_one, Set.mem_setOf_eq, Fin.range_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 j : Fin (n + 1)
hij : i < j
⊢ (↑i : ℕ) < n

Tactic:
lt_of_lt_of_le hij (Nat.lt_succ_iff.mp j.2)

Premises used: Fin.isLt, Nat.lt_succ_iff, Iff.mp, lt_of_lt_of_le
-- 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 + 1)
hij : i < j
⊢ (↑i : ℕ) < n

Tactic:
exact lt_of_lt_of_le hij (Nat.lt_succ_iff.mp j.2)

Premises used: Nat.lt_succ_iff, Iff.mp, lt_of_lt_of_le
-- 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 + 1)
hij : i < j
⊢ Membership.mem (γ := Set (Fin (n + 1))) (Set.range Fin.castSucc) i

Tactic:
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)
-- 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 + 1)
hij : i < j
hi : Membership.mem (γ := Set (Fin (n + 1))) (Set.range Fin.castSucc) i
succ :
  ∀ (i : Fin n) (hij : i.castSucc < j),
    Function.extend Fin.castSucc k (fun (x : Fin (n + 1)) ↦ f.natDegree) i.castSucc <
      Function.extend Fin.castSucc k (fun (x : Fin (n + 1)) ↦ f.natDegree) j
⊢ Function.extend Fin.castSucc k (fun (x : Fin (n + 1)) ↦ f.natDegree) i <
    Function.extend Fin.castSucc k (fun (x : Fin (n + 1)) ↦ f.natDegree) j

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
j : Fin (n + 1)
i : Fin n
hij : i.castSucc < j
succ : k i < Function.extend Fin.castSucc k (fun (x : Fin (n + 1)) ↦ f.natDegree) j
⊢ Function.extend Fin.castSucc k (fun (x : Fin (n + 1)) ↦ f.natDegree) i.castSucc <
    Function.extend Fin.castSucc k (fun (x : Fin (n + 1)) ↦ f.natDegree) j

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
j : Fin (n + 1)
i : Fin n
hij : i.castSucc < j
pos :
  ∀ (hj : ∃ (j₀ : Fin n), j₀.castSucc = j), k i < Function.extend Fin.castSucc k (fun (x : Fin (n + 1)) ↦ f.natDegree) j
neg :
  ∀ (hj : ¬∃ (j₀ : Fin n), j₀.castSucc = j),
    k i < Function.extend Fin.castSucc k (fun (x : Fin (n + 1)) ↦ f.natDegree) j
⊢ k i < Function.extend Fin.castSucc k (fun (x : Fin (n + 1)) ↦ f.natDegree) j

Tactic:
by_cases hj : ∃ j₀, Fin.castSucc j₀ = j