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)
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) ≤ HMul.hMul (α := Submodule R S) spanCoeffs(q) spanCoeffs(p)
have bc : span R coeffs(p) ≤ spanCoeffs(p) ⊔ HMul.hMul (α := Submodule R S) (span R coeffs(q)) spanCoeffs(p)
Tactic: rw [Submodule.sup_mul, one_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 : ℕ
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) * HMul.hMul (α := Submodule R S) spanCoeffs(q) spanCoeffs(p) =
    HPow.hPow (α := Submodule R S) spanCoeffs(q) (deg(r) + 1) * spanCoeffs(p)
have 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)
Tactic: rw [pow_succ, mul_assoc]
-- 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)
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)
⊢ 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)
have 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)
Tactic: rw [pow_succ, mul_assoc]
-- 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) * spanCoeffs(p) ≤
    HPow.hPow (α := Submodule R S) spanCoeffs(q) deg(p) * spanCoeffs(p)
have bc : LE.le (α := Submodule R S) 1 spanCoeffs(q)
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)
bc : LE.le (α := Submodule R S) 1 spanCoeffs(q)
⊢ HPow.hPow (α := Submodule R S) spanCoeffs(q) (deg(r) + 1) * spanCoeffs(p) ≤
    HPow.hPow (α := Submodule R S) spanCoeffs(q) deg(p) * spanCoeffs(p)
have bc₁ : deg(r) + 1 ≤ deg(p)
Tactic: gcongr
-- 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))
deg_r_lt_deg_p : deg(r) < deg(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 H'' : 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]
-- 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)
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)
have neg : (p.leadingCoeff * if i = deg(p) - deg(q) then 1 else 0) ∈
  HPow.hPow (α := Submodule R S) spanCoeffs(q) deg(p) * spanCoeffs(p)
Tactic: refine ⟨add_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 : ℕ
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)
⊢ (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₁ : (r.divModByMonicAux hq).1.coeff i ∈ HPow.hPow (α := Submodule R S) spanCoeffs(q) deg(p) * spanCoeffs(p)
Tactic: refine ⟨add_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 : ℕ
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)
⊢ (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₂ : (r.divModByMonicAux hq).2.coeff i ∈ HPow.hPow (α := Submodule R S) spanCoeffs(q) deg(p) * spanCoeffs(p)
Tactic: refine ⟨add_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 : ℕ
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) ∈
    HPow.hPow (α := Submodule R S) spanCoeffs(q) deg(p) * spanCoeffs(p)
have pos : i = deg(p) - deg(q) → p.leadingCoeff * 1 ∈ 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
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)
⊢ (p.leadingCoeff * if i = deg(p) - deg(q) then 1 else 0) ∈
    HPow.hPow (α := Submodule R S) spanCoeffs(q) deg(p) * spanCoeffs(p)
have neg : ¬i = deg(p) - deg(q) → p.leadingCoeff * 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
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 * 1 ∈ HPow.hPow (α := Submodule R S) spanCoeffs(q) deg(p) * spanCoeffs(p)
have pos : p.leadingCoeff ∈ HPow.hPow (α := Submodule R S) spanCoeffs(q) deg(p) * spanCoeffs(p)
Tactic: simp only [mul_one, mul_zero]
-- 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)
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 * 0 ∈ HPow.hPow (α := Submodule R S) spanCoeffs(q) deg(p) * spanCoeffs(p)
have neg : 0 ∈ HPow.hPow (α := Submodule R S) spanCoeffs(q) deg(p) * spanCoeffs(p)
Tactic: simp only [mul_one, mul_zero]
-- 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]
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 : ℕ
⊢ coeff (if hq : q.Monic then (p.divModByMonicAux hq).2 else p) i ∈ Mq ^ deg(p) * Mp
have pos : ∀ (H : q.Monic), (p.divModByMonicAux H).2.coeff i ∈ Mq ^ deg(p) * Mp
Tactic: split_ifs with H
-- 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]
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
⊢ coeff (if hq : q.Monic then (p.divModByMonicAux hq).2 else p) i ∈ Mq ^ deg(p) * Mp
have neg : ∀ (H : ¬q.Monic), p.coeff i ∈ Mq ^ deg(p) * Mp
Tactic: split_ifs with H
-- 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]
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
have pos : HPow.hPow (α := Submodule R S) spanCoeffs(q) deg(p) * spanCoeffs(p) ≤ Mq ^ deg(p) * Mp
Tactic: refine SetLike.le_def.mp ?_ (coeff_divModByMonicAux_mem_span_pow_mul_span (R := R) p q H i).2
-- 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]
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
⊢ HPow.hPow (α := Submodule R S) spanCoeffs(q) deg(p) * spanCoeffs(p) ≤ Mq ^ deg(p) * Mp
have pos : spanCoeffs(q) ≤ Mq
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]
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
⊢ HPow.hPow (α := Submodule R S) spanCoeffs(q) deg(p) * spanCoeffs(p) ≤ Mq ^ deg(p) * Mp
have pos₁ : spanCoeffs(p) ≤ Mp
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]
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.coeff i ∈ Mq ^ deg(p) * Mp
have neg : HPow.hPow (α := S) 1 deg(p) * p.coeff i ∈ Mq ^ deg(p) * Mp
Tactic: rw [← one_mul (p.coeff i), ← one_pow p.natDegree]
-- 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]
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 : ℕ
⊢ coeff (if hq : q.Monic then (p.divModByMonicAux hq).1 else 0) i ∈ Mq ^ deg(p) * Mp
have pos : ∀ (H : q.Monic), (p.divModByMonicAux H).1.coeff i ∈ Mq ^ deg(p) * Mp
Tactic: split_ifs with H
-- 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]
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).1.coeff i ∈ Mq ^ deg(p) * Mp
⊢ coeff (if hq : q.Monic then (p.divModByMonicAux hq).1 else 0) i ∈ Mq ^ deg(p) * Mp
have neg : ∀ (H : ¬q.Monic), coeff 0 i ∈ Mq ^ deg(p) * Mp
Tactic: split_ifs with H
-- 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]
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).1.coeff i ∈ Mq ^ deg(p) * Mp
have pos : HPow.hPow (α := Submodule R S) spanCoeffs(q) deg(p) * spanCoeffs(p) ≤ Mq ^ deg(p) * Mp
Tactic: refine SetLike.le_def.mp ?_ (coeff_divModByMonicAux_mem_span_pow_mul_span (R := R) p q H i).1
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.CoeffMem (goal)
Goal:
ι : Type u_1
R : Type u_2
inst : CommRing R
inst_1 : DecidableEq ι
i j : ι
hij : i ≠ j
v : ι → R[X]
⊢ Eq (α := Ideal R[X]) (span (Set.range (Function.update (β := fun (a : ι) ↦ R[X]) v j (v j %ₘ v i))))
    (span (Set.range v))
have rw : Eq (α := Ideal R[X]) (span (Set.range (Function.update (β := fun (a : ι) ↦ R[X]) v j (v j - v i * (v j /ₘ v i)))))
  (span (Set.range v))
Tactic: rw [modByMonic_eq_sub_mul_div, mul_comm, ← smul_eq_mul, Ideal.span, Ideal.span,
    Submodule.span_range_update_sub_smul hij]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.CoeffMem (goal)
Goal:
ι : Type u_1
R : Type u_2
inst : CommRing R
inst_1 : DecidableEq ι
i j : ι
hij : i ≠ j
v : ι → R[X]
rw :
  Eq (α := Ideal R[X]) (span (Set.range (Function.update (β := fun (a : ι) ↦ R[X]) v j (v j - v i * (v j /ₘ v i)))))
    (span (Set.range v))
⊢ Eq (α := Ideal R[X]) (span (Set.range (Function.update (β := fun (a : ι) ↦ R[X]) v j (v j %ₘ v i))))
    (span (Set.range v))
have rw₁ : Eq (α := Ideal R[X]) (span (Set.range (Function.update (β := fun (a : ι) ↦ R[X]) v j (v j - v j /ₘ v i * v i))))
  (span (Set.range v))
Tactic: rw [modByMonic_eq_sub_mul_div, mul_comm, ← smul_eq_mul, Ideal.span, Ideal.span,
    Submodule.span_range_update_sub_smul hij]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.CoeffMem (goal)
Goal:
ι : Type u_1
R : Type u_2
inst : CommRing R
inst_1 : DecidableEq ι
i j : ι
hij : i ≠ j
v : ι → R[X]
rw :
  Eq (α := Ideal R[X]) (span (Set.range (Function.update (β := fun (a : ι) ↦ R[X]) v j (v j - v i * (v j /ₘ v i)))))
    (span (Set.range v))
rw₁ :
  Eq (α := Ideal R[X]) (span (Set.range (Function.update (β := fun (a : ι) ↦ R[X]) v j (v j - v j /ₘ v i * v i))))
    (span (Set.range v))
⊢ Eq (α := Ideal R[X]) (span (Set.range (Function.update (β := fun (a : ι) ↦ R[X]) v j (v j %ₘ v i))))
    (span (Set.range v))
have rw₂ : Eq (α := Ideal R[X]) (span (Set.range (Function.update (β := fun (a : ι) ↦ R[X]) v j (v j - (v j /ₘ v i) • v i))))
  (span (Set.range v))
Tactic: rw [modByMonic_eq_sub_mul_div, mul_comm, ← smul_eq_mul, Ideal.span, Ideal.span,
    Submodule.span_range_update_sub_smul hij]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.CoeffMem (goal)
Goal:
ι : Type u_1
R : Type u_2
inst : CommRing R
inst_1 : DecidableEq ι
i j : ι
hij : i ≠ j
v : ι → R[X]
rw :
  Eq (α := Ideal R[X]) (span (Set.range (Function.update (β := fun (a : ι) ↦ R[X]) v j (v j - v i * (v j /ₘ v i)))))
    (span (Set.range v))
rw₁ :
  Eq (α := Ideal R[X]) (span (Set.range (Function.update (β := fun (a : ι) ↦ R[X]) v j (v j - v j /ₘ v i * v i))))
    (span (Set.range v))
rw₂ :
  Eq (α := Ideal R[X]) (span (Set.range (Function.update (β := fun (a : ι) ↦ R[X]) v j (v j - (v j /ₘ v i) • v i))))
    (span (Set.range v))
⊢ Eq (α := Ideal R[X]) (span (Set.range (Function.update (β := fun (a : ι) ↦ R[X]) v j (v j %ₘ v i))))
    (span (Set.range v))
have rw₃ : Eq (α := Ideal R[X])
  (Submodule.span R[X] (Set.range (Function.update (β := fun (a : ι) ↦ R[X]) v j (v j - (v j /ₘ v i) • v i))))
  (span (Set.range v))
Tactic: rw [modByMonic_eq_sub_mul_div, mul_comm, ← smul_eq_mul, Ideal.span, Ideal.span,
    Submodule.span_range_update_sub_smul hij]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.CoeffMem (goal)
Goal:
ι : Type u_1
R : Type u_2
inst : CommRing R
inst_1 : DecidableEq ι
i j : ι
hij : i ≠ j
v : ι → R[X]
rw :
  Eq (α := Ideal R[X]) (span (Set.range (Function.update (β := fun (a : ι) ↦ R[X]) v j (v j - v i * (v j /ₘ v i)))))
    (span (Set.range v))
rw₁ :
  Eq (α := Ideal R[X]) (span (Set.range (Function.update (β := fun (a : ι) ↦ R[X]) v j (v j - v j /ₘ v i * v i))))
    (span (Set.range v))
rw₂ :
  Eq (α := Ideal R[X]) (span (Set.range (Function.update (β := fun (a : ι) ↦ R[X]) v j (v j - (v j /ₘ v i) • v i))))
    (span (Set.range v))
rw₃ :
  Eq (α := Ideal R[X])
    (Submodule.span R[X] (Set.range (Function.update (β := fun (a : ι) ↦ R[X]) v j (v j - (v j /ₘ v i) • v i))))
    (span (Set.range v))
⊢ Eq (α := Ideal R[X]) (span (Set.range (Function.update (β := fun (a : ι) ↦ R[X]) v j (v j %ₘ v i))))
    (span (Set.range v))
have rw₄ : Eq (α := Ideal R[X])
  (Submodule.span R[X] (Set.range (Function.update (β := fun (a : ι) ↦ R[X]) v j (v j - (v j /ₘ v i) • v i))))
  (Submodule.span R[X] (Set.range v))
Tactic: rw [modByMonic_eq_sub_mul_div, mul_comm, ← smul_eq_mul, Ideal.span, Ideal.span,
    Submodule.span_range_update_sub_smul hij]