awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Coeff (goal)
Goal:
R : Type u_1
inst : Ring R
p : R[X]
n : ℕ
a : R
n_1 : ℕ
⊢ (p.update n a).coeff n_1 =
    (p + HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (a - p.coeff n) : R[X]) (HPow.hPow (α := R[X]) X n)).coeff n_1
have a₁ : (if n_1 = n then a else p.coeff n_1) = p.coeff n_1 + if n_1 = n then a - p.coeff n else 0
Tactic: rw [coeff_update_apply, coeff_add, coeff_C_mul_X_pow]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Coeff (goal)
Goal:
R : Type u_1
inst : Ring R
p : R[X]
n : ℕ
a : R
n_1 : ℕ
⊢ (if n_1 = n then a else p.coeff n_1) = p.coeff n_1 + if n_1 = n then a - p.coeff n else 0
have pos : ∀ (h : n_1 = n), a = p.coeff n_1 + (a - p.coeff n)
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Coeff (goal)
Goal:
R : Type u_1
inst : Ring R
p : R[X]
n : ℕ
a : R
n_1 : ℕ
pos : ∀ (h : n_1 = n), a = p.coeff n_1 + (a - p.coeff n)
⊢ (if n_1 = n then a else p.coeff n_1) = p.coeff n_1 + if n_1 = n then a - p.coeff n else 0
have neg : ∀ (h : ¬n_1 = n), p.coeff n_1 = p.coeff n_1 + 0
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Coeff (goal)
Goal:
m n : ℕ
R : Type u_1
inst : Semiring R
inst_1 : CharZero R
⊢ Eq.{u_1 + 1} (α := R[X]) (↑m : R[X]) (↑n : R[X]) ↔ m = n
have mp : Eq.{u_1 + 1} (α := R[X]) (↑m : R[X]) (↑n : R[X]) → m = n
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Coeff (goal)
Goal:
m n : ℕ
R : Type u_1
inst : Semiring R
inst_1 : CharZero R
mp : Eq.{u_1 + 1} (α := R[X]) (↑m : R[X]) (↑n : R[X]) → m = n
⊢ Eq.{u_1 + 1} (α := R[X]) (↑m : R[X]) (↑n : R[X]) ↔ m = n
have mpr : m = n → Eq.{u_1 + 1} (α := R[X]) (↑m : R[X]) (↑n : R[X])
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Coeff (hypothesis)
Goal:
m n : ℕ
R : Type u_1
inst : Semiring R
inst_1 : CharZero R
h : Eq.{u_1 + 1} (α := R[X]) (↑m : R[X]) (↑n : R[X])
⊢ m = n
have h₁ : Eq.{u_1 + 1} (α := R) (coeff (↑m : R[X]) 0) (coeff (↑n : R[X]) 0)
Tactic: apply_fun fun p => p.coeff 0 at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Coeff (goal)
Goal:
i : ℤ
R : Type u_1
inst : Ring R
⊢ Eq.{u_1 + 1} (α := R) (coeff (↑i : R[X]) 0) (↑i : R)
have ofNat : ∀ (a : ℕ), Eq.{u_1 + 1} (α := R) (coeff (↑(Int.ofNat a) : R[X]) 0) (↑(Int.ofNat a) : R)
Tactic: cases i
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Coeff (goal)
Goal:
i : ℤ
R : Type u_1
inst : Ring R
ofNat : ∀ (a : ℕ), Eq.{u_1 + 1} (α := R) (coeff (↑(Int.ofNat a) : R[X]) 0) (↑(Int.ofNat a) : R)
⊢ Eq.{u_1 + 1} (α := R) (coeff (↑i : R[X]) 0) (↑i : R)
have negSucc : ∀ (a : ℕ), Eq.{u_1 + 1} (α := R) (coeff (↑(Int.negSucc a) : R[X]) 0) (↑(Int.negSucc a) : R)
Tactic: cases i
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Coeff (goal)
Goal:
m n : ℤ
R : Type u_1
inst : Ring R
inst_1 : CharZero R
⊢ Eq.{u_1 + 1} (α := R[X]) (↑m : R[X]) (↑n : R[X]) ↔ m = n
have mp : Eq.{u_1 + 1} (α := R[X]) (↑m : R[X]) (↑n : R[X]) → m = n
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Coeff (goal)
Goal:
m n : ℤ
R : Type u_1
inst : Ring R
inst_1 : CharZero R
mp : Eq.{u_1 + 1} (α := R[X]) (↑m : R[X]) (↑n : R[X]) → m = n
⊢ Eq.{u_1 + 1} (α := R[X]) (↑m : R[X]) (↑n : R[X]) ↔ m = n
have mpr : m = n → Eq.{u_1 + 1} (α := R[X]) (↑m : R[X]) (↑n : R[X])
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Coeff (hypothesis)
Goal:
m n : ℤ
R : Type u_1
inst : Ring R
inst_1 : CharZero R
h : Eq.{u_1 + 1} (α := R[X]) (↑m : R[X]) (↑n : R[X])
⊢ m = n
have h₁ : Eq.{u_1 + 1} (α := R) (coeff (↑m : R[X]) 0) (coeff (↑n : R[X]) 0)
Tactic: apply_fun fun p => p.coeff 0 at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Coeff (goal)
Goal:
R : Type u
S : Type v
a b : R
n_1 m : ℕ
inst : Semiring R
p_1 q r : R[X]
p : ℕ
inst_1 : CharP R p
n : ℕ
⊢ Eq.{u + 1} (α := R[X]) (↑n : R[X]) 0 ↔ p ∣ n
have rw : Eq.{u + 1} (α := R[X]) (↑n : R[X]) 0 ↔ Eq.{u + 1} (α := R) (↑n : R) 0
Tactic: rw [← CharP.cast_eq_zero_iff R, ← C_inj (R := R), map_natCast, C_0]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Coeff (goal)
Goal:
R : Type u
S : Type v
a b : R
n_1 m : ℕ
inst : Semiring R
p_1 q r : R[X]
p : ℕ
inst_1 : CharP R p
n : ℕ
rw : Eq.{u + 1} (α := R[X]) (↑n : R[X]) 0 ↔ Eq.{u + 1} (α := R) (↑n : R) 0
⊢ Eq.{u + 1} (α := R[X]) (↑n : R[X]) 0 ↔ p ∣ n
have rw₁ : Eq.{u + 1} (α := R[X]) (↑n : R[X]) 0 ↔ Eq.{u + 1} (α := R[X]) ((C : (a : R) → R[X]) (↑n : R)) ((C : (a : R) → R[X]) 0)
Tactic: rw [← CharP.cast_eq_zero_iff R, ← C_inj (R := R), map_natCast, C_0]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Coeff (goal)
Goal:
R : Type u
S : Type v
a b : R
n_1 m : ℕ
inst : Semiring R
p_1 q r : R[X]
p : ℕ
inst_1 : CharP R p
n : ℕ
rw : Eq.{u + 1} (α := R[X]) (↑n : R[X]) 0 ↔ Eq.{u + 1} (α := R) (↑n : R) 0
rw₁ :
  Eq.{u + 1} (α := R[X]) (↑n : R[X]) 0 ↔ Eq.{u + 1} (α := R[X]) ((C : (a : R) → R[X]) (↑n : R)) ((C : (a : R) → R[X]) 0)
⊢ Eq.{u + 1} (α := R[X]) (↑n : R[X]) 0 ↔ p ∣ n
have rw₂ : Eq.{u + 1} (α := R[X]) (↑n : R[X]) 0 ↔ Eq.{u + 1} (α := R[X]) (↑n : R[X]) ((C : (a : R) → R[X]) 0)
Tactic: rw [← CharP.cast_eq_zero_iff R, ← C_inj (R := R), map_natCast, C_0]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Coeff (goal)
Goal:
R : Type u
S : Type v
a b : R
n_1 m : ℕ
inst : Semiring R
p_1 q r : R[X]
p : ℕ
inst_1 : CharP R p
n : ℕ
rw : Eq.{u + 1} (α := R[X]) (↑n : R[X]) 0 ↔ Eq.{u + 1} (α := R) (↑n : R) 0
rw₁ :
  Eq.{u + 1} (α := R[X]) (↑n : R[X]) 0 ↔ Eq.{u + 1} (α := R[X]) ((C : (a : R) → R[X]) (↑n : R)) ((C : (a : R) → R[X]) 0)
rw₂ : Eq.{u + 1} (α := R[X]) (↑n : R[X]) 0 ↔ Eq.{u + 1} (α := R[X]) (↑n : R[X]) ((C : (a : R) → R[X]) 0)
⊢ Eq.{u + 1} (α := R[X]) (↑n : R[X]) 0 ↔ p ∣ n
have rw₃ : Eq.{u + 1} (α := R[X]) (↑n : R[X]) 0 ↔ Eq.{u + 1} (α := R[X]) (↑n : R[X]) 0
Tactic: rw [← CharP.cast_eq_zero_iff R, ← C_inj (R := R), map_natCast, C_0]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.CoeffList (goal)
Goal:
R : Type u_1
inst : Semiring R
inst_1 : DecidableEq R
P : R[X]
⊢ P.coeffList.length = if P = 0 then 0 else P.natDegree + 1
have pos : ∀ (h : P = 0), P.coeffList.length = if P = 0 then 0 else P.natDegree + 1
Tactic: by_cases h : P = 0
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.CoeffList (goal)
Goal:
R : Type u_1
inst : Semiring R
inst_1 : DecidableEq R
P : R[X]
pos : ∀ (h : P = 0), P.coeffList.length = if P = 0 then 0 else P.natDegree + 1
⊢ P.coeffList.length = if P = 0 then 0 else P.natDegree + 1
have neg : ∀ (h : ¬P = 0), P.coeffList.length = if P = 0 then 0 else P.natDegree + 1
Tactic: by_cases h : P = 0
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.CoeffList (hypothesis)
Goal:
R : Type u_1
inst : Semiring R
P : R[X]
h : P.nextCoeff ≠ 0
⊢ P.leadingCoeff :: P.eraseLead.coeffList = P.coeffList
have h₂ : P ≠ 0
Tactic: have h₂ := ne_zero_of_natDegree_gt (natDegree_pos_of_nextCoeff_ne_zero h)
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.CoeffList (hypothesis)
Goal:
R : Type u_1
inst : Semiring R
P : R[X]
h : P.nextCoeff ≠ 0
h₂ : P ≠ 0
⊢ P.leadingCoeff :: P.eraseLead.coeffList = P.coeffList
have h₃ : ¬P.eraseLead = 0
Tactic: have h₃ := mt nextCoeff_eq_zero_of_eraseLead_eq_zero h
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.CoeffList (hypothesis)
Goal:
R : Type u_1
inst : Semiring R
x : R
hx : x ≠ 0
n : ℕ
⊢ coeffList ((monomial n : (a : R) → R[X]) x) = x :: List.replicate n 0
have h : ¬Eq (α := R[X]) ((monomial n : (a : R) → R[X]) x : R[X]) (0 : R[X])
Tactic: have h := mt (Polynomial.monomial_eq_zero_iff x n).mp hx
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.CoeffList (goal)
Goal:
R : Type u_1
inst : Semiring R
x : R
hx : x ≠ 0
n : ℕ
h : ¬Eq (α := R[X]) ((monomial n : (a : R) → R[X]) x : R[X]) (0 : R[X])
⊢ coeffList ((monomial n : (a : R) → R[X]) x) = x :: List.replicate n 0
have apply : ∀ (n_1 : ℕ) (h₁ : n_1 < List.length.{u_1} (α := R) (coeffList ((monomial n : (a : R) → R[X]) x)))
  (h₂ : n_1 < (x :: List.replicate n 0).length),
  List.get (coeffList ((monomial n : (a : R) → R[X]) x))
      (⟨n_1, h₁⟩ : Fin (List.length.{u_1} (α := R) (coeffList ((monomial n : (a : R) → R[X]) x)))) =
    (x :: List.replicate n 0).get (⟨n_1, h₂⟩ : Fin (x :: List.replicate n 0).length)
Tactic: apply List.ext_get (by classical simp [hx])
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.CoeffList (hypothesis)
Goal:
R : Type u_1
inst : Semiring R
x : R
hx : x ≠ 0
n : ℕ
h : ¬Eq (α := R[X]) ((monomial n : (a : R) → R[X]) x : R[X]) (0 : R[X])
k : ℕ
h₁_1 : k + 1 < List.length.{u_1} (α := R) (coeffList ((monomial n : (a : R) → R[X]) x))
h₁ : k + 1 < (x :: List.replicate n 0).length
⊢ List.get (coeffList ((monomial n : (a : R) → R[X]) x))
      (⟨k + 1, h₁_1⟩ : Fin (List.length.{u_1} (α := R) (coeffList ((monomial n : (a : R) → R[X]) x)))) =
    (x :: List.replicate n 0).get (⟨k + 1, h₁⟩ : Fin (x :: List.replicate n 0).length)
have h₂ : k + 1 < n + 1
Tactic: rw [List.length_cons, List.length_replicate] at h₁
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.CoeffList (hypothesis)
Goal:
R : Type u_1
inst : Semiring R
x : R
hx : x ≠ 0
n : ℕ
h : ¬Eq (α := R[X]) ((monomial n : (a : R) → R[X]) x : R[X]) (0 : R[X])
k : ℕ
h₁_1 : k + 1 < List.length.{u_1} (α := R) (coeffList ((monomial n : (a : R) → R[X]) x))
h₁_2 : k + 1 < (x :: List.replicate n 0).length
h₁ : k + 1 < n + 1
⊢ List.get (coeffList ((monomial n : (a : R) → R[X]) x))
      (⟨k + 1, h₁_1⟩ : Fin (List.length.{u_1} (α := R) (coeffList ((monomial n : (a : R) → R[X]) x)))) =
    (x :: List.replicate n 0).get (⟨k + 1, h₁_2⟩ : Fin (x :: List.replicate n 0).length)
have this : (natDegree.{u_1} (R := R) ((monomial n : (a : R) → R[X]) x)).succ = n + 1
Tactic: have : ((monomial n) x).natDegree.succ = n + 1 := by
      simp [Polynomial.natDegree_monomial_eq n hx]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.CoeffList (goal)
Goal:
R : Type u_1
inst : Semiring R
P : R[X]
h : P ≠ 0
⊢ P.coeffList = P.leadingCoeff :: (List.replicate (P.natDegree - P.eraseLead.degree.succ) 0 ++ P.eraseLead.coeffList)
have pos : ∀ (hdp : P.natDegree = 0),
  P.coeffList = P.leadingCoeff :: (List.replicate (P.natDegree - P.eraseLead.degree.succ) 0 ++ P.eraseLead.coeffList)
Tactic: by_cases hdp : P.natDegree = 0
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.CoeffList (goal)
Goal:
R : Type u_1
inst : Semiring R
P : R[X]
h : P ≠ 0
pos :
  ∀ (hdp : P.natDegree = 0),
    P.coeffList = P.leadingCoeff :: (List.replicate (P.natDegree - P.eraseLead.degree.succ) 0 ++ P.eraseLead.coeffList)
⊢ P.coeffList = P.leadingCoeff :: (List.replicate (P.natDegree - P.eraseLead.degree.succ) 0 ++ P.eraseLead.coeffList)
have neg : ∀ (hdp : ¬P.natDegree = 0),
  P.coeffList = P.leadingCoeff :: (List.replicate (P.natDegree - P.eraseLead.degree.succ) 0 ++ P.eraseLead.coeffList)
Tactic: by_cases hdp : P.natDegree = 0
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.CoeffList (goal)
Goal:
R : Type u_1
inst : Semiring R
P : R[X]
h : P ≠ 0
hdp : P.natDegree = 0
⊢ P.coeffList = P.leadingCoeff :: (List.replicate (P.natDegree - P.eraseLead.degree.succ) 0 ++ P.eraseLead.coeffList)
have pos : ∀ (h : Ne (α := R[X]) ((C : (a : R) → R[X]) (P.coeff 0) : R[X]) (0 : R[X])) (hdp : P.natDegree = 0),
  coeffList ((C : (a : R) → R[X]) (P.coeff 0)) =
    leadingCoeff ((C : (a : R) → R[X]) (P.coeff 0)) ::
      HAppend.hAppend (α := List R)
        (List.replicate
          (natDegree.{u_1} (R := R) ((C : (a : R) → R[X]) (P.coeff 0)) -
            (degree.{u_1} (R := R) (eraseLead ((C : (a : R) → R[X]) (P.coeff 0)))).succ)
          0)
        (coeffList (eraseLead ((C : (a : R) → R[X]) (P.coeff 0))))
Tactic: rw [eq_C_of_natDegree_eq_zero hdp] at h ⊢
Cleared hypotheses: h, hdp
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.CoeffList (goal)
Goal:
R : Type u_1
inst : Semiring R
P : R[X]
h : P ≠ 0
hdp : ¬P.natDegree = 0
⊢ P.coeffList = P.leadingCoeff :: (List.replicate (P.natDegree - P.eraseLead.degree.succ) 0 ++ P.eraseLead.coeffList)
have pos : ∀ (hep : P.eraseLead = 0),
  P.coeffList = P.leadingCoeff :: (List.replicate (P.natDegree - P.eraseLead.degree.succ) 0 ++ P.eraseLead.coeffList)
Tactic: by_cases hep : P.eraseLead = 0
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.CoeffList (goal)
Goal:
R : Type u_1
inst : Semiring R
P : R[X]
h : P ≠ 0
hdp : ¬P.natDegree = 0
pos :
  ∀ (hep : P.eraseLead = 0),
    P.coeffList = P.leadingCoeff :: (List.replicate (P.natDegree - P.eraseLead.degree.succ) 0 ++ P.eraseLead.coeffList)
⊢ P.coeffList = P.leadingCoeff :: (List.replicate (P.natDegree - P.eraseLead.degree.succ) 0 ++ P.eraseLead.coeffList)
have neg : ∀ (hep : ¬P.eraseLead = 0),
  P.coeffList = P.leadingCoeff :: (List.replicate (P.natDegree - P.eraseLead.degree.succ) 0 ++ P.eraseLead.coeffList)
Tactic: by_cases hep : P.eraseLead = 0
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.CoeffList (hypothesis)
Goal:
R : Type u_1
inst : Semiring R
P : R[X]
h : P ≠ 0
hdp : ¬P.natDegree = 0
hep : P.eraseLead = 0
⊢ P.coeffList = P.leadingCoeff :: (List.replicate (P.natDegree - P.eraseLead.degree.succ) 0 ++ P.eraseLead.coeffList)
have h₂ : (monomial P.natDegree : (a : R) → R[X]) P.leadingCoeff = P
Tactic: have h₂ : .monomial P.natDegree P.leadingCoeff = P := by
      simpa [hep] using P.eraseLead_add_monomial_natDegree_leadingCoeff
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.CoeffList (goal)
Goal:
R : Type u_1
inst : Semiring R
P : R[X]
h : P ≠ 0
hdp : ¬P.natDegree = 0
hep : P.eraseLead = 0
h₂ : (monomial P.natDegree : (a : R) → R[X]) P.leadingCoeff = P
⊢ P.coeffList = P.leadingCoeff :: (List.replicate (P.natDegree - P.eraseLead.degree.succ) 0 ++ P.eraseLead.coeffList)
have pos : coeffList ((monomial P.natDegree : (a : R) → R[X]) P.leadingCoeff) =
  P.leadingCoeff :: (List.replicate (P.natDegree - P.eraseLead.degree.succ) 0 ++ P.eraseLead.coeffList)
Tactic: nth_rewrite 1 [← h₂]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.CoeffList (hypothesis)
Goal:
R : Type u_1
inst : Semiring R
P : R[X]
h : P ≠ 0
hdp : ¬P.natDegree = 0
hep : ¬P.eraseLead = 0
⊢ P.coeffList = P.leadingCoeff :: (List.replicate (P.natDegree - P.eraseLead.degree.succ) 0 ++ P.eraseLead.coeffList)
have h₁ : P.degree.succ = P.natDegree + 1
Tactic: have h₁ := withBotSucc_degree_eq_natDegree_add_one h
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.CoeffList (hypothesis)
Goal:
R : Type u_1
inst : Semiring R
P : R[X]
h : P ≠ 0
hdp : ¬P.natDegree = 0
hep : ¬P.eraseLead = 0
h₁ : P.degree.succ = P.natDegree + 1
⊢ P.coeffList = P.leadingCoeff :: (List.replicate (P.natDegree - P.eraseLead.degree.succ) 0 ++ P.eraseLead.coeffList)
have h₂ : P.eraseLead.degree.succ = P.eraseLead.natDegree + 1
Tactic: have h₂ := withBotSucc_degree_eq_natDegree_add_one hep
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.CoeffList (goal)
Goal:
R : Type u_1
inst : Semiring R
P : R[X]
h : P ≠ 0
hdp : ¬P.natDegree = 0
hep : ¬P.eraseLead = 0
h₁ : P.degree.succ = P.natDegree + 1
h₂ : P.eraseLead.degree.succ = P.eraseLead.natDegree + 1
⊢ ∃ (d : ℕ), P.natDegree = P.eraseLead.natDegree + 1 + d ∧ d = P.natDegree - P.eraseLead.degree.succ
have h₃ : P.natDegree = P.eraseLead.natDegree + 1 + (P.natDegree - P.eraseLead.natDegree - 1) ∧
  P.natDegree - P.eraseLead.natDegree - 1 = P.natDegree - P.eraseLead.degree.succ
Tactic: use P.natDegree - P.eraseLead.natDegree - 1
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.CoeffList (hypothesis)
Goal:
R : Type u_1
inst : Semiring R
P : R[X]
h : P ≠ 0
hdp : ¬P.natDegree = 0
hep : ¬P.eraseLead = 0
h₁ : P.degree.succ = P.natDegree + 1
h₂ : P.eraseLead.degree.succ = P.eraseLead.natDegree + 1
⊢ P.natDegree = P.eraseLead.natDegree + 1 + (P.natDegree - P.eraseLead.natDegree - 1) ∧
    P.natDegree - P.eraseLead.natDegree - 1 = P.natDegree - P.eraseLead.degree.succ
have this : P.eraseLead.natDegree ≤ P.natDegree - 1
Tactic: have := eraseLead_natDegree_le P
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.CoeffList (goal)
Goal:
R : Type u_1
inst : Semiring R
P : R[X]
h : P ≠ 0
hdp : ¬P.natDegree = 0
hep : ¬P.eraseLead = 0
h₁ : P.degree.succ = P.natDegree + 1
h₂ : P.eraseLead.degree.succ = P.eraseLead.natDegree + 1
⊢ P.coeffList = P.leadingCoeff :: (List.replicate (P.natDegree - P.eraseLead.degree.succ) 0 ++ P.eraseLead.coeffList)
have neg : ∀ (n : ℕ) (hn : P.natDegree = P.eraseLead.natDegree + 1 + n) (hn2 : n = P.natDegree - P.eraseLead.degree.succ),
  P.coeffList = P.leadingCoeff :: (List.replicate (P.natDegree - P.eraseLead.degree.succ) 0 ++ P.eraseLead.coeffList)
Tactic: obtain ⟨n, hn, hn2⟩ : ∃ d, P.natDegree = P.eraseLead.natDegree + 1 + d ∧
      d = P.natDegree - P.eraseLead.degree.succ := by
    use P.natDegree - P.eraseLead.natDegree - 1
    have := eraseLead_natDegree_le P
    lia
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.CoeffList (goal)
Goal:
R : Type u_1
inst : Semiring R
P : R[X]
h : P ≠ 0
hdp : ¬P.natDegree = 0
hep : ¬P.eraseLead = 0
h₁ : P.degree.succ = P.natDegree + 1
h₂ : P.eraseLead.degree.succ = P.eraseLead.natDegree + 1
n : ℕ
hn : P.natDegree = P.eraseLead.natDegree + 1 + n
hn2 : n = P.natDegree - P.eraseLead.degree.succ
⊢ P.coeffList = P.leadingCoeff :: (List.replicate (P.natDegree - P.eraseLead.degree.succ) 0 ++ P.eraseLead.coeffList)
have neg : P.coeffList = P.leadingCoeff :: (List.replicate n 0 ++ P.eraseLead.coeffList)
Tactic: rw [← hn2]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.CoeffList (goal)
Goal:
R : Type u_1
inst : Semiring R
P : R[X]
h : P ≠ 0
hdp : ¬P.natDegree = 0
hep : ¬P.eraseLead = 0
h₁ : P.degree.succ = P.natDegree + 1
h₂ : P.eraseLead.degree.succ = P.eraseLead.natDegree + 1
n : ℕ
hn : P.natDegree = P.eraseLead.natDegree + 1 + n
⊢ P.coeffList = P.leadingCoeff :: (List.replicate n 0 ++ P.eraseLead.coeffList)
have neg : ∀ (i : ℕ),
  getElem? (valid := fun (as : List R) (i : ℕ) ↦ i < as.length) P.coeffList i =
    getElem? (valid := fun (as : List R) (i : ℕ) ↦ i < as.length)
      (P.leadingCoeff :: (List.replicate n 0 ++ P.eraseLead.coeffList)) i
Tactic: apply List.ext_getElem?
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.CoeffList (goal)
Goal:
R : Type u_1
inst : Semiring R
P : R[X]
h : P ≠ 0
hdp : ¬P.natDegree = 0
hep : ¬P.eraseLead = 0
h₁ : P.degree.succ = P.natDegree + 1
h₂ : P.eraseLead.degree.succ = P.eraseLead.natDegree + 1
n : ℕ
hn : P.natDegree = P.eraseLead.natDegree + 1 + n
⊢ getElem? (valid := fun (as : List R) (i : ℕ) ↦ i < as.length) P.coeffList 0 =
    getElem? (valid := fun (as : List R) (i : ℕ) ↦ i < as.length)
      (P.leadingCoeff :: (List.replicate n 0 ++ P.eraseLead.coeffList)) 0
have neg : ∀ (w : List R) (h : P.coeffList = P.leadingCoeff :: w),
  getElem? (valid := fun (as : List R) (i : ℕ) ↦ i < as.length) P.coeffList 0 =
    getElem? (valid := fun (as : List R) (i : ℕ) ↦ i < as.length)
      (P.leadingCoeff :: (List.replicate n 0 ++ P.eraseLead.coeffList)) 0
Tactic: obtain ⟨w, h⟩ := (coeffList_eq_cons_leadingCoeff h)
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.CoeffList (goal)
Goal:
R : Type u_1
inst : Semiring R
P : R[X]
h : P ≠ 0
hdp : ¬P.natDegree = 0
hep : ¬P.eraseLead = 0
h₁ : P.degree.succ = P.natDegree + 1
h₂ : P.eraseLead.degree.succ = P.eraseLead.natDegree + 1
n : ℕ
hn : P.natDegree = P.eraseLead.natDegree + 1 + n
k : ℕ
⊢ getElem? (valid := fun (as : List R) (i : ℕ) ↦ i < as.length) P.coeffList (k + 1) =
    getElem? (valid := fun (as : List R) (i : ℕ) ↦ i < as.length)
      (P.leadingCoeff :: (List.replicate n 0 ++ P.eraseLead.coeffList)) (k + 1)
have neg : getElem? (valid := fun (as : List R) (i : ℕ) ↦ i < as.length) (List.map P.coeff (List.range P.degree.succ)).reverse
    (k + 1) =
  getElem? (valid := fun (as : List R) (i : ℕ) ↦ i < as.length)
    (P.leadingCoeff ::
      (List.replicate n 0 ++ (List.map P.eraseLead.coeff (List.range P.eraseLead.degree.succ)).reverse))
    (k + 1)
Tactic: simp only [coeffList, List.map_reverse]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.CoeffList (goal)
Goal:
R : Type u_1
inst : Semiring R
P : R[X]
h : P ≠ 0
hdp : ¬P.natDegree = 0
hep : ¬P.eraseLead = 0
h₁ : P.degree.succ = P.natDegree + 1
h₂ : P.eraseLead.degree.succ = P.eraseLead.natDegree + 1
n : ℕ
hn : P.natDegree = P.eraseLead.natDegree + 1 + n
k : ℕ
⊢ getElem? (valid := fun (as : List R) (i : ℕ) ↦ i < as.length) (List.map P.coeff (List.range P.degree.succ)).reverse
      (k + 1) =
    getElem? (valid := fun (as : List R) (i : ℕ) ↦ i < as.length)
      (P.leadingCoeff ::
        (List.replicate n 0 ++ (List.map P.eraseLead.coeff (List.range P.eraseLead.degree.succ)).reverse))
      (k + 1)
have pos : ∀ (hkd : P.natDegree + 1 ≤ k + 1),
  getElem? (valid := fun (as : List R) (i : ℕ) ↦ i < as.length) (List.map P.coeff (List.range P.degree.succ)).reverse
      (k + 1) =
    getElem? (valid := fun (as : List R) (i : ℕ) ↦ i < as.length)
      (P.leadingCoeff ::
        (List.replicate n 0 ++ (List.map P.eraseLead.coeff (List.range P.eraseLead.degree.succ)).reverse))
      (k + 1)
Tactic: by_cases! hkd : P.natDegree + 1 ≤ k + 1
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.CoeffList (goal)
Goal:
R : Type u_1
inst : Semiring R
P : R[X]
h : P ≠ 0
hdp : ¬P.natDegree = 0
hep : ¬P.eraseLead = 0
h₁ : P.degree.succ = P.natDegree + 1
h₂ : P.eraseLead.degree.succ = P.eraseLead.natDegree + 1
n : ℕ
hn : P.natDegree = P.eraseLead.natDegree + 1 + n
k : ℕ
pos :
  ∀ (hkd : P.natDegree + 1 ≤ k + 1),
    getElem? (valid := fun (as : List R) (i : ℕ) ↦ i < as.length) (List.map P.coeff (List.range P.degree.succ)).reverse
        (k + 1) =
      getElem? (valid := fun (as : List R) (i : ℕ) ↦ i < as.length)
        (P.leadingCoeff ::
          (List.replicate n 0 ++ (List.map P.eraseLead.coeff (List.range P.eraseLead.degree.succ)).reverse))
        (k + 1)
⊢ getElem? (valid := fun (as : List R) (i : ℕ) ↦ i < as.length) (List.map P.coeff (List.range P.degree.succ)).reverse
      (k + 1) =
    getElem? (valid := fun (as : List R) (i : ℕ) ↦ i < as.length)
      (P.leadingCoeff ::
        (List.replicate n 0 ++ (List.map P.eraseLead.coeff (List.range P.eraseLead.degree.succ)).reverse))
      (k + 1)
have neg : ∀ (hkd : k + 1 < P.natDegree + 1),
  getElem? (valid := fun (as : List R) (i : ℕ) ↦ i < as.length) (List.map P.coeff (List.range P.degree.succ)).reverse
      (k + 1) =
    getElem? (valid := fun (as : List R) (i : ℕ) ↦ i < as.length)
      (P.leadingCoeff ::
        (List.replicate n 0 ++ (List.map P.eraseLead.coeff (List.range P.eraseLead.degree.succ)).reverse))
      (k + 1)
Tactic: by_cases! hkd : P.natDegree + 1 ≤ k + 1
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.CoeffList (goal)
Goal:
R : Type u_1
inst : Semiring R
P : R[X]
h : P ≠ 0
hdp : ¬P.natDegree = 0
hep : ¬P.eraseLead = 0
h₁ : P.degree.succ = P.natDegree + 1
h₂ : P.eraseLead.degree.succ = P.eraseLead.natDegree + 1
n : ℕ
hn : P.natDegree = P.eraseLead.natDegree + 1 + n
k : ℕ
hkd : P.natDegree + 1 ≤ k + 1
⊢ getElem? (valid := fun (as : List R) (i : ℕ) ↦ i < as.length) (List.map P.coeff (List.range P.degree.succ)).reverse
      (k + 1) =
    getElem? (valid := fun (as : List R) (i : ℕ) ↦ i < as.length)
      (P.leadingCoeff ::
        (List.replicate n 0 ++ (List.map P.eraseLead.coeff (List.range P.eraseLead.degree.succ)).reverse))
      (k + 1)
have pos : none =
  getElem? (valid := fun (as : List R) (i : ℕ) ↦ i < as.length)
    (P.leadingCoeff ::
      (List.replicate n 0 ++ (List.map P.eraseLead.coeff (List.range P.eraseLead.degree.succ)).reverse))
    (k + 1)
Tactic: rw [List.getElem?_eq_none]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.CoeffList (goal)
Goal:
R : Type u_1
inst : Semiring R
P : R[X]
h : P ≠ 0
hdp : ¬P.natDegree = 0
hep : ¬P.eraseLead = 0
h₁ : P.degree.succ = P.natDegree + 1
h₂ : P.eraseLead.degree.succ = P.eraseLead.natDegree + 1
n : ℕ
hn : P.natDegree = P.eraseLead.natDegree + 1 + n
k : ℕ
hkd : P.natDegree + 1 ≤ k + 1
pos :
  none =
    getElem? (valid := fun (as : List R) (i : ℕ) ↦ i < as.length)
      (P.leadingCoeff ::
        (List.replicate n 0 ++ (List.map P.eraseLead.coeff (List.range P.eraseLead.degree.succ)).reverse))
      (k + 1)
⊢ getElem? (valid := fun (as : List R) (i : ℕ) ↦ i < as.length) (List.map P.coeff (List.range P.degree.succ)).reverse
      (k + 1) =
    getElem? (valid := fun (as : List R) (i : ℕ) ↦ i < as.length)
      (P.leadingCoeff ::
        (List.replicate n 0 ++ (List.map P.eraseLead.coeff (List.range P.eraseLead.degree.succ)).reverse))
      (k + 1)
have pos₁ : (List.map P.coeff (List.range P.degree.succ)).reverse.length ≤ k + 1
Tactic: rw [List.getElem?_eq_none]