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
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 : ℕ
fu : ℕ → ℕ
fu0 : ∀ {n : ℕ}, n ≤ k → fu n = 0
fc : ∀ {n m : ℕ}, k ≤ n → n < m → fu n < fu m
φ_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_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
FG : f.natDegree < k
neg :
  ∀ (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
⊢ (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
have neg₁ : ∀ (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),
  (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: cases k
Cleared hypotheses: k, fu0, fc, φ_k, FG
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.EraseLead (goal)
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
⊢ (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
have neg : (HAdd.hAdd (α := S[X]) (β := S[X]) (0 : S[X]) ((φ : (a : R[X]) → S[X]) g : S[X])).natDegree = fu g.natDegree
Tactic: rwa [φ_k FG, zero_add]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.EraseLead (goal)
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
⊢ #(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
have rw : #(image k univ) = n
Tactic: rw [this, univ.card_image_of_injective hk, card_fin]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.EraseLead (goal)
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
⊢ #(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
have rw₁ : card (α := Fin n) univ = n
Tactic: rw [this, univ.card_image_of_injective hk, card_fin]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.EraseLead (goal)
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
⊢ #(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
have rw₂ : n = n
Tactic: rw [this, univ.card_image_of_injective hk, card_fin]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.EraseLead (goal)
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
⊢ #(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
have 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
Tactic: suffices (∑ i, C (x i) * X ^ k i).support = image k univ by
    rw [this, univ.card_image_of_injective hk, card_fin]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.EraseLead (goal)
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
⊢ 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
have 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
Tactic: simp_rw [Finset.ext_iff, mem_support_iff, finsetSum_coeff, coeff_C_mul_X_pow, mem_image,
    mem_univ, true_and]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.EraseLead (goal)
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
have 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
Tactic: refine fun i => ⟨fun h => ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.EraseLead (goal)
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
⊢ ∀ (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
have 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
Tactic: refine fun i => ⟨fun h => ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.EraseLead (goal)
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
⊢ ∃ (a : Fin n), k a = i
have 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
Tactic: obtain ⟨j, _, h⟩ := exists_ne_zero_of_sum_ne_zero h
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.EraseLead (goal)
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
⊢ Ne.{u_1 + 1} (α := R) (∑ x_1 : Fin n, if k j = k x_1 then x x_1 else 0) 0
have refine_2 : x j ≠ 0
Tactic: rw [sum_eq_single_of_mem j (mem_univ j), if_pos rfl]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.EraseLead (goal)
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
⊢ Ne.{u_1 + 1} (α := R) (∑ x_1 : Fin n, if k j = k x_1 then x x_1 else 0) 0
have 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
Tactic: rw [sum_eq_single_of_mem j (mem_univ j), if_pos rfl]
-- 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 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))
Tactic: refine ⟨?_, fun ⟨k, x, hk, hx, hf⟩ => hf.symm ▸ card_support_eq' k x hk.injective hx⟩
-- 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 + 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))
have 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))
Tactic: obtain ⟨k, x, hk, hx, hf⟩ := hn (card_support_eraseLead' h)
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.EraseLead (hypothesis)
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 + 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))
have H : ¬∃ (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
-- 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
⊢ ∃ (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))
have succ : StrictMono (Function.extend Fin.castSucc k fun (x : Fin (n + 1)) ↦ f.natDegree)
Tactic: refine
      ⟨Function.extend Fin.castSucc k fun _ => f.natDegree,
        Function.extend Fin.castSucc x fun _ => f.leadingCoeff, ?_, ?_, ?_⟩
-- 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
succ : StrictMono (Function.extend Fin.castSucc k fun (x : Fin (n + 1)) ↦ f.natDegree)
⊢ ∃ (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))
have succ₁ : ∀ (i : Fin (n + 1)), Function.extend Fin.castSucc x (fun (x : Fin (n + 1)) ↦ f.leadingCoeff) i ≠ 0
Tactic: refine
      ⟨Function.extend Fin.castSucc k fun _ => f.natDegree,
        Function.extend Fin.castSucc x fun _ => f.leadingCoeff, ?_, ?_, ?_⟩
-- 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
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
⊢ ∃ (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))
have 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))
Tactic: refine
      ⟨Function.extend Fin.castSucc k fun _ => f.natDegree,
        Function.extend Fin.castSucc x fun _ => f.leadingCoeff, ?_, ?_, ?_⟩
-- 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 j : Fin (n + 1)
hij : i < j
⊢ Membership.mem (γ := Set (Fin (n + 1))) (Set.range Fin.castSucc) i
have simp : (↑i : ℕ) < n
Tactic: simp only [Fin.range_castSucc, Nat.succ_eq_add_one, Set.mem_setOf_eq]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.EraseLead (hypothesis)
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
⊢ 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
have hi : 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)
-- 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 j : Fin (n + 1)
hij : i < j
hi : Membership.mem (γ := Set (Fin (n + 1))) (Set.range Fin.castSucc) i
⊢ 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
have 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
Tactic: obtain ⟨i, rfl⟩ := hi
Cleared hypotheses: i, hij, 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
j : Fin (n + 1)
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
have succ : k i < Function.extend Fin.castSucc k (fun (x : Fin (n + 1)) ↦ f.natDegree) j
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
j : Fin (n + 1)
i : Fin n
hij : i.castSucc < j
⊢ k i < Function.extend Fin.castSucc k (fun (x : Fin (n + 1)) ↦ f.natDegree) j
have pos : ∀ (hj : ∃ (j₀ : Fin n), j₀.castSucc = 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
-- 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
pos :
  ∀ (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
have neg : ∀ (hj : ¬∃ (j₀ : Fin n), j₀.castSucc = 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
-- 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 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
Tactic: obtain ⟨j, rfl⟩ := hj
Cleared hypotheses: j, hij, 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
i j : Fin n
hij : i.castSucc < j.castSucc
⊢ k i < Function.extend Fin.castSucc k (fun (x : Fin (n + 1)) ↦ f.natDegree) j.castSucc
have pos : k i < k j
Tactic: rwa [Fin.strictMono_castSucc.injective.extend_apply, hk.lt_iff_lt,
          ← Fin.castSucc_lt_castSucc_iff]
-- 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 j : Fin n
hij : i.castSucc < j.castSucc
pos : k i < k j
⊢ k i < Function.extend Fin.castSucc k (fun (x : Fin (n + 1)) ↦ f.natDegree) j.castSucc
have pos₁ : i < j
Tactic: rwa [Fin.strictMono_castSucc.injective.extend_apply, hk.lt_iff_lt,
          ← Fin.castSucc_lt_castSucc_iff]