awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.CoeffMem (goal)
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)
⊢ 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)
have 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)
Tactic: split_ifs with hpq
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.CoeffMem (goal)
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
        (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)
have 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)
Tactic: simp only [coeff_add, coeff_C_mul, coeff_X_pow]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.CoeffMem (goal)
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
⊢ (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)
have 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)
Tactic: generalize hr : (p - q * (C p.leadingCoeff * X ^ (deg(p) - deg(q)))) = r
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.CoeffMem (goal)
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
⊢ (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)
have 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)
Tactic: by_cases hr' : r = 0
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.CoeffMem (goal)
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)
⊢ (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)
have 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)
Tactic: by_cases hr' : r = 0
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.CoeffMem (goal)
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
⊢ (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)
have pos : (if i = deg(p) - deg(q) then p.leadingCoeff else 0) ∈
  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]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.CoeffMem (goal)
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
⊢ (if i = deg(p) - deg(q) then p.leadingCoeff else 0) ∈
    HPow.hPow (α := Submodule R S) spanCoeffs(q) deg(p) * spanCoeffs(p)
have pos : i = deg(p) - deg(q) → p.leadingCoeff ∈ HPow.hPow (α := Submodule R S) spanCoeffs(q) deg(p) * spanCoeffs(p)
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.CoeffMem (goal)
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)
⊢ (if i = deg(p) - deg(q) then p.leadingCoeff else 0) ∈
    HPow.hPow (α := Submodule R S) spanCoeffs(q) deg(p) * spanCoeffs(p)
have neg : ¬i = deg(p) - deg(q) → 0 ∈ HPow.hPow (α := Submodule R S) spanCoeffs(q) deg(p) * spanCoeffs(p)
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.CoeffMem (goal)
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))
have 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)
Tactic: rw [span_le, ← hr]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.CoeffMem (goal)
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 -
          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)
have 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)
Tactic: rw [coeff_sub, ← mul_assoc, coeff_mul_X_pow', coeff_mul_C]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.CoeffMem (goal)
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 - 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)
have hx : p.coeff i ∈ span R coeffs(p) ⊔ HMul.hMul (α := Submodule R S) (span R coeffs(q)) (span R coeffs(p))
Tactic: apply sub_mem
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.CoeffMem (goal)
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))
⊢ (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)
have 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))
Tactic: apply sub_mem
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.CoeffMem (goal)
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 : ℕ
⊢ (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))
have 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))
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.CoeffMem (goal)
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))
⊢ (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))
have neg : ¬deg(p) - deg(q) ≤ i → 0 ∈ span R coeffs(p) ⊔ HMul.hMul (α := Submodule R S) (span R coeffs(q)) (span R coeffs(p))
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.CoeffMem (goal)
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))
have pos : Membership.mem (γ := Submodule R S) (span R coeffs(q)) (q.coeff (i - (deg(p) - deg(q))))
Tactic: refine SetLike.le_def.mp le_sup_right (mul_mem_mul ?_ ?_)
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.CoeffMem (goal)
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))))
⊢ 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))
have pos₁ : Membership.mem (γ := Submodule R S) (span R coeffs(p)) p.leadingCoeff
Tactic: refine SetLike.le_def.mp le_sup_right (mul_mem_mul ?_ ?_)
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.CoeffMem (hypothesis)
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
⊢ (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)
have H : 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 _
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.CoeffMem (hypothesis)
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))
⊢ (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)
have deg_r_lt_deg_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)
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.CoeffMem (goal)
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) *
      (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)
have 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)
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.CoeffMem (goal)
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 ⊔ (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)
have 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)
Tactic: simp only [sup_le_iff]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.CoeffMem (goal)
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)
have bc : 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⟩