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
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)
⊢ span R coeffs(p) ≤ spanCoeffs(p) ⊔ HMul.hMul (α := Submodule R S) (span R coeffs(q)) spanCoeffs(p)

Tactic:
le_sup_of_le_left le_sup_right

Premises used: Set.Mem, le_sup_of_le_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)
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)
⊢ span R coeffs(p) ≤ spanCoeffs(p) ⊔ HMul.hMul (α := Submodule R S) (span R coeffs(q)) spanCoeffs(p)

Tactic:
exact le_sup_of_le_left le_sup_right

Premises used: le_sup_of_le_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)
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)
rw :
  HPow.hPow (α := Submodule R S) spanCoeffs(q) deg(r) * HMul.hMul (α := Submodule R S) spanCoeffs(q) spanCoeffs(p) =
    HPow.hPow (α := Submodule R S) spanCoeffs(q) deg(r) * spanCoeffs(q) * spanCoeffs(p)
rw₁ rw₂ :
  HPow.hPow (α := Submodule R S) spanCoeffs(q) deg(r) * HMul.hMul (α := Submodule R S) spanCoeffs(q) spanCoeffs(p) =
    HPow.hPow (α := Submodule R S) spanCoeffs(q) deg(r) * HMul.hMul (α := Submodule R S) spanCoeffs(q) spanCoeffs(p)
⊢ HPow.hPow (α := Submodule R S) spanCoeffs(q) deg(r) * HMul.hMul (α := Submodule R S) spanCoeffs(q) spanCoeffs(p) =
    HPow.hPow (α := Submodule R S) spanCoeffs(q) (deg(r) + 1) * spanCoeffs(p)

Tactic:
rw [pow_succ, mul_assoc]

Premises used: pow_succ, mul_assoc
-- 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 : LE.le (α := Submodule R S) 1 spanCoeffs(q)
bc₁ : deg(r) + 1 ≤ deg(p)
⊢ HPow.hPow (α := Submodule R S) spanCoeffs(q) (deg(r) + 1) * spanCoeffs(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 : ℕ
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)
⊢ LE.le (α := Submodule R S) 1 spanCoeffs(q)

Tactic:
le_sup_left

Premises used: le_sup_left, Set.Mem, setOf
-- 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)
⊢ deg(r) + 1 ≤ deg(p)

Tactic:
deg_r_lt_deg_p

Premises used: Nat.lt
-- 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)
⊢ LE.le (α := Submodule R S) 1 spanCoeffs(q)

Tactic:
exacts [le_sup_left, deg_r_lt_deg_p]

Premises used: le_sup_left
-- 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(p) * spanCoeffs(p)

Tactic:
have H'' := calc
      spanCoeffs(q) ^ deg(r) * spanCoeffs(r)
      _ ≤ spanCoeffs(q) ^ deg(r) *
          (1 ⊔ (span R coeffs(p) ⊔ span R coeffs(q) * span R coeffs(p))) := by gcongr
      _ ≤ spanCoeffs(q) ^ deg(r) * (spanCoeffs(q) * spanCoeffs(p)) := by
        gcongr
        simp only [sup_le_iff]
        refine ⟨one_le_mul le_sup_left le_sup_left, ?_, mul_le_mul' le_sup_right le_sup_right⟩
        rw [Submodule.sup_mul, one_mul]
        exact le_sup_of_le_left le_sup_right
      _ = spanCoeffs(q) ^ (deg(r) + 1) * spanCoeffs(p) := by rw [pow_succ, mul_assoc]
      _ ≤ spanCoeffs(q) ^ deg(p) * spanCoeffs(p) := by gcongr; exacts [le_sup_left, deg_r_lt_deg_p]
-- 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)
H'' :
  HPow.hPow (α := Submodule R S) spanCoeffs(q) deg(r) * spanCoeffs(r) ≤
    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:
⟨add_mem ?_ ?_, ?_⟩

Premises used: And.intro, AddMemClass.add_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_lt_deg_p : deg(r) < deg(p)
H'' :
  HPow.hPow (α := Submodule R S) spanCoeffs(q) deg(r) * spanCoeffs(r) ≤
    HPow.hPow (α := Submodule R S) spanCoeffs(q) deg(p) * spanCoeffs(p)
neg :
  (p.leadingCoeff * if i = deg(p) - deg(q) then 1 else 0) ∈
    HPow.hPow (α := Submodule R S) spanCoeffs(q) deg(p) * spanCoeffs(p)
neg₁ : (r.divModByMonicAux hq).1.coeff i ∈ HPow.hPow (α := Submodule R S) spanCoeffs(q) deg(p) * spanCoeffs(p)
neg₂ : (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:
refine ⟨add_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_lt_deg_p : deg(r) < deg(p)
H'' :
  HPow.hPow (α := Submodule R S) spanCoeffs(q) deg(r) * spanCoeffs(r) ≤
    HPow.hPow (α := Submodule R S) spanCoeffs(q) deg(p) * spanCoeffs(p)
pos : i = deg(p) - deg(q) → p.leadingCoeff * 1 ∈ HPow.hPow (α := Submodule R S) spanCoeffs(q) deg(p) * spanCoeffs(p)
neg : ¬i = deg(p) - deg(q) → p.leadingCoeff * 0 ∈ HPow.hPow (α := Submodule R S) spanCoeffs(q) deg(p) * spanCoeffs(p)
⊢ (p.leadingCoeff * if i = deg(p) - deg(q) then 1 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 : 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)
H'' :
  HPow.hPow (α := Submodule R S) spanCoeffs(q) deg(r) * spanCoeffs(r) ≤
    HPow.hPow (α := Submodule R S) spanCoeffs(q) deg(p) * spanCoeffs(p)
h : i = deg(p) - deg(q)
pos : p.leadingCoeff ∈ HPow.hPow (α := Submodule R S) spanCoeffs(q) deg(p) * spanCoeffs(p)
⊢ p.leadingCoeff * 1 ∈ HPow.hPow (α := Submodule R S) spanCoeffs(q) deg(p) * spanCoeffs(p)

Tactic:
simp only [mul_one, mul_zero]

Premises used: MulZeroClass.mul_zero, mul_one
-- 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)
H'' :
  HPow.hPow (α := Submodule R S) spanCoeffs(q) deg(r) * spanCoeffs(r) ≤
    HPow.hPow (α := Submodule R S) spanCoeffs(q) deg(p) * spanCoeffs(p)
h : ¬i = deg(p) - deg(q)
neg : 0 ∈ HPow.hPow (α := Submodule R S) spanCoeffs(q) deg(p) * spanCoeffs(p)
⊢ p.leadingCoeff * 0 ∈ HPow.hPow (α := Submodule R S) spanCoeffs(q) deg(p) * spanCoeffs(p)

Tactic:
simp only [mul_one, mul_zero]

Premises used: MulZeroClass.mul_zero, mul_one
-- 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)
H'' :
  HPow.hPow (α := Submodule R S) spanCoeffs(q) deg(r) * spanCoeffs(r) ≤
    HPow.hPow (α := Submodule R S) spanCoeffs(q) deg(p) * spanCoeffs(p)
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 : 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)
H'' :
  HPow.hPow (α := Submodule R S) spanCoeffs(q) deg(r) * spanCoeffs(r) ≤
    HPow.hPow (α := Submodule R S) spanCoeffs(q) deg(p) * spanCoeffs(p)
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 : 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)
H'' :
  HPow.hPow (α := Submodule R S) spanCoeffs(q) deg(r) * spanCoeffs(r) ≤
    HPow.hPow (α := Submodule R S) spanCoeffs(q) deg(p) * spanCoeffs(p)
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
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)
H'' :
  HPow.hPow (α := Submodule R S) spanCoeffs(q) deg(r) * spanCoeffs(r) ≤
    HPow.hPow (α := Submodule R S) spanCoeffs(q) deg(p) * spanCoeffs(p)
⊢ (r.divModByMonicAux hq).1.coeff i ∈ HPow.hPow (α := Submodule R S) spanCoeffs(q) deg(p) * spanCoeffs(p)

Tactic:
H'' (coeff_divModByMonicAux_mem_span_pow_mul_span r _ hq i).1

Premises used: And.left
-- 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)
H'' :
  HPow.hPow (α := Submodule R S) spanCoeffs(q) deg(r) * spanCoeffs(r) ≤
    HPow.hPow (α := Submodule R S) spanCoeffs(q) deg(p) * spanCoeffs(p)
⊢ (r.divModByMonicAux hq).1.coeff i ∈ HPow.hPow (α := Submodule R S) spanCoeffs(q) deg(p) * spanCoeffs(p)

Tactic:
exact H'' (coeff_divModByMonicAux_mem_span_pow_mul_span r _ hq i).1

Premises used: And.left
-- 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)
H'' :
  HPow.hPow (α := Submodule R S) spanCoeffs(q) deg(r) * spanCoeffs(r) ≤
    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:
H'' (coeff_divModByMonicAux_mem_span_pow_mul_span _ _ hq i).2

Premises used: And.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)
H'' :
  HPow.hPow (α := Submodule R S) spanCoeffs(q) deg(r) * spanCoeffs(r) ≤
    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:
exact H'' (coeff_divModByMonicAux_mem_span_pow_mul_span _ _ hq i).2

Premises used: And.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]
Mp : Submodule R S
hp : ∀ (i : ℕ), p.coeff i ∈ Mp
hp' : 1 ∈ Mp
Mq : Submodule R S
hq : ∀ (i : ℕ), q.coeff i ∈ Mq
hq' : 1 ∈ Mq
i : ℕ
pos : ∀ (H : q.Monic), (p.divModByMonicAux H).2.coeff i ∈ Mq ^ deg(p) * Mp
neg : ∀ (H : ¬q.Monic), p.coeff i ∈ Mq ^ deg(p) * Mp
⊢ coeff (if hq : q.Monic then (p.divModByMonicAux hq).2 else p) i ∈ Mq ^ deg(p) * Mp

Tactic:
split_ifs with 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]
Mp : Submodule R S
hp : ∀ (i : ℕ), p.coeff i ∈ Mp
hp' : 1 ∈ Mp
Mq : Submodule R S
hq : ∀ (i : ℕ), q.coeff i ∈ Mq
hq' : 1 ∈ Mq
i : ℕ
H : q.Monic
⊢ (p.divModByMonicAux H).2.coeff i ∈ Mq ^ deg(p) * Mp

Tactic:
SetLike.le_def.mp ?_ (coeff_divModByMonicAux_mem_span_pow_mul_span (R := R) p q H i).2

Premises used: SetLike.le_def, Polynomial.coeff_divModByMonicAux_mem_span_pow_mul_span, And.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]
Mp : Submodule R S
hp : ∀ (i : ℕ), p.coeff i ∈ Mp
hp' : 1 ∈ Mp
Mq : Submodule R S
hq : ∀ (i : ℕ), q.coeff i ∈ Mq
hq' : 1 ∈ Mq
i : ℕ
H : q.Monic
pos : HPow.hPow (α := Submodule R S) spanCoeffs(q) deg(p) * spanCoeffs(p) ≤ Mq ^ deg(p) * Mp
⊢ (p.divModByMonicAux H).2.coeff i ∈ Mq ^ deg(p) * Mp

Tactic:
refine SetLike.le_def.mp ?_ (coeff_divModByMonicAux_mem_span_pow_mul_span (R := R) p q H i).2

Premises used: SetLike.le_def, Polynomial.coeff_divModByMonicAux_mem_span_pow_mul_span, And.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]
Mp : Submodule R S
hp : ∀ (i : ℕ), p.coeff i ∈ Mp
hp' : 1 ∈ Mp
Mq : Submodule R S
hq : ∀ (i : ℕ), q.coeff i ∈ Mq
hq' : 1 ∈ Mq
i : ℕ
H : q.Monic
pos : spanCoeffs(q) ≤ Mq
pos₁ : spanCoeffs(p) ≤ Mp
⊢ HPow.hPow (α := Submodule R S) spanCoeffs(q) deg(p) * spanCoeffs(p) ≤ Mq ^ deg(p) * Mp

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]
Mp : Submodule R S
hp : ∀ (i : ℕ), p.coeff i ∈ Mp
hp' : 1 ∈ Mp
Mq : Submodule R S
hq : ∀ (i : ℕ), q.coeff i ∈ Mq
hq' : 1 ∈ Mq
i : ℕ
H : q.Monic
⊢ 1 ≤ Mq

Tactic:
simpa
-- 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]
Mp : Submodule R S
hp : ∀ (i : ℕ), p.coeff i ∈ Mp
hp' : 1 ∈ Mp
Mq : Submodule R S
hq : ∀ (i : ℕ), q.coeff i ∈ Mq
hq' : 1 ∈ Mq
i : ℕ
H : q.Monic
⊢ Submodule.span R coeffs(q) ≤ Mq

Tactic:
simpa [Submodule.span_le, Set.range_subset_iff]

Premises used: Set.range_subset_iff, 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]
Mp : Submodule R S
hp : ∀ (i : ℕ), p.coeff i ∈ Mp
hp' : 1 ∈ Mp
Mq : Submodule R S
hq : ∀ (i : ℕ), q.coeff i ∈ Mq
hq' : 1 ∈ Mq
i : ℕ
H : q.Monic
⊢ spanCoeffs(q) ≤ Mq

Tactic:
exact sup_le (by simpa) (by simpa [Submodule.span_le, Set.range_subset_iff])

Premises used: sup_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]
Mp : Submodule R S
hp : ∀ (i : ℕ), p.coeff i ∈ Mp
hp' : 1 ∈ Mp
Mq : Submodule R S
hq : ∀ (i : ℕ), q.coeff i ∈ Mq
hq' : 1 ∈ Mq
i : ℕ
H : q.Monic
⊢ 1 ≤ Mp

Tactic:
simpa
-- 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]
Mp : Submodule R S
hp : ∀ (i : ℕ), p.coeff i ∈ Mp
hp' : 1 ∈ Mp
Mq : Submodule R S
hq : ∀ (i : ℕ), q.coeff i ∈ Mq
hq' : 1 ∈ Mq
i : ℕ
H : q.Monic
⊢ Submodule.span R coeffs(p) ≤ Mp

Tactic:
simpa [Submodule.span_le, Set.range_subset_iff]

Premises used: Set.range_subset_iff, 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]
Mp : Submodule R S
hp : ∀ (i : ℕ), p.coeff i ∈ Mp
hp' : 1 ∈ Mp
Mq : Submodule R S
hq : ∀ (i : ℕ), q.coeff i ∈ Mq
hq' : 1 ∈ Mq
i : ℕ
H : q.Monic
⊢ spanCoeffs(p) ≤ Mp

Tactic:
exact sup_le (by simpa) (by simpa [Submodule.span_le, Set.range_subset_iff])

Premises used: sup_le