awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Trunc (goal)
Goal:
R : Type u_2
inst : CommSemiring R
f : R⟦X⟧
n a : ℕ
zero :
  Eq (α := R[X])
    ((trunc n : (a : R⟦X⟧) → R[X]) (HPow.hPow (α := R⟦X⟧) (β := ℕ) (↑((trunc n : (a : R⟦X⟧) → R[X]) f) : R⟦X⟧) 0) :
      R[X])
    ((trunc n : (a : R⟦X⟧) → R[X]) (HPow.hPow (β := ℕ) f 0) : R[X])
⊢ Eq (α := R[X])
    ((trunc n : (a : R⟦X⟧) → R[X]) (HPow.hPow (α := R⟦X⟧) (↑((trunc n : (a : R⟦X⟧) → R[X]) f) : R⟦X⟧) a) : R[X])
    ((trunc n : (a : R⟦X⟧) → R[X]) (f ^ a) : R[X])
have succ : ∀ (a : ℕ)
  (ih :
    Eq (α := R[X])
      ((trunc n : (a : R⟦X⟧) → R[X]) (HPow.hPow (α := R⟦X⟧) (↑((trunc n : (a : R⟦X⟧) → R[X]) f) : R⟦X⟧) a) : R[X])
      ((trunc n : (a : R⟦X⟧) → R[X]) (f ^ a) : R[X])),
  Eq (α := R[X])
    ((trunc n : (a : R⟦X⟧) → R[X]) (HPow.hPow (α := R⟦X⟧) (↑((trunc n : (a : R⟦X⟧) → R[X]) f) : R⟦X⟧) (a + 1)) : R[X])
    ((trunc n : (a : R⟦X⟧) → R[X]) (f ^ (a + 1)) : R[X])
Tactic: induction a with
  | zero =>
    rw [pow_zero, pow_zero]
  | succ a ih =>
    rw [_root_.pow_succ', _root_.pow_succ', trunc_trunc_mul,
      ← trunc_trunc_mul_trunc, ih, trunc_trunc_mul_trunc]
Cleared hypotheses: a
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Trunc (goal)
Goal:
R : Type u_2
inst : CommSemiring R
n : ℕ
f : R[X]
hn : f.natDegree < n
⊢ (trunc n : (a : R⟦X⟧) → R[X]) (↑f : R⟦X⟧) = f
have rw : (↑((trunc n : (a : R⟦X⟧) → R[X]) (↑f : R⟦X⟧)) : R⟦X⟧) = (↑f : R⟦X⟧)
Tactic: rw [← Polynomial.coe_inj]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Trunc (goal)
Goal:
R : Type u_2
inst : CommSemiring R
n : ℕ
f : R[X]
hn : f.natDegree < n
⊢ (↑((trunc n : (a : R⟦X⟧) → R[X]) (↑f : R⟦X⟧)) : R⟦X⟧) = (↑f : R⟦X⟧)
have h : ∀ (m : ℕ),
  Eq (α := R) ((coeff m : (a : R⟦X⟧) → R) (↑((trunc n : (a : R⟦X⟧) → R[X]) (↑f : R⟦X⟧)) : R⟦X⟧) : R)
    ((coeff m : (a : R⟦X⟧) → R) (↑f : R⟦X⟧) : R)
Tactic: ext m
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Trunc (goal)
Goal:
R : Type u_2
inst : CommSemiring R
n : ℕ
f : R[X]
hn : f.natDegree < n
m : ℕ
⊢ Eq (α := R) ((coeff m : (a : R⟦X⟧) → R) (↑((trunc n : (a : R⟦X⟧) → R[X]) (↑f : R⟦X⟧)) : R⟦X⟧) : R)
    ((coeff m : (a : R⟦X⟧) → R) (↑f : R⟦X⟧) : R)
have h : Eq (α := R) (if m < n then (coeff m : (a : R⟦X⟧) → R) (↑f : R⟦X⟧) else 0 : R)
  ((coeff m : (a : R⟦X⟧) → R) (↑f : R⟦X⟧) : R)
Tactic: rw [coeff_coe, coeff_trunc]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Trunc (goal)
Goal:
R : Type u_2
inst : CommSemiring R
n : ℕ
f : R[X]
hn : f.natDegree < n
m : ℕ
⊢ Eq (α := R) (if m < n then (coeff m : (a : R⟦X⟧) → R) (↑f : R⟦X⟧) else 0 : R)
    ((coeff m : (a : R⟦X⟧) → R) (↑f : R⟦X⟧) : R)
have h : m < n → Eq (α := R) ((coeff m : (a : R⟦X⟧) → R) (↑f : R⟦X⟧) : R) ((coeff m : (a : R⟦X⟧) → R) (↑f : R⟦X⟧) : R)
Tactic: split
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Trunc (goal)
Goal:
R : Type u_2
inst : CommSemiring R
n : ℕ
f : R[X]
hn : f.natDegree < n
m : ℕ
h : m < n → Eq (α := R) ((coeff m : (a : R⟦X⟧) → R) (↑f : R⟦X⟧) : R) ((coeff m : (a : R⟦X⟧) → R) (↑f : R⟦X⟧) : R)
⊢ Eq (α := R) (if m < n then (coeff m : (a : R⟦X⟧) → R) (↑f : R⟦X⟧) else 0 : R)
    ((coeff m : (a : R⟦X⟧) → R) (↑f : R⟦X⟧) : R)
have h₁ : ¬m < n → Eq (α := R) (0 : R) ((coeff m : (a : R⟦X⟧) → R) (↑f : R⟦X⟧) : R)
Tactic: split
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Trunc (hypothesis)
Goal:
R : Type u_2
inst : CommSemiring R
n : ℕ
f : R[X]
hn : f.natDegree < n
m : ℕ
h : ¬m < n
⊢ Eq (α := R) (0 : R) ((coeff m : (a : R⟦X⟧) → R) (↑f : R⟦X⟧) : R)
have h₁ : n ≤ m
Tactic: rw [not_lt] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Trunc (goal)
Goal:
R : Type u_2
inst : CommSemiring R
n : ℕ
f : R[X]
hn : f.natDegree < n
m : ℕ
h : n ≤ m
⊢ Eq (α := R) (0 : R) ((coeff m : (a : R⟦X⟧) → R) (↑f : R⟦X⟧) : R)
have rw : 0 = f.coeff m
Tactic: rw [coeff_coe]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Trunc (goal)
Goal:
R : Type u_2
inst : CommSemiring R
n : ℕ
f : R[X]
hn : f.natDegree < n
m : ℕ
h : n ≤ m
⊢ 0 = f.coeff m
have symm : f.coeff m = 0
Tactic: symm
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Trunc (goal)
Goal:
R : Type u_2
inst : CommSemiring R
n m : ℕ
f : R⟦X⟧
h : n < m
⊢ Eq (α := R) ((coeff n : (a : R⟦X⟧) → R) (↑((trunc m : (a : R⟦X⟧) → R[X]) f) : R⟦X⟧) : R)
    ((coeff n : (a : R⟦X⟧) → R) f : R)
have rwa : Eq (α := R) (Polynomial.coeff ((trunc m : (a : R⟦X⟧) → R[X]) f) n : R) ((coeff n : (a : R⟦X⟧) → R) f : R)
Tactic: rwa [coeff_coe, coeff_trunc, if_pos]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Trunc (goal)
Goal:
R : Type u_2
inst : CommSemiring R
n m : ℕ
f : R⟦X⟧
h : n < m
rwa : Eq (α := R) (Polynomial.coeff ((trunc m : (a : R⟦X⟧) → R[X]) f) n : R) ((coeff n : (a : R⟦X⟧) → R) f : R)
⊢ Eq (α := R) ((coeff n : (a : R⟦X⟧) → R) (↑((trunc m : (a : R⟦X⟧) → R[X]) f) : R⟦X⟧) : R)
    ((coeff n : (a : R⟦X⟧) → R) f : R)
have rwa₁ : Eq (α := R) (if n < m then (coeff n : (a : R⟦X⟧) → R) f else 0 : R) ((coeff n : (a : R⟦X⟧) → R) f : R)
Tactic: rwa [coeff_coe, coeff_trunc, if_pos]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Trunc (goal)
Goal:
R : Type u_2
inst : CommSemiring R
n m : ℕ
f : R⟦X⟧
h : n < m
rwa : Eq (α := R) (Polynomial.coeff ((trunc m : (a : R⟦X⟧) → R[X]) f) n : R) ((coeff n : (a : R⟦X⟧) → R) f : R)
rwa₁ : Eq (α := R) (if n < m then (coeff n : (a : R⟦X⟧) → R) f else 0 : R) ((coeff n : (a : R⟦X⟧) → R) f : R)
⊢ Eq (α := R) ((coeff n : (a : R⟦X⟧) → R) (↑((trunc m : (a : R⟦X⟧) → R[X]) f) : R⟦X⟧) : R)
    ((coeff n : (a : R⟦X⟧) → R) f : R)
have rwa₂ : Eq (α := R) ((coeff n : (a : R⟦X⟧) → R) f : R) ((coeff n : (a : R⟦X⟧) → R) f : R)
Tactic: rwa [coeff_coe, coeff_trunc, if_pos]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Trunc (goal)
Goal:
R : Type u_2
inst : CommSemiring R
n a b : ℕ
f g : R⟦X⟧
ha : n < a
hb : n < b
⊢ Eq (α := R) ((coeff n : (a : R⟦X⟧) → R) (f * g) : R)
    ((coeff n : (a : R⟦X⟧) → R)
        (HMul.hMul (α := R⟦X⟧) (↑((trunc a : (a : R⟦X⟧) → R[X]) f) : R⟦X⟧)
          (↑((trunc b : (a : R⟦X⟧) → R[X]) g) : R⟦X⟧)) :
      R)
have symm : Eq (α := R)
  ((coeff n : (a : R⟦X⟧) → R)
      (HMul.hMul (α := R⟦X⟧) (↑((trunc a : (a : R⟦X⟧) → R[X]) f) : R⟦X⟧) (↑((trunc b : (a : R⟦X⟧) → R[X]) g) : R⟦X⟧)) :
    R)
  ((coeff n : (a : R⟦X⟧) → R) (f * g) : R)
Tactic: symm
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Trunc (goal)
Goal:
R : Type u_2
inst : CommSemiring R
n a b : ℕ
f g : R⟦X⟧
ha : n < a
hb : n < b
⊢ Eq (α := R)
    ((coeff n : (a : R⟦X⟧) → R)
        (HMul.hMul (α := R⟦X⟧) (↑((trunc a : (a : R⟦X⟧) → R[X]) f) : R⟦X⟧)
          (↑((trunc b : (a : R⟦X⟧) → R[X]) g) : R⟦X⟧)) :
      R)
    ((coeff n : (a : R⟦X⟧) → R) (f * g) : R)
have rw : Eq (α := R)
  ((coeff n : (a : R⟦X⟧) → R)
      (↑((trunc n.succ : (a : R⟦X⟧) → R[X])
            (HMul.hMul (α := R⟦X⟧) (↑((trunc a : (a : R⟦X⟧) → R[X]) f) : R⟦X⟧)
              (↑((trunc b : (a : R⟦X⟧) → R[X]) g) : R⟦X⟧))) :
        R⟦X⟧) :
    R)
  ((coeff n : (a : R⟦X⟧) → R) (f * g) : R)
Tactic: rw [← coeff_coe_trunc_of_lt n.lt_succ_self, ← trunc_trunc_mul_trunc, trunc_trunc_of_le f ha,
    trunc_trunc_of_le g hb, trunc_trunc_mul_trunc, coeff_coe_trunc_of_lt n.lt_succ_self]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Trunc (goal)
Goal:
R : Type u_2
inst : CommSemiring R
n a b : ℕ
f g : R⟦X⟧
ha : n < a
hb : n < b
rw :
  Eq (α := R)
    ((coeff n : (a : R⟦X⟧) → R)
        (↑((trunc n.succ : (a : R⟦X⟧) → R[X])
              (HMul.hMul (α := R⟦X⟧) (↑((trunc a : (a : R⟦X⟧) → R[X]) f) : R⟦X⟧)
                (↑((trunc b : (a : R⟦X⟧) → R[X]) g) : R⟦X⟧))) :
          R⟦X⟧) :
      R)
    ((coeff n : (a : R⟦X⟧) → R) (f * g) : R)
⊢ Eq (α := R)
    ((coeff n : (a : R⟦X⟧) → R)
        (HMul.hMul (α := R⟦X⟧) (↑((trunc a : (a : R⟦X⟧) → R[X]) f) : R⟦X⟧)
          (↑((trunc b : (a : R⟦X⟧) → R[X]) g) : R⟦X⟧)) :
      R)
    ((coeff n : (a : R⟦X⟧) → R) (f * g) : R)
have rw₁ : Eq (α := R)
  ((coeff n : (a : R⟦X⟧) → R)
      (↑((trunc n.succ : (a : R⟦X⟧) → R[X])
            (HMul.hMul (α := R⟦X⟧)
              (↑((trunc n.succ : (a : R⟦X⟧) → R[X]) (↑((trunc a : (a : R⟦X⟧) → R[X]) f) : R⟦X⟧)) : R⟦X⟧)
              (↑((trunc n.succ : (a : R⟦X⟧) → R[X]) (↑((trunc b : (a : R⟦X⟧) → R[X]) g) : R⟦X⟧)) : R⟦X⟧))) :
        R⟦X⟧) :
    R)
  ((coeff n : (a : R⟦X⟧) → R) (f * g) : R)
Tactic: rw [← coeff_coe_trunc_of_lt n.lt_succ_self, ← trunc_trunc_mul_trunc, trunc_trunc_of_le f ha,
    trunc_trunc_of_le g hb, trunc_trunc_mul_trunc, coeff_coe_trunc_of_lt n.lt_succ_self]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Trunc (goal)
Goal:
R : Type u_2
inst : CommSemiring R
n a b : ℕ
f g : R⟦X⟧
ha : n < a
hb : n < b
rw :
  Eq (α := R)
    ((coeff n : (a : R⟦X⟧) → R)
        (↑((trunc n.succ : (a : R⟦X⟧) → R[X])
              (HMul.hMul (α := R⟦X⟧) (↑((trunc a : (a : R⟦X⟧) → R[X]) f) : R⟦X⟧)
                (↑((trunc b : (a : R⟦X⟧) → R[X]) g) : R⟦X⟧))) :
          R⟦X⟧) :
      R)
    ((coeff n : (a : R⟦X⟧) → R) (f * g) : R)
rw₁ :
  Eq (α := R)
    ((coeff n : (a : R⟦X⟧) → R)
        (↑((trunc n.succ : (a : R⟦X⟧) → R[X])
              (HMul.hMul (α := R⟦X⟧)
                (↑((trunc n.succ : (a : R⟦X⟧) → R[X]) (↑((trunc a : (a : R⟦X⟧) → R[X]) f) : R⟦X⟧)) : R⟦X⟧)
                (↑((trunc n.succ : (a : R⟦X⟧) → R[X]) (↑((trunc b : (a : R⟦X⟧) → R[X]) g) : R⟦X⟧)) : R⟦X⟧))) :
          R⟦X⟧) :
      R)
    ((coeff n : (a : R⟦X⟧) → R) (f * g) : R)
⊢ Eq (α := R)
    ((coeff n : (a : R⟦X⟧) → R)
        (HMul.hMul (α := R⟦X⟧) (↑((trunc a : (a : R⟦X⟧) → R[X]) f) : R⟦X⟧)
          (↑((trunc b : (a : R⟦X⟧) → R[X]) g) : R⟦X⟧)) :
      R)
    ((coeff n : (a : R⟦X⟧) → R) (f * g) : R)
have rw₂ : Eq (α := R)
  ((coeff n : (a : R⟦X⟧) → R)
      (↑((trunc n.succ : (a : R⟦X⟧) → R[X])
            (HMul.hMul (α := R⟦X⟧) (↑((trunc n.succ : (a : R⟦X⟧) → R[X]) f) : R⟦X⟧)
              (↑((trunc n.succ : (a : R⟦X⟧) → R[X]) (↑((trunc b : (a : R⟦X⟧) → R[X]) g) : R⟦X⟧)) : R⟦X⟧))) :
        R⟦X⟧) :
    R)
  ((coeff n : (a : R⟦X⟧) → R) (f * g) : R)
Tactic: rw [← coeff_coe_trunc_of_lt n.lt_succ_self, ← trunc_trunc_mul_trunc, trunc_trunc_of_le f ha,
    trunc_trunc_of_le g hb, trunc_trunc_mul_trunc, coeff_coe_trunc_of_lt n.lt_succ_self]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Trunc (goal)
Goal:
R : Type u_2
inst : CommSemiring R
n a b : ℕ
f g : R⟦X⟧
ha : n < a
hb : n < b
rw :
  Eq (α := R)
    ((coeff n : (a : R⟦X⟧) → R)
        (↑((trunc n.succ : (a : R⟦X⟧) → R[X])
              (HMul.hMul (α := R⟦X⟧) (↑((trunc a : (a : R⟦X⟧) → R[X]) f) : R⟦X⟧)
                (↑((trunc b : (a : R⟦X⟧) → R[X]) g) : R⟦X⟧))) :
          R⟦X⟧) :
      R)
    ((coeff n : (a : R⟦X⟧) → R) (f * g) : R)
rw₁ :
  Eq (α := R)
    ((coeff n : (a : R⟦X⟧) → R)
        (↑((trunc n.succ : (a : R⟦X⟧) → R[X])
              (HMul.hMul (α := R⟦X⟧)
                (↑((trunc n.succ : (a : R⟦X⟧) → R[X]) (↑((trunc a : (a : R⟦X⟧) → R[X]) f) : R⟦X⟧)) : R⟦X⟧)
                (↑((trunc n.succ : (a : R⟦X⟧) → R[X]) (↑((trunc b : (a : R⟦X⟧) → R[X]) g) : R⟦X⟧)) : R⟦X⟧))) :
          R⟦X⟧) :
      R)
    ((coeff n : (a : R⟦X⟧) → R) (f * g) : R)
rw₂ :
  Eq (α := R)
    ((coeff n : (a : R⟦X⟧) → R)
        (↑((trunc n.succ : (a : R⟦X⟧) → R[X])
              (HMul.hMul (α := R⟦X⟧) (↑((trunc n.succ : (a : R⟦X⟧) → R[X]) f) : R⟦X⟧)
                (↑((trunc n.succ : (a : R⟦X⟧) → R[X]) (↑((trunc b : (a : R⟦X⟧) → R[X]) g) : R⟦X⟧)) : R⟦X⟧))) :
          R⟦X⟧) :
      R)
    ((coeff n : (a : R⟦X⟧) → R) (f * g) : R)
⊢ Eq (α := R)
    ((coeff n : (a : R⟦X⟧) → R)
        (HMul.hMul (α := R⟦X⟧) (↑((trunc a : (a : R⟦X⟧) → R[X]) f) : R⟦X⟧)
          (↑((trunc b : (a : R⟦X⟧) → R[X]) g) : R⟦X⟧)) :
      R)
    ((coeff n : (a : R⟦X⟧) → R) (f * g) : R)
have rw₃ : Eq (α := R)
  ((coeff n : (a : R⟦X⟧) → R)
      (↑((trunc n.succ : (a : R⟦X⟧) → R[X])
            (HMul.hMul (α := R⟦X⟧) (↑((trunc n.succ : (a : R⟦X⟧) → R[X]) f) : R⟦X⟧)
              (↑((trunc n.succ : (a : R⟦X⟧) → R[X]) g) : R⟦X⟧))) :
        R⟦X⟧) :
    R)
  ((coeff n : (a : R⟦X⟧) → R) (f * g) : R)
Tactic: rw [← coeff_coe_trunc_of_lt n.lt_succ_self, ← trunc_trunc_mul_trunc, trunc_trunc_of_le f ha,
    trunc_trunc_of_le g hb, trunc_trunc_mul_trunc, coeff_coe_trunc_of_lt n.lt_succ_self]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Trunc (goal)
Goal:
R : Type u_2
inst : CommSemiring R
n a b : ℕ
f g : R⟦X⟧
ha : n < a
hb : n < b
rw :
  Eq (α := R)
    ((coeff n : (a : R⟦X⟧) → R)
        (↑((trunc n.succ : (a : R⟦X⟧) → R[X])
              (HMul.hMul (α := R⟦X⟧) (↑((trunc a : (a : R⟦X⟧) → R[X]) f) : R⟦X⟧)
                (↑((trunc b : (a : R⟦X⟧) → R[X]) g) : R⟦X⟧))) :
          R⟦X⟧) :
      R)
    ((coeff n : (a : R⟦X⟧) → R) (f * g) : R)
rw₁ :
  Eq (α := R)
    ((coeff n : (a : R⟦X⟧) → R)
        (↑((trunc n.succ : (a : R⟦X⟧) → R[X])
              (HMul.hMul (α := R⟦X⟧)
                (↑((trunc n.succ : (a : R⟦X⟧) → R[X]) (↑((trunc a : (a : R⟦X⟧) → R[X]) f) : R⟦X⟧)) : R⟦X⟧)
                (↑((trunc n.succ : (a : R⟦X⟧) → R[X]) (↑((trunc b : (a : R⟦X⟧) → R[X]) g) : R⟦X⟧)) : R⟦X⟧))) :
          R⟦X⟧) :
      R)
    ((coeff n : (a : R⟦X⟧) → R) (f * g) : R)
rw₂ :
  Eq (α := R)
    ((coeff n : (a : R⟦X⟧) → R)
        (↑((trunc n.succ : (a : R⟦X⟧) → R[X])
              (HMul.hMul (α := R⟦X⟧) (↑((trunc n.succ : (a : R⟦X⟧) → R[X]) f) : R⟦X⟧)
                (↑((trunc n.succ : (a : R⟦X⟧) → R[X]) (↑((trunc b : (a : R⟦X⟧) → R[X]) g) : R⟦X⟧)) : R⟦X⟧))) :
          R⟦X⟧) :
      R)
    ((coeff n : (a : R⟦X⟧) → R) (f * g) : R)
rw₃ :
  Eq (α := R)
    ((coeff n : (a : R⟦X⟧) → R)
        (↑((trunc n.succ : (a : R⟦X⟧) → R[X])
              (HMul.hMul (α := R⟦X⟧) (↑((trunc n.succ : (a : R⟦X⟧) → R[X]) f) : R⟦X⟧)
                (↑((trunc n.succ : (a : R⟦X⟧) → R[X]) g) : R⟦X⟧))) :
          R⟦X⟧) :
      R)
    ((coeff n : (a : R⟦X⟧) → R) (f * g) : R)
⊢ Eq (α := R)
    ((coeff n : (a : R⟦X⟧) → R)
        (HMul.hMul (α := R⟦X⟧) (↑((trunc a : (a : R⟦X⟧) → R[X]) f) : R⟦X⟧)
          (↑((trunc b : (a : R⟦X⟧) → R[X]) g) : R⟦X⟧)) :
      R)
    ((coeff n : (a : R⟦X⟧) → R) (f * g) : R)
have rw₄ : Eq (α := R) ((coeff n : (a : R⟦X⟧) → R) (↑((trunc n.succ : (a : R⟦X⟧) → R[X]) (f * g)) : R⟦X⟧) : R)
  ((coeff n : (a : R⟦X⟧) → R) (f * g) : R)
Tactic: rw [← coeff_coe_trunc_of_lt n.lt_succ_self, ← trunc_trunc_mul_trunc, trunc_trunc_of_le f ha,
    trunc_trunc_of_le g hb, trunc_trunc_mul_trunc, coeff_coe_trunc_of_lt n.lt_succ_self]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Trunc (goal)
Goal:
R : Type u_2
inst : CommSemiring R
n a b : ℕ
f g : R⟦X⟧
ha : n < a
hb : n < b
rw :
  Eq (α := R)
    ((coeff n : (a : R⟦X⟧) → R)
        (↑((trunc n.succ : (a : R⟦X⟧) → R[X])
              (HMul.hMul (α := R⟦X⟧) (↑((trunc a : (a : R⟦X⟧) → R[X]) f) : R⟦X⟧)
                (↑((trunc b : (a : R⟦X⟧) → R[X]) g) : R⟦X⟧))) :
          R⟦X⟧) :
      R)
    ((coeff n : (a : R⟦X⟧) → R) (f * g) : R)
rw₁ :
  Eq (α := R)
    ((coeff n : (a : R⟦X⟧) → R)
        (↑((trunc n.succ : (a : R⟦X⟧) → R[X])
              (HMul.hMul (α := R⟦X⟧)
                (↑((trunc n.succ : (a : R⟦X⟧) → R[X]) (↑((trunc a : (a : R⟦X⟧) → R[X]) f) : R⟦X⟧)) : R⟦X⟧)
                (↑((trunc n.succ : (a : R⟦X⟧) → R[X]) (↑((trunc b : (a : R⟦X⟧) → R[X]) g) : R⟦X⟧)) : R⟦X⟧))) :
          R⟦X⟧) :
      R)
    ((coeff n : (a : R⟦X⟧) → R) (f * g) : R)
rw₂ :
  Eq (α := R)
    ((coeff n : (a : R⟦X⟧) → R)
        (↑((trunc n.succ : (a : R⟦X⟧) → R[X])
              (HMul.hMul (α := R⟦X⟧) (↑((trunc n.succ : (a : R⟦X⟧) → R[X]) f) : R⟦X⟧)
                (↑((trunc n.succ : (a : R⟦X⟧) → R[X]) (↑((trunc b : (a : R⟦X⟧) → R[X]) g) : R⟦X⟧)) : R⟦X⟧))) :
          R⟦X⟧) :
      R)
    ((coeff n : (a : R⟦X⟧) → R) (f * g) : R)
rw₃ :
  Eq (α := R)
    ((coeff n : (a : R⟦X⟧) → R)
        (↑((trunc n.succ : (a : R⟦X⟧) → R[X])
              (HMul.hMul (α := R⟦X⟧) (↑((trunc n.succ : (a : R⟦X⟧) → R[X]) f) : R⟦X⟧)
                (↑((trunc n.succ : (a : R⟦X⟧) → R[X]) g) : R⟦X⟧))) :
          R⟦X⟧) :
      R)
    ((coeff n : (a : R⟦X⟧) → R) (f * g) : R)
rw₄ :
  Eq (α := R) ((coeff n : (a : R⟦X⟧) → R) (↑((trunc n.succ : (a : R⟦X⟧) → R[X]) (f * g)) : R⟦X⟧) : R)
    ((coeff n : (a : R⟦X⟧) → R) (f * g) : R)
⊢ Eq (α := R)
    ((coeff n : (a : R⟦X⟧) → R)
        (HMul.hMul (α := R⟦X⟧) (↑((trunc a : (a : R⟦X⟧) → R[X]) f) : R⟦X⟧)
          (↑((trunc b : (a : R⟦X⟧) → R[X]) g) : R⟦X⟧)) :
      R)
    ((coeff n : (a : R⟦X⟧) → R) (f * g) : R)
have rw₅ : Eq (α := R) ((coeff n : (a : R⟦X⟧) → R) (f * g) : R) ((coeff n : (a : R⟦X⟧) → R) (f * g) : R)
Tactic: rw [← coeff_coe_trunc_of_lt n.lt_succ_self, ← trunc_trunc_mul_trunc, trunc_trunc_of_le f ha,
    trunc_trunc_of_le g hb, trunc_trunc_mul_trunc, coeff_coe_trunc_of_lt n.lt_succ_self]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Trunc (goal)
Goal:
R : Type u_1
inst : Ring R
n : ℕ
φ ψ : R⟦X⟧
⊢ (trunc n : (a : R⟦X⟧) → R[X]) (φ - ψ) =
    HSub.hSub (α := R[X]) (β := R[X]) ((trunc n : (a : R⟦X⟧) → R[X]) φ : R[X]) ((trunc n : (a : R⟦X⟧) → R[X]) ψ : R[X])
have a : ∀ (i : ℕ),
  Polynomial.coeff ((trunc n : (a : R⟦X⟧) → R[X]) (φ - ψ)) i =
    (HSub.hSub (α := R[X]) (β := R[X]) ((trunc n : (a : R⟦X⟧) → R[X]) φ : R[X])
          ((trunc n : (a : R⟦X⟧) → R[X]) ψ : R[X])).coeff
      i
Tactic: ext i
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Trunc (goal)
Goal:
R : Type u_1
S : Type u_2
inst : Semiring R
inst_1 : Semiring S
f : R →+* S
p : R⟦X⟧
n : ℕ
⊢ (trunc n : (a : S⟦X⟧) → S[X]) ((map f : (a : R⟦X⟧) → S⟦X⟧) p) = Polynomial.map f ((trunc n : (a : R⟦X⟧) → R[X]) p)
have a : ∀ (m : ℕ),
  Polynomial.coeff ((trunc n : (a : S⟦X⟧) → S[X]) ((map f : (a : R⟦X⟧) → S⟦X⟧) p)) m =
    (Polynomial.map f ((trunc n : (a : R⟦X⟧) → R[X]) p)).coeff m
Tactic: ext m
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.WeierstrassPreparation (goal)
Goal:
A : Type u_1
inst : CommRing A
g : A⟦X⟧
I : Ideal A
⊢ IsWeierstrassDivisionAt 0 g 0 0 I
have degree_lt : Polynomial.degree.{u_1} (R := A) 0 <
  (↑(order.{u_1} (R := A ⧸ I) ((map (Ideal.Quotient.mk I) : (a : A⟦X⟧) → (A ⧸ I)⟦X⟧) g)).toNat : WithBot ℕ)
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.WeierstrassPreparation (goal)
Goal:
A : Type u_1
inst : CommRing A
g : A⟦X⟧
I : Ideal A
degree_lt :
  Polynomial.degree.{u_1} (R := A) 0 <
    (↑(order.{u_1} (R := A ⧸ I) ((map (Ideal.Quotient.mk I) : (a : A⟦X⟧) → (A ⧸ I)⟦X⟧) g)).toNat : WithBot ℕ)
⊢ IsWeierstrassDivisionAt 0 g 0 0 I
have eq_mul_add : 0 = g * 0 + (↑0 : A⟦X⟧)
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.WeierstrassPreparation (hypothesis)
Goal:
A : Type u_1
inst : CommRing A
f g q : A⟦X⟧
r : A[X]
I : Ideal A
H : f.IsWeierstrassDivisionAt g q r I
i : ℕ
hi : i < (order.{u_1} (R := A ⧸ I) ((map (Ideal.Quotient.mk I) : (a : A⟦X⟧) → (A ⧸ I)⟦X⟧) g)).toNat
⊢ Membership.mem (α := A) I ((coeff i : (a : A⟦X⟧) → A) (f - (↑r : A⟦X⟧)) : A)
have H₁ : f = g * q + (↑r : A⟦X⟧)
Tactic: replace H := H.2
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.WeierstrassPreparation (hypothesis)
Goal:
A : Type u_1
inst : CommRing A
f g q : A⟦X⟧
r : A[X]
I : Ideal A
i : ℕ
hi : i < (order.{u_1} (R := A ⧸ I) ((map (Ideal.Quotient.mk I) : (a : A⟦X⟧) → (A ⧸ I)⟦X⟧) g)).toNat
H : f = g * q + (↑r : A⟦X⟧)
⊢ Membership.mem (α := A) I ((coeff i : (a : A⟦X⟧) → A) (f - (↑r : A⟦X⟧)) : A)
have H₁ : f - (↑r : A⟦X⟧) = g * q
Tactic: rw [← sub_eq_iff_eq_add] at H
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.WeierstrassPreparation (goal)
Goal:
A : Type u_1
inst : CommRing A
f g q : A⟦X⟧
r : A[X]
I : Ideal A
i : ℕ
hi : i < (order.{u_1} (R := A ⧸ I) ((map (Ideal.Quotient.mk I) : (a : A⟦X⟧) → (A ⧸ I)⟦X⟧) g)).toNat
H : f - (↑r : A⟦X⟧) = g * q
⊢ Membership.mem (α := A) I ((coeff i : (a : A⟦X⟧) → A) (f - (↑r : A⟦X⟧)) : A)
have rw : Membership.mem (α := A) I ((coeff i : (a : A⟦X⟧) → A) (g * q) : A)
Tactic: rw [H]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.WeierstrassPreparation (goal)
Goal:
A : Type u_1
inst : CommRing A
f g q : A⟦X⟧
r : A[X]
I : Ideal A
i : ℕ
hi : i < (order.{u_1} (R := A ⧸ I) ((map (Ideal.Quotient.mk I) : (a : A⟦X⟧) → (A ⧸ I)⟦X⟧) g)).toNat
H : f - (↑r : A⟦X⟧) = g * q
⊢ Membership.mem (α := A) I ((coeff i : (a : A⟦X⟧) → A) (g * q) : A)
have refine : ∀ (j : ℕ) (hj : j ≤ i), Membership.mem (α := A) I ((coeff j : (a : A⟦X⟧) → A) g : A)
Tactic: refine coeff_mul_mem_ideal_of_coeff_left_mem_ideal i (fun j hj ↦ ?_) i le_rfl
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.WeierstrassPreparation (hypothesis)
Goal:
A : Type u_1
inst : CommRing A
f g q : A⟦X⟧
r : A[X]
I : Ideal A
i : ℕ
hi : i < (order.{u_1} (R := A ⧸ I) ((map (Ideal.Quotient.mk I) : (a : A⟦X⟧) → (A ⧸ I)⟦X⟧) g)).toNat
H : f - (↑r : A⟦X⟧) = g * q
j : ℕ
hj : j ≤ i
⊢ Membership.mem (α := A) I ((coeff j : (a : A⟦X⟧) → A) g : A)
have this : Eq (α := A ⧸ I) ((coeff j : (a : (A ⧸ I)⟦X⟧) → A ⧸ I) ((map (Ideal.Quotient.mk I) : (a : A⟦X⟧) → (A ⧸ I)⟦X⟧) g) : A ⧸ I)
  (0 : A ⧸ I)
Tactic: have := coeff_of_lt_order_toNat _ (lt_of_le_of_lt hj hi)
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.WeierstrassPreparation (goal)
Goal:
A : Type u_1
inst : CommRing A
f g q : A⟦X⟧
r : A[X]
I : Ideal A
i : ℕ
hi : i < (order.{u_1} (R := A ⧸ I) ((map (Ideal.Quotient.mk I) : (a : A⟦X⟧) → (A ⧸ I)⟦X⟧) g)).toNat
H : f - (↑r : A⟦X⟧) = g * q
j : ℕ
hj : j ≤ i
this :
  Eq (α := A ⧸ I)
    ((coeff j : (a : (A ⧸ I)⟦X⟧) → A ⧸ I) ((map (Ideal.Quotient.mk I) : (a : A⟦X⟧) → (A ⧸ I)⟦X⟧) g) : A ⧸ I) (0 : A ⧸ I)
⊢ Membership.mem (α := A) I ((coeff j : (a : A⟦X⟧) → A) g : A)
have rwa : ∀ (this : Eq (α := A ⧸ I) ((Ideal.Quotient.mk I : (a : A) → A ⧸ I) ((coeff j : (a : A⟦X⟧) → A) g) : A ⧸ I) (0 : A ⧸ I)),
  Membership.mem (α := A) I ((coeff j : (a : A⟦X⟧) → A) g : A)
Tactic: rwa [coeff_map, ← RingHom.mem_ker, Ideal.mk_ker] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.WeierstrassPreparation (goal)
Goal:
A : Type u_1
inst : CommRing A
f g q : A⟦X⟧
r : A[X]
I : Ideal A
i : ℕ
hi : i < (order.{u_1} (R := A ⧸ I) ((map (Ideal.Quotient.mk I) : (a : A⟦X⟧) → (A ⧸ I)⟦X⟧) g)).toNat
H : f - (↑r : A⟦X⟧) = g * q
j : ℕ
hj : j ≤ i
this :
  Eq (α := A ⧸ I)
    ((coeff j : (a : (A ⧸ I)⟦X⟧) → A ⧸ I) ((map (Ideal.Quotient.mk I) : (a : A⟦X⟧) → (A ⧸ I)⟦X⟧) g) : A ⧸ I) (0 : A ⧸ I)
rwa :
  ∀
    (this :
      Eq (α := A ⧸ I) ((Ideal.Quotient.mk I : (a : A) → A ⧸ I) ((coeff j : (a : A⟦X⟧) → A) g) : A ⧸ I) (0 : A ⧸ I)),
    Membership.mem (α := A) I ((coeff j : (a : A⟦X⟧) → A) g : A)
⊢ Membership.mem (α := A) I ((coeff j : (a : A⟦X⟧) → A) g : A)
have rwa₁ : ∀
  (this :
    Membership.mem (α := A) (γ := Ideal A) (RingHom.ker (F := A →+* A ⧸ I) (Ideal.Quotient.mk I))
      ((coeff j : (a : A⟦X⟧) → A) g : A)),
  Membership.mem (α := A) I ((coeff j : (a : A⟦X⟧) → A) g : A)
Tactic: rwa [coeff_map, ← RingHom.mem_ker, Ideal.mk_ker] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.WeierstrassPreparation (goal)
Goal:
A : Type u_1
inst : CommRing A
f g q : A⟦X⟧
r : A[X]
I : Ideal A
i : ℕ
hi : i < (order.{u_1} (R := A ⧸ I) ((map (Ideal.Quotient.mk I) : (a : A⟦X⟧) → (A ⧸ I)⟦X⟧) g)).toNat
H : f - (↑r : A⟦X⟧) = g * q
j : ℕ
hj : j ≤ i
this :
  Eq (α := A ⧸ I)
    ((coeff j : (a : (A ⧸ I)⟦X⟧) → A ⧸ I) ((map (Ideal.Quotient.mk I) : (a : A⟦X⟧) → (A ⧸ I)⟦X⟧) g) : A ⧸ I) (0 : A ⧸ I)
rwa :
  ∀
    (this :
      Eq (α := A ⧸ I) ((Ideal.Quotient.mk I : (a : A) → A ⧸ I) ((coeff j : (a : A⟦X⟧) → A) g) : A ⧸ I) (0 : A ⧸ I)),
    Membership.mem (α := A) I ((coeff j : (a : A⟦X⟧) → A) g : A)
rwa₁ :
  ∀
    (this :
      Membership.mem (α := A) (γ := Ideal A) (RingHom.ker (F := A →+* A ⧸ I) (Ideal.Quotient.mk I))
        ((coeff j : (a : A⟦X⟧) → A) g : A)),
    Membership.mem (α := A) I ((coeff j : (a : A⟦X⟧) → A) g : A)
⊢ Membership.mem (α := A) I ((coeff j : (a : A⟦X⟧) → A) g : A)
have rwa₂ : ∀ (this : Membership.mem (α := A) I ((coeff j : (a : A⟦X⟧) → A) g : A)),
  Membership.mem (α := A) I ((coeff j : (a : A⟦X⟧) → A) g : A)
Tactic: rwa [coeff_map, ← RingHom.mem_ker, Ideal.mk_ker] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.WeierstrassPreparation (goal)
Goal:
A : Type u_1
inst : CommRing A
f g q : A⟦X⟧
r : A[X]
I : Ideal A
f' q' : A⟦X⟧
r' : A[X]
H : f.IsWeierstrassDivisionAt g q r I
H' : f'.IsWeierstrassDivisionAt g q' r' I
⊢ f + f' = g * (q + q') + (↑(r + r') : A⟦X⟧)
have rw : g * q + (↑r : A⟦X⟧) + (g * q' + (↑r' : A⟦X⟧)) = g * (q + q') + ((↑r : A⟦X⟧) + (↑r' : A⟦X⟧))
Tactic: rw [H.eq_mul_add, H'.eq_mul_add, Polynomial.coe_add]