-- 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 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
⊢ (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)).1.coeff
        i ∈
      spanCoeffs(q) ^ deg(p) * spanCoeffs(p) ∧
    (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)).2.coeff
        i ∈
      spanCoeffs(q) ^ deg(p) * spanCoeffs(p)

Tactic:
simp only [coeff_add, coeff_C_mul, coeff_X_pow]

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
⊢ (p.leadingCoeff * if i = deg(p) - deg(q) then 1 else 0) +
        ((p - q * (C p.leadingCoeff * X ^ (deg(p) - deg(q)))).divModByMonicAux hq).1.coeff i ∈
      spanCoeffs(q) ^ deg(p) * spanCoeffs(p) ∧
    ((p - q * (C p.leadingCoeff * X ^ (deg(p) - deg(q)))).divModByMonicAux hq).2.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(p) ⊔ span R coeffs(q) * spanCoeffs(p)

Tactic:
exact le_sup_of_le_left le_sup_right

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 : ℕ
⊢ (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)

Tactic:
have H₀ (i) : p.coeff i ∈ spanCoeffs(q) ^ deg(p) * spanCoeffs(p) := by
  refine Submodule.mul_le_mul_left (pow_le_pow_left' le_sup_left _) ?_
  simp only [one_pow, one_mul]
  exact SetLike.le_def.mp le_sup_right (subset_span (mem_range_self i))

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)
⊢ (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 neg.refine_2
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)
H'' : spanCoeffs(q) ^ deg(r) * spanCoeffs(r) ≤ spanCoeffs(q) ^ deg(p) * spanCoeffs(p)
⊢ (r.divModByMonicAux hq).1.coeff i ∈ spanCoeffs(q) ^ deg(p) * spanCoeffs(p)

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

Result:
no goals

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)
⊢ (0, p).1.coeff i ∈ spanCoeffs(q) ^ deg(p) * spanCoeffs(p) ∧ (0, p).2.coeff i ∈ spanCoeffs(q) ^ deg(p) * spanCoeffs(p)

Tactic:
simpa using H₀ _

Result:
no goals