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
f : R⟦X⟧
n : ℕ
rw :
  ∑ m ∈ Ico 0 n.succ, (Polynomial.monomial m : (a : R) → R[X]) ((coeff m : (a : R⟦X⟧) → R) f) =
    HAdd.hAdd (α := R[X]) (β := R[X]) ((trunc n : (a : R⟦X⟧) → R[X]) f : R[X])
      ((Polynomial.monomial n : (a : R) → R[X]) ((coeff n : (a : R⟦X⟧) → R) f) : R[X])
⊢ (trunc n.succ : (a : R⟦X⟧) → R[X]) f =
    HAdd.hAdd (α := R[X]) (β := R[X]) ((trunc n : (a : R⟦X⟧) → R[X]) f : R[X])
      ((Polynomial.monomial n : (a : R) → R[X]) ((coeff n : (a : R⟦X⟧) → R) f) : R[X])
have rw₁ : ∑ m ∈ range n.succ, (Polynomial.monomial m : (a : R) → R[X]) ((coeff m : (a : R⟦X⟧) → R) f) =
  HAdd.hAdd (α := R[X]) (β := R[X]) ((trunc n : (a : R⟦X⟧) → R[X]) f : R[X])
    ((Polynomial.monomial n : (a : R) → R[X]) ((coeff n : (a : R⟦X⟧) → R) f) : R[X])
Tactic: rw [trunc_apply, Ico_zero_eq_range, sum_range_succ, trunc_apply, Ico_zero_eq_range]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Trunc (goal)
Goal:
R : Type u_1
inst : Semiring R
f : R⟦X⟧
n : ℕ
rw :
  ∑ m ∈ Ico 0 n.succ, (Polynomial.monomial m : (a : R) → R[X]) ((coeff m : (a : R⟦X⟧) → R) f) =
    HAdd.hAdd (α := R[X]) (β := R[X]) ((trunc n : (a : R⟦X⟧) → R[X]) f : R[X])
      ((Polynomial.monomial n : (a : R) → R[X]) ((coeff n : (a : R⟦X⟧) → R) f) : R[X])
rw₁ :
  ∑ m ∈ range n.succ, (Polynomial.monomial m : (a : R) → R[X]) ((coeff m : (a : R⟦X⟧) → R) f) =
    HAdd.hAdd (α := R[X]) (β := R[X]) ((trunc n : (a : R⟦X⟧) → R[X]) f : R[X])
      ((Polynomial.monomial n : (a : R) → R[X]) ((coeff n : (a : R⟦X⟧) → R) f) : R[X])
⊢ (trunc n.succ : (a : R⟦X⟧) → R[X]) f =
    HAdd.hAdd (α := R[X]) (β := R[X]) ((trunc n : (a : R⟦X⟧) → R[X]) f : R[X])
      ((Polynomial.monomial n : (a : R) → R[X]) ((coeff n : (a : R⟦X⟧) → R) f) : R[X])
have rw₂ : HAdd.hAdd (α := R[X]) (β := R[X])
    (∑ x ∈ range n, (Polynomial.monomial x : (a : R) → R[X]) ((coeff x : (a : R⟦X⟧) → R) f) : R[X])
    ((Polynomial.monomial n : (a : R) → R[X]) ((coeff n : (a : R⟦X⟧) → R) f) : R[X]) =
  HAdd.hAdd (α := R[X]) (β := R[X]) ((trunc n : (a : R⟦X⟧) → R[X]) f : R[X])
    ((Polynomial.monomial n : (a : R) → R[X]) ((coeff n : (a : R⟦X⟧) → R) f) : R[X])
Tactic: rw [trunc_apply, Ico_zero_eq_range, sum_range_succ, trunc_apply, Ico_zero_eq_range]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Trunc (goal)
Goal:
R : Type u_1
inst : Semiring R
f : R⟦X⟧
n : ℕ
rw :
  ∑ m ∈ Ico 0 n.succ, (Polynomial.monomial m : (a : R) → R[X]) ((coeff m : (a : R⟦X⟧) → R) f) =
    HAdd.hAdd (α := R[X]) (β := R[X]) ((trunc n : (a : R⟦X⟧) → R[X]) f : R[X])
      ((Polynomial.monomial n : (a : R) → R[X]) ((coeff n : (a : R⟦X⟧) → R) f) : R[X])
rw₁ :
  ∑ m ∈ range n.succ, (Polynomial.monomial m : (a : R) → R[X]) ((coeff m : (a : R⟦X⟧) → R) f) =
    HAdd.hAdd (α := R[X]) (β := R[X]) ((trunc n : (a : R⟦X⟧) → R[X]) f : R[X])
      ((Polynomial.monomial n : (a : R) → R[X]) ((coeff n : (a : R⟦X⟧) → R) f) : R[X])
rw₂ :
  HAdd.hAdd (α := R[X]) (β := R[X])
      (∑ x ∈ range n, (Polynomial.monomial x : (a : R) → R[X]) ((coeff x : (a : R⟦X⟧) → R) f) : R[X])
      ((Polynomial.monomial n : (a : R) → R[X]) ((coeff n : (a : R⟦X⟧) → R) f) : R[X]) =
    HAdd.hAdd (α := R[X]) (β := R[X]) ((trunc n : (a : R⟦X⟧) → R[X]) f : R[X])
      ((Polynomial.monomial n : (a : R) → R[X]) ((coeff n : (a : R⟦X⟧) → R) f) : R[X])
⊢ (trunc n.succ : (a : R⟦X⟧) → R[X]) f =
    HAdd.hAdd (α := R[X]) (β := R[X]) ((trunc n : (a : R⟦X⟧) → R[X]) f : R[X])
      ((Polynomial.monomial n : (a : R) → R[X]) ((coeff n : (a : R⟦X⟧) → R) f) : R[X])
have rw₃ : HAdd.hAdd (α := R[X]) (β := R[X])
    (∑ x ∈ range n, (Polynomial.monomial x : (a : R) → R[X]) ((coeff x : (a : R⟦X⟧) → R) f) : R[X])
    ((Polynomial.monomial n : (a : R) → R[X]) ((coeff n : (a : R⟦X⟧) → R) f) : R[X]) =
  HAdd.hAdd (α := R[X]) (β := R[X])
    (∑ m ∈ Ico 0 n, (Polynomial.monomial m : (a : R) → R[X]) ((coeff m : (a : R⟦X⟧) → R) f) : R[X])
    ((Polynomial.monomial n : (a : R) → R[X]) ((coeff n : (a : R⟦X⟧) → R) f) : R[X])
Tactic: rw [trunc_apply, Ico_zero_eq_range, sum_range_succ, trunc_apply, Ico_zero_eq_range]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Trunc (goal)
Goal:
R : Type u_1
inst : Semiring R
f : R⟦X⟧
n : ℕ
rw :
  ∑ m ∈ Ico 0 n.succ, (Polynomial.monomial m : (a : R) → R[X]) ((coeff m : (a : R⟦X⟧) → R) f) =
    HAdd.hAdd (α := R[X]) (β := R[X]) ((trunc n : (a : R⟦X⟧) → R[X]) f : R[X])
      ((Polynomial.monomial n : (a : R) → R[X]) ((coeff n : (a : R⟦X⟧) → R) f) : R[X])
rw₁ :
  ∑ m ∈ range n.succ, (Polynomial.monomial m : (a : R) → R[X]) ((coeff m : (a : R⟦X⟧) → R) f) =
    HAdd.hAdd (α := R[X]) (β := R[X]) ((trunc n : (a : R⟦X⟧) → R[X]) f : R[X])
      ((Polynomial.monomial n : (a : R) → R[X]) ((coeff n : (a : R⟦X⟧) → R) f) : R[X])
rw₂ :
  HAdd.hAdd (α := R[X]) (β := R[X])
      (∑ x ∈ range n, (Polynomial.monomial x : (a : R) → R[X]) ((coeff x : (a : R⟦X⟧) → R) f) : R[X])
      ((Polynomial.monomial n : (a : R) → R[X]) ((coeff n : (a : R⟦X⟧) → R) f) : R[X]) =
    HAdd.hAdd (α := R[X]) (β := R[X]) ((trunc n : (a : R⟦X⟧) → R[X]) f : R[X])
      ((Polynomial.monomial n : (a : R) → R[X]) ((coeff n : (a : R⟦X⟧) → R) f) : R[X])
rw₃ :
  HAdd.hAdd (α := R[X]) (β := R[X])
      (∑ x ∈ range n, (Polynomial.monomial x : (a : R) → R[X]) ((coeff x : (a : R⟦X⟧) → R) f) : R[X])
      ((Polynomial.monomial n : (a : R) → R[X]) ((coeff n : (a : R⟦X⟧) → R) f) : R[X]) =
    HAdd.hAdd (α := R[X]) (β := R[X])
      (∑ m ∈ Ico 0 n, (Polynomial.monomial m : (a : R) → R[X]) ((coeff m : (a : R⟦X⟧) → R) f) : R[X])
      ((Polynomial.monomial n : (a : R) → R[X]) ((coeff n : (a : R⟦X⟧) → R) f) : R[X])
⊢ (trunc n.succ : (a : R⟦X⟧) → R[X]) f =
    HAdd.hAdd (α := R[X]) (β := R[X]) ((trunc n : (a : R⟦X⟧) → R[X]) f : R[X])
      ((Polynomial.monomial n : (a : R) → R[X]) ((coeff n : (a : R⟦X⟧) → R) f) : R[X])
have rw₄ : HAdd.hAdd (α := R[X]) (β := R[X])
    (∑ x ∈ range n, (Polynomial.monomial x : (a : R) → R[X]) ((coeff x : (a : R⟦X⟧) → R) f) : R[X])
    ((Polynomial.monomial n : (a : R) → R[X]) ((coeff n : (a : R⟦X⟧) → R) f) : R[X]) =
  HAdd.hAdd (α := R[X]) (β := R[X])
    (∑ m ∈ range n, (Polynomial.monomial m : (a : R) → R[X]) ((coeff m : (a : R⟦X⟧) → R) f) : R[X])
    ((Polynomial.monomial n : (a : R) → R[X]) ((coeff n : (a : R⟦X⟧) → R) f) : R[X])
Tactic: rw [trunc_apply, Ico_zero_eq_range, sum_range_succ, trunc_apply, Ico_zero_eq_range]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Trunc (goal)
Goal:
R : Type u_1
inst : Semiring R
S : Type u_2
inst_1 : Semiring S
s : S
G : R →+* S
f : R⟦X⟧
⊢ eval₂ G s ((trunc 0 : (a : R⟦X⟧) → R[X]) f) =
    ∑ i ∈ range 0, HMul.hMul (α := S) ((G : (a : R) → S) ((coeff i : (a : R⟦X⟧) → R) f : R) : S) (s ^ i)
have zero : eval₂ G s 0 = ∑ i ∈ range 0, HMul.hMul (α := S) ((G : (a : R) → S) ((coeff i : (a : R⟦X⟧) → R) f : R) : S) (s ^ i)
Tactic: rw [trunc_zero', range_zero, sum_empty, eval₂_zero]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Trunc (goal)
Goal:
R : Type u_1
inst : Semiring R
S : Type u_2
inst_1 : Semiring S
s : S
G : R →+* S
f : R⟦X⟧
zero :
  eval₂ G s 0 = ∑ i ∈ range 0, HMul.hMul (α := S) ((G : (a : R) → S) ((coeff i : (a : R⟦X⟧) → R) f : R) : S) (s ^ i)
⊢ eval₂ G s ((trunc 0 : (a : R⟦X⟧) → R[X]) f) =
    ∑ i ∈ range 0, HMul.hMul (α := S) ((G : (a : R) → S) ((coeff i : (a : R⟦X⟧) → R) f : R) : S) (s ^ i)
have zero₁ : eval₂ G s 0 = ∑ i ∈ ∅, HMul.hMul (α := S) ((G : (a : R) → S) ((coeff i : (a : R⟦X⟧) → R) f : R) : S) (s ^ i)
Tactic: rw [trunc_zero', range_zero, sum_empty, eval₂_zero]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Trunc (goal)
Goal:
R : Type u_1
inst : Semiring R
S : Type u_2
inst_1 : Semiring S
s : S
G : R →+* S
f : R⟦X⟧
zero :
  eval₂ G s 0 = ∑ i ∈ range 0, HMul.hMul (α := S) ((G : (a : R) → S) ((coeff i : (a : R⟦X⟧) → R) f : R) : S) (s ^ i)
zero₁ : eval₂ G s 0 = ∑ i ∈ ∅, HMul.hMul (α := S) ((G : (a : R) → S) ((coeff i : (a : R⟦X⟧) → R) f : R) : S) (s ^ i)
⊢ eval₂ G s ((trunc 0 : (a : R⟦X⟧) → R[X]) f) =
    ∑ i ∈ range 0, HMul.hMul (α := S) ((G : (a : R) → S) ((coeff i : (a : R⟦X⟧) → R) f : R) : S) (s ^ i)
have zero₂ : eval₂ G s 0 = 0
Tactic: rw [trunc_zero', range_zero, sum_empty, eval₂_zero]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Trunc (goal)
Goal:
R : Type u_1
inst : Semiring R
S : Type u_2
inst_1 : Semiring S
s : S
G : R →+* S
f : R⟦X⟧
zero :
  eval₂ G s 0 = ∑ i ∈ range 0, HMul.hMul (α := S) ((G : (a : R) → S) ((coeff i : (a : R⟦X⟧) → R) f : R) : S) (s ^ i)
zero₁ : eval₂ G s 0 = ∑ i ∈ ∅, HMul.hMul (α := S) ((G : (a : R) → S) ((coeff i : (a : R⟦X⟧) → R) f : R) : S) (s ^ i)
zero₂ : eval₂ G s 0 = 0
⊢ eval₂ G s ((trunc 0 : (a : R⟦X⟧) → R[X]) f) =
    ∑ i ∈ range 0, HMul.hMul (α := S) ((G : (a : R) → S) ((coeff i : (a : R⟦X⟧) → R) f : R) : S) (s ^ i)
have zero₃ : Eq.{u_2 + 1} (α := S) 0 0
Tactic: rw [trunc_zero', range_zero, sum_empty, eval₂_zero]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Trunc (hypothesis)
Goal:
R : Type u_1
inst : Semiring R
S : Type u_2
inst_1 : Semiring S
s : S
G : R →+* S
f : R⟦X⟧
n : ℕ
⊢ eval₂ G s ((trunc (n + 1) : (a : R⟦X⟧) → R[X]) f) =
    ∑ i ∈ range (n + 1), HMul.hMul (α := S) ((G : (a : R) → S) ((coeff i : (a : R⟦X⟧) → R) f : R) : S) (s ^ i)
have this : natDegree.{u_1} (R := R) ((trunc (n + 1) : (a : R⟦X⟧) → R[X]) f) < n + 1
Tactic: have := natDegree_trunc_lt f n
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Trunc (goal)
Goal:
R : Type u_1
inst : Semiring R
S : Type u_2
inst_1 : Semiring S
s : S
G : R →+* S
f : R⟦X⟧
n : ℕ
this : natDegree.{u_1} (R := R) ((trunc (n + 1) : (a : R⟦X⟧) → R[X]) f) < n + 1
⊢ eval₂ G s ((trunc (n + 1) : (a : R⟦X⟧) → R[X]) f) =
    ∑ i ∈ range (n + 1), HMul.hMul (α := S) ((G : (a : R) → S) ((coeff i : (a : R⟦X⟧) → R) f : R) : S) (s ^ i)
have succ : Eq.{u_2 + 1} (α := S)
  (∑ i ∈ range (n + 1),
    HMul.hMul (α := S) ((G : (a : R) → S) (Polynomial.coeff ((trunc (n + 1) : (a : R⟦X⟧) → R[X]) f) i) : S) (s ^ i))
  (∑ i ∈ range (n + 1), HMul.hMul (α := S) ((G : (a : R) → S) ((coeff i : (a : R⟦X⟧) → R) f : R) : S) (s ^ i))
Tactic: rw [eval₂_eq_sum_range' (hn := this)]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Trunc (goal)
Goal:
R : Type u_1
inst : Semiring R
S : Type u_2
inst_1 : Semiring S
s : S
G : R →+* S
f : R⟦X⟧
n : ℕ
this : natDegree.{u_1} (R := R) ((trunc (n + 1) : (a : R⟦X⟧) → R[X]) f) < n + 1
⊢ Eq.{u_2 + 1} (α := S)
    (∑ i ∈ range (n + 1),
      HMul.hMul (α := S) ((G : (a : R) → S) (Polynomial.coeff ((trunc (n + 1) : (a : R⟦X⟧) → R[X]) f) i) : S) (s ^ i))
    (∑ i ∈ range (n + 1), HMul.hMul (α := S) ((G : (a : R) → S) ((coeff i : (a : R⟦X⟧) → R) f : R) : S) (s ^ i))
have succ : ∀ x ∈ range (n + 1),
  HMul.hMul (α := S) ((G : (a : R) → S) (Polynomial.coeff ((trunc (n + 1) : (a : R⟦X⟧) → R[X]) f) x) : S) (s ^ x) =
    HMul.hMul (α := S) ((G : (a : R) → S) ((coeff x : (a : R⟦X⟧) → R) f : R) : S) (s ^ x)
Tactic: apply sum_congr rfl
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Trunc (hypothesis)
Goal:
R : Type u_1
inst : Semiring R
S : Type u_2
inst_1 : Semiring S
s : S
G : R →+* S
f : R⟦X⟧
n : ℕ
this : natDegree.{u_1} (R := R) ((trunc (n + 1) : (a : R⟦X⟧) → R[X]) f) < n + 1
x : ℕ
h : x ∈ range (n + 1)
⊢ HMul.hMul (α := S) ((G : (a : R) → S) (Polynomial.coeff ((trunc (n + 1) : (a : R⟦X⟧) → R[X]) f) x) : S) (s ^ x) =
    HMul.hMul (α := S) ((G : (a : R) → S) ((coeff x : (a : R⟦X⟧) → R) f : R) : S) (s ^ x)
have h₁ : x < n + 1
Tactic: rw [mem_range] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Trunc (goal)
Goal:
R : Type u_1
inst : Semiring R
S : Type u_2
inst_1 : Semiring S
s : S
G : R →+* S
f : R⟦X⟧
n : ℕ
this : natDegree.{u_1} (R := R) ((trunc (n + 1) : (a : R⟦X⟧) → R[X]) f) < n + 1
x : ℕ
h : x < n + 1
⊢ HMul.hMul (α := S) ((G : (a : R) → S) (Polynomial.coeff ((trunc (n + 1) : (a : R⟦X⟧) → R[X]) f) x) : S) (s ^ x) =
    HMul.hMul (α := S) ((G : (a : R) → S) ((coeff x : (a : R⟦X⟧) → R) f : R) : S) (s ^ x)
have succ : Eq (α := R) (Polynomial.coeff ((trunc (n + 1) : (a : R⟦X⟧) → R[X]) f) x : R) ((coeff x : (a : R⟦X⟧) → R) f : R)
Tactic: congr
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Trunc (goal)
Goal:
R : Type u_1
inst : Semiring R
S : Type u_2
inst_1 : Semiring S
s : S
G : R →+* S
f : R⟦X⟧
n : ℕ
this : natDegree.{u_1} (R := R) ((trunc (n + 1) : (a : R⟦X⟧) → R[X]) f) < n + 1
x : ℕ
h : x < n + 1
⊢ Eq (α := R) (Polynomial.coeff ((trunc (n + 1) : (a : R⟦X⟧) → R[X]) f) x : R) ((coeff x : (a : R⟦X⟧) → R) f : R)
have succ : Eq (α := R) (if x < n + 1 then (coeff x : (a : R⟦X⟧) → R) f else 0 : R) ((coeff x : (a : R⟦X⟧) → R) f : R)
Tactic: rw [coeff_trunc, if_pos h]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Trunc (goal)
Goal:
R : Type u_1
inst : Semiring R
S : Type u_2
inst_1 : Semiring S
s : S
G : R →+* S
f : R⟦X⟧
n : ℕ
this : natDegree.{u_1} (R := R) ((trunc (n + 1) : (a : R⟦X⟧) → R[X]) f) < n + 1
x : ℕ
h : x < n + 1
succ : Eq (α := R) (if x < n + 1 then (coeff x : (a : R⟦X⟧) → R) f else 0 : R) ((coeff x : (a : R⟦X⟧) → R) f : R)
⊢ Eq (α := R) (Polynomial.coeff ((trunc (n + 1) : (a : R⟦X⟧) → R[X]) f) x : R) ((coeff x : (a : R⟦X⟧) → R) f : R)
have succ₁ : Eq (α := R) ((coeff x : (a : R⟦X⟧) → R) f : R) ((coeff x : (a : R⟦X⟧) → R) f : R)
Tactic: rw [coeff_trunc, if_pos h]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Trunc (goal)
Goal:
R : Type u_1
inst : Semiring R
S : Type u_2
inst_1 : Semiring S
s : S
G : R →+* S
n : ℕ
f : R⟦X⟧
⊢ eval₂ G s ((trunc n : (a : R⟦X⟧) → R[X]) f) =
    ∑ i ∈ range n, HMul.hMul (α := S) ((G : (a : R) → S) ((coeff i : (a : R⟦X⟧) → R) f : R) : S) (s ^ i)
have zero : eval₂ G s ((trunc 0 : (a : R⟦X⟧) → R[X]) f) =
  ∑ i ∈ range 0, HMul.hMul (α := S) ((G : (a : R) → S) ((coeff i : (a : R⟦X⟧) → R) f : R) : S) (s ^ i)
Tactic: cases n with
  | zero =>
    rw [trunc_zero', range_zero, sum_empty, eval₂_zero]
  | succ n =>
    have := natDegree_trunc_lt f n
    rw [eval₂_eq_sum_range' (hn := this)]
    apply sum_congr rfl
    intro _ h
    rw [mem_range] at h
    congr
    rw [coeff_trunc, if_pos h]
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Trunc (goal)
Goal:
R : Type u_1
inst : Semiring R
S : Type u_2
inst_1 : Semiring S
s : S
G : R →+* S
n : ℕ
f : R⟦X⟧
zero :
  eval₂ G s ((trunc 0 : (a : R⟦X⟧) → R[X]) f) =
    ∑ i ∈ range 0, HMul.hMul (α := S) ((G : (a : R) → S) ((coeff i : (a : R⟦X⟧) → R) f : R) : S) (s ^ i)
⊢ eval₂ G s ((trunc n : (a : R⟦X⟧) → R[X]) f) =
    ∑ i ∈ range n, HMul.hMul (α := S) ((G : (a : R) → S) ((coeff i : (a : R⟦X⟧) → R) f : R) : S) (s ^ i)
have succ : ∀ (n : ℕ),
  eval₂ G s ((trunc (n + 1) : (a : R⟦X⟧) → R[X]) f) =
    ∑ i ∈ range (n + 1), HMul.hMul (α := S) ((G : (a : R) → S) ((coeff i : (a : R⟦X⟧) → R) f : R) : S) (s ^ i)
Tactic: cases n with
  | zero =>
    rw [trunc_zero', range_zero, sum_empty, eval₂_zero]
  | succ n =>
    have := natDegree_trunc_lt f n
    rw [eval₂_eq_sum_range' (hn := this)]
    apply sum_congr rfl
    intro _ h
    rw [mem_range] at h
    congr
    rw [coeff_trunc, if_pos h]
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Trunc (goal)
Goal:
R : Type u_1
inst : Semiring R
n : ℕ
⊢ Eq.{u_1 + 1} (α := R[X]) ((trunc (n + 2) : (a : R⟦X⟧) → R[X]) X : R[X]) (Polynomial.X : R[X])
have a : ∀ (d : ℕ),
  Eq.{u_1 + 1} (α := R) (Polynomial.coeff ((trunc (n + 2) : (a : R⟦X⟧) → R[X]) X) d) (Polynomial.coeff Polynomial.X d)
Tactic: ext d
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Trunc (goal)
Goal:
R : Type u_1
inst : Semiring R
n d : ℕ
⊢ Eq.{u_1 + 1} (α := R) (Polynomial.coeff ((trunc (n + 2) : (a : R⟦X⟧) → R[X]) X) d) (Polynomial.coeff Polynomial.X d)
have a : Eq.{u_1 + 1} (α := R) (if d < n + 2 then if d = 1 then 1 else 0 else 0) (Polynomial.coeff Polynomial.X d)
Tactic: rw [coeff_trunc, coeff_X]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Trunc (goal)
Goal:
R : Type u_1
inst : Semiring R
n d : ℕ
⊢ Eq.{u_1 + 1} (α := R) (if d < n + 2 then if d = 1 then 1 else 0 else 0) (Polynomial.coeff Polynomial.X d)
have pos : ∀ (h₁ : d < n + 2) (h₂ : d = 1), Eq.{u_1 + 1} (α := R) 1 (Polynomial.coeff Polynomial.X d)
Tactic: split_ifs with h₁ h₂
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Trunc (goal)
Goal:
R : Type u_1
inst : Semiring R
n d : ℕ
pos : ∀ (h₁ : d < n + 2) (h₂ : d = 1), Eq.{u_1 + 1} (α := R) 1 (Polynomial.coeff Polynomial.X d)
⊢ Eq.{u_1 + 1} (α := R) (if d < n + 2 then if d = 1 then 1 else 0 else 0) (Polynomial.coeff Polynomial.X d)
have neg : ∀ (h₁ : d < n + 2) (h₂ : ¬d = 1), Eq.{u_1 + 1} (α := R) 0 (Polynomial.coeff Polynomial.X d)
Tactic: split_ifs with h₁ h₂
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Trunc (goal)
Goal:
R : Type u_1
inst : Semiring R
n d : ℕ
pos : ∀ (h₁ : d < n + 2) (h₂ : d = 1), Eq.{u_1 + 1} (α := R) 1 (Polynomial.coeff Polynomial.X d)
neg : ∀ (h₁ : d < n + 2) (h₂ : ¬d = 1), Eq.{u_1 + 1} (α := R) 0 (Polynomial.coeff Polynomial.X d)
⊢ Eq.{u_1 + 1} (α := R) (if d < n + 2 then if d = 1 then 1 else 0 else 0) (Polynomial.coeff Polynomial.X d)
have neg₁ : ∀ (h₁ : ¬d < n + 2), Eq.{u_1 + 1} (α := R) 0 (Polynomial.coeff Polynomial.X d)
Tactic: split_ifs with h₁ h₂
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Trunc (goal)
Goal:
R : Type u_1
inst : Semiring R
n d : ℕ
h₁ : d < n + 2
h₂ : d = 1
⊢ Eq.{u_1 + 1} (α := R) 1 (Polynomial.coeff Polynomial.X d)
have pos : Eq.{u_1 + 1} (α := R) 1 (Polynomial.coeff Polynomial.X 1)
Tactic: rw [h₂, coeff_X_one]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Trunc (goal)
Goal:
R : Type u_1
inst : Semiring R
n d : ℕ
h₁ : d < n + 2
h₂ : d = 1
pos : Eq.{u_1 + 1} (α := R) 1 (Polynomial.coeff Polynomial.X 1)
⊢ Eq.{u_1 + 1} (α := R) 1 (Polynomial.coeff Polynomial.X d)
have pos₁ : Eq.{u_1 + 1} (α := R) 1 1
Tactic: rw [h₂, coeff_X_one]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Trunc (goal)
Goal:
R : Type u_1
inst : Semiring R
n d : ℕ
h₁ : d < n + 2
h₂ : ¬d = 1
⊢ Eq.{u_1 + 1} (α := R) 0 (Polynomial.coeff Polynomial.X d)
have neg : Eq.{u_1 + 1} (α := R) 0 0
Tactic: rw [coeff_X_of_ne_one h₂]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Trunc (goal)
Goal:
R : Type u_1
inst : Semiring R
n d : ℕ
h₁ : ¬d < n + 2
⊢ Eq.{u_1 + 1} (α := R) 0 (Polynomial.coeff Polynomial.X d)
have neg : d ≠ 1
Tactic: rw [coeff_X_of_ne_one]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Trunc (goal)
Goal:
R : Type u_1
inst : Semiring R
n d : ℕ
h₁ : ¬d < n + 2
hd : d = 1
⊢ False
have neg : d < n + 2
Tactic: apply h₁
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Trunc (goal)
Goal:
R : Type u_1
inst : Semiring R
n d : ℕ
h₁ : ¬d < n + 2
hd : d = 1
⊢ d < n + 2
have neg : 1 < n + 2
Tactic: rw [hd]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Trunc (goal)
Goal:
R : Type u_1
inst : Semiring R
n : ℕ
hn : 2 ≤ n
⊢ Eq.{u_1 + 1} (α := R[X]) ((trunc n : (a : R⟦X⟧) → R[X]) X : R[X]) (Polynomial.X : R[X])
have obtain : ∀ (n : ℕ) (hn : 2 ≤ n + 2),
  Eq.{u_1 + 1} (α := R[X]) ((trunc (n + 2) : (a : R⟦X⟧) → R[X]) X : R[X]) (Polynomial.X : R[X])
Tactic: obtain ⟨n, rfl⟩ := Nat.exists_eq_add_of_le' hn
Cleared hypotheses: n, hn
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Trunc (goal)
Goal:
R : Type u_1
inst : Semiring R
p : R⟦X⟧
⊢ Eq (α := R[X]) ((trunc 1 : (a : R⟦X⟧) → R[X]) p : R[X])
    ((Polynomial.C : (a : R) → R[X]) ((coeff 0 : (a : R⟦X⟧) → R) p) : R[X])
have a : ∀ (i : ℕ),
  Eq.{u_1 + 1} (α := R) (Polynomial.coeff ((trunc 1 : (a : R⟦X⟧) → R[X]) p) i)
    (Polynomial.coeff ((Polynomial.C : (a : R) → R[X]) ((coeff 0 : (a : R⟦X⟧) → R) p)) i)
Tactic: ext i
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Trunc (goal)
Goal:
R : Type u_1
inst : Semiring R
n : ℕ
r : R
f : R⟦X⟧
⊢ (trunc n : (a : R⟦X⟧) → R[X]) (HMul.hMul (α := R⟦X⟧) ((C : (a : R) → R⟦X⟧) r : R⟦X⟧) f) =
    HMul.hMul (α := R[X]) (β := R[X]) ((Polynomial.C : (a : R) → R[X]) r : R[X])
      ((trunc n : (a : R⟦X⟧) → R[X]) f : R[X])
have a : ∀ (i : ℕ),
  Polynomial.coeff ((trunc n : (a : R⟦X⟧) → R[X]) (HMul.hMul (α := R⟦X⟧) ((C : (a : R) → R⟦X⟧) r : R⟦X⟧) f)) i =
    (HMul.hMul (α := R[X]) (β := R[X]) ((Polynomial.C : (a : R) → R[X]) r : R[X])
          ((trunc n : (a : R⟦X⟧) → R[X]) f : R[X])).coeff
      i
Tactic: ext i
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Trunc (goal)
Goal:
R : Type u_1
inst : Semiring R
n : ℕ
f : R⟦X⟧
r : R
⊢ (trunc n : (a : R⟦X⟧) → R[X]) (HMul.hMul (β := R⟦X⟧) f ((C : (a : R) → R⟦X⟧) r : R⟦X⟧)) =
    HMul.hMul (α := R[X]) (β := R[X]) ((trunc n : (a : R⟦X⟧) → R[X]) f : R[X])
      ((Polynomial.C : (a : R) → R[X]) r : R[X])
have a : ∀ (i : ℕ),
  Polynomial.coeff ((trunc n : (a : R⟦X⟧) → R[X]) (HMul.hMul (β := R⟦X⟧) f ((C : (a : R) → R⟦X⟧) r : R⟦X⟧))) i =
    (HMul.hMul (α := R[X]) (β := R[X]) ((trunc n : (a : R⟦X⟧) → R[X]) f : R[X])
          ((Polynomial.C : (a : R) → R[X]) r : R[X])).coeff
      i
Tactic: ext i
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Trunc (goal)
Goal:
R : Type u_1
inst : Semiring R
n : ℕ
f : R⟦X⟧
⊢ f =
    (mk fun (i : ℕ) ↦ (coeff (i + n) : (a : R⟦X⟧) → R) f) * HPow.hPow (α := R⟦X⟧) X n +
      (↑((trunc n : (a : R⟦X⟧) → R[X]) f) : R⟦X⟧)
have h : ∀ (j : ℕ),
  Eq (α := R) ((coeff j : (a : R⟦X⟧) → R) f : R)
    ((coeff j : (a : R⟦X⟧) → R)
        ((mk fun (i : ℕ) ↦ (coeff (i + n) : (a : R⟦X⟧) → R) f) * HPow.hPow (α := R⟦X⟧) X n +
          (↑((trunc n : (a : R⟦X⟧) → R[X]) f) : R⟦X⟧)) :
      R)
Tactic: ext j
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Trunc (goal)
Goal:
R : Type u_1
inst : Semiring R
n : ℕ
f : R⟦X⟧
j : ℕ
⊢ Eq (α := R) ((coeff j : (a : R⟦X⟧) → R) f : R)
    ((coeff j : (a : R⟦X⟧) → R)
        ((mk fun (i : ℕ) ↦ (coeff (i + n) : (a : R⟦X⟧) → R) f) * HPow.hPow (α := R⟦X⟧) X n +
          (↑((trunc n : (a : R⟦X⟧) → R[X]) f) : R⟦X⟧)) :
      R)
have h : (coeff j : (a : R⟦X⟧) → R) f =
  HAdd.hAdd (α := R) (β := R)
    (if n ≤ j then (coeff (j - n) : (a : R⟦X⟧) → R) (mk fun (i : ℕ) ↦ (coeff (i + n) : (a : R⟦X⟧) → R) f) else 0 : R)
    (if j < n then (coeff j : (a : R⟦X⟧) → R) f else 0 : R)
Tactic: rw [map_add, Polynomial.coeff_coe, coeff_mul_X_pow', coeff_trunc]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Trunc (goal)
Goal:
R : Type u_1
inst : Semiring R
n : ℕ
f : R⟦X⟧
j : ℕ
⊢ (coeff j : (a : R⟦X⟧) → R) f =
    HAdd.hAdd (α := R) (β := R)
      (if n ≤ j then (coeff (j - n) : (a : R⟦X⟧) → R) (mk fun (i : ℕ) ↦ (coeff (i + n) : (a : R⟦X⟧) → R) f) else 0 : R)
      (if j < n then (coeff j : (a : R⟦X⟧) → R) f else 0 : R)
have h : (coeff j : (a : R⟦X⟧) → R) f =
  if n ≤ j then
    HAdd.hAdd (α := R) (β := R)
      ((coeff (j - n) : (a : R⟦X⟧) → R) (mk fun (i : ℕ) ↦ (coeff (i + n) : (a : R⟦X⟧) → R) f) : R) (0 : R)
  else HAdd.hAdd (α := R) (β := R) (0 : R) ((coeff j : (a : R⟦X⟧) → R) f : R)
Tactic: simp_rw [← not_le, ite_not, ite_add_ite]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Trunc (goal)
Goal:
R : Type u_1
inst : Semiring R
n : ℕ
f : R⟦X⟧
⊢ f =
    (HPow.hPow (α := R⟦X⟧) X n * mk fun (i : ℕ) ↦ (coeff (i + n) : (a : R⟦X⟧) → R) f) +
      (↑((trunc n : (a : R⟦X⟧) → R[X]) f) : R⟦X⟧)
have rw : f =
  (mk fun (i : ℕ) ↦ (coeff (i + n) : (a : R⟦X⟧) → R) f) * HPow.hPow (α := R⟦X⟧) X n +
    (↑((trunc n : (a : R⟦X⟧) → R[X]) f) : R⟦X⟧)
Tactic: rw [← (commute_X_pow _ n).eq, ← eq_shift_mul_X_pow_add_trunc]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Trunc (goal)
Goal:
R : Type u_1
inst : Semiring R
n : ℕ
f : R⟦X⟧
rw :
  f =
    (mk fun (i : ℕ) ↦ (coeff (i + n) : (a : R⟦X⟧) → R) f) * HPow.hPow (α := R⟦X⟧) X n +
      (↑((trunc n : (a : R⟦X⟧) → R[X]) f) : R⟦X⟧)
⊢ f =
    (HPow.hPow (α := R⟦X⟧) X n * mk fun (i : ℕ) ↦ (coeff (i + n) : (a : R⟦X⟧) → R) f) +
      (↑((trunc n : (a : R⟦X⟧) → R[X]) f) : R⟦X⟧)
have rw₁ : f = f
Tactic: rw [← (commute_X_pow _ n).eq, ← eq_shift_mul_X_pow_add_trunc]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Trunc (goal)
Goal:
R : Type u_1
inst : Semiring R
r : R
n : ℕ
⊢ (monomial n : (a : R) → R⟦X⟧) r = HMul.hMul (α := R⟦X⟧) ((C : (a : R) → R⟦X⟧) r : R⟦X⟧) (HPow.hPow (α := R⟦X⟧) X n)
have h : ∀ (n_1 : ℕ),
  Eq (α := R) ((coeff n_1 : (a : R⟦X⟧) → R) ((monomial n : (a : R) → R⟦X⟧) r : R⟦X⟧) : R)
    ((coeff n_1 : (a : R⟦X⟧) → R) (HMul.hMul (α := R⟦X⟧) ((C : (a : R) → R⟦X⟧) r : R⟦X⟧) (HPow.hPow (α := R⟦X⟧) X n)) :
      R)
Tactic: ext