awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
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
pos :
  ∀ (hr' : r = 0),
    (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)
neg :
  ∀ (hr' : ¬r = 0),
    (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) + (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)

Tactic:
by_cases hr' : r = 0
-- 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
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
hr' : r = 0
pos :
  (if i = deg(p) - deg(q) then p.leadingCoeff else 0) ∈
    HPow.hPow (α := Submodule R S) spanCoeffs(q) deg(p) * spanCoeffs(p)
⊢ (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)

Tactic:
simp only [mul_ite, mul_one, mul_zero, hr', divModByMonicAux, degree_zero, le_bot_iff,
        degree_eq_bot, ne_eq, not_true_eq_false, and_false, ↓reduceDIte, coeff_zero, add_zero,
        Submodule.zero_mem, and_true]

Premises used: le_bot_iff, and_true, mul_ite, reduceDIte, not_true_eq_false, Polynomial.degree_zero, ne_eq, Polynomial.divModByMonicAux, MulZeroClass.mul_zero, Submodule.zero_mem, Polynomial.coeff_zero, and_false, mul_one, add_zero, Polynomial.degree_eq_bot
-- 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
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
hr' : r = 0
pos : i = deg(p) - deg(q) → p.leadingCoeff ∈ HPow.hPow (α := Submodule R S) spanCoeffs(q) deg(p) * spanCoeffs(p)
neg : ¬i = deg(p) - deg(q) → 0 ∈ HPow.hPow (α := Submodule R S) spanCoeffs(q) deg(p) * spanCoeffs(p)
⊢ (if i = deg(p) - deg(q) then p.leadingCoeff else 0) ∈
    HPow.hPow (α := Submodule R S) spanCoeffs(q) deg(p) * spanCoeffs(p)

Tactic:
split_ifs
-- 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
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
hr' : r = 0
h : i = deg(p) - deg(q)
⊢ p.leadingCoeff ∈ HPow.hPow (α := Submodule R S) spanCoeffs(q) deg(p) * spanCoeffs(p)

Tactic:
H₀ _

Premises used: Set.Mem, Polynomial.leadingCoeff
-- 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
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
hr' : r = 0
h : ¬i = deg(p) - deg(q)
⊢ 0 ∈ HPow.hPow (α := Submodule R S) spanCoeffs(q) deg(p) * spanCoeffs(p)

Tactic:
zero_mem _

Premises used: ZeroMemClass.zero_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 : ℕ
H₀ : ∀ (i : ℕ), p.coeff i ∈ HPow.hPow (α := Submodule R S) spanCoeffs(q) deg(p) * spanCoeffs(p)
hpq : q.degree ≤ p.degree ∧ p ≠ 0
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
hr' : r = 0
h : i = deg(p) - deg(q)
⊢ p.leadingCoeff ∈ HPow.hPow (α := Submodule R S) spanCoeffs(q) deg(p) * spanCoeffs(p)

Tactic:
exacts [H₀ _, zero_mem _]

Premises used: ZeroMemClass.zero_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 : ℕ
H₀ : ∀ (i : ℕ), p.coeff i ∈ HPow.hPow (α := Submodule R S) spanCoeffs(q) deg(p) * spanCoeffs(p)
hpq : q.degree ≤ p.degree ∧ p ≠ 0
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
hr' : ¬r = 0
rw :
  coeffs(p -
        q *
          HMul.hMul (α := S[X]) ((C : (a : S) → S[X]) p.leadingCoeff : S[X])
            (HPow.hPow (α := S[X]) X (deg(p) - deg(q)))) ⊆
    (↑(span R coeffs(p) ⊔ HMul.hMul (α := Submodule R S) (span R coeffs(q)) (span R coeffs(p))) : Set S)
⊢ span R coeffs(r) ≤ span R coeffs(p) ⊔ HMul.hMul (α := Submodule R S) (span R coeffs(q)) (span R coeffs(p))

Tactic:
rw [span_le, ← hr]

Premises used: Submodule.span_le
-- 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 : ℕ
H₀ : ∀ (i : ℕ), p.coeff i ∈ HPow.hPow (α := Submodule R S) spanCoeffs(q) deg(p) * spanCoeffs(p)
hpq : q.degree ≤ p.degree ∧ p ≠ 0
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
hr' : ¬r = 0
i : ℕ
rw :
  (p.coeff i - if deg(p) - deg(q) ≤ i then q.coeff (i - (deg(p) - deg(q))) * p.leadingCoeff else 0) ∈
    (↑(span R coeffs(p) ⊔ HMul.hMul (α := Submodule R S) (span R coeffs(q)) (span R coeffs(p))) : Set S)
⊢ (p -
          q *
            HMul.hMul (α := S[X]) ((C : (a : S) → S[X]) p.leadingCoeff : S[X])
              (HPow.hPow (α := S[X]) X (deg(p) - deg(q)))).coeff
      i ∈
    (↑(span R coeffs(p) ⊔ HMul.hMul (α := Submodule R S) (span R coeffs(q)) (span R coeffs(p))) : Set S)

Tactic:
rw [coeff_sub, ← mul_assoc, coeff_mul_X_pow', coeff_mul_C]

Premises used: mul_assoc, Polynomial.coeff_mul_C, Polynomial.coeff_sub, Polynomial.coeff_mul_X_pow'
-- 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 : ℕ
H₀ : ∀ (i : ℕ), p.coeff i ∈ HPow.hPow (α := Submodule R S) spanCoeffs(q) deg(p) * spanCoeffs(p)
hpq : q.degree ≤ p.degree ∧ p ≠ 0
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
hr' : ¬r = 0
i : ℕ
hx : p.coeff i ∈ span R coeffs(p) ⊔ HMul.hMul (α := Submodule R S) (span R coeffs(q)) (span R coeffs(p))
hy :
  (if deg(p) - deg(q) ≤ i then q.coeff (i - (deg(p) - deg(q))) * p.leadingCoeff else 0) ∈
    span R coeffs(p) ⊔ HMul.hMul (α := Submodule R S) (span R coeffs(q)) (span R coeffs(p))
⊢ (p.coeff i - if deg(p) - deg(q) ≤ i then q.coeff (i - (deg(p) - deg(q))) * p.leadingCoeff else 0) ∈
    (↑(span R coeffs(p) ⊔ HMul.hMul (α := Submodule R S) (span R coeffs(q)) (span R coeffs(p))) : Set S)

Tactic:
apply sub_mem

Premises used: sub_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 : ℕ
H₀ : ∀ (i : ℕ), p.coeff i ∈ HPow.hPow (α := Submodule R S) spanCoeffs(q) deg(p) * spanCoeffs(p)
hpq : q.degree ≤ p.degree ∧ p ≠ 0
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
hr' : ¬r = 0
i : ℕ
⊢ p.coeff i ∈ span R coeffs(p) ⊔ HMul.hMul (α := Submodule R S) (span R coeffs(q)) (span R coeffs(p))

Tactic:
SetLike.le_def.mp le_sup_left (subset_span (mem_range_self _))

Premises used: Set.mem_range_self, le_sup_left, 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 : ℕ
H₀ : ∀ (i : ℕ), p.coeff i ∈ HPow.hPow (α := Submodule R S) spanCoeffs(q) deg(p) * spanCoeffs(p)
hpq : q.degree ≤ p.degree ∧ p ≠ 0
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
hr' : ¬r = 0
i : ℕ
⊢ p.coeff i ∈ span R coeffs(p) ⊔ HMul.hMul (α := Submodule R S) (span R coeffs(q)) (span R coeffs(p))

Tactic:
exact SetLike.le_def.mp le_sup_left (subset_span (mem_range_self _))

Premises used: Set.mem_range_self, le_sup_left, 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 : ℕ
H₀ : ∀ (i : ℕ), p.coeff i ∈ HPow.hPow (α := Submodule R S) spanCoeffs(q) deg(p) * spanCoeffs(p)
hpq : q.degree ≤ p.degree ∧ p ≠ 0
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
hr' : ¬r = 0
i : ℕ
pos :
  deg(p) - deg(q) ≤ i →
    q.coeff (i - (deg(p) - deg(q))) * p.leadingCoeff ∈
      span R coeffs(p) ⊔ HMul.hMul (α := Submodule R S) (span R coeffs(q)) (span R coeffs(p))
neg : ¬deg(p) - deg(q) ≤ i → 0 ∈ span R coeffs(p) ⊔ HMul.hMul (α := Submodule R S) (span R coeffs(q)) (span R coeffs(p))
⊢ (if deg(p) - deg(q) ≤ i then q.coeff (i - (deg(p) - deg(q))) * p.leadingCoeff else 0) ∈
    span R coeffs(p) ⊔ HMul.hMul (α := Submodule R S) (span R coeffs(q)) (span R coeffs(p))

Tactic:
split_ifs
-- 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 : ℕ
H₀ : ∀ (i : ℕ), p.coeff i ∈ HPow.hPow (α := Submodule R S) spanCoeffs(q) deg(p) * spanCoeffs(p)
hpq : q.degree ≤ p.degree ∧ p ≠ 0
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
hr' : ¬r = 0
i : ℕ
h : deg(p) - deg(q) ≤ i
⊢ q.coeff (i - (deg(p) - deg(q))) * p.leadingCoeff ∈
    span R coeffs(p) ⊔ HMul.hMul (α := Submodule R S) (span R coeffs(q)) (span R coeffs(p))

Tactic:
SetLike.le_def.mp le_sup_right (mul_mem_mul ?_ ?_)

Premises used: Submodule.mul_mem_mul, SetLike.le_def, le_sup_right, Iff.mp
-- 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 : ℕ
H₀ : ∀ (i : ℕ), p.coeff i ∈ HPow.hPow (α := Submodule R S) spanCoeffs(q) deg(p) * spanCoeffs(p)
hpq : q.degree ≤ p.degree ∧ p ≠ 0
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
hr' : ¬r = 0
i : ℕ
h : deg(p) - deg(q) ≤ i
pos : Membership.mem (γ := Submodule R S) (span R coeffs(q)) (q.coeff (i - (deg(p) - deg(q))))
pos₁ : Membership.mem (γ := Submodule R S) (span R coeffs(p)) p.leadingCoeff
⊢ q.coeff (i - (deg(p) - deg(q))) * p.leadingCoeff ∈
    span R coeffs(p) ⊔ HMul.hMul (α := Submodule R S) (span R coeffs(q)) (span R coeffs(p))

Tactic:
refine SetLike.le_def.mp le_sup_right (mul_mem_mul ?_ ?_)

Premises used: Submodule.mul_mem_mul, SetLike.le_def, le_sup_right, Iff.mp
-- 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 : ℕ
H₀ : ∀ (i : ℕ), p.coeff i ∈ HPow.hPow (α := Submodule R S) spanCoeffs(q) deg(p) * spanCoeffs(p)
hpq : q.degree ≤ p.degree ∧ p ≠ 0
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
hr' : ¬r = 0
i : ℕ
h : deg(p) - deg(q) ≤ i
⊢ Membership.mem (γ := Submodule R S) (span R coeffs(q)) (q.coeff (i - (deg(p) - deg(q))))

Tactic:
subset_span ⟨_, rfl⟩

Premises used: Set.Mem, Exists.intro, Submodule.subset_span, rfl
-- 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 : ℕ
H₀ : ∀ (i : ℕ), p.coeff i ∈ HPow.hPow (α := Submodule R S) spanCoeffs(q) deg(p) * spanCoeffs(p)
hpq : q.degree ≤ p.degree ∧ p ≠ 0
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
hr' : ¬r = 0
i : ℕ
h : deg(p) - deg(q) ≤ i
⊢ Membership.mem (γ := Submodule R S) (span R coeffs(q)) (q.coeff (i - (deg(p) - deg(q))))

Tactic:
exact subset_span ⟨_, rfl⟩
-- 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 : ℕ
H₀ : ∀ (i : ℕ), p.coeff i ∈ HPow.hPow (α := Submodule R S) spanCoeffs(q) deg(p) * spanCoeffs(p)
hpq : q.degree ≤ p.degree ∧ p ≠ 0
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
hr' : ¬r = 0
i : ℕ
h : deg(p) - deg(q) ≤ i
⊢ Membership.mem (γ := Submodule R S) (span R coeffs(p)) p.leadingCoeff

Tactic:
subset_span ⟨_, rfl⟩

Premises used: Set.Mem, Exists.intro, Submodule.subset_span, rfl
-- 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 : ℕ
H₀ : ∀ (i : ℕ), p.coeff i ∈ HPow.hPow (α := Submodule R S) spanCoeffs(q) deg(p) * spanCoeffs(p)
hpq : q.degree ≤ p.degree ∧ p ≠ 0
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
hr' : ¬r = 0
i : ℕ
h : deg(p) - deg(q) ≤ i
⊢ Membership.mem (γ := Submodule R S) (span R coeffs(p)) p.leadingCoeff

Tactic:
exact subset_span ⟨_, rfl⟩
-- 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 : ℕ
H₀ : ∀ (i : ℕ), p.coeff i ∈ HPow.hPow (α := Submodule R S) spanCoeffs(q) deg(p) * spanCoeffs(p)
hpq : q.degree ≤ p.degree ∧ p ≠ 0
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
hr' : ¬r = 0
i : ℕ
h : ¬deg(p) - deg(q) ≤ i
⊢ 0 ∈ span R coeffs(p) ⊔ HMul.hMul (α := Submodule R S) (span R coeffs(q)) (span R coeffs(p))

Tactic:
zero_mem _

Premises used: ZeroMemClass.zero_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 : ℕ
H₀ : ∀ (i : ℕ), p.coeff i ∈ HPow.hPow (α := Submodule R S) spanCoeffs(q) deg(p) * spanCoeffs(p)
hpq : q.degree ≤ p.degree ∧ p ≠ 0
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
hr' : ¬r = 0
i : ℕ
h : ¬deg(p) - deg(q) ≤ i
⊢ 0 ∈ span R coeffs(p) ⊔ HMul.hMul (α := Submodule R S) (span R coeffs(q)) (span R coeffs(p))

Tactic:
exact zero_mem _

Premises used: ZeroMemClass.zero_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 : ℕ
H₀ : ∀ (i : ℕ), p.coeff i ∈ HPow.hPow (α := Submodule R S) spanCoeffs(q) deg(p) * spanCoeffs(p)
hpq : q.degree ≤ p.degree ∧ p ≠ 0
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
hr' : ¬r = 0
⊢ span R coeffs(r) ≤ span R coeffs(p) ⊔ HMul.hMul (α := Submodule R S) (span R coeffs(q)) (span R coeffs(p))

Tactic:
have H : span R coeffs(r) ≤ span R coeffs(p) ⊔ span R coeffs(q) * span R coeffs(p) := by
      rw [span_le, ← hr]
      rintro _ ⟨i, rfl⟩
      rw [coeff_sub, ← mul_assoc, coeff_mul_X_pow', coeff_mul_C]
      apply sub_mem
      · exact SetLike.le_def.mp le_sup_left (subset_span (mem_range_self _))
      · split_ifs
        · refine SetLike.le_def.mp le_sup_right (mul_mem_mul ?_ ?_) <;> exact subset_span ⟨_, rfl⟩
        · exact zero_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 : ℕ
H₀ : ∀ (i : ℕ), p.coeff i ∈ HPow.hPow (α := Submodule R S) spanCoeffs(q) deg(p) * spanCoeffs(p)
hpq : q.degree ≤ p.degree ∧ p ≠ 0
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
hr' : ¬r = 0
H : span R coeffs(r) ≤ span R coeffs(p) ⊔ HMul.hMul (α := Submodule R S) (span R coeffs(q)) (span R coeffs(p))
⊢ deg(r) < deg(p)

Tactic:
have deg_r_lt_deg_p : deg(r) < deg(p) := natDegree_lt_natDegree hr' (hr ▸ div_wf_lemma hpq hq)
-- 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
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
hr' : ¬r = 0
H : span R coeffs(r) ≤ span R coeffs(p) ⊔ HMul.hMul (α := Submodule R S) (span R coeffs(q)) (span R coeffs(p))
deg_r_lt_deg_p : deg(r) < deg(p)
⊢ HPow.hPow (α := Submodule R S) spanCoeffs(q) deg(r) * spanCoeffs(r) ≤
    HPow.hPow (α := Submodule R S) spanCoeffs(q) deg(r) *
      (1 ⊔ (span R coeffs(p) ⊔ HMul.hMul (α := Submodule R S) (span R coeffs(q)) (span R coeffs(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 : ℕ
H₀ : ∀ (i : ℕ), p.coeff i ∈ HPow.hPow (α := Submodule R S) spanCoeffs(q) deg(p) * spanCoeffs(p)
hpq : q.degree ≤ p.degree ∧ p ≠ 0
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
hr' : ¬r = 0
H : span R coeffs(r) ≤ span R coeffs(p) ⊔ HMul.hMul (α := Submodule R S) (span R coeffs(q)) (span R coeffs(p))
deg_r_lt_deg_p : deg(r) < deg(p)
bc :
  1 ⊔ (span R coeffs(p) ⊔ HMul.hMul (α := Submodule R S) (span R coeffs(q)) (span R coeffs(p))) ≤
    HMul.hMul (α := Submodule R S) spanCoeffs(q) spanCoeffs(p)
⊢ HPow.hPow (α := Submodule R S) spanCoeffs(q) deg(r) *
      (1 ⊔ (span R coeffs(p) ⊔ HMul.hMul (α := Submodule R S) (span R coeffs(q)) (span R coeffs(p)))) ≤
    HPow.hPow (α := Submodule R S) spanCoeffs(q) deg(r) * HMul.hMul (α := Submodule R S) spanCoeffs(q) 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 : ℕ
H₀ : ∀ (i : ℕ), p.coeff i ∈ HPow.hPow (α := Submodule R S) spanCoeffs(q) deg(p) * spanCoeffs(p)
hpq : q.degree ≤ p.degree ∧ p ≠ 0
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
hr' : ¬r = 0
H : span R coeffs(r) ≤ span R coeffs(p) ⊔ HMul.hMul (α := Submodule R S) (span R coeffs(q)) (span R coeffs(p))
deg_r_lt_deg_p : deg(r) < deg(p)
bc :
  1 ≤ HMul.hMul (α := Submodule R S) spanCoeffs(q) spanCoeffs(p) ∧
    span R coeffs(p) ≤ HMul.hMul (α := Submodule R S) spanCoeffs(q) spanCoeffs(p) ∧
      HMul.hMul (α := Submodule R S) (span R coeffs(q)) (span R coeffs(p)) ≤
        HMul.hMul (α := Submodule R S) spanCoeffs(q) spanCoeffs(p)
⊢ 1 ⊔ (span R coeffs(p) ⊔ HMul.hMul (α := Submodule R S) (span R coeffs(q)) (span R coeffs(p))) ≤
    HMul.hMul (α := Submodule R S) spanCoeffs(q) spanCoeffs(p)

Tactic:
simp only [sup_le_iff]

Premises used: sup_le_iff
-- 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
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
hr' : ¬r = 0
H : span R coeffs(r) ≤ span R coeffs(p) ⊔ HMul.hMul (α := Submodule R S) (span R coeffs(q)) (span R coeffs(p))
deg_r_lt_deg_p : deg(r) < deg(p)
⊢ 1 ≤ HMul.hMul (α := Submodule R S) spanCoeffs(q) spanCoeffs(p) ∧
    span R coeffs(p) ≤ HMul.hMul (α := Submodule R S) spanCoeffs(q) spanCoeffs(p) ∧
      HMul.hMul (α := Submodule R S) (span R coeffs(q)) (span R coeffs(p)) ≤
        HMul.hMul (α := Submodule R S) spanCoeffs(q) spanCoeffs(p)

Tactic:
⟨one_le_mul le_sup_left le_sup_left, ?_, mul_le_mul' le_sup_right le_sup_right⟩

Premises used: le_sup_left, le_sup_right, And.intro, one_le_mul, mul_le_mul'
-- 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
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
hr' : ¬r = 0
H : span R coeffs(r) ≤ span R coeffs(p) ⊔ HMul.hMul (α := Submodule R S) (span R coeffs(q)) (span R coeffs(p))
deg_r_lt_deg_p : deg(r) < deg(p)
bc : span R coeffs(p) ≤ HMul.hMul (α := Submodule R S) spanCoeffs(q) spanCoeffs(p)
⊢ 1 ≤ HMul.hMul (α := Submodule R S) spanCoeffs(q) spanCoeffs(p) ∧
    span R coeffs(p) ≤ HMul.hMul (α := Submodule R S) spanCoeffs(q) spanCoeffs(p) ∧
      HMul.hMul (α := Submodule R S) (span R coeffs(q)) (span R coeffs(p)) ≤
        HMul.hMul (α := Submodule R S) spanCoeffs(q) spanCoeffs(p)

Tactic:
refine ⟨one_le_mul le_sup_left le_sup_left, ?_, mul_le_mul' le_sup_right 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)
hpq : q.degree ≤ p.degree ∧ p ≠ 0
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
hr' : ¬r = 0
H : span R coeffs(r) ≤ span R coeffs(p) ⊔ HMul.hMul (α := Submodule R S) (span R coeffs(q)) (span R coeffs(p))
deg_r_lt_deg_p : deg(r) < deg(p)
bc : span R coeffs(p) ≤ spanCoeffs(p) ⊔ HMul.hMul (α := Submodule R S) (span R coeffs(q)) spanCoeffs(p)
⊢ span R coeffs(p) ≤ HMul.hMul (α := Submodule R S) spanCoeffs(q) spanCoeffs(p)

Tactic:
rw [Submodule.sup_mul, one_mul]

Premises used: Submodule.sup_mul, one_mul