awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Derivative (goal)
Goal:
R : Type u_1
inst : CommSemiring R
f g : R⟦X⟧
n : ℕ
⊢ Eq (α := R) ((coeff n : (a : R⟦X⟧) → R) (f + g).derivativeFun : R)
    ((coeff n : (a : R⟦X⟧) → R) (f.derivativeFun + g.derivativeFun) : R)
have h : HMul.hMul (α := R) ((coeff (n + 1) : (a : R⟦X⟧) → R) (f + g) : R) (HAdd.hAdd (α := R) (↑n : R) 1) =
  (coeff n : (a : R⟦X⟧) → R) (f.derivativeFun + g.derivativeFun)
Tactic: rw [coeff_derivativeFun, map_add, map_add, coeff_derivativeFun,
    coeff_derivativeFun, add_mul]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Derivative (goal)
Goal:
R : Type u_1
inst : CommSemiring R
f g : R⟦X⟧
n : ℕ
h :
  HMul.hMul (α := R) ((coeff (n + 1) : (a : R⟦X⟧) → R) (f + g) : R) (HAdd.hAdd (α := R) (↑n : R) 1) =
    (coeff n : (a : R⟦X⟧) → R) (f.derivativeFun + g.derivativeFun)
⊢ Eq (α := R) ((coeff n : (a : R⟦X⟧) → R) (f + g).derivativeFun : R)
    ((coeff n : (a : R⟦X⟧) → R) (f.derivativeFun + g.derivativeFun) : R)
have h₁ : HAdd.hAdd (α := R) (β := R) ((coeff (n + 1) : (a : R⟦X⟧) → R) f : R) ((coeff (n + 1) : (a : R⟦X⟧) → R) g : R) *
    HAdd.hAdd (α := R) (↑n : R) 1 =
  (coeff n : (a : R⟦X⟧) → R) (f.derivativeFun + g.derivativeFun)
Tactic: rw [coeff_derivativeFun, map_add, map_add, coeff_derivativeFun,
    coeff_derivativeFun, add_mul]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Derivative (goal)
Goal:
R : Type u_1
inst : CommSemiring R
f g : R⟦X⟧
n : ℕ
h :
  HMul.hMul (α := R) ((coeff (n + 1) : (a : R⟦X⟧) → R) (f + g) : R) (HAdd.hAdd (α := R) (↑n : R) 1) =
    (coeff n : (a : R⟦X⟧) → R) (f.derivativeFun + g.derivativeFun)
h₁ :
  HAdd.hAdd (α := R) (β := R) ((coeff (n + 1) : (a : R⟦X⟧) → R) f : R) ((coeff (n + 1) : (a : R⟦X⟧) → R) g : R) *
      HAdd.hAdd (α := R) (↑n : R) 1 =
    (coeff n : (a : R⟦X⟧) → R) (f.derivativeFun + g.derivativeFun)
⊢ Eq (α := R) ((coeff n : (a : R⟦X⟧) → R) (f + g).derivativeFun : R)
    ((coeff n : (a : R⟦X⟧) → R) (f.derivativeFun + g.derivativeFun) : R)
have h₂ : HAdd.hAdd (α := R) (β := R) ((coeff (n + 1) : (a : R⟦X⟧) → R) f : R) ((coeff (n + 1) : (a : R⟦X⟧) → R) g : R) *
    HAdd.hAdd (α := R) (↑n : R) 1 =
  HAdd.hAdd (α := R) (β := R) ((coeff n : (a : R⟦X⟧) → R) f.derivativeFun : R)
    ((coeff n : (a : R⟦X⟧) → R) g.derivativeFun : R)
Tactic: rw [coeff_derivativeFun, map_add, map_add, coeff_derivativeFun,
    coeff_derivativeFun, add_mul]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Derivative (goal)
Goal:
R : Type u_1
inst : CommSemiring R
f g : R⟦X⟧
n : ℕ
h :
  HMul.hMul (α := R) ((coeff (n + 1) : (a : R⟦X⟧) → R) (f + g) : R) (HAdd.hAdd (α := R) (↑n : R) 1) =
    (coeff n : (a : R⟦X⟧) → R) (f.derivativeFun + g.derivativeFun)
h₁ :
  HAdd.hAdd (α := R) (β := R) ((coeff (n + 1) : (a : R⟦X⟧) → R) f : R) ((coeff (n + 1) : (a : R⟦X⟧) → R) g : R) *
      HAdd.hAdd (α := R) (↑n : R) 1 =
    (coeff n : (a : R⟦X⟧) → R) (f.derivativeFun + g.derivativeFun)
h₂ :
  HAdd.hAdd (α := R) (β := R) ((coeff (n + 1) : (a : R⟦X⟧) → R) f : R) ((coeff (n + 1) : (a : R⟦X⟧) → R) g : R) *
      HAdd.hAdd (α := R) (↑n : R) 1 =
    HAdd.hAdd (α := R) (β := R) ((coeff n : (a : R⟦X⟧) → R) f.derivativeFun : R)
      ((coeff n : (a : R⟦X⟧) → R) g.derivativeFun : R)
⊢ Eq (α := R) ((coeff n : (a : R⟦X⟧) → R) (f + g).derivativeFun : R)
    ((coeff n : (a : R⟦X⟧) → R) (f.derivativeFun + g.derivativeFun) : R)
have h₃ : HAdd.hAdd (α := R) (β := R) ((coeff (n + 1) : (a : R⟦X⟧) → R) f : R) ((coeff (n + 1) : (a : R⟦X⟧) → R) g : R) *
    HAdd.hAdd (α := R) (↑n : R) 1 =
  HAdd.hAdd (β := R) (HMul.hMul (α := R) ((coeff (n + 1) : (a : R⟦X⟧) → R) f : R) (HAdd.hAdd (α := R) (↑n : R) 1))
    ((coeff n : (a : R⟦X⟧) → R) g.derivativeFun : R)
Tactic: rw [coeff_derivativeFun, map_add, map_add, coeff_derivativeFun,
    coeff_derivativeFun, add_mul]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Derivative (goal)
Goal:
R : Type u_1
inst : CommSemiring R
f g : R⟦X⟧
n : ℕ
h :
  HMul.hMul (α := R) ((coeff (n + 1) : (a : R⟦X⟧) → R) (f + g) : R) (HAdd.hAdd (α := R) (↑n : R) 1) =
    (coeff n : (a : R⟦X⟧) → R) (f.derivativeFun + g.derivativeFun)
h₁ :
  HAdd.hAdd (α := R) (β := R) ((coeff (n + 1) : (a : R⟦X⟧) → R) f : R) ((coeff (n + 1) : (a : R⟦X⟧) → R) g : R) *
      HAdd.hAdd (α := R) (↑n : R) 1 =
    (coeff n : (a : R⟦X⟧) → R) (f.derivativeFun + g.derivativeFun)
h₂ :
  HAdd.hAdd (α := R) (β := R) ((coeff (n + 1) : (a : R⟦X⟧) → R) f : R) ((coeff (n + 1) : (a : R⟦X⟧) → R) g : R) *
      HAdd.hAdd (α := R) (↑n : R) 1 =
    HAdd.hAdd (α := R) (β := R) ((coeff n : (a : R⟦X⟧) → R) f.derivativeFun : R)
      ((coeff n : (a : R⟦X⟧) → R) g.derivativeFun : R)
h₃ :
  HAdd.hAdd (α := R) (β := R) ((coeff (n + 1) : (a : R⟦X⟧) → R) f : R) ((coeff (n + 1) : (a : R⟦X⟧) → R) g : R) *
      HAdd.hAdd (α := R) (↑n : R) 1 =
    HAdd.hAdd (β := R) (HMul.hMul (α := R) ((coeff (n + 1) : (a : R⟦X⟧) → R) f : R) (HAdd.hAdd (α := R) (↑n : R) 1))
      ((coeff n : (a : R⟦X⟧) → R) g.derivativeFun : R)
⊢ Eq (α := R) ((coeff n : (a : R⟦X⟧) → R) (f + g).derivativeFun : R)
    ((coeff n : (a : R⟦X⟧) → R) (f.derivativeFun + g.derivativeFun) : R)
have h₄ : HAdd.hAdd (α := R) (β := R) ((coeff (n + 1) : (a : R⟦X⟧) → R) f : R) ((coeff (n + 1) : (a : R⟦X⟧) → R) g : R) *
    HAdd.hAdd (α := R) (↑n : R) 1 =
  HMul.hMul (α := R) ((coeff (n + 1) : (a : R⟦X⟧) → R) f : R) (HAdd.hAdd (α := R) (↑n : R) 1) +
    HMul.hMul (α := R) ((coeff (n + 1) : (a : R⟦X⟧) → R) g : R) (HAdd.hAdd (α := R) (↑n : R) 1)
Tactic: rw [coeff_derivativeFun, map_add, map_add, coeff_derivativeFun,
    coeff_derivativeFun, add_mul]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Derivative (goal)
Goal:
R : Type u_1
inst : CommSemiring R
f g : R⟦X⟧
n : ℕ
h :
  HMul.hMul (α := R) ((coeff (n + 1) : (a : R⟦X⟧) → R) (f + g) : R) (HAdd.hAdd (α := R) (↑n : R) 1) =
    (coeff n : (a : R⟦X⟧) → R) (f.derivativeFun + g.derivativeFun)
h₁ :
  HAdd.hAdd (α := R) (β := R) ((coeff (n + 1) : (a : R⟦X⟧) → R) f : R) ((coeff (n + 1) : (a : R⟦X⟧) → R) g : R) *
      HAdd.hAdd (α := R) (↑n : R) 1 =
    (coeff n : (a : R⟦X⟧) → R) (f.derivativeFun + g.derivativeFun)
h₂ :
  HAdd.hAdd (α := R) (β := R) ((coeff (n + 1) : (a : R⟦X⟧) → R) f : R) ((coeff (n + 1) : (a : R⟦X⟧) → R) g : R) *
      HAdd.hAdd (α := R) (↑n : R) 1 =
    HAdd.hAdd (α := R) (β := R) ((coeff n : (a : R⟦X⟧) → R) f.derivativeFun : R)
      ((coeff n : (a : R⟦X⟧) → R) g.derivativeFun : R)
h₃ :
  HAdd.hAdd (α := R) (β := R) ((coeff (n + 1) : (a : R⟦X⟧) → R) f : R) ((coeff (n + 1) : (a : R⟦X⟧) → R) g : R) *
      HAdd.hAdd (α := R) (↑n : R) 1 =
    HAdd.hAdd (β := R) (HMul.hMul (α := R) ((coeff (n + 1) : (a : R⟦X⟧) → R) f : R) (HAdd.hAdd (α := R) (↑n : R) 1))
      ((coeff n : (a : R⟦X⟧) → R) g.derivativeFun : R)
h₄ :
  HAdd.hAdd (α := R) (β := R) ((coeff (n + 1) : (a : R⟦X⟧) → R) f : R) ((coeff (n + 1) : (a : R⟦X⟧) → R) g : R) *
      HAdd.hAdd (α := R) (↑n : R) 1 =
    HMul.hMul (α := R) ((coeff (n + 1) : (a : R⟦X⟧) → R) f : R) (HAdd.hAdd (α := R) (↑n : R) 1) +
      HMul.hMul (α := R) ((coeff (n + 1) : (a : R⟦X⟧) → R) g : R) (HAdd.hAdd (α := R) (↑n : R) 1)
⊢ Eq (α := R) ((coeff n : (a : R⟦X⟧) → R) (f + g).derivativeFun : R)
    ((coeff n : (a : R⟦X⟧) → R) (f.derivativeFun + g.derivativeFun) : R)
have h₅ : HMul.hMul (α := R) ((coeff (n + 1) : (a : R⟦X⟧) → R) f : R) (HAdd.hAdd (α := R) (↑n : R) 1) +
    HMul.hMul (α := R) ((coeff (n + 1) : (a : R⟦X⟧) → R) g : R) (HAdd.hAdd (α := R) (↑n : R) 1) =
  HMul.hMul (α := R) ((coeff (n + 1) : (a : R⟦X⟧) → R) f : R) (HAdd.hAdd (α := R) (↑n : R) 1) +
    HMul.hMul (α := R) ((coeff (n + 1) : (a : R⟦X⟧) → R) g : R) (HAdd.hAdd (α := R) (↑n : R) 1)
Tactic: rw [coeff_derivativeFun, map_add, map_add, coeff_derivativeFun,
    coeff_derivativeFun, add_mul]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Derivative (goal)
Goal:
R : Type u_1
inst : CommSemiring R
r : R
⊢ Eq.{u_1 + 1} (α := R⟦X⟧) (derivativeFun ((C : (a : R) → R⟦X⟧) r)) 0
have h : ∀ (n : ℕ),
  Eq.{u_1 + 1} (α := R) ((coeff n : (a : R⟦X⟧) → R) (derivativeFun ((C : (a : R) → R⟦X⟧) r)) : R)
    ((coeff n : (a : R⟦X⟧) → R) 0 : R)
Tactic: ext n
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Derivative (goal)
Goal:
R : Type u_1
inst : CommSemiring R
r : R
n : ℕ
⊢ Eq.{u_1 + 1} (α := R) ((coeff n : (a : R⟦X⟧) → R) (derivativeFun ((C : (a : R) → R⟦X⟧) r)) : R)
    ((coeff n : (a : R⟦X⟧) → R) 0 : R)
have h : HMul.hMul (α := R) ((coeff (n + 1) : (a : R⟦X⟧) → R) ((C : (a : R) → R⟦X⟧) r : R⟦X⟧) : R)
    (HAdd.hAdd (α := R) (↑n : R) 1) =
  (coeff n : (a : R⟦X⟧) → R) 0
Tactic: rw [coeff_derivativeFun, coeff_succ_C, zero_mul, (coeff n).map_zero]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Derivative (goal)
Goal:
R : Type u_1
inst : CommSemiring R
r : R
n : ℕ
h :
  HMul.hMul (α := R) ((coeff (n + 1) : (a : R⟦X⟧) → R) ((C : (a : R) → R⟦X⟧) r : R⟦X⟧) : R)
      (HAdd.hAdd (α := R) (↑n : R) 1) =
    (coeff n : (a : R⟦X⟧) → R) 0
⊢ Eq.{u_1 + 1} (α := R) ((coeff n : (a : R⟦X⟧) → R) (derivativeFun ((C : (a : R) → R⟦X⟧) r)) : R)
    ((coeff n : (a : R⟦X⟧) → R) 0 : R)
have h₁ : 0 * HAdd.hAdd (α := R) (↑n : R) 1 = (coeff n : (a : R⟦X⟧) → R) 0
Tactic: rw [coeff_derivativeFun, coeff_succ_C, zero_mul, (coeff n).map_zero]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Derivative (goal)
Goal:
R : Type u_1
inst : CommSemiring R
r : R
n : ℕ
h :
  HMul.hMul (α := R) ((coeff (n + 1) : (a : R⟦X⟧) → R) ((C : (a : R) → R⟦X⟧) r : R⟦X⟧) : R)
      (HAdd.hAdd (α := R) (↑n : R) 1) =
    (coeff n : (a : R⟦X⟧) → R) 0
h₁ : 0 * HAdd.hAdd (α := R) (↑n : R) 1 = (coeff n : (a : R⟦X⟧) → R) 0
⊢ Eq.{u_1 + 1} (α := R) ((coeff n : (a : R⟦X⟧) → R) (derivativeFun ((C : (a : R) → R⟦X⟧) r)) : R)
    ((coeff n : (a : R⟦X⟧) → R) 0 : R)
have h₂ : Eq.{u_1 + 1} (α := R) (0 : R) ((coeff n : (a : R⟦X⟧) → R) 0 : R)
Tactic: rw [coeff_derivativeFun, coeff_succ_C, zero_mul, (coeff n).map_zero]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Derivative (goal)
Goal:
R : Type u_1
inst : CommSemiring R
r : R
n : ℕ
h :
  HMul.hMul (α := R) ((coeff (n + 1) : (a : R⟦X⟧) → R) ((C : (a : R) → R⟦X⟧) r : R⟦X⟧) : R)
      (HAdd.hAdd (α := R) (↑n : R) 1) =
    (coeff n : (a : R⟦X⟧) → R) 0
h₁ : 0 * HAdd.hAdd (α := R) (↑n : R) 1 = (coeff n : (a : R⟦X⟧) → R) 0
h₂ : Eq.{u_1 + 1} (α := R) (0 : R) ((coeff n : (a : R⟦X⟧) → R) 0 : R)
⊢ Eq.{u_1 + 1} (α := R) ((coeff n : (a : R⟦X⟧) → R) (derivativeFun ((C : (a : R) → R⟦X⟧) r)) : R)
    ((coeff n : (a : R⟦X⟧) → R) 0 : R)
have h₃ : Eq.{u_1 + 1} (α := R) 0 0
Tactic: rw [coeff_derivativeFun, coeff_succ_C, zero_mul, (coeff n).map_zero]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Derivative (goal)
Goal:
R : Type u_1
inst : CommSemiring R
f : R⟦X⟧
n : ℕ
⊢ Eq (α := R[X]) ((trunc n : (a : R⟦X⟧) → R[X]) f.derivativeFun : R[X])
    ((derivative : (a : R[X]) → R[X]) ((trunc (n + 1) : (a : R⟦X⟧) → R[X]) f) : R[X])
have a : ∀ (d : ℕ),
  Eq.{u_1 + 1} (α := R) (Polynomial.coeff ((trunc n : (a : R⟦X⟧) → R[X]) f.derivativeFun) d)
    (Polynomial.coeff ((derivative : (a : R[X]) → R[X]) ((trunc (n + 1) : (a : R⟦X⟧) → R[X]) f)) d)
Tactic: ext d
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Derivative (goal)
Goal:
R : Type u_1
inst : CommSemiring R
f : R⟦X⟧
n d : ℕ
⊢ Eq.{u_1 + 1} (α := R) (Polynomial.coeff ((trunc n : (a : R⟦X⟧) → R[X]) f.derivativeFun) d)
    (Polynomial.coeff ((derivative : (a : R[X]) → R[X]) ((trunc (n + 1) : (a : R⟦X⟧) → R[X]) f)) d)
have a : Eq (α := R) (if d < n then (coeff d : (a : R⟦X⟧) → R) f.derivativeFun else 0 : R)
  (Polynomial.coeff ((derivative : (a : R[X]) → R[X]) ((trunc (n + 1) : (a : R⟦X⟧) → R[X]) f)) d : R)
Tactic: rw [coeff_trunc]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Derivative (goal)
Goal:
R : Type u_1
inst : CommSemiring R
f : R⟦X⟧
n d : ℕ
⊢ Eq (α := R) (if d < n then (coeff d : (a : R⟦X⟧) → R) f.derivativeFun else 0 : R)
    (Polynomial.coeff ((derivative : (a : R[X]) → R[X]) ((trunc (n + 1) : (a : R⟦X⟧) → R[X]) f)) d : R)
have pos : ∀ (h : d < n),
  Eq (α := R) ((coeff d : (a : R⟦X⟧) → R) f.derivativeFun : R)
    (Polynomial.coeff ((derivative : (a : R[X]) → R[X]) ((trunc (n + 1) : (a : R⟦X⟧) → R[X]) f)) d : R)
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Derivative (goal)
Goal:
R : Type u_1
inst : CommSemiring R
f : R⟦X⟧
n d : ℕ
pos :
  ∀ (h : d < n),
    Eq (α := R) ((coeff d : (a : R⟦X⟧) → R) f.derivativeFun : R)
      (Polynomial.coeff ((derivative : (a : R[X]) → R[X]) ((trunc (n + 1) : (a : R⟦X⟧) → R[X]) f)) d : R)
⊢ Eq (α := R) (if d < n then (coeff d : (a : R⟦X⟧) → R) f.derivativeFun else 0 : R)
    (Polynomial.coeff ((derivative : (a : R[X]) → R[X]) ((trunc (n + 1) : (a : R⟦X⟧) → R[X]) f)) d : R)
have neg : ∀ (h : ¬d < n),
  Eq.{u_1 + 1} (α := R) 0
    (Polynomial.coeff ((derivative : (a : R[X]) → R[X]) ((trunc (n + 1) : (a : R⟦X⟧) → R[X]) f)) d)
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Derivative (hypothesis)
Goal:
R : Type u_1
inst : CommSemiring R
f : R⟦X⟧
n d : ℕ
h : d < n
⊢ Eq (α := R) ((coeff d : (a : R⟦X⟧) → R) f.derivativeFun : R)
    (Polynomial.coeff ((derivative : (a : R[X]) → R[X]) ((trunc (n + 1) : (a : R⟦X⟧) → R[X]) f)) d : R)
have this : d + 1 < n + 1
Tactic: have : d + 1 < n + 1 := succ_lt_succ_iff.2 h
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Derivative (goal)
Goal:
R : Type u_1
inst : CommSemiring R
f : R⟦X⟧
n d : ℕ
h : d < n
this : d + 1 < n + 1
⊢ Eq (α := R) ((coeff d : (a : R⟦X⟧) → R) f.derivativeFun : R)
    (Polynomial.coeff ((derivative : (a : R[X]) → R[X]) ((trunc (n + 1) : (a : R⟦X⟧) → R[X]) f)) d : R)
have pos : HMul.hMul (α := R) ((coeff (d + 1) : (a : R⟦X⟧) → R) f : R) (HAdd.hAdd (α := R) (↑d : R) 1) =
  Polynomial.coeff ((derivative : (a : R[X]) → R[X]) ((trunc (n + 1) : (a : R⟦X⟧) → R[X]) f)) d
Tactic: rw [coeff_derivativeFun, coeff_derivative, coeff_trunc, if_pos this]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Derivative (goal)
Goal:
R : Type u_1
inst : CommSemiring R
f : R⟦X⟧
n d : ℕ
h : d < n
this : d + 1 < n + 1
pos :
  HMul.hMul (α := R) ((coeff (d + 1) : (a : R⟦X⟧) → R) f : R) (HAdd.hAdd (α := R) (↑d : R) 1) =
    Polynomial.coeff ((derivative : (a : R[X]) → R[X]) ((trunc (n + 1) : (a : R⟦X⟧) → R[X]) f)) d
⊢ Eq (α := R) ((coeff d : (a : R⟦X⟧) → R) f.derivativeFun : R)
    (Polynomial.coeff ((derivative : (a : R[X]) → R[X]) ((trunc (n + 1) : (a : R⟦X⟧) → R[X]) f)) d : R)
have pos₁ : HMul.hMul (α := R) ((coeff (d + 1) : (a : R⟦X⟧) → R) f : R) (HAdd.hAdd (α := R) (↑d : R) 1) =
  Polynomial.coeff ((trunc (n + 1) : (a : R⟦X⟧) → R[X]) f) (d + 1) * HAdd.hAdd (α := R) (↑d : R) 1
Tactic: rw [coeff_derivativeFun, coeff_derivative, coeff_trunc, if_pos this]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Derivative (goal)
Goal:
R : Type u_1
inst : CommSemiring R
f : R⟦X⟧
n d : ℕ
h : d < n
this : d + 1 < n + 1
pos :
  HMul.hMul (α := R) ((coeff (d + 1) : (a : R⟦X⟧) → R) f : R) (HAdd.hAdd (α := R) (↑d : R) 1) =
    Polynomial.coeff ((derivative : (a : R[X]) → R[X]) ((trunc (n + 1) : (a : R⟦X⟧) → R[X]) f)) d
pos₁ :
  HMul.hMul (α := R) ((coeff (d + 1) : (a : R⟦X⟧) → R) f : R) (HAdd.hAdd (α := R) (↑d : R) 1) =
    Polynomial.coeff ((trunc (n + 1) : (a : R⟦X⟧) → R[X]) f) (d + 1) * HAdd.hAdd (α := R) (↑d : R) 1
⊢ Eq (α := R) ((coeff d : (a : R⟦X⟧) → R) f.derivativeFun : R)
    (Polynomial.coeff ((derivative : (a : R[X]) → R[X]) ((trunc (n + 1) : (a : R⟦X⟧) → R[X]) f)) d : R)
have pos₂ : HMul.hMul (α := R) ((coeff (d + 1) : (a : R⟦X⟧) → R) f : R) (HAdd.hAdd (α := R) (↑d : R) 1) =
  HMul.hMul (α := R) (if d + 1 < n + 1 then (coeff (d + 1) : (a : R⟦X⟧) → R) f else 0 : R)
    (HAdd.hAdd (α := R) (↑d : R) 1)
Tactic: rw [coeff_derivativeFun, coeff_derivative, coeff_trunc, if_pos this]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Derivative (goal)
Goal:
R : Type u_1
inst : CommSemiring R
f : R⟦X⟧
n d : ℕ
h : d < n
this : d + 1 < n + 1
pos :
  HMul.hMul (α := R) ((coeff (d + 1) : (a : R⟦X⟧) → R) f : R) (HAdd.hAdd (α := R) (↑d : R) 1) =
    Polynomial.coeff ((derivative : (a : R[X]) → R[X]) ((trunc (n + 1) : (a : R⟦X⟧) → R[X]) f)) d
pos₁ :
  HMul.hMul (α := R) ((coeff (d + 1) : (a : R⟦X⟧) → R) f : R) (HAdd.hAdd (α := R) (↑d : R) 1) =
    Polynomial.coeff ((trunc (n + 1) : (a : R⟦X⟧) → R[X]) f) (d + 1) * HAdd.hAdd (α := R) (↑d : R) 1
pos₂ :
  HMul.hMul (α := R) ((coeff (d + 1) : (a : R⟦X⟧) → R) f : R) (HAdd.hAdd (α := R) (↑d : R) 1) =
    HMul.hMul (α := R) (if d + 1 < n + 1 then (coeff (d + 1) : (a : R⟦X⟧) → R) f else 0 : R)
      (HAdd.hAdd (α := R) (↑d : R) 1)
⊢ Eq (α := R) ((coeff d : (a : R⟦X⟧) → R) f.derivativeFun : R)
    (Polynomial.coeff ((derivative : (a : R[X]) → R[X]) ((trunc (n + 1) : (a : R⟦X⟧) → R[X]) f)) d : R)
have pos₃ : HMul.hMul (α := R) ((coeff (d + 1) : (a : R⟦X⟧) → R) f : R) (HAdd.hAdd (α := R) (↑d : R) 1) =
  HMul.hMul (α := R) ((coeff (d + 1) : (a : R⟦X⟧) → R) f : R) (HAdd.hAdd (α := R) (↑d : R) 1)
Tactic: rw [coeff_derivativeFun, coeff_derivative, coeff_trunc, if_pos this]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Derivative (hypothesis)
Goal:
R : Type u_1
inst : CommSemiring R
f : R⟦X⟧
n d : ℕ
h : ¬d < n
⊢ Eq.{u_1 + 1} (α := R) 0
    (Polynomial.coeff ((derivative : (a : R[X]) → R[X]) ((trunc (n + 1) : (a : R⟦X⟧) → R[X]) f)) d)
have this : ¬d + 1 < n + 1
Tactic: have : ¬d + 1 < n + 1 := by rwa [succ_lt_succ_iff]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Derivative (goal)
Goal:
R : Type u_1
inst : CommSemiring R
f : R⟦X⟧
n d : ℕ
h : ¬d < n
this : ¬d + 1 < n + 1
⊢ Eq.{u_1 + 1} (α := R) 0
    (Polynomial.coeff ((derivative : (a : R[X]) → R[X]) ((trunc (n + 1) : (a : R⟦X⟧) → R[X]) f)) d)
have neg : 0 = Polynomial.coeff ((trunc (n + 1) : (a : R⟦X⟧) → R[X]) f) (d + 1) * HAdd.hAdd (α := R) (↑d : R) 1
Tactic: rw [coeff_derivative, coeff_trunc, if_neg this, zero_mul]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Derivative (goal)
Goal:
R : Type u_1
inst : CommSemiring R
f : R⟦X⟧
n d : ℕ
h : ¬d < n
this : ¬d + 1 < n + 1
neg : 0 = Polynomial.coeff ((trunc (n + 1) : (a : R⟦X⟧) → R[X]) f) (d + 1) * HAdd.hAdd (α := R) (↑d : R) 1
⊢ Eq.{u_1 + 1} (α := R) 0
    (Polynomial.coeff ((derivative : (a : R[X]) → R[X]) ((trunc (n + 1) : (a : R⟦X⟧) → R[X]) f)) d)
have neg₁ : 0 =
  HMul.hMul (α := R) (if d + 1 < n + 1 then (coeff (d + 1) : (a : R⟦X⟧) → R) f else 0 : R)
    (HAdd.hAdd (α := R) (↑d : R) 1)
Tactic: rw [coeff_derivative, coeff_trunc, if_neg this, zero_mul]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Derivative (goal)
Goal:
R : Type u_1
inst : CommSemiring R
f : R⟦X⟧
n d : ℕ
h : ¬d < n
this : ¬d + 1 < n + 1
neg : 0 = Polynomial.coeff ((trunc (n + 1) : (a : R⟦X⟧) → R[X]) f) (d + 1) * HAdd.hAdd (α := R) (↑d : R) 1
neg₁ :
  0 =
    HMul.hMul (α := R) (if d + 1 < n + 1 then (coeff (d + 1) : (a : R⟦X⟧) → R) f else 0 : R)
      (HAdd.hAdd (α := R) (↑d : R) 1)
⊢ Eq.{u_1 + 1} (α := R) 0
    (Polynomial.coeff ((derivative : (a : R[X]) → R[X]) ((trunc (n + 1) : (a : R⟦X⟧) → R[X]) f)) d)
have neg₂ : 0 = 0 * HAdd.hAdd (α := R) (↑d : R) 1
Tactic: rw [coeff_derivative, coeff_trunc, if_neg this, zero_mul]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Derivative (goal)
Goal:
R : Type u_1
inst : CommSemiring R
f : R⟦X⟧
n d : ℕ
h : ¬d < n
this : ¬d + 1 < n + 1
neg : 0 = Polynomial.coeff ((trunc (n + 1) : (a : R⟦X⟧) → R[X]) f) (d + 1) * HAdd.hAdd (α := R) (↑d : R) 1
neg₁ :
  0 =
    HMul.hMul (α := R) (if d + 1 < n + 1 then (coeff (d + 1) : (a : R⟦X⟧) → R) f else 0 : R)
      (HAdd.hAdd (α := R) (↑d : R) 1)
neg₂ : 0 = 0 * HAdd.hAdd (α := R) (↑d : R) 1
⊢ Eq.{u_1 + 1} (α := R) 0
    (Polynomial.coeff ((derivative : (a : R[X]) → R[X]) ((trunc (n + 1) : (a : R⟦X⟧) → R[X]) f)) d)
have neg₃ : Eq.{u_1 + 1} (α := R) 0 0
Tactic: rw [coeff_derivative, coeff_trunc, if_neg this, zero_mul]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Derivative (goal)
Goal:
R : Type u_1
inst : CommSemiring R
f g : R[X]
⊢ ((↑f : R⟦X⟧) * (↑g : R⟦X⟧)).derivativeFun =
    (↑f : R⟦X⟧) * (↑((derivative : (a : R[X]) → R[X]) g) : R⟦X⟧) +
      (↑g : R⟦X⟧) * (↑((derivative : (a : R[X]) → R[X]) f) : R⟦X⟧)
have rw : (↑(f * g) : R⟦X⟧).derivativeFun =
  (↑f : R⟦X⟧) * (↑((derivative : (a : R[X]) → R[X]) g) : R⟦X⟧) +
    (↑g : R⟦X⟧) * (↑((derivative : (a : R[X]) → R[X]) f) : R⟦X⟧)
Tactic: rw [← coe_mul, derivativeFun_coe, derivative_mul,
    add_comm, mul_comm _ g, ← coe_mul, ← coe_mul, Polynomial.coe_add]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Derivative (goal)
Goal:
R : Type u_1
inst : CommSemiring R
f g : R[X]
rw :
  (↑(f * g) : R⟦X⟧).derivativeFun =
    (↑f : R⟦X⟧) * (↑((derivative : (a : R[X]) → R[X]) g) : R⟦X⟧) +
      (↑g : R⟦X⟧) * (↑((derivative : (a : R[X]) → R[X]) f) : R⟦X⟧)
⊢ ((↑f : R⟦X⟧) * (↑g : R⟦X⟧)).derivativeFun =
    (↑f : R⟦X⟧) * (↑((derivative : (a : R[X]) → R[X]) g) : R⟦X⟧) +
      (↑g : R⟦X⟧) * (↑((derivative : (a : R[X]) → R[X]) f) : R⟦X⟧)
have rw₁ : (↑((derivative : (a : R[X]) → R[X]) (f * g)) : R⟦X⟧) =
  (↑f : R⟦X⟧) * (↑((derivative : (a : R[X]) → R[X]) g) : R⟦X⟧) +
    (↑g : R⟦X⟧) * (↑((derivative : (a : R[X]) → R[X]) f) : R⟦X⟧)
Tactic: rw [← coe_mul, derivativeFun_coe, derivative_mul,
    add_comm, mul_comm _ g, ← coe_mul, ← coe_mul, Polynomial.coe_add]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Derivative (goal)
Goal:
R : Type u_1
inst : CommSemiring R
f g : R[X]
rw :
  (↑(f * g) : R⟦X⟧).derivativeFun =
    (↑f : R⟦X⟧) * (↑((derivative : (a : R[X]) → R[X]) g) : R⟦X⟧) +
      (↑g : R⟦X⟧) * (↑((derivative : (a : R[X]) → R[X]) f) : R⟦X⟧)
rw₁ :
  (↑((derivative : (a : R[X]) → R[X]) (f * g)) : R⟦X⟧) =
    (↑f : R⟦X⟧) * (↑((derivative : (a : R[X]) → R[X]) g) : R⟦X⟧) +
      (↑g : R⟦X⟧) * (↑((derivative : (a : R[X]) → R[X]) f) : R⟦X⟧)
⊢ ((↑f : R⟦X⟧) * (↑g : R⟦X⟧)).derivativeFun =
    (↑f : R⟦X⟧) * (↑((derivative : (a : R[X]) → R[X]) g) : R⟦X⟧) +
      (↑g : R⟦X⟧) * (↑((derivative : (a : R[X]) → R[X]) f) : R⟦X⟧)
have rw₂ : (↑(HMul.hMul (α := R[X]) ((derivative : (a : R[X]) → R[X]) f : R[X]) g +
        HMul.hMul (β := R[X]) f ((derivative : (a : R[X]) → R[X]) g : R[X])) :
    R⟦X⟧) =
  (↑f : R⟦X⟧) * (↑((derivative : (a : R[X]) → R[X]) g) : R⟦X⟧) +
    (↑g : R⟦X⟧) * (↑((derivative : (a : R[X]) → R[X]) f) : R⟦X⟧)
Tactic: rw [← coe_mul, derivativeFun_coe, derivative_mul,
    add_comm, mul_comm _ g, ← coe_mul, ← coe_mul, Polynomial.coe_add]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Derivative (goal)
Goal:
R : Type u_1
inst : CommSemiring R
f g : R[X]
rw :
  (↑(f * g) : R⟦X⟧).derivativeFun =
    (↑f : R⟦X⟧) * (↑((derivative : (a : R[X]) → R[X]) g) : R⟦X⟧) +
      (↑g : R⟦X⟧) * (↑((derivative : (a : R[X]) → R[X]) f) : R⟦X⟧)
rw₁ :
  (↑((derivative : (a : R[X]) → R[X]) (f * g)) : R⟦X⟧) =
    (↑f : R⟦X⟧) * (↑((derivative : (a : R[X]) → R[X]) g) : R⟦X⟧) +
      (↑g : R⟦X⟧) * (↑((derivative : (a : R[X]) → R[X]) f) : R⟦X⟧)
rw₂ :
  (↑(HMul.hMul (α := R[X]) ((derivative : (a : R[X]) → R[X]) f : R[X]) g +
          HMul.hMul (β := R[X]) f ((derivative : (a : R[X]) → R[X]) g : R[X])) :
      R⟦X⟧) =
    (↑f : R⟦X⟧) * (↑((derivative : (a : R[X]) → R[X]) g) : R⟦X⟧) +
      (↑g : R⟦X⟧) * (↑((derivative : (a : R[X]) → R[X]) f) : R⟦X⟧)
⊢ ((↑f : R⟦X⟧) * (↑g : R⟦X⟧)).derivativeFun =
    (↑f : R⟦X⟧) * (↑((derivative : (a : R[X]) → R[X]) g) : R⟦X⟧) +
      (↑g : R⟦X⟧) * (↑((derivative : (a : R[X]) → R[X]) f) : R⟦X⟧)
have rw₃ : (↑(HMul.hMul (β := R[X]) f ((derivative : (a : R[X]) → R[X]) g : R[X]) +
        HMul.hMul (α := R[X]) ((derivative : (a : R[X]) → R[X]) f : R[X]) g) :
    R⟦X⟧) =
  (↑f : R⟦X⟧) * (↑((derivative : (a : R[X]) → R[X]) g) : R⟦X⟧) +
    (↑g : R⟦X⟧) * (↑((derivative : (a : R[X]) → R[X]) f) : R⟦X⟧)
Tactic: rw [← coe_mul, derivativeFun_coe, derivative_mul,
    add_comm, mul_comm _ g, ← coe_mul, ← coe_mul, Polynomial.coe_add]