awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Trunc (goal)
Goal:
R : Type u_1
inst : Semiring R
n : ℕ
p : R⟦X⟧
⊢ Eq (α := R[X]) ((trunc n : (a : R⟦X⟧) → R[X]) (HPow.hPow (α := R⟦X⟧) X n * p) : R[X]) (0 : R[X])
have a : ∀ (n_1 : ℕ),
  Eq.{u_1 + 1} (α := R) (Polynomial.coeff ((trunc n : (a : R⟦X⟧) → R[X]) (HPow.hPow (α := R⟦X⟧) X n * p)) n_1)
    (Polynomial.coeff 0 n_1)
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Trunc (goal)
Goal:
R : Type u_2
inst : CommSemiring R
n m : ℕ
f : R⟦X⟧
hnm : n ≤ m
⊢ Eq (α := R[X]) ((trunc n : (a : R⟦X⟧) → R[X]) (↑((trunc m : (a : R⟦X⟧) → R[X]) f) : R⟦X⟧) : R[X])
    ((trunc n : (a : R⟦X⟧) → R[X]) f : R[X])
have a : ∀ (d : ℕ),
  Eq.{u_2 + 1} (α := R) (Polynomial.coeff ((trunc n : (a : R⟦X⟧) → R[X]) (↑((trunc m : (a : R⟦X⟧) → R[X]) f) : R⟦X⟧)) d)
    (Polynomial.coeff ((trunc n : (a : R⟦X⟧) → R[X]) f) d)
Tactic: ext d
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Trunc (goal)
Goal:
R : Type u_2
inst : CommSemiring R
n m : ℕ
f : R⟦X⟧
hnm : n ≤ m
d : ℕ
⊢ Eq.{u_2 + 1} (α := R) (Polynomial.coeff ((trunc n : (a : R⟦X⟧) → R[X]) (↑((trunc m : (a : R⟦X⟧) → R[X]) f) : R⟦X⟧)) d)
    (Polynomial.coeff ((trunc n : (a : R⟦X⟧) → R[X]) f) d)
have a : Eq (α := R) (if d < n then Polynomial.coeff ((trunc m : (a : R⟦X⟧) → R[X]) f) d else 0 : R)
  (if d < n then (coeff d : (a : R⟦X⟧) → R) f else 0 : R)
Tactic: rw [coeff_trunc, coeff_trunc, coeff_coe]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Trunc (goal)
Goal:
R : Type u_2
inst : CommSemiring R
n m : ℕ
f : R⟦X⟧
hnm : n ≤ m
d : ℕ
⊢ Eq (α := R) (if d < n then Polynomial.coeff ((trunc m : (a : R⟦X⟧) → R[X]) f) d else 0 : R)
    (if d < n then (coeff d : (a : R⟦X⟧) → R) f else 0 : R)
have pos : ∀ (h : d < n), Eq (α := R) (Polynomial.coeff ((trunc m : (a : R⟦X⟧) → R[X]) f) d : R) ((coeff d : (a : R⟦X⟧) → R) f : R)
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Trunc (goal)
Goal:
R : Type u_2
inst : CommSemiring R
n m : ℕ
f : R⟦X⟧
hnm : n ≤ m
d : ℕ
pos :
  ∀ (h : d < n),
    Eq (α := R) (Polynomial.coeff ((trunc m : (a : R⟦X⟧) → R[X]) f) d : R) ((coeff d : (a : R⟦X⟧) → R) f : R)
⊢ Eq (α := R) (if d < n then Polynomial.coeff ((trunc m : (a : R⟦X⟧) → R[X]) f) d else 0 : R)
    (if d < n then (coeff d : (a : R⟦X⟧) → R) f else 0 : R)
have neg : ∀ (h : ¬d < n), Eq.{u_2 + 1} (α := R) 0 0
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Trunc (goal)
Goal:
R : Type u_2
inst : CommSemiring R
n m : ℕ
f : R⟦X⟧
hnm : n ≤ m
d : ℕ
h : d < n
⊢ Eq (α := R) (Polynomial.coeff ((trunc m : (a : R⟦X⟧) → R[X]) f) d : R) ((coeff d : (a : R⟦X⟧) → R) f : R)
have pos : Eq (α := R) (if d < m then (coeff d : (a : R⟦X⟧) → R) f else 0 : R) ((coeff d : (a : R⟦X⟧) → R) f : R)
Tactic: rw [coeff_trunc, if_pos <| lt_of_lt_of_le h hnm]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Trunc (goal)
Goal:
R : Type u_2
inst : CommSemiring R
n m : ℕ
f : R⟦X⟧
hnm : n ≤ m
d : ℕ
h : d < n
pos : Eq (α := R) (if d < m then (coeff d : (a : R⟦X⟧) → R) f else 0 : R) ((coeff d : (a : R⟦X⟧) → R) f : R)
⊢ Eq (α := R) (Polynomial.coeff ((trunc m : (a : R⟦X⟧) → R[X]) f) d : R) ((coeff d : (a : R⟦X⟧) → R) f : R)
have pos₁ : Eq (α := R) ((coeff d : (a : R⟦X⟧) → R) f : R) ((coeff d : (a : R⟦X⟧) → R) f : R)
Tactic: rw [coeff_trunc, if_pos <| lt_of_lt_of_le h hnm]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Trunc (goal)
Goal:
R : Type u_2
inst : CommSemiring R
n : ℕ
f g : R⟦X⟧
⊢ Eq (α := R[X]) ((trunc n : (a : R⟦X⟧) → R[X]) ((↑((trunc n : (a : R⟦X⟧) → R[X]) f) : R⟦X⟧) * g) : R[X])
    ((trunc n : (a : R⟦X⟧) → R[X]) (f * g) : R[X])
have a : ∀ (m : ℕ),
  Eq.{u_2 + 1} (α := R)
    (Polynomial.coeff ((trunc n : (a : R⟦X⟧) → R[X]) ((↑((trunc n : (a : R⟦X⟧) → R[X]) f) : R⟦X⟧) * g)) m)
    (Polynomial.coeff ((trunc n : (a : R⟦X⟧) → R[X]) (f * g)) m)
Tactic: ext m
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Trunc (goal)
Goal:
R : Type u_2
inst : CommSemiring R
n : ℕ
f g : R⟦X⟧
m : ℕ
⊢ Eq.{u_2 + 1} (α := R)
    (Polynomial.coeff ((trunc n : (a : R⟦X⟧) → R[X]) ((↑((trunc n : (a : R⟦X⟧) → R[X]) f) : R⟦X⟧) * g)) m)
    (Polynomial.coeff ((trunc n : (a : R⟦X⟧) → R[X]) (f * g)) m)
have a : Eq (α := R) (if m < n then (coeff m : (a : R⟦X⟧) → R) ((↑((trunc n : (a : R⟦X⟧) → R[X]) f) : R⟦X⟧) * g) else 0 : R)
  (if m < n then (coeff m : (a : R⟦X⟧) → R) (f * g) else 0 : R)
Tactic: rw [coeff_trunc, coeff_trunc]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Trunc (goal)
Goal:
R : Type u_2
inst : CommSemiring R
n : ℕ
f g : R⟦X⟧
m : ℕ
⊢ Eq (α := R) (if m < n then (coeff m : (a : R⟦X⟧) → R) ((↑((trunc n : (a : R⟦X⟧) → R[X]) f) : R⟦X⟧) * g) else 0 : R)
    (if m < n then (coeff m : (a : R⟦X⟧) → R) (f * g) else 0 : R)
have pos : ∀ (h : m < n),
  Eq (α := R) ((coeff m : (a : R⟦X⟧) → R) ((↑((trunc n : (a : R⟦X⟧) → R[X]) f) : R⟦X⟧) * g) : R)
    ((coeff m : (a : R⟦X⟧) → R) (f * g) : R)
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Trunc (goal)
Goal:
R : Type u_2
inst : CommSemiring R
n : ℕ
f g : R⟦X⟧
m : ℕ
pos :
  ∀ (h : m < n),
    Eq (α := R) ((coeff m : (a : R⟦X⟧) → R) ((↑((trunc n : (a : R⟦X⟧) → R[X]) f) : R⟦X⟧) * g) : R)
      ((coeff m : (a : R⟦X⟧) → R) (f * g) : R)
⊢ Eq (α := R) (if m < n then (coeff m : (a : R⟦X⟧) → R) ((↑((trunc n : (a : R⟦X⟧) → R[X]) f) : R⟦X⟧) * g) else 0 : R)
    (if m < n then (coeff m : (a : R⟦X⟧) → R) (f * g) else 0 : R)
have neg : ∀ (h : ¬m < n), Eq.{u_2 + 1} (α := R) 0 0
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Trunc (goal)
Goal:
R : Type u_2
inst : CommSemiring R
n : ℕ
f g : R⟦X⟧
m : ℕ
h : m < n
⊢ Eq (α := R) ((coeff m : (a : R⟦X⟧) → R) ((↑((trunc n : (a : R⟦X⟧) → R[X]) f) : R⟦X⟧) * g) : R)
    ((coeff m : (a : R⟦X⟧) → R) (f * g) : R)
have pos : ∀ x ∈ @antidiagonal _ instAddMonoid _ m,
  HMul.hMul (α := R) (β := R) ((coeff x.1 : (a : R⟦X⟧) → R) (↑((trunc n : (a : R⟦X⟧) → R[X]) f) : R⟦X⟧) : R)
      ((coeff x.2 : (a : R⟦X⟧) → R) g : R) =
    HMul.hMul (α := R) (β := R) ((coeff x.1 : (a : R⟦X⟧) → R) f : R) ((coeff x.2 : (a : R⟦X⟧) → R) g : R)
Tactic: rw [coeff_mul, coeff_mul, sum_congr rfl]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Trunc (hypothesis)
Goal:
R : Type u_2
inst : CommSemiring R
n : ℕ
f g : R⟦X⟧
m : ℕ
h : m < n
x : ℕ × ℕ
hab : x ∈ @antidiagonal _ instAddMonoid _ m
⊢ HMul.hMul (α := R) (β := R) ((coeff x.1 : (a : R⟦X⟧) → R) (↑((trunc n : (a : R⟦X⟧) → R[X]) f) : R⟦X⟧) : R)
      ((coeff x.2 : (a : R⟦X⟧) → R) g : R) =
    HMul.hMul (α := R) (β := R) ((coeff x.1 : (a : R⟦X⟧) → R) f : R) ((coeff x.2 : (a : R⟦X⟧) → R) g : R)
have ha : x.1 < n
Tactic: have ha := lt_of_le_of_lt (antidiagonal.fst_le hab) h
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Trunc (goal)
Goal:
R : Type u_2
inst : CommSemiring R
n : ℕ
f g : R⟦X⟧
m : ℕ
h : m < n
x : ℕ × ℕ
hab : x ∈ @antidiagonal _ instAddMonoid _ m
ha : x.1 < n
⊢ HMul.hMul (α := R) (β := R) ((coeff x.1 : (a : R⟦X⟧) → R) (↑((trunc n : (a : R⟦X⟧) → R[X]) f) : R⟦X⟧) : R)
      ((coeff x.2 : (a : R⟦X⟧) → R) g : R) =
    HMul.hMul (α := R) (β := R) ((coeff x.1 : (a : R⟦X⟧) → R) f : R) ((coeff x.2 : (a : R⟦X⟧) → R) g : R)
have pos : HMul.hMul (α := R) (β := R) (Polynomial.coeff ((trunc n : (a : R⟦X⟧) → R[X]) f) x.1 : R)
    ((coeff x.2 : (a : R⟦X⟧) → R) g : R) =
  HMul.hMul (α := R) (β := R) ((coeff x.1 : (a : R⟦X⟧) → R) f : R) ((coeff x.2 : (a : R⟦X⟧) → R) g : R)
Tactic: rw [coeff_coe, coeff_trunc, if_pos ha]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Trunc (goal)
Goal:
R : Type u_2
inst : CommSemiring R
n : ℕ
f g : R⟦X⟧
m : ℕ
h : m < n
x : ℕ × ℕ
hab : x ∈ @antidiagonal _ instAddMonoid _ m
ha : x.1 < n
pos :
  HMul.hMul (α := R) (β := R) (Polynomial.coeff ((trunc n : (a : R⟦X⟧) → R[X]) f) x.1 : R)
      ((coeff x.2 : (a : R⟦X⟧) → R) g : R) =
    HMul.hMul (α := R) (β := R) ((coeff x.1 : (a : R⟦X⟧) → R) f : R) ((coeff x.2 : (a : R⟦X⟧) → R) g : R)
⊢ HMul.hMul (α := R) (β := R) ((coeff x.1 : (a : R⟦X⟧) → R) (↑((trunc n : (a : R⟦X⟧) → R[X]) f) : R⟦X⟧) : R)
      ((coeff x.2 : (a : R⟦X⟧) → R) g : R) =
    HMul.hMul (α := R) (β := R) ((coeff x.1 : (a : R⟦X⟧) → R) f : R) ((coeff x.2 : (a : R⟦X⟧) → R) g : R)
have pos₁ : HMul.hMul (α := R) (β := R) (if x.1 < n then (coeff x.1 : (a : R⟦X⟧) → R) f else 0 : R)
    ((coeff x.2 : (a : R⟦X⟧) → R) g : R) =
  HMul.hMul (α := R) (β := R) ((coeff x.1 : (a : R⟦X⟧) → R) f : R) ((coeff x.2 : (a : R⟦X⟧) → R) g : R)
Tactic: rw [coeff_coe, coeff_trunc, if_pos ha]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Trunc (goal)
Goal:
R : Type u_2
inst : CommSemiring R
n : ℕ
f g : R⟦X⟧
m : ℕ
h : m < n
x : ℕ × ℕ
hab : x ∈ @antidiagonal _ instAddMonoid _ m
ha : x.1 < n
pos :
  HMul.hMul (α := R) (β := R) (Polynomial.coeff ((trunc n : (a : R⟦X⟧) → R[X]) f) x.1 : R)
      ((coeff x.2 : (a : R⟦X⟧) → R) g : R) =
    HMul.hMul (α := R) (β := R) ((coeff x.1 : (a : R⟦X⟧) → R) f : R) ((coeff x.2 : (a : R⟦X⟧) → R) g : R)
pos₁ :
  HMul.hMul (α := R) (β := R) (if x.1 < n then (coeff x.1 : (a : R⟦X⟧) → R) f else 0 : R)
      ((coeff x.2 : (a : R⟦X⟧) → R) g : R) =
    HMul.hMul (α := R) (β := R) ((coeff x.1 : (a : R⟦X⟧) → R) f : R) ((coeff x.2 : (a : R⟦X⟧) → R) g : R)
⊢ HMul.hMul (α := R) (β := R) ((coeff x.1 : (a : R⟦X⟧) → R) (↑((trunc n : (a : R⟦X⟧) → R[X]) f) : R⟦X⟧) : R)
      ((coeff x.2 : (a : R⟦X⟧) → R) g : R) =
    HMul.hMul (α := R) (β := R) ((coeff x.1 : (a : R⟦X⟧) → R) f : R) ((coeff x.2 : (a : R⟦X⟧) → R) g : R)
have pos₂ : HMul.hMul (α := R) (β := R) ((coeff x.1 : (a : R⟦X⟧) → R) f : R) ((coeff x.2 : (a : R⟦X⟧) → R) g : R) =
  HMul.hMul (α := R) (β := R) ((coeff x.1 : (a : R⟦X⟧) → R) f : R) ((coeff x.2 : (a : R⟦X⟧) → R) g : R)
Tactic: rw [coeff_coe, coeff_trunc, if_pos ha]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Trunc (goal)
Goal:
R : Type u_2
inst : CommSemiring R
n : ℕ
f g : R⟦X⟧
⊢ Eq (α := R[X]) ((trunc n : (a : R⟦X⟧) → R[X]) (f * (↑((trunc n : (a : R⟦X⟧) → R[X]) g) : R⟦X⟧)) : R[X])
    ((trunc n : (a : R⟦X⟧) → R[X]) (f * g) : R[X])
have rw : Eq (α := R[X]) ((trunc n : (a : R⟦X⟧) → R[X]) ((↑((trunc n : (a : R⟦X⟧) → R[X]) g) : R⟦X⟧) * f) : R[X])
  ((trunc n : (a : R⟦X⟧) → R[X]) (f * g) : R[X])
Tactic: rw [mul_comm, trunc_trunc_mul, mul_comm]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Trunc (goal)
Goal:
R : Type u_2
inst : CommSemiring R
n : ℕ
f g : R⟦X⟧
rw :
  Eq (α := R[X]) ((trunc n : (a : R⟦X⟧) → R[X]) ((↑((trunc n : (a : R⟦X⟧) → R[X]) g) : R⟦X⟧) * f) : R[X])
    ((trunc n : (a : R⟦X⟧) → R[X]) (f * g) : R[X])
⊢ Eq (α := R[X]) ((trunc n : (a : R⟦X⟧) → R[X]) (f * (↑((trunc n : (a : R⟦X⟧) → R[X]) g) : R⟦X⟧)) : R[X])
    ((trunc n : (a : R⟦X⟧) → R[X]) (f * g) : R[X])
have rw₁ : Eq (α := R[X]) ((trunc n : (a : R⟦X⟧) → R[X]) (g * f) : R[X]) ((trunc n : (a : R⟦X⟧) → R[X]) (f * g) : R[X])
Tactic: rw [mul_comm, trunc_trunc_mul, mul_comm]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Trunc (goal)
Goal:
R : Type u_2
inst : CommSemiring R
n : ℕ
f g : R⟦X⟧
rw :
  Eq (α := R[X]) ((trunc n : (a : R⟦X⟧) → R[X]) ((↑((trunc n : (a : R⟦X⟧) → R[X]) g) : R⟦X⟧) * f) : R[X])
    ((trunc n : (a : R⟦X⟧) → R[X]) (f * g) : R[X])
rw₁ : Eq (α := R[X]) ((trunc n : (a : R⟦X⟧) → R[X]) (g * f) : R[X]) ((trunc n : (a : R⟦X⟧) → R[X]) (f * g) : R[X])
⊢ Eq (α := R[X]) ((trunc n : (a : R⟦X⟧) → R[X]) (f * (↑((trunc n : (a : R⟦X⟧) → R[X]) g) : R⟦X⟧)) : R[X])
    ((trunc n : (a : R⟦X⟧) → R[X]) (f * g) : R[X])
have rw₂ : Eq (α := R[X]) ((trunc n : (a : R⟦X⟧) → R[X]) (f * g) : R[X]) ((trunc n : (a : R⟦X⟧) → R[X]) (f * g) : R[X])
Tactic: rw [mul_comm, trunc_trunc_mul, mul_comm]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Trunc (goal)
Goal:
R : Type u_2
inst : CommSemiring R
n : ℕ
f g : R⟦X⟧
⊢ Eq (α := R[X])
    ((trunc n : (a : R⟦X⟧) → R[X])
        (HMul.hMul (α := R⟦X⟧) (↑((trunc n : (a : R⟦X⟧) → R[X]) f) : R⟦X⟧)
          (↑((trunc n : (a : R⟦X⟧) → R[X]) g) : R⟦X⟧)) :
      R[X])
    ((trunc n : (a : R⟦X⟧) → R[X]) (f * g) : R[X])
have rw : Eq (α := R[X]) ((trunc n : (a : R⟦X⟧) → R[X]) (f * (↑((trunc n : (a : R⟦X⟧) → R[X]) g) : R⟦X⟧)) : R[X])
  ((trunc n : (a : R⟦X⟧) → R[X]) (f * g) : R[X])
Tactic: rw [trunc_trunc_mul, trunc_mul_trunc]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Trunc (goal)
Goal:
R : Type u_2
inst : CommSemiring R
n : ℕ
f g : R⟦X⟧
rw :
  Eq (α := R[X]) ((trunc n : (a : R⟦X⟧) → R[X]) (f * (↑((trunc n : (a : R⟦X⟧) → R[X]) g) : R⟦X⟧)) : R[X])
    ((trunc n : (a : R⟦X⟧) → R[X]) (f * g) : R[X])
⊢ Eq (α := R[X])
    ((trunc n : (a : R⟦X⟧) → R[X])
        (HMul.hMul (α := R⟦X⟧) (↑((trunc n : (a : R⟦X⟧) → R[X]) f) : R⟦X⟧)
          (↑((trunc n : (a : R⟦X⟧) → R[X]) g) : R⟦X⟧)) :
      R[X])
    ((trunc n : (a : R⟦X⟧) → R[X]) (f * g) : R[X])
have rw₁ : Eq (α := R[X]) ((trunc n : (a : R⟦X⟧) → R[X]) (f * g) : R[X]) ((trunc n : (a : R⟦X⟧) → R[X]) (f * g) : R[X])
Tactic: rw [trunc_trunc_mul, trunc_mul_trunc]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Trunc (goal)
Goal:
R : Type u_2
inst : CommSemiring R
f : R⟦X⟧
n : ℕ
⊢ 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])
have zero : Eq (α := R[X]) ((trunc n : (a : R⟦X⟧) → R[X]) 1 : R[X]) ((trunc n : (a : R⟦X⟧) → R[X]) (HPow.hPow (β := ℕ) f 0) : R[X])
Tactic: rw [pow_zero, pow_zero]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Trunc (goal)
Goal:
R : Type u_2
inst : CommSemiring R
f : R⟦X⟧
n : ℕ
zero :
  Eq (α := R[X]) ((trunc n : (a : R⟦X⟧) → R[X]) 1 : 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⟧) 0) :
      R[X])
    ((trunc n : (a : R⟦X⟧) → R[X]) (HPow.hPow (β := ℕ) f 0) : R[X])
have zero₁ : Eq.{u_2 + 1} (α := R[X]) ((trunc n : (a : R⟦X⟧) → R[X]) 1) ((trunc n : (a : R⟦X⟧) → R[X]) 1)
Tactic: rw [pow_zero, pow_zero]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Trunc (goal)
Goal:
R : Type u_2
inst : CommSemiring R
f : R⟦X⟧
n 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])
have succ : Eq (α := R[X])
  ((trunc n : (a : R⟦X⟧) → R[X])
      ((↑((trunc n : (a : R⟦X⟧) → R[X]) f) : 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 + 1)) : R[X])
Tactic: rw [_root_.pow_succ', _root_.pow_succ', trunc_trunc_mul,
      ← trunc_trunc_mul_trunc, ih, trunc_trunc_mul_trunc]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Trunc (goal)
Goal:
R : Type u_2
inst : CommSemiring R
f : R⟦X⟧
n 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])
succ :
  Eq (α := R[X])
    ((trunc n : (a : R⟦X⟧) → R[X])
        ((↑((trunc n : (a : R⟦X⟧) → R[X]) f) : 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 + 1)) : 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])
have succ₁ : Eq (α := R[X])
  ((trunc n : (a : R⟦X⟧) → R[X])
      ((↑((trunc n : (a : R⟦X⟧) → R[X]) f) : 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 * f ^ a) : R[X])
Tactic: rw [_root_.pow_succ', _root_.pow_succ', trunc_trunc_mul,
      ← trunc_trunc_mul_trunc, ih, trunc_trunc_mul_trunc]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Trunc (goal)
Goal:
R : Type u_2
inst : CommSemiring R
f : R⟦X⟧
n 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])
succ :
  Eq (α := R[X])
    ((trunc n : (a : R⟦X⟧) → R[X])
        ((↑((trunc n : (a : R⟦X⟧) → R[X]) f) : 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 + 1)) : R[X])
succ₁ :
  Eq (α := R[X])
    ((trunc n : (a : R⟦X⟧) → R[X])
        ((↑((trunc n : (a : R⟦X⟧) → R[X]) f) : 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 * 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])
have succ₂ : Eq (α := R[X])
  ((trunc n : (a : R⟦X⟧) → R[X]) (f * 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 * f ^ a) : R[X])
Tactic: rw [_root_.pow_succ', _root_.pow_succ', trunc_trunc_mul,
      ← trunc_trunc_mul_trunc, ih, trunc_trunc_mul_trunc]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Trunc (goal)
Goal:
R : Type u_2
inst : CommSemiring R
f : R⟦X⟧
n 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])
succ :
  Eq (α := R[X])
    ((trunc n : (a : R⟦X⟧) → R[X])
        ((↑((trunc n : (a : R⟦X⟧) → R[X]) f) : 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 + 1)) : R[X])
succ₁ :
  Eq (α := R[X])
    ((trunc n : (a : R⟦X⟧) → R[X])
        ((↑((trunc n : (a : R⟦X⟧) → R[X]) f) : 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 * f ^ a) : R[X])
succ₂ :
  Eq (α := R[X])
    ((trunc n : (a : R⟦X⟧) → R[X]) (f * 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 * 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])
have succ₃ : Eq (α := R[X])
  ((trunc n : (a : R⟦X⟧) → R[X])
      (HMul.hMul (α := R⟦X⟧) (↑((trunc n : (a : R⟦X⟧) → R[X]) f) : 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⟧)) :
    R[X])
  ((trunc n : (a : R⟦X⟧) → R[X]) (f * f ^ a) : R[X])
Tactic: rw [_root_.pow_succ', _root_.pow_succ', trunc_trunc_mul,
      ← trunc_trunc_mul_trunc, ih, trunc_trunc_mul_trunc]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Trunc (goal)
Goal:
R : Type u_2
inst : CommSemiring R
f : R⟦X⟧
n 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])
succ :
  Eq (α := R[X])
    ((trunc n : (a : R⟦X⟧) → R[X])
        ((↑((trunc n : (a : R⟦X⟧) → R[X]) f) : 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 + 1)) : R[X])
succ₁ :
  Eq (α := R[X])
    ((trunc n : (a : R⟦X⟧) → R[X])
        ((↑((trunc n : (a : R⟦X⟧) → R[X]) f) : 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 * f ^ a) : R[X])
succ₂ :
  Eq (α := R[X])
    ((trunc n : (a : R⟦X⟧) → R[X]) (f * 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 * f ^ a) : R[X])
succ₃ :
  Eq (α := R[X])
    ((trunc n : (a : R⟦X⟧) → R[X])
        (HMul.hMul (α := R⟦X⟧) (↑((trunc n : (a : R⟦X⟧) → R[X]) f) : 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⟧)) :
      R[X])
    ((trunc n : (a : R⟦X⟧) → R[X]) (f * 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])
have succ₄ : Eq (α := R[X])
  ((trunc n : (a : R⟦X⟧) → R[X])
      (HMul.hMul (α := R⟦X⟧) (↑((trunc n : (a : R⟦X⟧) → R[X]) f) : R⟦X⟧)
        (↑((trunc n : (a : R⟦X⟧) → R[X]) (f ^ a)) : R⟦X⟧)) :
    R[X])
  ((trunc n : (a : R⟦X⟧) → R[X]) (f * f ^ a) : R[X])
Tactic: rw [_root_.pow_succ', _root_.pow_succ', trunc_trunc_mul,
      ← trunc_trunc_mul_trunc, ih, trunc_trunc_mul_trunc]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Trunc (goal)
Goal:
R : Type u_2
inst : CommSemiring R
f : R⟦X⟧
n 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])
succ :
  Eq (α := R[X])
    ((trunc n : (a : R⟦X⟧) → R[X])
        ((↑((trunc n : (a : R⟦X⟧) → R[X]) f) : 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 + 1)) : R[X])
succ₁ :
  Eq (α := R[X])
    ((trunc n : (a : R⟦X⟧) → R[X])
        ((↑((trunc n : (a : R⟦X⟧) → R[X]) f) : 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 * f ^ a) : R[X])
succ₂ :
  Eq (α := R[X])
    ((trunc n : (a : R⟦X⟧) → R[X]) (f * 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 * f ^ a) : R[X])
succ₃ :
  Eq (α := R[X])
    ((trunc n : (a : R⟦X⟧) → R[X])
        (HMul.hMul (α := R⟦X⟧) (↑((trunc n : (a : R⟦X⟧) → R[X]) f) : 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⟧)) :
      R[X])
    ((trunc n : (a : R⟦X⟧) → R[X]) (f * f ^ a) : R[X])
succ₄ :
  Eq (α := R[X])
    ((trunc n : (a : R⟦X⟧) → R[X])
        (HMul.hMul (α := R⟦X⟧) (↑((trunc n : (a : R⟦X⟧) → R[X]) f) : R⟦X⟧)
          (↑((trunc n : (a : R⟦X⟧) → R[X]) (f ^ a)) : R⟦X⟧)) :
      R[X])
    ((trunc n : (a : R⟦X⟧) → R[X]) (f * 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])
have succ₅ : Eq (α := R[X]) ((trunc n : (a : R⟦X⟧) → R[X]) (f * f ^ a) : R[X]) ((trunc n : (a : R⟦X⟧) → R[X]) (f * f ^ a) : R[X])
Tactic: rw [_root_.pow_succ', _root_.pow_succ', trunc_trunc_mul,
      ← trunc_trunc_mul_trunc, ih, trunc_trunc_mul_trunc]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Trunc (goal)
Goal:
R : Type u_2
inst : CommSemiring R
f : R⟦X⟧
n a : ℕ
⊢ 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 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])
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