-- Mathlib/Algebra/Polynomial/CoeffMem.lean
lemma coeff_divModByMonicAux_mem_span_pow_mul_span : ∀ (p q : S[X]) (hq : q.Monic) (i),
    (p.divModByMonicAux hq).1.coeff i ∈ spanCoeffs(q) ^ deg(p) * spanCoeffs(p) ∧
    (p.divModByMonicAux hq).2.coeff i ∈ spanCoeffs(q) ^ deg(p) * spanCoeffs(p)
  | p, q, hq, i => by
    rw [divModByMonicAux]
    have H₀ (i) : p.coeff i ∈ spanCoeffs(q) ^ deg(p) * spanCoeffs(p)

Proof state:
case bc
R : Type u_2
S : Type u_3
inst✝² : CommRing R
inst✝¹ : Ring S
inst✝ : Algebra R S
p q : S[X]
hq : q.Monic
i : ℕ
H₀ : ∀ (i : ℕ), p.coeff i ∈ spanCoeffs(q) ^ deg(p) * spanCoeffs(p)
hpq : q.degree ≤ p.degree ∧ p ≠ 0
r : S[X]
hr : p - q * (C p.leadingCoeff * X ^ (deg(p) - deg(q))) = r
hr' : ¬r = 0
H : span R coeffs(r) ≤ span R coeffs(p) ⊔ span R coeffs(q) * span R coeffs(p)
deg_r_lt_deg_p : deg(r) < deg(p)
⊢ span R coeffs(p) ≤ spanCoeffs(q) * spanCoeffs(p)

Tactic:
rw [Submodule.sup_mul, one_mul]

Result:
case bc
R : Type u_2
S : Type u_3
inst✝² : CommRing R
inst✝¹ : Ring S
inst✝ : Algebra R S
p q : S[X]
hq : q.Monic
i : ℕ
H₀ : ∀ (i : ℕ), p.coeff i ∈ spanCoeffs(q) ^ deg(p) * spanCoeffs(p)
hpq : q.degree ≤ p.degree ∧ p ≠ 0
r : S[X]
hr : p - q * (C p.leadingCoeff * X ^ (deg(p) - deg(q))) = r
hr' : ¬r = 0
H : span R coeffs(r) ≤ span R coeffs(p) ⊔ span R coeffs(q) * span R coeffs(p)
deg_r_lt_deg_p : deg(r) < deg(p)
⊢ span R coeffs(p) ≤ spanCoeffs(p) ⊔ span R coeffs(q) * spanCoeffs(p)

Proof state:
case neg
R : Type u_2
S : Type u_3
inst✝² : CommRing R
inst✝¹ : Ring S
inst✝ : Algebra R S
p q : S[X]
hq : q.Monic
i✝ : ℕ
H₀ : ∀ (i : ℕ), p.coeff i ∈ spanCoeffs(q) ^ deg(p) * spanCoeffs(p)
hpq : q.degree ≤ p.degree ∧ p ≠ 0
r : S[X]
hr : p - q * (C p.leadingCoeff * X ^ (deg(p) - deg(q))) = r
hr' : ¬r = 0
i : ℕ
h✝ : ¬deg(p) - deg(q) ≤ i
⊢ 0 ∈ span R coeffs(p) ⊔ span R coeffs(q) * span R coeffs(p)

Tactic:
exact zero_mem _

Result:
no goals

Proof state:
R : Type u_2
S : Type u_3
inst✝² : CommRing R
inst✝¹ : Ring S
inst✝ : Algebra R S
p q : S[X]
hq : q.Monic
i : ℕ
⊢ (p.divModByMonicAux hq).1.coeff i ∈ spanCoeffs(q) ^ deg(p) * spanCoeffs(p) ∧
    (p.divModByMonicAux hq).2.coeff i ∈ spanCoeffs(q) ^ deg(p) * spanCoeffs(p)

Tactic:
rw [divModByMonicAux]

Result:
R : Type u_2
S : Type u_3
inst✝² : CommRing R
inst✝¹ : Ring S
inst✝ : Algebra R S
p q : S[X]
hq : q.Monic
i : ℕ
⊢ (if h : q.degree ≤ p.degree ∧ p ≠ 0 then
              let z := C p.leadingCoeff * X ^ (deg(p) - deg(q));
              let_fun _wf := ⋯;
              let dm := (p - q * z).divModByMonicAux hq;
              (z + dm.1, dm.2)
            else (0, p)).1.coeff
        i ∈
      spanCoeffs(q) ^ deg(p) * spanCoeffs(p) ∧
    (if h : q.degree ≤ p.degree ∧ p ≠ 0 then
              let z := C p.leadingCoeff * X ^ (deg(p) - deg(q));
              let_fun _wf := ⋯;
              let dm := (p - q * z).divModByMonicAux hq;
              (z + dm.1, dm.2)
            else (0, p)).2.coeff
        i ∈
      spanCoeffs(q) ^ deg(p) * spanCoeffs(p)

Proof state:
case pos
R : Type u_2
S : Type u_3
inst✝² : CommRing R
inst✝¹ : Ring S
inst✝ : Algebra R S
p q : S[X]
hq : q.Monic
i : ℕ
H₀ : ∀ (i : ℕ), p.coeff i ∈ spanCoeffs(q) ^ deg(p) * spanCoeffs(p)
hpq : q.degree ≤ p.degree ∧ p ≠ 0
r : S[X]
hr : p - q * (C p.leadingCoeff * X ^ (deg(p) - deg(q))) = r
hr' : r = 0
⊢ (p.leadingCoeff * if i = deg(p) - deg(q) then 1 else 0) + (r.divModByMonicAux hq).1.coeff i ∈
      spanCoeffs(q) ^ deg(p) * spanCoeffs(p) ∧
    (r.divModByMonicAux hq).2.coeff i ∈ 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, Prod.mk_zero_zero,
  Prod.fst_zero, coeff_zero, add_zero, Prod.snd_zero, Submodule.zero_mem, and_true]

Result:
case pos
R : Type u_2
S : Type u_3
inst✝² : CommRing R
inst✝¹ : Ring S
inst✝ : Algebra R S
p q : S[X]
hq : q.Monic
i : ℕ
H₀ : ∀ (i : ℕ), p.coeff i ∈ spanCoeffs(q) ^ deg(p) * spanCoeffs(p)
hpq : q.degree ≤ p.degree ∧ p ≠ 0
r : S[X]
hr : p - q * (C p.leadingCoeff * X ^ (deg(p) - deg(q))) = r
hr' : r = 0
⊢ (if i = deg(p) - deg(q) then p.leadingCoeff else 0) ∈ spanCoeffs(q) ^ deg(p) * spanCoeffs(p)

Proof state:
case pos
R : Type u_2
S : Type u_3
inst✝² : CommRing R
inst✝¹ : Ring S
inst✝ : Algebra R S
p q : S[X]
hq : q.Monic
i : ℕ
H₀ : ∀ (i : ℕ), p.coeff i ∈ spanCoeffs(q) ^ deg(p) * spanCoeffs(p)
hpq : q.degree ≤ p.degree ∧ p ≠ 0
r : S[X]
hr : p - q * (C p.leadingCoeff * X ^ (deg(p) - deg(q))) = r
hr' : r = 0
⊢ (if i = deg(p) - deg(q) then p.leadingCoeff else 0) ∈ spanCoeffs(q) ^ deg(p) * spanCoeffs(p)

Tactic:
split_ifs

Result:
case pos
R : Type u_2
S : Type u_3
inst✝² : CommRing R
inst✝¹ : Ring S
inst✝ : Algebra R S
p q : S[X]
hq : q.Monic
i : ℕ
H₀ : ∀ (i : ℕ), p.coeff i ∈ spanCoeffs(q) ^ deg(p) * spanCoeffs(p)
hpq : q.degree ≤ p.degree ∧ p ≠ 0
r : S[X]
hr : p - q * (C p.leadingCoeff * X ^ (deg(p) - deg(q))) = r
hr' : r = 0
h✝ : i = deg(p) - deg(q)
⊢ p.leadingCoeff ∈ spanCoeffs(q) ^ deg(p) * spanCoeffs(p)

case neg
R : Type u_2
S : Type u_3
inst✝² : CommRing R
inst✝¹ : Ring S
inst✝ : Algebra R S
p q : S[X]
hq : q.Monic
i : ℕ
H₀ : ∀ (i : ℕ), p.coeff i ∈ spanCoeffs(q) ^ deg(p) * spanCoeffs(p)
hpq : q.degree ≤ p.degree ∧ p ≠ 0
r : S[X]
hr : p - q * (C p.leadingCoeff * X ^ (deg(p) - deg(q))) = r
hr' : r = 0
h✝ : ¬i = deg(p) - deg(q)
⊢ 0 ∈ spanCoeffs(q) ^ deg(p) * spanCoeffs(p)

Proof state:
case pos
R : Type u_2
S : Type u_3
inst✝² : CommRing R
inst✝¹ : Ring S
inst✝ : Algebra R S
p q : S[X]
hq : q.Monic
i✝ : ℕ
H₀ : ∀ (i : ℕ), p.coeff i ∈ spanCoeffs(q) ^ deg(p) * spanCoeffs(p)
hpq : q.degree ≤ p.degree ∧ p ≠ 0
r : S[X]
hr : p - q * (C p.leadingCoeff * 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) ⊔ span R coeffs(q) * span R coeffs(p)

Tactic:
refine SetLike.le_def.mp le_sup_right (mul_mem_mul ?_ ?_) <;> exact subset_span ⟨_, rfl⟩

Result:
no goals

Proof state:
case intro
R : Type u_2
S : Type u_3
inst✝² : CommRing R
inst✝¹ : Ring S
inst✝ : Algebra R S
p q : S[X]
hq : q.Monic
i✝ : ℕ
H₀ : ∀ (i : ℕ), p.coeff i ∈ spanCoeffs(q) ^ deg(p) * spanCoeffs(p)
hpq : q.degree ≤ p.degree ∧ p ≠ 0
r : S[X]
hr : p - q * (C p.leadingCoeff * X ^ (deg(p) - deg(q))) = r
hr' : ¬r = 0
i : ℕ
⊢ (p - q * (C p.leadingCoeff * X ^ (deg(p) - deg(q)))).coeff i ∈
    ↑(span R coeffs(p) ⊔ span R coeffs(q) * span R coeffs(p))

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

Result:
case intro
R : Type u_2
S : Type u_3
inst✝² : CommRing R
inst✝¹ : Ring S
inst✝ : Algebra R S
p q : S[X]
hq : q.Monic
i✝ : ℕ
H₀ : ∀ (i : ℕ), p.coeff i ∈ spanCoeffs(q) ^ deg(p) * spanCoeffs(p)
hpq : q.degree ≤ p.degree ∧ p ≠ 0
r : S[X]
hr : p - q * (C p.leadingCoeff * X ^ (deg(p) - deg(q))) = r
hr' : ¬r = 0
i : ℕ
⊢ (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) ⊔ span R coeffs(q) * span R coeffs(p))

Proof state:
R : Type u_2
S : Type u_3
inst✝² : CommRing R
inst✝¹ : Ring S
inst✝ : Algebra R S
p q : S[X]
hq : q.Monic
i : ℕ
H₀ : ∀ (i : ℕ), p.coeff i ∈ spanCoeffs(q) ^ deg(p) * spanCoeffs(p)
hpq : q.degree ≤ p.degree ∧ p ≠ 0
r : S[X]
hr : p - q * (C p.leadingCoeff * X ^ (deg(p) - deg(q))) = r
hr' : ¬r = 0
⊢ span R coeffs(r) ≤ span R coeffs(p) ⊔ span R coeffs(q) * span R coeffs(p)

Tactic:
rw [span_le, ← hr]

Result:
R : Type u_2
S : Type u_3
inst✝² : CommRing R
inst✝¹ : Ring S
inst✝ : Algebra R S
p q : S[X]
hq : q.Monic
i : ℕ
H₀ : ∀ (i : ℕ), p.coeff i ∈ spanCoeffs(q) ^ deg(p) * spanCoeffs(p)
hpq : q.degree ≤ p.degree ∧ p ≠ 0
r : S[X]
hr : p - q * (C p.leadingCoeff * X ^ (deg(p) - deg(q))) = r
hr' : ¬r = 0
⊢ coeffs(p - q * (C p.leadingCoeff * X ^ (deg(p) - deg(q)))) ⊆ ↑(span R coeffs(p) ⊔ span R coeffs(q) * span R coeffs(p))