awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Polynomial.CoeffList
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])
h₁_1 : 0 < List.length.{u_1} (α := R) (coeffList ((monomial n : (a : R) → R[X]) x))
h₁ : 0 < (x :: List.replicate n 0).length
⊢ List.get (coeffList ((monomial n : (a : R) → R[X]) x))
      (⟨0, h₁_1⟩ : Fin (List.length.{u_1} (α := R) (coeffList ((monomial n : (a : R) → R[X]) x)))) =
    (x :: List.replicate n 0).get (⟨0, h₁⟩ : Fin (x :: List.replicate n 0).length)

Tactic:
exact (coeffList_eq_cons_leadingCoeff h).rec (by simp_all)
-- Module: Mathlib.Algebra.Polynomial.CoeffList
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
⊢ k + 1 < n + 1

Tactic:
rw [List.length_cons, List.length_replicate] at h₁

Premises used: List.length_cons, List.length_replicate
-- Module: Mathlib.Algebra.Polynomial.CoeffList
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
⊢ (natDegree.{u_1} (R := R) ((monomial n : (a : R) → R[X]) x)).succ = n + 1

Tactic:
simp [Polynomial.natDegree_monomial_eq n hx]

Premises used: Polynomial.natDegree_monomial_eq
-- Module: Mathlib.Algebra.Polynomial.CoeffList
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
⊢ (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]
-- Module: Mathlib.Algebra.Polynomial.CoeffList
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
this : (natDegree.{u_1} (R := R) ((monomial n : (a : R) → R[X]) x)).succ = n + 1
⊢ natDegree.{u_1} (R := R) ((monomial n : (a : R) → R[X]) x) - (k + 1) ≠ n

Tactic:
lia
-- Module: Mathlib.Algebra.Polynomial.CoeffList
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
this : (natDegree.{u_1} (R := R) ((monomial n : (a : R) → R[X]) x)).succ = 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)

Tactic:
simpa [coeffList, withBotSucc_degree_eq_natDegree_add_one h]
      using Polynomial.coeff_monomial_of_ne _ (by lia)

Premises used: Polynomial.coeff_monomial_of_ne, Polynomial.coeffList, Polynomial.withBotSucc_degree_eq_natDegree_add_one
-- Module: Mathlib.Algebra.Polynomial.CoeffList
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)
neg :
  ∀ (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)

Tactic:
by_cases hdp : P.natDegree = 0

Premises used: Polynomial.natDegree
-- Module: Mathlib.Algebra.Polynomial.CoeffList
Goal:
R : Type u_1
inst : Semiring R
P : R[X]
h : P ≠ 0
hdp : P.natDegree = 0
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))))
⊢ P.coeffList = P.leadingCoeff :: (List.replicate (P.natDegree - P.eraseLead.degree.succ) 0 ++ P.eraseLead.coeffList)

Tactic:
rw [eq_C_of_natDegree_eq_zero hdp] at h ⊢

Premises used: Polynomial.eq_C_of_natDegree_eq_zero
-- Module: Mathlib.Algebra.Polynomial.CoeffList
Goal:
R : Type u_1
inst : Semiring R
P : R[X]
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:
simp [coeffList_C (C_ne_zero.mp h)]

Premises used: Polynomial.coeffList_C, Iff.mp, Polynomial.C_ne_zero
-- Module: Mathlib.Algebra.Polynomial.CoeffList
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)
neg :
  ∀ (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)

Tactic:
by_cases hep : P.eraseLead = 0

Premises used: Polynomial.eraseLead
-- Module: Mathlib.Algebra.Polynomial.CoeffList
Goal:
R : Type u_1
inst : Semiring R
P : R[X]
h : P ≠ 0
hdp : ¬P.natDegree = 0
hep : P.eraseLead = 0
⊢ (monomial P.natDegree : (a : R) → R[X]) P.leadingCoeff = P

Tactic:
simpa [hep] using P.eraseLead_add_monomial_natDegree_leadingCoeff

Premises used: Polynomial.eraseLead_add_monomial_natDegree_leadingCoeff
-- Module: Mathlib.Algebra.Polynomial.CoeffList
Goal:
R : Type u_1
inst : Semiring R
P : R[X]
h : P ≠ 0
hdp : ¬P.natDegree = 0
hep : P.eraseLead = 0
⊢ (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
-- Module: Mathlib.Algebra.Polynomial.CoeffList
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
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)
⊢ P.coeffList = P.leadingCoeff :: (List.replicate (P.natDegree - P.eraseLead.degree.succ) 0 ++ P.eraseLead.coeffList)

Tactic:
nth_rewrite 1 [← h₂]
-- Module: Mathlib.Algebra.Polynomial.CoeffList
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
⊢ 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:
simp [coeffList_monomial (Polynomial.leadingCoeff_ne_zero.mpr h), hep]

Premises used: Iff.mpr, Polynomial.leadingCoeff_ne_zero, Polynomial.coeffList_monomial
-- Module: Mathlib.Algebra.Polynomial.CoeffList
Goal:
R : Type u_1
inst : Semiring R
P : R[X]
h : P ≠ 0
hdp : ¬P.natDegree = 0
hep : ¬P.eraseLead = 0
⊢ P.degree.succ = P.natDegree + 1

Tactic:
have h₁ := withBotSucc_degree_eq_natDegree_add_one h
-- Module: Mathlib.Algebra.Polynomial.CoeffList
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.eraseLead.degree.succ = P.eraseLead.natDegree + 1

Tactic:
have h₂ := withBotSucc_degree_eq_natDegree_add_one hep
-- Module: Mathlib.Algebra.Polynomial.CoeffList
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
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
⊢ ∃ (d : ℕ), P.natDegree = P.eraseLead.natDegree + 1 + d ∧ d = P.natDegree - P.eraseLead.degree.succ

Tactic:
use P.natDegree - P.eraseLead.natDegree - 1

Premises used: Polynomial.eraseLead, Polynomial.natDegree
-- Module: Mathlib.Algebra.Polynomial.CoeffList
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.eraseLead.natDegree ≤ P.natDegree - 1

Tactic:
have := eraseLead_natDegree_le P
-- Module: Mathlib.Algebra.Polynomial.CoeffList
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
this : P.eraseLead.natDegree ≤ P.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

Tactic:
lia
-- Module: Mathlib.Algebra.Polynomial.CoeffList
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
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)
⊢ 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

Premises used: WithBot.succ, Polynomial.degree, Polynomial.eraseLead, Polynomial.natDegree
-- Module: Mathlib.Algebra.Polynomial.CoeffList
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
neg : P.coeffList = P.leadingCoeff :: (List.replicate n 0 ++ P.eraseLead.coeffList)
⊢ P.coeffList = P.leadingCoeff :: (List.replicate (P.natDegree - P.eraseLead.degree.succ) 0 ++ P.eraseLead.coeffList)

Tactic:
rw [← hn2]
-- Module: Mathlib.Algebra.Polynomial.CoeffList
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
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
⊢ P.coeffList = P.leadingCoeff :: (List.replicate n 0 ++ P.eraseLead.coeffList)

Tactic:
apply List.ext_getElem?

Premises used: List.ext_getElem?
-- Module: Mathlib.Algebra.Polynomial.CoeffList
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
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
⊢ 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)

Premises used: Polynomial.coeffList_eq_cons_leadingCoeff
-- Module: Mathlib.Algebra.Polynomial.CoeffList
Goal:
R : Type u_1
inst : Semiring R
P : R[X]
h_1 : 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
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:
simp_all
-- Module: Mathlib.Algebra.Polynomial.CoeffList
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 : ℕ
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)
⊢ 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)

Tactic:
simp only [coeffList, List.map_reverse]

Premises used: Polynomial.coeffList, List.map_reverse
-- Module: Mathlib.Algebra.Polynomial.CoeffList
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)
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)
⊢ 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

Premises used: Polynomial.natDegree
-- Module: Mathlib.Algebra.Polynomial.CoeffList
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)
pos₁ : (List.map P.coeff (List.range P.degree.succ)).reverse.length ≤ 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:
rw [List.getElem?_eq_none]

Premises used: List.getElem?_eq_none
-- Module: Mathlib.Algebra.Polynomial.CoeffList
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 : n + P.eraseLead.degree.succ ≤ k
⊢ 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:
simp
-- Module: Mathlib.Algebra.Polynomial.CoeffList
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 : P.degree.succ ≤ k + 1
⊢ (List.map P.coeff (List.range P.degree.succ)).reverse.length ≤ k + 1

Tactic:
simp
-- Module: Mathlib.Algebra.Polynomial.CoeffList
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
⊢ n + P.eraseLead.degree.succ ≤ k

Tactic:
lia
-- Module: Mathlib.Algebra.Polynomial.CoeffList
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
⊢ P.degree.succ ≤ k + 1

Tactic:
lia
-- Module: Mathlib.Algebra.Polynomial.CoeffList
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 : k + 1 < P.natDegree + 1
neg :
  ∀ (dk : ℕ) (hdk : P.natDegree = k + 1 + dk),
    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)

Tactic:
obtain ⟨dk, hdk⟩ := exists_add_of_le (Nat.le_of_lt_succ hkd)

Premises used: ExistsAddOfLE.exists_add_of_le, Nat.le_of_lt_succ
-- Module: Mathlib.Algebra.Polynomial.CoeffList
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 : k + 1 < P.natDegree + 1
dk : ℕ
hdk : P.natDegree = k + 1 + dk
⊢ k + 1 < (List.map P.coeff (List.range P.degree.succ)).length

Tactic:
simpa [withBotSucc_degree_eq_natDegree_add_one h] using hkd

Premises used: Polynomial.withBotSucc_degree_eq_natDegree_add_one
-- Module: Mathlib.Algebra.Polynomial.CoeffList
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 : k + 1 < P.natDegree + 1
dk : ℕ
hdk : P.natDegree = k + 1 + dk
⊢ P.degree.succ - 1 - (k + 1) < P.degree.succ

Tactic:
lia
-- Module: Mathlib.Algebra.Polynomial.CoeffList
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 : k + 1 < P.natDegree + 1
dk : ℕ
hdk : P.natDegree = k + 1 + dk
neg :
  some (P.coeff (P.degree.succ - 1 - (k + 1))) =
    getElem? (valid := fun (as : List R) (i : ℕ) ↦ i < as.length)
      (List.replicate n 0 ++ (List.map P.eraseLead.coeff (List.range P.eraseLead.degree.succ)).reverse) 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)

Tactic:
rw [List.getElem?_reverse (by simpa [withBotSucc_degree_eq_natDegree_add_one h] using hkd),
    List.getElem?_cons_succ, List.length_map, List.length_range, List.getElem?_map,
    List.getElem?_range (by lia), Option.map_some]

Premises used: List.getElem?_cons_succ, List.length_range, List.getElem?_range, List.getElem?_map, List.getElem?_reverse, Option.map_some, List.length_map
-- Module: Mathlib.Algebra.Polynomial.CoeffList
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 : k + 1 < P.natDegree + 1
dk : ℕ
hdk : P.natDegree = k + 1 + dk
arg : P.coeff (P.degree.succ - 1 - (k + 1))
| some (P.coeff (P.degree.succ - 1 - (k + 1)))

Tactic:
arg 1
-- Module: Mathlib.Algebra.Polynomial.CoeffList
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 : k + 1 < P.natDegree + 1
dk : ℕ
hdk : P.natDegree = k + 1 + dk
⊢ dk ≠ P.natDegree

Tactic:
lia
-- Module: Mathlib.Algebra.Polynomial.CoeffList
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 : k + 1 < P.natDegree + 1
dk : ℕ
hdk : P.natDegree = k + 1 + dk
rw : P.coeff (P.degree.succ - 1 - (k + 1)) = P.coeff dk
⊢ P.coeff (P.degree.succ - 1 - (k + 1)) = P.eraseLead.coeff dk

Tactic:
rw [eraseLead_coeff_of_ne (f := P) dk (by lia)]

Premises used: Polynomial.eraseLead_coeff_of_ne