awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.PowerSeries.Trunc
Goal:
R : Type u_1
inst : Semiring R
n : ℕ
φ ψ : R⟦X⟧
m : ℕ
simp :
  (if m < n then (coeff m : (a : R⟦X⟧) → R) (φ + ψ) else 0) =
    HAdd.hAdd (α := R) (β := R) (if m < n then (coeff m : (a : R⟦X⟧) → R) φ else 0 : R)
      (if m < n then (coeff m : (a : R⟦X⟧) → R) ψ else 0 : R)
⊢ Polynomial.coeff (trunc_aux n (φ + ψ)) m = (HAdd.hAdd (α := R[X]) (trunc_aux n φ) (trunc_aux n ψ)).coeff m

Tactic:
simp only [coeff_trunc_aux, Polynomial.coeff_add]

Premises used: Polynomial.coeff_add, _private.0.PowerSeries.coeff_trunc_aux
-- Module: Mathlib.RingTheory.PowerSeries.Trunc
Goal:
R : Type u_1
inst : Semiring R
n : ℕ
φ ψ : R⟦X⟧
m : ℕ
pos :
  ∀ (H : m < n),
    (coeff m : (a : R⟦X⟧) → R) (φ + ψ) =
      HAdd.hAdd (α := R) (β := R) ((coeff m : (a : R⟦X⟧) → R) φ : R) ((coeff m : (a : R⟦X⟧) → R) ψ : R)
neg : ∀ (H : ¬m < n), 0 = HAdd.hAdd (α := R) 0 0
⊢ (if m < n then (coeff m : (a : R⟦X⟧) → R) (φ + ψ) else 0) =
    HAdd.hAdd (α := R) (β := R) (if m < n then (coeff m : (a : R⟦X⟧) → R) φ else 0 : R)
      (if m < n then (coeff m : (a : R⟦X⟧) → R) ψ else 0 : R)

Tactic:
split_ifs with H
-- Module: Mathlib.RingTheory.PowerSeries.Trunc
Goal:
R : Type u_1
inst : Semiring R
n : ℕ
φ ψ : R⟦X⟧
m : ℕ
H : m < n
⊢ (coeff m : (a : R⟦X⟧) → R) (φ + ψ) =
    HAdd.hAdd (α := R) (β := R) ((coeff m : (a : R⟦X⟧) → R) φ : R) ((coeff m : (a : R⟦X⟧) → R) ψ : R)

Tactic:
rfl
-- Module: Mathlib.RingTheory.PowerSeries.Trunc
Goal:
R : Type u_1
inst : Semiring R
n : ℕ
φ ψ : R⟦X⟧
m : ℕ
H : ¬m < n
neg neg₁ : Eq.{u_1 + 1} (α := R) 0 0
⊢ 0 = HAdd.hAdd (α := R) 0 0

Tactic:
rw [zero_add]

Premises used: zero_add
-- Module: Mathlib.RingTheory.PowerSeries.Trunc
Goal:
R : Type u_1
inst : Semiring R
n : ℕ
t : R
φ : R⟦X⟧
a :
  ∀ (n_1 : ℕ),
    Polynomial.coeff (trunc_aux n (t • φ)) n_1 =
      (HSMul.hSMul (α := R) (β := R[X]) ((RingHom.id R : (a : R) → R) t : R) (trunc_aux n φ)).coeff n_1
⊢ trunc_aux n (t • φ) = HSMul.hSMul (α := R) (β := R[X]) ((RingHom.id R : (a : R) → R) t : R) (trunc_aux n φ)

Tactic:
ext
-- Module: Mathlib.RingTheory.PowerSeries.Trunc
Goal:
R : Type u_1
inst : Semiring R
n : ℕ
t : R
φ : R⟦X⟧
n_1 : ℕ
⊢ Polynomial.coeff (trunc_aux n (t • φ)) n_1 =
    (HSMul.hSMul (α := R) (β := R[X]) ((RingHom.id R : (a : R) → R) t : R) (trunc_aux n φ)).coeff n_1

Tactic:
simp [trunc_aux, Polynomial.coeff_monomial]

Premises used: Polynomial.coeff_monomial, _private.0.PowerSeries.trunc_aux
-- Module: Mathlib.RingTheory.PowerSeries.Trunc
Goal:
R : Type u_1
inst : Semiring R
n : ℕ
φ : R⟦X⟧
⊢ Eq (α := R[X]) ((trunc n : (a : R⟦X⟧) → R[X]) φ : R[X])
    (∑ m ∈ Ico 0 n, (Polynomial.monomial m : (a : R) → R[X]) ((coeff m : (a : R⟦X⟧) → R) φ) : R[X])

Tactic:
rfl

Premises used: Multiset.sum, Multiset.foldr, _private.0.PowerSeries.trunc_aux, Finset.sum, rfl
-- Module: Mathlib.RingTheory.PowerSeries.Trunc
Goal:
R : Type u_1
inst : Semiring R
m n : ℕ
φ : R⟦X⟧
⊢ Eq (α := R) (Polynomial.coeff ((trunc n : (a : R⟦X⟧) → R[X]) φ) m : R)
    (if m < n then (coeff m : (a : R⟦X⟧) → R) φ else 0 : R)

Tactic:
simp [trunc, coeff_trunc_aux]

Premises used: _private.0.PowerSeries.coeff_trunc_aux, PowerSeries.trunc
-- Module: Mathlib.RingTheory.PowerSeries.Trunc
Goal:
R : Type u_1
inst : Semiring R
n m : ℕ
⊢ Eq.{u_1 + 1} (α := R) (Polynomial.coeff ((trunc (n + 1) : (a : R⟦X⟧) → R[X]) 1) m) (Polynomial.coeff 1 m)

Tactic:
grind [PowerSeries.coeff_trunc, PowerSeries.coeff_one, Polynomial.coeff_one]

Premises used: Polynomial.coeff_one, PowerSeries.coeff_trunc, PowerSeries.coeff_one
-- Module: Mathlib.RingTheory.PowerSeries.Trunc
Goal:
R : Type u_1
inst : Semiring R
n : ℕ
a : R
m : ℕ
rw : (if m < n + 1 then if m = 0 then a else 0 else 0) = if m = 0 then a else 0
⊢ Eq.{u_1 + 1} (α := R) (Polynomial.coeff ((trunc (n + 1) : (a : R⟦X⟧) → R[X]) ((C : (a : R) → R⟦X⟧) a)) m)
    (Polynomial.coeff ((Polynomial.C : (a : R) → R[X]) a) m)

Tactic:
rw [coeff_trunc, coeff_C, Polynomial.coeff_C]

Premises used: PowerSeries.coeff_trunc, Polynomial.coeff_C, PowerSeries.coeff_C
-- Module: Mathlib.RingTheory.PowerSeries.Trunc
Goal:
R : Type u_1
inst : Semiring R
n : ℕ
a : R
m : ℕ
pos : ∀ (H : m < n + 1), m = 0 → a = a
neg : ∀ (H : m < n + 1), ¬m = 0 → Eq.{u_1 + 1} (α := R) 0 0
pos₁ : ∀ (H : ¬m < n + 1), m = 0 → 0 = a
neg₁ : ∀ (H : ¬m < n + 1), ¬m = 0 → Eq.{u_1 + 1} (α := R) 0 0
⊢ (if m < n + 1 then if m = 0 then a else 0 else 0) = if m = 0 then a else 0

Tactic:
split_ifs with H
-- Module: Mathlib.RingTheory.PowerSeries.Trunc
Goal:
R : Type u_1
inst : Semiring R
n : ℕ
a : R
m : ℕ
H : m < n + 1
h : m = 0
⊢ a = a

Tactic:
rfl
-- Module: Mathlib.RingTheory.PowerSeries.Trunc
Goal:
R : Type u_1
inst : Semiring R
n : ℕ
a : R
m : ℕ
H : m < n + 1
h : m = 0
⊢ a = a

Tactic:
first | rfl | try simp_all
-- Module: Mathlib.RingTheory.PowerSeries.Trunc
Goal:
R : Type u_1
inst : Semiring R
n : ℕ
a : R
m : ℕ
H : m < n + 1
h : ¬m = 0
⊢ Eq.{u_1 + 1} (α := R) 0 0

Tactic:
rfl
-- Module: Mathlib.RingTheory.PowerSeries.Trunc
Goal:
R : Type u_1
inst : Semiring R
n : ℕ
a : R
m : ℕ
H : m < n + 1
h : ¬m = 0
⊢ Eq.{u_1 + 1} (α := R) 0 0

Tactic:
first | rfl | try simp_all
-- Module: Mathlib.RingTheory.PowerSeries.Trunc
Goal:
R : Type u_1
inst : Semiring R
n : ℕ
a : R
m : ℕ
H : ¬m < n + 1
h : m = 0
⊢ 0 = a

Tactic:
simp_all
-- Module: Mathlib.RingTheory.PowerSeries.Trunc
Goal:
R : Type u_1
inst : Semiring R
n : ℕ
a : R
m : ℕ
H : ¬m < n + 1
h : m = 0
⊢ 0 = a

Tactic:
try simp_all
-- Module: Mathlib.RingTheory.PowerSeries.Trunc
Goal:
R : Type u_1
inst : Semiring R
n : ℕ
a : R
m : ℕ
H : ¬m < n + 1
h : m = 0
⊢ 0 = a

Tactic:
first | rfl | try simp_all
-- Module: Mathlib.RingTheory.PowerSeries.Trunc
Goal:
R : Type u_1
inst : Semiring R
n : ℕ
a : R
m : ℕ
H : ¬m < n + 1
h : ¬m = 0
⊢ Eq.{u_1 + 1} (α := R) 0 0

Tactic:
rfl
-- Module: Mathlib.RingTheory.PowerSeries.Trunc
Goal:
R : Type u_1
inst : Semiring R
n : ℕ
a : R
m : ℕ
H : ¬m < n + 1
h : ¬m = 0
⊢ Eq.{u_1 + 1} (α := R) 0 0

Tactic:
first | rfl | try simp_all
-- Module: Mathlib.RingTheory.PowerSeries.Trunc
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])
rw₄ 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])
⊢ (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])

Tactic:
rw [trunc_apply, Ico_zero_eq_range, sum_range_succ, trunc_apply, Ico_zero_eq_range]

Premises used: PowerSeries.trunc_apply, Nat.Ico_zero_eq_range, Finset.sum_range_succ
-- Module: Mathlib.RingTheory.PowerSeries.Trunc
Goal:
R : Type u_1
inst : Semiring R
f : R⟦X⟧
n : ℕ
⊢ natDegree.{u_1} (R := R) ((trunc (n + 1) : (a : R⟦X⟧) → R[X]) f) < n + 1

Tactic:
simp +contextual [natDegree_le_iff_coeff_eq_zero, coeff_trunc]

Premises used: Polynomial.natDegree_le_iff_coeff_eq_zero, PowerSeries.coeff_trunc
-- Module: Mathlib.RingTheory.PowerSeries.Trunc
Goal:
R : Type u_1
inst : Semiring R
f : R⟦X⟧
⊢ Eq (α := R[X]) ((trunc 0 : (a : R⟦X⟧) → R[X]) f : R[X]) (0 : R[X])

Tactic:
rfl

Premises used: Multiset.sum, Multiset.foldr, _private.0.PowerSeries.trunc_aux, List.foldr, Finset.sum, rfl
-- Module: Mathlib.RingTheory.PowerSeries.Trunc
Goal:
R : Type u_1
inst : Semiring R
f : R⟦X⟧
n : ℕ
⊢ degree.{u_1} (R := R) ((trunc n : (a : R⟦X⟧) → R[X]) f) < (↑n : WithBot ℕ)

Tactic:
simp +contextual [degree_lt_iff_coeff_zero, coeff_trunc]

Premises used: PowerSeries.coeff_trunc, Polynomial.degree_lt_iff_coeff_zero
-- Module: Mathlib.RingTheory.PowerSeries.Trunc
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
zero₃ zero₄ : Eq.{u_2 + 1} (α := 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)

Tactic:
rw [trunc_zero', range_zero, sum_empty, eval₂_zero]

Premises used: Polynomial.eval₂_zero, Finset.sum_empty, PowerSeries.trunc_zero', Finset.range_zero
-- Module: Mathlib.RingTheory.PowerSeries.Trunc
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 : ℕ
⊢ natDegree.{u_1} (R := R) ((trunc (n + 1) : (a : R⟦X⟧) → R[X]) f) < n + 1

Tactic:
have := natDegree_trunc_lt f n
-- Module: Mathlib.RingTheory.PowerSeries.Trunc
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
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))
⊢ 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:
rw [eval₂_eq_sum_range' (hn := this)]

Premises used: Polynomial.eval₂_eq_sum_range'
-- Module: Mathlib.RingTheory.PowerSeries.Trunc
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
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)
⊢ 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:
apply sum_congr rfl

Premises used: Finset.sum_congr, rfl
-- Module: Mathlib.RingTheory.PowerSeries.Trunc
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)
⊢ x < n + 1

Tactic:
rw [mem_range] at h

Premises used: Finset.mem_range
-- Module: Mathlib.RingTheory.PowerSeries.Trunc
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) (Polynomial.coeff ((trunc (n + 1) : (a : R⟦X⟧) → R[X]) f) x : R) ((coeff x : (a : R⟦X⟧) → R) f : R)
⊢ 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:
congr
-- Module: Mathlib.RingTheory.PowerSeries.Trunc
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)
succ₁ succ₂ : Eq (α := R) ((coeff x : (a : R⟦X⟧) → R) f : 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)

Tactic:
rw [coeff_trunc, if_pos h]

Premises used: PowerSeries.coeff_trunc, if_pos
-- Module: Mathlib.RingTheory.PowerSeries.Trunc
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)
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)
⊢ 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)

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]

Premises used: PowerSeries.coeff_trunc, Polynomial.eval₂_zero, Finset.mem_range, Nat.zero, Finset.sum_empty, Nat.succ, PowerSeries.trunc_zero', Finset.sum_congr, rfl, Finset.range_zero
-- Module: Mathlib.RingTheory.PowerSeries.Trunc
Goal:
R : Type u_1
inst : Semiring R
n : ℕ
a :
  ∀ (d : ℕ),
    Eq.{u_1 + 1} (α := R) (Polynomial.coeff ((trunc (n + 2) : (a : R⟦X⟧) → R[X]) X) d) (Polynomial.coeff Polynomial.X d)
⊢ Eq.{u_1 + 1} (α := R[X]) ((trunc (n + 2) : (a : R⟦X⟧) → R[X]) X : R[X]) (Polynomial.X : R[X])

Tactic:
ext d
-- Module: Mathlib.RingTheory.PowerSeries.Trunc
Goal:
R : Type u_1
inst : Semiring R
n d : ℕ
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)
⊢ Eq.{u_1 + 1} (α := R) (Polynomial.coeff ((trunc (n + 2) : (a : R⟦X⟧) → R[X]) X) d) (Polynomial.coeff Polynomial.X d)

Tactic:
rw [coeff_trunc, coeff_X]

Premises used: PowerSeries.coeff_trunc, PowerSeries.coeff_X
-- Module: Mathlib.RingTheory.PowerSeries.Trunc
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)
neg₁ : ∀ (h₁ : ¬d < n + 2), 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)

Tactic:
split_ifs with h₁ h₂
-- Module: Mathlib.RingTheory.PowerSeries.Trunc
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)
pos₁ pos₂ : Eq.{u_1 + 1} (α := R) 1 1
⊢ Eq.{u_1 + 1} (α := R) 1 (Polynomial.coeff Polynomial.X d)

Tactic:
rw [h₂, coeff_X_one]

Premises used: Polynomial.coeff_X_one
-- Module: Mathlib.RingTheory.PowerSeries.Trunc
Goal:
R : Type u_1
inst : Semiring R
n d : ℕ
h₁ : d < n + 2
h₂ : ¬d = 1
neg neg₁ : Eq.{u_1 + 1} (α := R) 0 0
⊢ Eq.{u_1 + 1} (α := R) 0 (Polynomial.coeff Polynomial.X d)

Tactic:
rw [coeff_X_of_ne_one h₂]

Premises used: Polynomial.coeff_X_of_ne_one
-- Module: Mathlib.RingTheory.PowerSeries.Trunc
Goal:
R : Type u_1
inst : Semiring R
n d : ℕ
h₁ : ¬d < n + 2
neg : d ≠ 1
⊢ Eq.{u_1 + 1} (α := R) 0 (Polynomial.coeff Polynomial.X d)

Tactic:
rw [coeff_X_of_ne_one]

Premises used: Polynomial.coeff_X_of_ne_one
-- Module: Mathlib.RingTheory.PowerSeries.Trunc
Goal:
R : Type u_1
inst : Semiring R
n d : ℕ
h₁ : ¬d < n + 2
hd : d = 1
neg : d < n + 2
⊢ False

Tactic:
apply h₁
-- Module: Mathlib.RingTheory.PowerSeries.Trunc
Goal:
R : Type u_1
inst : Semiring R
n d : ℕ
h₁ : ¬d < n + 2
hd : d = 1
neg : 1 < n + 2
⊢ d < n + 2

Tactic:
rw [hd]
-- Module: Mathlib.RingTheory.PowerSeries.Trunc
Goal:
R : Type u_1
inst : Semiring R
n d : ℕ
h₁ : ¬d < n + 2
hd : d = 1
⊢ 1 < n + 2

Tactic:
n.one_lt_succ_succ

Premises used: Nat.one_lt_succ_succ
-- Module: Mathlib.RingTheory.PowerSeries.Trunc
Goal:
R : Type u_1
inst : Semiring R
n d : ℕ
h₁ : ¬d < n + 2
hd : d = 1
⊢ 1 < n + 2

Tactic:
exact n.one_lt_succ_succ

Premises used: Nat.one_lt_succ_succ
-- Module: Mathlib.RingTheory.PowerSeries.Trunc
Goal:
R : Type u_1
inst : Semiring R
n : ℕ
hn : 2 ≤ n
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])
⊢ Eq.{u_1 + 1} (α := R[X]) ((trunc n : (a : R⟦X⟧) → R[X]) X : R[X]) (Polynomial.X : R[X])

Tactic:
obtain ⟨n, rfl⟩ := Nat.exists_eq_add_of_le' hn

Premises used: Nat.exists_eq_add_of_le', rfl
-- Module: Mathlib.RingTheory.PowerSeries.Trunc
Goal:
R : Type u_1
inst : Semiring R
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:
trunc_X n

Premises used: PowerSeries.trunc_X
-- Module: Mathlib.RingTheory.PowerSeries.Trunc
Goal:
R : Type u_1
inst : Semiring R
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:
exact trunc_X n

Premises used: PowerSeries.trunc_X
-- Module: Mathlib.RingTheory.PowerSeries.Trunc
Goal:
R : Type u_1
inst : Semiring R
p : R⟦X⟧
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)
⊢ 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])

Tactic:
ext i
-- Module: Mathlib.RingTheory.PowerSeries.Trunc
Goal:
R : Type u_1
inst : Semiring R
p : R⟦X⟧
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:
simp +contextual [coeff_trunc, Polynomial.coeff_C]

Premises used: PowerSeries.coeff_trunc, Polynomial.coeff_C
-- Module: Mathlib.RingTheory.PowerSeries.Trunc
Goal:
R : Type u_1
inst : Semiring R
⊢ Eq.{u_1 + 1} (α := R[X]) ((trunc 1 : (a : R⟦X⟧) → R[X]) X : R[X]) (0 : R[X])

Tactic:
simp
-- Module: Mathlib.RingTheory.PowerSeries.Trunc
Goal:
R : Type u_1
inst : Semiring R
n : ℕ
r : R
f : R⟦X⟧
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
⊢ (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])

Tactic:
ext i
-- Module: Mathlib.RingTheory.PowerSeries.Trunc
Goal:
R : Type u_1
inst : Semiring R
n : ℕ
r : R
f : R⟦X⟧
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:
simp [coeff_trunc]

Premises used: PowerSeries.coeff_trunc
-- Module: Mathlib.RingTheory.PowerSeries.Trunc
Goal:
R : Type u_1
inst : Semiring R
n : ℕ
f : R⟦X⟧
r : R
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
⊢ (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])

Tactic:
ext i
-- Module: Mathlib.RingTheory.PowerSeries.Trunc
Goal:
R : Type u_1
inst : Semiring R
n : ℕ
f : R⟦X⟧
r : R
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:
simp [coeff_trunc]

Premises used: PowerSeries.coeff_trunc
-- Module: Mathlib.RingTheory.PowerSeries.Trunc
Goal:
R : Type u_1
inst : Semiring R
n : ℕ
f : R⟦X⟧
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)
⊢ 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:
ext j
-- Module: Mathlib.RingTheory.PowerSeries.Trunc
Goal:
R : Type u_1
inst : Semiring R
n : ℕ
f : R⟦X⟧
j : ℕ
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)
⊢ 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:
rw [map_add, Polynomial.coeff_coe, coeff_mul_X_pow', coeff_trunc]

Premises used: PowerSeries.coeff_trunc, map_add, PowerSeries.coeff_mul_X_pow', Polynomial.coeff_coe
-- Module: Mathlib.RingTheory.PowerSeries.Trunc
Goal:
R : Type u_1
inst : Semiring R
n : ℕ
f : R⟦X⟧
j : ℕ
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)
⊢ (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:
simp_rw [← not_le, ite_not, ite_add_ite]

Premises used: not_le, ite_not, ite_add_ite
-- Module: Mathlib.RingTheory.PowerSeries.Trunc
Goal:
R : Type u_1
inst : Semiring R
n : ℕ
f : R⟦X⟧
j : ℕ
⊢ (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 +contextual