awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
⊢ 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)
have pos : n + P.eraseLead.degree.succ ≤ k
Tactic: simp
-- 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
⊢ (List.map P.coeff (List.range P.degree.succ)).reverse.length ≤ k + 1
have pos : P.degree.succ ≤ k + 1
Tactic: simp
-- 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 : 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)
have 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)
Tactic: obtain ⟨dk, hdk⟩ := exists_add_of_le (Nat.le_of_lt_succ hkd)
-- 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 : k + 1 < P.natDegree + 1
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)
have 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
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]
-- 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 : k + 1 < P.natDegree + 1
dk : ℕ
hdk : P.natDegree = k + 1 + dk
| some (P.coeff (P.degree.succ - 1 - (k + 1)))
have arg : P.coeff (P.degree.succ - 1 - (k + 1))
Tactic: arg 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 : k + 1 < P.natDegree + 1
dk : ℕ
hdk : P.natDegree = k + 1 + dk
⊢ P.coeff (P.degree.succ - 1 - (k + 1)) = P.eraseLead.coeff dk
have rw : P.coeff (P.degree.succ - 1 - (k + 1)) = P.coeff dk
Tactic: rw [eraseLead_coeff_of_ne (f := P) dk (by 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
k : ℕ
hkd : k + 1 < P.natDegree + 1
dk : ℕ
hdk : P.natDegree = k + 1 + dk
⊢ P.coeff (P.degree.succ - 1 - (k + 1)) = P.coeff dk
have e_a : P.degree.succ - 1 - (k + 1) = dk
Tactic: congr
-- 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 : k + 1 < P.natDegree + 1
dk : ℕ
hdk : P.natDegree = k + 1 + dk
| some (P.coeff (P.degree.succ - 1 - (k + 1)))
have arg : P.coeff (P.degree.succ - 1 - (k + 1))
Tactic: arg 1; equals P.eraseLead.coeff dk =>
    rw [eraseLead_coeff_of_ne (f := P) dk (by lia)]
    congr
    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
k : ℕ
hkd : k + 1 < P.natDegree + 1
dk : ℕ
hdk : P.natDegree = k + 1 + dk
⊢ 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
have neg : some (P.eraseLead.coeff dk) =
  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
Tactic: conv_lhs => arg 1; equals P.eraseLead.coeff dk =>
    rw [eraseLead_coeff_of_ne (f := P) dk (by lia)]
    congr
    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
k : ℕ
hkd : k + 1 < P.natDegree + 1
dk : ℕ
hdk : P.natDegree = k + 1 + dk
⊢ some (P.eraseLead.coeff dk) =
    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
have pos : ∀ (hkn : k < n),
  some (P.eraseLead.coeff dk) =
    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
Tactic: by_cases! hkn : k < n
-- 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 : k + 1 < P.natDegree + 1
dk : ℕ
hdk : P.natDegree = k + 1 + dk
pos :
  ∀ (hkn : k < n),
    some (P.eraseLead.coeff dk) =
      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
⊢ some (P.eraseLead.coeff dk) =
    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
have neg : ∀ (hkn : n ≤ k),
  some (P.eraseLead.coeff dk) =
    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
Tactic: by_cases! hkn : k < n
-- 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 : k + 1 < P.natDegree + 1
dk : ℕ
hdk : P.natDegree = k + 1 + dk
hkn : n ≤ k
⊢ some (P.eraseLead.coeff dk) =
    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
have neg : some (P.eraseLead.coeff dk) =
  Option.map P.eraseLead.coeff
    (getElem? (valid := fun (as : List ℕ) (i : ℕ) ↦ i < as.length) (List.range P.eraseLead.degree.succ)
      ((List.map P.eraseLead.coeff (List.range P.eraseLead.degree.succ)).length - 1 - (k - n)))
Tactic: rw [List.getElem?_append_right (List.length_replicate ▸ hkn),
      List.length_replicate, List.getElem?_reverse, List.getElem?_map]
-- 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 : k + 1 < P.natDegree + 1
dk : ℕ
hdk : P.natDegree = k + 1 + dk
hkn : n ≤ k
neg :
  some (P.eraseLead.coeff dk) =
    Option.map P.eraseLead.coeff
      (getElem? (valid := fun (as : List ℕ) (i : ℕ) ↦ i < as.length) (List.range P.eraseLead.degree.succ)
        ((List.map P.eraseLead.coeff (List.range P.eraseLead.degree.succ)).length - 1 - (k - n)))
⊢ some (P.eraseLead.coeff dk) =
    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
have neg₁ : k - n < (List.map P.eraseLead.coeff (List.range P.eraseLead.degree.succ)).length
Tactic: rw [List.getElem?_append_right (List.length_replicate ▸ hkn),
      List.length_replicate, List.getElem?_reverse, List.getElem?_map]
-- 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 : k + 1 < P.natDegree + 1
dk : ℕ
hdk : P.natDegree = k + 1 + dk
hkn : n ≤ k
⊢ some (P.eraseLead.coeff dk) =
    Option.map P.eraseLead.coeff
      (getElem? (valid := fun (as : List ℕ) (i : ℕ) ↦ i < as.length) (List.range P.eraseLead.degree.succ)
        ((List.map P.eraseLead.coeff (List.range P.eraseLead.degree.succ)).length - 1 - (k - n)))
have neg : some (P.eraseLead.coeff dk) = some (P.eraseLead.coeff (P.eraseLead.degree.succ - 1 - (k - n)))
Tactic: rw [List.length_map, List.length_range,
        List.getElem?_range (by lia), Option.map_some]
-- 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 : k + 1 < P.natDegree + 1
dk : ℕ
hdk : P.natDegree = k + 1 + dk
hkn : n ≤ k
⊢ some (P.eraseLead.coeff dk) = some (P.eraseLead.coeff (P.eraseLead.degree.succ - 1 - (k - n)))
have neg : dk = P.eraseLead.degree.succ - 1 - (k - n)
Tactic: congr 2
-- 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 : k + 1 < P.natDegree + 1
dk : ℕ
hdk : P.natDegree = k + 1 + dk
hkn : n ≤ k
⊢ k - n < (List.map P.eraseLead.coeff (List.range P.eraseLead.degree.succ)).length
have neg : k - n < P.eraseLead.degree.succ
Tactic: simp
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.CoeffList (goal)
Goal:
R : Type u_1
inst : Ring R
P : R[X]
⊢ (-P).coeffList = List.map (fun (x : R) ↦ -x) P.coeffList
have pos : ∀ (hp : P = 0), (-P).coeffList = List.map (fun (x : R) ↦ -x) P.coeffList
Tactic: by_cases hp : P = 0
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.CoeffList (goal)
Goal:
R : Type u_1
inst : Ring R
P : R[X]
pos : ∀ (hp : P = 0), (-P).coeffList = List.map (fun (x : R) ↦ -x) P.coeffList
⊢ (-P).coeffList = List.map (fun (x : R) ↦ -x) P.coeffList
have neg : ∀ (hp : ¬P = 0), (-P).coeffList = List.map (fun (x : R) ↦ -x) P.coeffList
Tactic: by_cases hp : P = 0
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.CoeffList (goal)
Goal:
R : Type u_1
inst : Ring R
P : R[X]
hp : P = 0
⊢ (-P).coeffList = List.map (fun (x : R) ↦ -x) P.coeffList
have pos : Eq.{u_1 + 1} (α := List R) (coeffList (-0)) (List.map (fun (x : R) ↦ -x) (coeffList 0))
Tactic: rw [hp, coeffList_zero, neg_zero, coeffList_zero, List.map_nil]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.CoeffList (goal)
Goal:
R : Type u_1
inst : Ring R
P : R[X]
hp : P = 0
pos : Eq.{u_1 + 1} (α := List R) (coeffList (-0)) (List.map (fun (x : R) ↦ -x) (coeffList 0))
⊢ (-P).coeffList = List.map (fun (x : R) ↦ -x) P.coeffList
have pos₁ : Eq.{u_1 + 1} (α := List R) (coeffList (-0)) (List.map (fun (x : R) ↦ -x) [])
Tactic: rw [hp, coeffList_zero, neg_zero, coeffList_zero, List.map_nil]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.CoeffList (goal)
Goal:
R : Type u_1
inst : Ring R
P : R[X]
hp : P = 0
pos : Eq.{u_1 + 1} (α := List R) (coeffList (-0)) (List.map (fun (x : R) ↦ -x) (coeffList 0))
pos₁ : Eq.{u_1 + 1} (α := List R) (coeffList (-0)) (List.map (fun (x : R) ↦ -x) [])
⊢ (-P).coeffList = List.map (fun (x : R) ↦ -x) P.coeffList
have pos₂ : Eq.{u_1 + 1} (α := List R) (coeffList 0) (List.map (fun (x : R) ↦ -x) [])
Tactic: rw [hp, coeffList_zero, neg_zero, coeffList_zero, List.map_nil]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.CoeffList (goal)
Goal:
R : Type u_1
inst : Ring R
P : R[X]
hp : P = 0
pos : Eq.{u_1 + 1} (α := List R) (coeffList (-0)) (List.map (fun (x : R) ↦ -x) (coeffList 0))
pos₁ : Eq.{u_1 + 1} (α := List R) (coeffList (-0)) (List.map (fun (x : R) ↦ -x) [])
pos₂ : Eq.{u_1 + 1} (α := List R) (coeffList 0) (List.map (fun (x : R) ↦ -x) [])
⊢ (-P).coeffList = List.map (fun (x : R) ↦ -x) P.coeffList
have pos₃ : Eq.{u_1 + 1} (α := List R) [] (List.map (fun (x : R) ↦ -x) [])
Tactic: rw [hp, coeffList_zero, neg_zero, coeffList_zero, List.map_nil]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.CoeffList (goal)
Goal:
R : Type u_1
inst : Ring R
P : R[X]
hp : P = 0
pos : Eq.{u_1 + 1} (α := List R) (coeffList (-0)) (List.map (fun (x : R) ↦ -x) (coeffList 0))
pos₁ : Eq.{u_1 + 1} (α := List R) (coeffList (-0)) (List.map (fun (x : R) ↦ -x) [])
pos₂ : Eq.{u_1 + 1} (α := List R) (coeffList 0) (List.map (fun (x : R) ↦ -x) [])
pos₃ : Eq.{u_1 + 1} (α := List R) [] (List.map (fun (x : R) ↦ -x) [])
⊢ (-P).coeffList = List.map (fun (x : R) ↦ -x) P.coeffList
have pos₄ : Eq.{u_1 + 1} (α := List R) [] []
Tactic: rw [hp, coeffList_zero, neg_zero, coeffList_zero, List.map_nil]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.CoeffList (goal)
Goal:
R : Type u_1
inst : Semiring R
inst_1 : NoZeroDivisors R
P : R[X]
x : R
hx : x ≠ 0
⊢ (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) x : R[X]) P).coeffList = List.map (fun (x_1 : R) ↦ x * x_1) P.coeffList
have pos : ∀ (hp : P = 0),
  (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) x : R[X]) P).coeffList = List.map (fun (x_1 : R) ↦ x * x_1) P.coeffList
Tactic: by_cases hp : P = 0
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.CoeffList (goal)
Goal:
R : Type u_1
inst : Semiring R
inst_1 : NoZeroDivisors R
P : R[X]
x : R
hx : x ≠ 0
pos :
  ∀ (hp : P = 0),
    (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) x : R[X]) P).coeffList = List.map (fun (x_1 : R) ↦ x * x_1) P.coeffList
⊢ (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) x : R[X]) P).coeffList = List.map (fun (x_1 : R) ↦ x * x_1) P.coeffList
have neg : ∀ (hp : ¬P = 0),
  (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) x : R[X]) P).coeffList = List.map (fun (x_1 : R) ↦ x * x_1) P.coeffList
Tactic: by_cases hp : P = 0
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.CoeffMem (goal)
Goal:
R : Type u_2
S : Type u_3
inst : CommRing R
inst_1 : Ring S
inst_2 : Algebra R S
p q : S[X]
hq : q.Monic
i : ℕ
⊢ (p.divModByMonicAux hq).1.coeff i ∈ HPow.hPow (α := Submodule R S) spanCoeffs(q) deg(p) * spanCoeffs(p) ∧
    (p.divModByMonicAux hq).2.coeff i ∈ HPow.hPow (α := Submodule R S) spanCoeffs(q) deg(p) * spanCoeffs(p)
have rw : coeff
      (if h : q.degree ≤ p.degree ∧ p ≠ 0 then
          have z :=
            HMul.hMul (α := S[X]) ((C : (a : S) → S[X]) p.leadingCoeff : S[X])
              (HPow.hPow (α := S[X]) X (deg(p) - deg(q)));
          have _wf := sorry;
          have dm := (p - q * z).divModByMonicAux hq;
          (z + dm.1, dm.2)
        else (0, p)).1
      i ∈
    HPow.hPow (α := Submodule R S) spanCoeffs(q) deg(p) * spanCoeffs(p) ∧
  coeff
      (if h : q.degree ≤ p.degree ∧ p ≠ 0 then
          have z :=
            HMul.hMul (α := S[X]) ((C : (a : S) → S[X]) p.leadingCoeff : S[X])
              (HPow.hPow (α := S[X]) X (deg(p) - deg(q)));
          have _wf := sorry;
          have dm := (p - q * z).divModByMonicAux hq;
          (z + dm.1, dm.2)
        else (0, p)).2
      i ∈
    HPow.hPow (α := Submodule R S) spanCoeffs(q) deg(p) * spanCoeffs(p)
Tactic: rw [divModByMonicAux]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.CoeffMem (goal)
Goal:
R : Type u_2
S : Type u_3
inst : CommRing R
inst_1 : Ring S
inst_2 : Algebra R S
p q : S[X]
hq : q.Monic
i_1 i : ℕ
⊢ p.coeff i ∈ HPow.hPow (α := Submodule R S) spanCoeffs(q) deg(p) * spanCoeffs(p)
have refine : span R coeffs(p) ≤ HPow.hPow (α := Submodule R S) spanCoeffs(q) deg(p) * spanCoeffs(p)
Tactic: refine SetLike.le_def.mp ?_ <| subset_span <| mem_range_self i
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.CoeffMem (goal)
Goal:
R : Type u_2
S : Type u_3
inst : CommRing R
inst_1 : Ring S
inst_2 : Algebra R S
p q : S[X]
hq : q.Monic
i_1 i : ℕ
⊢ HPow.hPow (α := Submodule R S) 1 deg(p) * span R coeffs(p) ≤
    HPow.hPow (α := Submodule R S) spanCoeffs(q) deg(p) * spanCoeffs(p)
have h₁ : LE.le (α := Submodule R S) 1 spanCoeffs(q)
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.CoeffMem (goal)
Goal:
R : Type u_2
S : Type u_3
inst : CommRing R
inst_1 : Ring S
inst_2 : Algebra R S
p q : S[X]
hq : q.Monic
i_1 i : ℕ
h₁ : LE.le (α := Submodule R S) 1 spanCoeffs(q)
⊢ HPow.hPow (α := Submodule R S) 1 deg(p) * span R coeffs(p) ≤
    HPow.hPow (α := Submodule R S) spanCoeffs(q) deg(p) * spanCoeffs(p)
have h₂ : LE.le (α := Submodule R S) (span R coeffs(p)) spanCoeffs(p)
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.CoeffMem (goal)
Goal:
R : Type u_2
S : Type u_3
inst : CommRing R
inst_1 : Ring S
inst_2 : Algebra R S
p q : S[X]
hq : q.Monic
i_1 i : ℕ
⊢ span R coeffs(p) ≤ HPow.hPow (α := Submodule R S) spanCoeffs(q) deg(p) * spanCoeffs(p)
have span : span R coeffs(p) = HPow.hPow (α := Submodule R S) 1 deg(p) * span R coeffs(p)
Tactic: calc
        span R coeffs(p)
        _ = 1 ^ deg(p) * span R coeffs(p) := by simp
        _ ≤ spanCoeffs(q) ^ deg(p) * spanCoeffs(p) := by gcongr; exacts [le_sup_left, le_sup_right]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.CoeffMem (goal)
Goal:
R : Type u_2
S : Type u_3
inst : CommRing R
inst_1 : Ring S
inst_2 : Algebra R S
p q : S[X]
hq : q.Monic
i_1 i : ℕ
span : Submodule.span R coeffs(p) = HPow.hPow (α := Submodule R S) 1 deg(p) * Submodule.span R coeffs(p)
⊢ Submodule.span R coeffs(p) ≤ HPow.hPow (α := Submodule R S) spanCoeffs(q) deg(p) * spanCoeffs(p)
have span₁ : HPow.hPow (α := Submodule R S) 1 deg(p) * Submodule.span R coeffs(p) ≤
  HPow.hPow (α := Submodule R S) spanCoeffs(q) deg(p) * spanCoeffs(p)
Tactic: calc
        span R coeffs(p)
        _ = 1 ^ deg(p) * span R coeffs(p) := by simp
        _ ≤ spanCoeffs(q) ^ deg(p) * spanCoeffs(p) := by gcongr; exacts [le_sup_left, le_sup_right]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.CoeffMem (hypothesis)
Goal:
R : Type u_2
S : Type u_3
inst : CommRing R
inst_1 : Ring S
inst_2 : Algebra R S
p q : S[X]
hq : q.Monic
i : ℕ
⊢ coeff
        (if h : q.degree ≤ p.degree ∧ p ≠ 0 then
            have z :=
              HMul.hMul (α := S[X]) ((C : (a : S) → S[X]) p.leadingCoeff : S[X])
                (HPow.hPow (α := S[X]) X (deg(p) - deg(q)));
            have _wf := ⋯;
            have dm := (p - q * z).divModByMonicAux hq;
            (z + dm.1, dm.2)
          else (0, p)).1
        i ∈
      HPow.hPow (α := Submodule R S) spanCoeffs(q) deg(p) * spanCoeffs(p) ∧
    coeff
        (if h : q.degree ≤ p.degree ∧ p ≠ 0 then
            have z :=
              HMul.hMul (α := S[X]) ((C : (a : S) → S[X]) p.leadingCoeff : S[X])
                (HPow.hPow (α := S[X]) X (deg(p) - deg(q)));
            have _wf := ⋯;
            have dm := (p - q * z).divModByMonicAux hq;
            (z + dm.1, dm.2)
          else (0, p)).2
        i ∈
      HPow.hPow (α := Submodule R S) spanCoeffs(q) deg(p) * spanCoeffs(p)
have H₀ : ∀ (i : ℕ), p.coeff i ∈ HPow.hPow (α := Submodule R S) spanCoeffs(q) deg(p) * spanCoeffs(p)
Tactic: have H₀ (i) : p.coeff i ∈ spanCoeffs(q) ^ deg(p) * spanCoeffs(p) := by
      refine SetLike.le_def.mp ?_ <| subset_span <| mem_range_self i
      calc
        span R coeffs(p)
        _ = 1 ^ deg(p) * span R coeffs(p) := by simp
        _ ≤ spanCoeffs(q) ^ deg(p) * spanCoeffs(p) := by gcongr; exacts [le_sup_left, le_sup_right]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.CoeffMem (goal)
Goal:
R : Type u_2
S : Type u_3
inst : CommRing R
inst_1 : Ring S
inst_2 : Algebra R S
p q : S[X]
hq : q.Monic
i : ℕ
H₀ : ∀ (i : ℕ), p.coeff i ∈ HPow.hPow (α := Submodule R S) spanCoeffs(q) deg(p) * spanCoeffs(p)
⊢ coeff
        (if h : q.degree ≤ p.degree ∧ p ≠ 0 then
            have z :=
              HMul.hMul (α := S[X]) ((C : (a : S) → S[X]) p.leadingCoeff : S[X])
                (HPow.hPow (α := S[X]) X (deg(p) - deg(q)));
            have _wf := ⋯;
            have dm := (p - q * z).divModByMonicAux hq;
            (z + dm.1, dm.2)
          else (0, p)).1
        i ∈
      HPow.hPow (α := Submodule R S) spanCoeffs(q) deg(p) * spanCoeffs(p) ∧
    coeff
        (if h : q.degree ≤ p.degree ∧ p ≠ 0 then
            have z :=
              HMul.hMul (α := S[X]) ((C : (a : S) → S[X]) p.leadingCoeff : S[X])
                (HPow.hPow (α := S[X]) X (deg(p) - deg(q)));
            have _wf := ⋯;
            have dm := (p - q * z).divModByMonicAux hq;
            (z + dm.1, dm.2)
          else (0, p)).2
        i ∈
      HPow.hPow (α := Submodule R S) spanCoeffs(q) deg(p) * spanCoeffs(p)
have pos : ∀ (hpq : q.degree ≤ p.degree ∧ p ≠ 0),
  coeff
        (have z :=
            HMul.hMul (α := S[X]) ((C : (a : S) → S[X]) p.leadingCoeff : S[X])
              (HPow.hPow (α := S[X]) X (deg(p) - deg(q)));
          have _wf := sorry;
          have dm := (p - q * z).divModByMonicAux hq;
          (z + dm.1, dm.2)).1
        i ∈
      HPow.hPow (α := Submodule R S) spanCoeffs(q) deg(p) * spanCoeffs(p) ∧
    coeff
        (have z :=
            HMul.hMul (α := S[X]) ((C : (a : S) → S[X]) p.leadingCoeff : S[X])
              (HPow.hPow (α := S[X]) X (deg(p) - deg(q)));
          have _wf := sorry;
          have dm := (p - q * z).divModByMonicAux hq;
          (z + dm.1, dm.2)).2
        i ∈
      HPow.hPow (α := Submodule R S) spanCoeffs(q) deg(p) * spanCoeffs(p)
Tactic: split_ifs with hpq