awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
e_a : P.degree.succ - 1 - (k + 1) = dk
⊢ P.coeff (P.degree.succ - 1 - (k + 1)) = P.coeff dk

Tactic:
congr
-- 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) = dk

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
arg arg₁ : P.coeff (P.degree.succ - 1 - (k + 1))
| some (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

Premises used: Polynomial.eraseLead, Polynomial.coeff, Polynomial.eraseLead_coeff_of_ne
-- 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.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.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:
conv_lhs => arg 1; equals P.eraseLead.coeff dk =>
    rw [eraseLead_coeff_of_ne (f := P) dk (by lia)]
    congr
    lia

Premises used: Polynomial.eraseLead, Polynomial.coeff, Polynomial.eraseLead_coeff_of_ne
-- 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
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
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
⊢ 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
-- 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
hkn : k < n
⊢ P.eraseLead.natDegree < dk

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
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:
simpa [List.getElem?_append, hkn] using coeff_eq_zero_of_natDegree_lt (by lia)

Premises used: List.getElem?_append, Polynomial.coeff_eq_zero_of_natDegree_lt
-- 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
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)))
neg₁ : k - n < (List.map P.eraseLead.coeff (List.range P.eraseLead.degree.succ)).length
⊢ 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:
rw [List.getElem?_append_right (List.length_replicate ▸ hkn),
      List.length_replicate, List.getElem?_reverse, List.getElem?_map]

Premises used: List.getElem?_append_right, List.length_replicate, List.getElem?_map, List.getElem?_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 : ℕ
hkd : k + 1 < P.natDegree + 1
dk : ℕ
hdk : P.natDegree = k + 1 + dk
hkn : n ≤ k
⊢ P.eraseLead.degree.succ - 1 - (k - n) < 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
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) = some (P.eraseLead.coeff (P.eraseLead.degree.succ - 1 - (k - n)))
⊢ 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.length_map, List.length_range,
        List.getElem?_range (by lia), Option.map_some]

Premises used: List.length_range, List.getElem?_range, 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
hkn : n ≤ k
neg : dk = P.eraseLead.degree.succ - 1 - (k - n)
⊢ some (P.eraseLead.coeff dk) = some (P.eraseLead.coeff (P.eraseLead.degree.succ - 1 - (k - n)))

Tactic:
congr 2
-- 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
hkn : n ≤ k
⊢ dk = P.eraseLead.degree.succ - 1 - (k - n)

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
hkn : n ≤ k
neg : k - n < P.eraseLead.degree.succ
⊢ k - n < (List.map P.eraseLead.coeff (List.range P.eraseLead.degree.succ)).length

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 : k + 1 < P.natDegree + 1
dk : ℕ
hdk : P.natDegree = k + 1 + dk
hkn : n ≤ k
⊢ k - n < P.eraseLead.degree.succ

Tactic:
lia
-- Module: Mathlib.Algebra.Polynomial.CoeffList
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
neg : ∀ (hp : ¬P = 0), (-P).coeffList = List.map (fun (x : R) ↦ -x) P.coeffList
⊢ (-P).coeffList = List.map (fun (x : R) ↦ -x) P.coeffList

Tactic:
by_cases hp : P = 0
-- Module: Mathlib.Algebra.Polynomial.CoeffList
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) [])
pos₄ pos₅ : Eq.{u_1 + 1} (α := List R) [] []
⊢ (-P).coeffList = List.map (fun (x : R) ↦ -x) P.coeffList

Tactic:
rw [hp, coeffList_zero, neg_zero, coeffList_zero, List.map_nil]

Premises used: Polynomial.coeffList_zero, neg_zero, List.map_nil
-- Module: Mathlib.Algebra.Polynomial.CoeffList
Goal:
R : Type u_1
inst : Ring R
P : R[X]
hp : ¬P = 0
⊢ (-P).coeffList = List.map (fun (x : R) ↦ -x) P.coeffList

Tactic:
simp [coeffList]

Premises used: Polynomial.coeffList
-- Module: Mathlib.Algebra.Polynomial.CoeffList
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
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
⊢ (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
-- Module: Mathlib.Algebra.Polynomial.CoeffList
Goal:
R : Type u_1
inst : Semiring R
inst_1 : NoZeroDivisors R
P : R[X]
x : R
hx : x ≠ 0
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:
simp [hp]
-- Module: Mathlib.Algebra.Polynomial.CoeffList
Goal:
R : Type u_1
inst : Semiring R
inst_1 : NoZeroDivisors R
P : R[X]
x : R
hx : x ≠ 0
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:
simp [coeffList, Polynomial.degree_C hx]

Premises used: Polynomial.degree_C, Polynomial.coeffList
-- Module: Mathlib.Algebra.Polynomial.CoeffMem
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 : ℕ
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 := ⋯;
            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)
⊢ (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)

Tactic:
rw [divModByMonicAux]

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

Tactic:
SetLike.le_def.mp ?_ <| subset_span <| mem_range_self i

Premises used: Set.mem_range_self, SetLike.le_def, Iff.mp, Submodule.subset_span
-- Module: Mathlib.Algebra.Polynomial.CoeffMem
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 : ℕ
refine : span R coeffs(p) ≤ HPow.hPow (α := Submodule R S) spanCoeffs(q) deg(p) * spanCoeffs(p)
⊢ p.coeff i ∈ HPow.hPow (α := Submodule R S) spanCoeffs(q) deg(p) * spanCoeffs(p)

Tactic:
refine SetLike.le_def.mp ?_ <| subset_span <| mem_range_self i

Premises used: Set.mem_range_self, SetLike.le_def, Iff.mp, Submodule.subset_span
-- Module: Mathlib.Algebra.Polynomial.CoeffMem
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) 1 deg(p) * span R coeffs(p)

Tactic:
simp
-- Module: Mathlib.Algebra.Polynomial.CoeffMem
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)
h₂ : LE.le (α := Submodule R S) (span R coeffs(p)) spanCoeffs(p)
⊢ HPow.hPow (α := Submodule R S) 1 deg(p) * span R coeffs(p) ≤
    HPow.hPow (α := Submodule R S) spanCoeffs(q) deg(p) * spanCoeffs(p)

Tactic:
gcongr
-- Module: Mathlib.Algebra.Polynomial.CoeffMem
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 : ℕ
⊢ LE.le (α := Submodule R S) 1 spanCoeffs(q)

Tactic:
le_sup_left

Premises used: le_sup_left, Set.Mem
-- Module: Mathlib.Algebra.Polynomial.CoeffMem
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 : ℕ
⊢ LE.le (α := Submodule R S) (span R coeffs(p)) spanCoeffs(p)

Tactic:
le_sup_right

Premises used: Set.Mem, le_sup_right
-- Module: Mathlib.Algebra.Polynomial.CoeffMem
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 : ℕ
⊢ LE.le (α := Submodule R S) 1 spanCoeffs(q)

Tactic:
exacts [le_sup_left, le_sup_right]

Premises used: le_sup_left, le_sup_right
-- Module: Mathlib.Algebra.Polynomial.CoeffMem
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)
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)
⊢ 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]

Premises used: Polynomial.coeff, Submodule.span, Set.range
-- Module: Mathlib.Algebra.Polynomial.CoeffMem
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 : ℕ
⊢ ∀ (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]
-- Module: Mathlib.Algebra.Polynomial.CoeffMem
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)
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 := ⋯;
            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 := ⋯;
            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)
neg :
  ∀ (hpq : ¬(q.degree ≤ p.degree ∧ p ≠ 0)),
    coeff (0, p).1 i ∈ HPow.hPow (α := Submodule R S) spanCoeffs(q) deg(p) * spanCoeffs(p) ∧
      (0, p).2.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)

Tactic:
split_ifs with hpq
-- Module: Mathlib.Algebra.Polynomial.CoeffMem
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)
hpq : ¬(q.degree ≤ p.degree ∧ p ≠ 0)
⊢ coeff (0, p).1 i ∈ HPow.hPow (α := Submodule R S) spanCoeffs(q) deg(p) * spanCoeffs(p) ∧
    (0, p).2.coeff i ∈ HPow.hPow (α := Submodule R S) spanCoeffs(q) deg(p) * spanCoeffs(p)

Tactic:
simpa using H₀ _
-- Module: Mathlib.Algebra.Polynomial.CoeffMem
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)
hpq : q.degree ≤ p.degree ∧ p ≠ 0
pos :
  (p.leadingCoeff * if i = deg(p) - deg(q) then 1 else 0) +
        ((p -
                    q *
                      HMul.hMul (α := S[X]) ((C : (a : S) → S[X]) p.leadingCoeff : S[X])
                        (HPow.hPow (α := S[X]) X (deg(p) - deg(q)))).divModByMonicAux
                hq).1.coeff
          i ∈
      HPow.hPow (α := Submodule R S) spanCoeffs(q) deg(p) * spanCoeffs(p) ∧
    ((p -
                  q *
                    HMul.hMul (α := S[X]) ((C : (a : S) → S[X]) p.leadingCoeff : S[X])
                      (HPow.hPow (α := S[X]) X (deg(p) - deg(q)))).divModByMonicAux
              hq).2.coeff
        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 := ⋯;
          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 := ⋯;
          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:
simp only [coeff_add, coeff_C_mul, coeff_X_pow]

Premises used: Polynomial.coeff_X_pow, Polynomial.coeff_C_mul, Polynomial.coeff_add
-- Module: Mathlib.Algebra.Polynomial.CoeffMem
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)
hpq : q.degree ≤ p.degree ∧ p ≠ 0
pos :
  ∀ (r : S[X])
    (hr :
      p -
          q *
            HMul.hMul (α := S[X]) ((C : (a : S) → S[X]) p.leadingCoeff : S[X])
              (HPow.hPow (α := S[X]) X (deg(p) - deg(q))) =
        r),
    (p.leadingCoeff * if i = deg(p) - deg(q) then 1 else 0) + (r.divModByMonicAux hq).1.coeff i ∈
        HPow.hPow (α := Submodule R S) spanCoeffs(q) deg(p) * spanCoeffs(p) ∧
      (r.divModByMonicAux hq).2.coeff i ∈ HPow.hPow (α := Submodule R S) spanCoeffs(q) deg(p) * spanCoeffs(p)
⊢ (p.leadingCoeff * if i = deg(p) - deg(q) then 1 else 0) +
        ((p -
                    q *
                      HMul.hMul (α := S[X]) ((C : (a : S) → S[X]) p.leadingCoeff : S[X])
                        (HPow.hPow (α := S[X]) X (deg(p) - deg(q)))).divModByMonicAux
                hq).1.coeff
          i ∈
      HPow.hPow (α := Submodule R S) spanCoeffs(q) deg(p) * spanCoeffs(p) ∧
    ((p -
                  q *
                    HMul.hMul (α := S[X]) ((C : (a : S) → S[X]) p.leadingCoeff : S[X])
                      (HPow.hPow (α := S[X]) X (deg(p) - deg(q)))).divModByMonicAux
              hq).2.coeff
        i ∈
      HPow.hPow (α := Submodule R S) spanCoeffs(q) deg(p) * spanCoeffs(p)

Tactic:
generalize hr : (p - q * (C p.leadingCoeff * X ^ (deg(p) - deg(q)))) = r

Premises used: Polynomial.C, HMul.hMul, HSub.hSub, Polynomial.leadingCoeff, HPow.hPow, Polynomial.natDegree, Polynomial.X, DFunLike.coe