awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.PowerSeries.Trunc
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⟧)
rw₁ rw₂ : f = f
⊢ 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⟧)

Tactic:
rw [← (commute_X_pow _ n).eq, ← eq_shift_mul_X_pow_add_trunc]

Premises used: PowerSeries.eq_shift_mul_X_pow_add_trunc, PowerSeries.commute_X_pow, Commute.eq
-- Module: Mathlib.RingTheory.PowerSeries.Trunc
Goal:
R : Type u_1
inst : Semiring R
r : R
n : ℕ
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)
⊢ (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)

Tactic:
ext
-- Module: Mathlib.RingTheory.PowerSeries.Trunc
Goal:
R : Type u_1
inst : Semiring R
r : R
n 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:
simp [coeff_X_pow, coeff_monomial]

Premises used: PowerSeries.coeff_monomial, PowerSeries.coeff_X_pow
-- Module: Mathlib.RingTheory.PowerSeries.Trunc
Goal:
R : Type u_1
inst : Semiring R
n : ℕ
p : R⟦X⟧
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)
⊢ Eq (α := R[X]) ((trunc n : (a : R⟦X⟧) → R[X]) (HPow.hPow (α := R⟦X⟧) X n * p) : R[X]) (0 : R[X])

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

Premises used: PowerSeries.coeff_trunc, PowerSeries.coeff_X_pow_mul'
-- Module: Mathlib.RingTheory.PowerSeries.Trunc
Goal:
R : Type u_2
inst : CommSemiring R
n m : ℕ
f : R⟦X⟧
hnm : n ≤ m
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)
⊢ 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])

Tactic:
ext d
-- Module: Mathlib.RingTheory.PowerSeries.Trunc
Goal:
R : Type u_2
inst : CommSemiring R
n m : ℕ
f : R⟦X⟧
hnm : n ≤ m
d : ℕ
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)
⊢ 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:
rw [coeff_trunc, coeff_trunc, coeff_coe]

Premises used: PowerSeries.coeff_trunc, Polynomial.coeff_coe
-- Module: Mathlib.RingTheory.PowerSeries.Trunc
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)
neg : ∀ (h : ¬d < n), Eq.{u_2 + 1} (α := R) 0 0
⊢ 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:
split_ifs with h
-- Module: Mathlib.RingTheory.PowerSeries.Trunc
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)
pos₁ pos₂ : Eq (α := R) ((coeff d : (a : R⟦X⟧) → R) f : 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)

Tactic:
rw [coeff_trunc, if_pos <| lt_of_lt_of_le h hnm]

Premises used: PowerSeries.coeff_trunc, if_pos, lt_of_lt_of_le
-- Module: Mathlib.RingTheory.PowerSeries.Trunc
Goal:
R : Type u_2
inst : CommSemiring R
n m : ℕ
f : R⟦X⟧
hnm : n ≤ m
d : ℕ
h : ¬d < n
⊢ Eq.{u_2 + 1} (α := R) 0 0

Tactic:
rfl
-- Module: Mathlib.RingTheory.PowerSeries.Trunc
Goal:
R : Type u_2
inst : CommSemiring R
n : ℕ
f : R⟦X⟧
⊢ Eq (α := R[X]) ((trunc n : (a : R⟦X⟧) → R[X]) (↑((trunc n : (a : R⟦X⟧) → R[X]) f) : R⟦X⟧) : R[X])
    ((trunc n : (a : R⟦X⟧) → R[X]) f : R[X])

Tactic:
trunc_trunc_of_le f

Premises used: PowerSeries.trunc_trunc_of_le
-- Module: Mathlib.RingTheory.PowerSeries.Trunc
Goal:
R : Type u_2
inst : CommSemiring R
n : ℕ
f g : R⟦X⟧
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)
⊢ 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])

Tactic:
ext m
-- Module: Mathlib.RingTheory.PowerSeries.Trunc
Goal:
R : Type u_2
inst : CommSemiring R
n : ℕ
f g : R⟦X⟧
m : ℕ
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)
⊢ 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:
rw [coeff_trunc, coeff_trunc]

Premises used: PowerSeries.coeff_trunc
-- Module: Mathlib.RingTheory.PowerSeries.Trunc
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)
neg : ∀ (h : ¬m < n), Eq.{u_2 + 1} (α := R) 0 0
⊢ 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:
split_ifs with h
-- Module: Mathlib.RingTheory.PowerSeries.Trunc
Goal:
R : Type u_2
inst : CommSemiring R
n : ℕ
f g : R⟦X⟧
m : ℕ
h : m < n
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)
⊢ 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:
rw [coeff_mul, coeff_mul, sum_congr rfl]

Premises used: PowerSeries.coeff_mul, Finset.sum_congr, rfl
-- Module: Mathlib.RingTheory.PowerSeries.Trunc
Goal:
R : Type u_2
inst : CommSemiring R
n : ℕ
f g : R⟦X⟧
m : ℕ
h : m < n
x : ℕ × ℕ
hab : x ∈ @antidiagonal _ instAddMonoid _ m
⊢ x.1 < n

Tactic:
have ha := lt_of_le_of_lt (antidiagonal.fst_le hab) h
-- Module: Mathlib.RingTheory.PowerSeries.Trunc
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)
pos₂ 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)
⊢ 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_coe, coeff_trunc, if_pos ha]

Premises used: PowerSeries.coeff_trunc, if_pos, Polynomial.coeff_coe
-- Module: Mathlib.RingTheory.PowerSeries.Trunc
Goal:
R : Type u_2
inst : CommSemiring R
n : ℕ
f g : R⟦X⟧
m : ℕ
h : ¬m < n
⊢ Eq.{u_2 + 1} (α := R) 0 0

Tactic:
rfl
-- Module: Mathlib.RingTheory.PowerSeries.Trunc
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])
rw₂ 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])
⊢ 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 [mul_comm, trunc_trunc_mul, mul_comm]

Premises used: PowerSeries.trunc_trunc_mul, mul_comm
-- Module: Mathlib.RingTheory.PowerSeries.Trunc
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])
rw₁ 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])
⊢ 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])

Tactic:
rw [trunc_trunc_mul, trunc_mul_trunc]

Premises used: PowerSeries.trunc_mul_trunc, PowerSeries.trunc_trunc_mul
-- Module: Mathlib.RingTheory.PowerSeries.Trunc
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])
zero₁ zero₂ : Eq.{u_2 + 1} (α := R[X]) ((trunc n : (a : R⟦X⟧) → R[X]) 1) ((trunc n : (a : R⟦X⟧) → R[X]) 1)
⊢ 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:
rw [pow_zero, pow_zero]

Premises used: pow_zero
-- Module: Mathlib.RingTheory.PowerSeries.Trunc
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])
succ₅ 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])
⊢ 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:
rw [_root_.pow_succ', _root_.pow_succ', trunc_trunc_mul,
      ← trunc_trunc_mul_trunc, ih, trunc_trunc_mul_trunc]

Premises used: PowerSeries.trunc_trunc_mul_trunc, PowerSeries.trunc_trunc_mul, pow_succ'
-- Module: Mathlib.RingTheory.PowerSeries.Trunc
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])
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])
⊢ 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])

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]

Premises used: PowerSeries.trunc_trunc_mul_trunc, PowerSeries.trunc_trunc_mul, pow_zero, Nat.zero, Nat.succ, pow_succ'
-- Module: Mathlib.RingTheory.PowerSeries.Trunc
Goal:
R : Type u_2
inst : CommSemiring R
n : ℕ
f : R[X]
hn : f.natDegree < n
rw : (↑((trunc n : (a : R⟦X⟧) → R[X]) (↑f : R⟦X⟧)) : R⟦X⟧) = (↑f : R⟦X⟧)
⊢ (trunc n : (a : R⟦X⟧) → R[X]) (↑f : R⟦X⟧) = f

Tactic:
rw [← Polynomial.coe_inj]

Premises used: Polynomial.coe_inj
-- Module: Mathlib.RingTheory.PowerSeries.Trunc
Goal:
R : Type u_2
inst : CommSemiring R
n : ℕ
f : R[X]
hn : f.natDegree < n
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)
⊢ (↑((trunc n : (a : R⟦X⟧) → R[X]) (↑f : R⟦X⟧)) : R⟦X⟧) = (↑f : R⟦X⟧)

Tactic:
ext m
-- Module: Mathlib.RingTheory.PowerSeries.Trunc
Goal:
R : Type u_2
inst : CommSemiring R
n : ℕ
f : R[X]
hn : f.natDegree < n
m : ℕ
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)
⊢ 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:
rw [coeff_coe, coeff_trunc]

Premises used: PowerSeries.coeff_trunc, Polynomial.coeff_coe
-- Module: Mathlib.RingTheory.PowerSeries.Trunc
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)
h₁ : ¬m < n → Eq (α := R) (0 : 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)

Tactic:
split
-- Module: Mathlib.RingTheory.PowerSeries.Trunc
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)

Tactic:
rfl
-- Module: Mathlib.RingTheory.PowerSeries.Trunc
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)

Tactic:
case isTrue h => rfl

Premises used: Decidable.isTrue
-- Module: Mathlib.RingTheory.PowerSeries.Trunc
Goal:
R : Type u_2
inst : CommSemiring R
n : ℕ
f : R[X]
hn : f.natDegree < n
m : ℕ
h : ¬m < n
⊢ n ≤ m

Tactic:
rw [not_lt] at h

Premises used: not_lt
-- Module: Mathlib.RingTheory.PowerSeries.Trunc
Goal:
R : Type u_2
inst : CommSemiring R
n : ℕ
f : R[X]
hn : f.natDegree < n
m : ℕ
h : n ≤ m
rw : 0 = f.coeff m
⊢ Eq (α := R) (0 : R) ((coeff m : (a : R⟦X⟧) → R) (↑f : R⟦X⟧) : R)

Tactic:
rw [coeff_coe]

Premises used: Polynomial.coeff_coe
-- Module: Mathlib.RingTheory.PowerSeries.Trunc
Goal:
R : Type u_2
inst : CommSemiring R
n : ℕ
f : R[X]
hn : f.natDegree < n
m : ℕ
h : n ≤ m
symm : f.coeff m = 0
⊢ 0 = f.coeff m

Tactic:
symm
-- Module: Mathlib.RingTheory.PowerSeries.Trunc
Goal:
R : Type u_2
inst : CommSemiring R
n : ℕ
f : R[X]
hn : f.natDegree < n
m : ℕ
h : n ≤ m
⊢ f.coeff m = 0

Tactic:
coeff_eq_zero_of_natDegree_lt <| lt_of_lt_of_le hn h

Premises used: Polynomial.coeff_eq_zero_of_natDegree_lt, lt_of_lt_of_le
-- Module: Mathlib.RingTheory.PowerSeries.Trunc
Goal:
R : Type u_2
inst : CommSemiring R
n : ℕ
f : R[X]
hn : f.natDegree < n
m : ℕ
h : n ≤ m
⊢ f.coeff m = 0

Tactic:
exact coeff_eq_zero_of_natDegree_lt <| lt_of_lt_of_le hn h

Premises used: Polynomial.coeff_eq_zero_of_natDegree_lt, lt_of_lt_of_le
-- Module: Mathlib.RingTheory.PowerSeries.Trunc
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)
rwa₂ : Eq (α := R) ((coeff n : (a : R⟦X⟧) → R) f : R) ((coeff n : (a : R⟦X⟧) → R) f : R)
hc : n < m
rwa₃ : Eq (α := R) ((coeff n : (a : R⟦X⟧) → R) f : R) ((coeff n : (a : R⟦X⟧) → R) f : R)
hc₁ hc₂ hc₃ : 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)

Tactic:
rwa [coeff_coe, coeff_trunc, if_pos]

Premises used: PowerSeries.coeff_trunc, if_pos, Polynomial.coeff_coe
-- Module: Mathlib.RingTheory.PowerSeries.Trunc
Goal:
R : Type u_2
inst : CommSemiring R
n a b : ℕ
f g : R⟦X⟧
ha : n < a
hb : n < b
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)
⊢ 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)

Tactic:
symm
-- Module: Mathlib.RingTheory.PowerSeries.Trunc
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)
rw₅ rw₆ : Eq (α := R) ((coeff n : (a : R⟦X⟧) → R) (f * g) : 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)

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]

Premises used: PowerSeries.trunc_trunc_mul_trunc, Nat.lt_succ_self, PowerSeries.trunc_trunc_of_le, PowerSeries.coeff_coe_trunc_of_lt
-- Module: Mathlib.RingTheory.PowerSeries.Trunc
Goal:
R : Type u_2
inst : CommSemiring R
d n : ℕ
f g : R⟦X⟧
h : d < n
⊢ Eq (α := R) ((coeff d : (a : R⟦X⟧) → R) (f * g) : R)
    ((coeff d : (a : R⟦X⟧) → R)
        (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)

Tactic:
coeff_mul_eq_coeff_trunc_mul_trunc₂ f g h h

Premises used: PowerSeries.coeff_mul_eq_coeff_trunc_mul_trunc₂
-- Module: Mathlib.RingTheory.PowerSeries.Trunc
Goal:
R : Type u_1
inst : Ring R
n : ℕ
φ ψ : R⟦X⟧
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
⊢ (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])

Tactic:
ext i
-- Module: Mathlib.RingTheory.PowerSeries.Trunc
Goal:
R : Type u_1
inst : Ring R
n : ℕ
φ ψ : R⟦X⟧
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:
simp
-- Module: Mathlib.RingTheory.PowerSeries.Trunc
Goal:
R : Type u_1
S : Type u_2
inst : Semiring R
inst_1 : Semiring S
f : R →+* S
p : R⟦X⟧
n : ℕ
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
⊢ (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)

Tactic:
ext m
-- Module: Mathlib.RingTheory.PowerSeries.Trunc
Goal:
R : Type u_1
S : Type u_2
inst : Semiring R
inst_1 : Semiring S
f : R →+* S
p : R⟦X⟧
n 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:
simp [coeff_trunc, apply_ite f]

Premises used: PowerSeries.coeff_trunc, apply_ite, DFunLike.coe
-- Module: Mathlib.RingTheory.PowerSeries.WeierstrassPreparation
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 ℕ)
eq_mul_add : 0 = g * 0 + (↑0 : A⟦X⟧)
⊢ IsWeierstrassDivisionAt 0 g 0 0 I

Tactic:
constructor