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]
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⟧)
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⟧)
⊢ ((↑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]) g ((derivative : (a : R[X]) → R[X]) f : 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⟧)
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⟧)
rw₄ :
  (↑(HMul.hMul (β := R[X]) f ((derivative : (a : R[X]) → R[X]) g : R[X]) +
          HMul.hMul (β := R[X]) g ((derivative : (a : R[X]) → R[X]) f : 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]) g ((derivative : (a : R[X]) → R[X]) f : R[X])) :
    R⟦X⟧) =
  (↑(HMul.hMul (β := R[X]) f ((derivative : (a : R[X]) → R[X]) g : R[X])) : 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⟧)
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⟧)
rw₄ :
  (↑(HMul.hMul (β := R[X]) f ((derivative : (a : R[X]) → R[X]) g : R[X]) +
          HMul.hMul (β := R[X]) g ((derivative : (a : R[X]) → R[X]) f : 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⟧)
rw₅ :
  (↑(HMul.hMul (β := R[X]) f ((derivative : (a : R[X]) → R[X]) g : R[X]) +
          HMul.hMul (β := R[X]) g ((derivative : (a : R[X]) → R[X]) f : R[X])) :
      R⟦X⟧) =
    (↑(HMul.hMul (β := R[X]) f ((derivative : (a : R[X]) → R[X]) g : R[X])) : 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]) g ((derivative : (a : R[X]) → R[X]) f : R[X])) :
    R⟦X⟧) =
  (↑(HMul.hMul (β := R[X]) f ((derivative : (a : R[X]) → R[X]) g : R[X])) : R⟦X⟧) +
    (↑(HMul.hMul (β := R[X]) g ((derivative : (a : R[X]) → R[X]) f : R[X])) : 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⟧)
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⟧)
rw₄ :
  (↑(HMul.hMul (β := R[X]) f ((derivative : (a : R[X]) → R[X]) g : R[X]) +
          HMul.hMul (β := R[X]) g ((derivative : (a : R[X]) → R[X]) f : 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⟧)
rw₅ :
  (↑(HMul.hMul (β := R[X]) f ((derivative : (a : R[X]) → R[X]) g : R[X]) +
          HMul.hMul (β := R[X]) g ((derivative : (a : R[X]) → R[X]) f : R[X])) :
      R⟦X⟧) =
    (↑(HMul.hMul (β := R[X]) f ((derivative : (a : R[X]) → R[X]) g : R[X])) : R⟦X⟧) +
      (↑g : R⟦X⟧) * (↑((derivative : (a : R[X]) → R[X]) f) : R⟦X⟧)
rw₆ :
  (↑(HMul.hMul (β := R[X]) f ((derivative : (a : R[X]) → R[X]) g : R[X]) +
          HMul.hMul (β := R[X]) g ((derivative : (a : R[X]) → R[X]) f : R[X])) :
      R⟦X⟧) =
    (↑(HMul.hMul (β := R[X]) f ((derivative : (a : R[X]) → R[X]) g : R[X])) : R⟦X⟧) +
      (↑(HMul.hMul (β := R[X]) g ((derivative : (a : R[X]) → R[X]) f : R[X])) : 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])) : R⟦X⟧) +
    (↑(HMul.hMul (β := R[X]) g ((derivative : (a : R[X]) → R[X]) f : R[X])) : R⟦X⟧) =
  (↑(HMul.hMul (β := R[X]) f ((derivative : (a : R[X]) → R[X]) g : R[X])) : R⟦X⟧) +
    (↑(HMul.hMul (β := R[X]) g ((derivative : (a : R[X]) → R[X]) f : R[X])) : 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⟧
⊢ (f * g).derivativeFun = f • g.derivativeFun + g • f.derivativeFun
have h : ∀ (n : ℕ),
  Eq (α := R) ((coeff n : (a : R⟦X⟧) → R) (f * g).derivativeFun : R)
    ((coeff n : (a : R⟦X⟧) → R) (f • g.derivativeFun + g • f.derivativeFun) : R)
Tactic: ext n
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Derivative (hypothesis)
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 • g.derivativeFun + g • f.derivativeFun) : R)
have h₁ : n < n + 1
Tactic: have h₁ : n < n + 1 := lt_succ_self n
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Derivative (hypothesis)
Goal:
R : Type u_1
inst : CommSemiring R
f g : R⟦X⟧
n : ℕ
h₁ : n < n + 1
⊢ Eq (α := R) ((coeff n : (a : R⟦X⟧) → R) (f * g).derivativeFun : R)
    ((coeff n : (a : R⟦X⟧) → R) (f • g.derivativeFun + g • f.derivativeFun) : R)
have h₂ : n < n + 1 + 1
Tactic: have h₂ : n < n + 1 + 1 := Nat.lt_add_right _ h₁
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Derivative (goal)
Goal:
R : Type u_1
inst : CommSemiring R
f g : R⟦X⟧
n : ℕ
h₁ : n < n + 1
h₂ : n < n + 1 + 1
⊢ Eq (α := R) ((coeff n : (a : R⟦X⟧) → R) (f * g).derivativeFun : R)
    ((coeff n : (a : R⟦X⟧) → R) (f • g.derivativeFun + g • f.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 • g.derivativeFun + g • f.derivativeFun)
Tactic: rw [coeff_derivativeFun, map_add, coeff_mul_eq_coeff_trunc_mul_trunc _ _ (lt_succ_self _),
    smul_eq_mul, smul_eq_mul, coeff_mul_eq_coeff_trunc_mul_trunc₂ g f.derivativeFun h₂ h₁,
    coeff_mul_eq_coeff_trunc_mul_trunc₂ f g.derivativeFun h₂ h₁, trunc_derivativeFun,
    trunc_derivativeFun, ← map_add, ← derivativeFun_coe_mul_coe, coeff_derivativeFun]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Derivative (goal)
Goal:
R : Type u_1
inst : CommSemiring R
f g : R⟦X⟧
n : ℕ
h₁ : n < n + 1
h₂ : n < n + 1 + 1
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 • g.derivativeFun + g • f.derivativeFun)
⊢ Eq (α := R) ((coeff n : (a : R⟦X⟧) → R) (f * g).derivativeFun : R)
    ((coeff n : (a : R⟦X⟧) → R) (f • g.derivativeFun + g • f.derivativeFun) : R)
have h₃ : HMul.hMul (α := R) ((coeff (n + 1) : (a : R⟦X⟧) → R) (f * g) : R) (HAdd.hAdd (α := R) (↑n : R) 1) =
  HAdd.hAdd (α := R) (β := R) ((coeff n : (a : R⟦X⟧) → R) (f • g.derivativeFun) : R)
    ((coeff n : (a : R⟦X⟧) → R) (g • f.derivativeFun) : R)
Tactic: rw [coeff_derivativeFun, map_add, coeff_mul_eq_coeff_trunc_mul_trunc _ _ (lt_succ_self _),
    smul_eq_mul, smul_eq_mul, coeff_mul_eq_coeff_trunc_mul_trunc₂ g f.derivativeFun h₂ h₁,
    coeff_mul_eq_coeff_trunc_mul_trunc₂ f g.derivativeFun h₂ h₁, trunc_derivativeFun,
    trunc_derivativeFun, ← map_add, ← derivativeFun_coe_mul_coe, coeff_derivativeFun]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Derivative (goal)
Goal:
R : Type u_1
inst : CommSemiring R
f g : R⟦X⟧
n : ℕ
h₁ : n < n + 1
h₂ : n < n + 1 + 1
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 • g.derivativeFun + g • f.derivativeFun)
h₃ :
  HMul.hMul (α := R) ((coeff (n + 1) : (a : R⟦X⟧) → R) (f * g) : R) (HAdd.hAdd (α := R) (↑n : R) 1) =
    HAdd.hAdd (α := R) (β := R) ((coeff n : (a : R⟦X⟧) → R) (f • g.derivativeFun) : R)
      ((coeff n : (a : R⟦X⟧) → R) (g • f.derivativeFun) : R)
⊢ Eq (α := R) ((coeff n : (a : R⟦X⟧) → R) (f * g).derivativeFun : R)
    ((coeff n : (a : R⟦X⟧) → R) (f • g.derivativeFun + g • f.derivativeFun) : R)
have h₄ : HMul.hMul (α := R)
    ((coeff (n + 1) : (a : R⟦X⟧) → R)
        (HMul.hMul (α := R⟦X⟧) (↑((trunc (n + 1).succ : (a : R⟦X⟧) → R[X]) f) : R⟦X⟧)
          (↑((trunc (n + 1).succ : (a : R⟦X⟧) → R[X]) g) : R⟦X⟧)) :
      R)
    (HAdd.hAdd (α := R) (↑n : R) 1) =
  HAdd.hAdd (α := R) (β := R) ((coeff n : (a : R⟦X⟧) → R) (f • g.derivativeFun) : R)
    ((coeff n : (a : R⟦X⟧) → R) (g • f.derivativeFun) : R)
Tactic: rw [coeff_derivativeFun, map_add, coeff_mul_eq_coeff_trunc_mul_trunc _ _ (lt_succ_self _),
    smul_eq_mul, smul_eq_mul, coeff_mul_eq_coeff_trunc_mul_trunc₂ g f.derivativeFun h₂ h₁,
    coeff_mul_eq_coeff_trunc_mul_trunc₂ f g.derivativeFun h₂ h₁, trunc_derivativeFun,
    trunc_derivativeFun, ← map_add, ← derivativeFun_coe_mul_coe, coeff_derivativeFun]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Derivative (goal)
Goal:
R : Type u_1
inst : CommSemiring R
f g : R⟦X⟧
n : ℕ
h₁ : n < n + 1
h₂ : n < n + 1 + 1
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 • g.derivativeFun + g • f.derivativeFun)
h₃ :
  HMul.hMul (α := R) ((coeff (n + 1) : (a : R⟦X⟧) → R) (f * g) : R) (HAdd.hAdd (α := R) (↑n : R) 1) =
    HAdd.hAdd (α := R) (β := R) ((coeff n : (a : R⟦X⟧) → R) (f • g.derivativeFun) : R)
      ((coeff n : (a : R⟦X⟧) → R) (g • f.derivativeFun) : R)
h₄ :
  HMul.hMul (α := R)
      ((coeff (n + 1) : (a : R⟦X⟧) → R)
          (HMul.hMul (α := R⟦X⟧) (↑((trunc (n + 1).succ : (a : R⟦X⟧) → R[X]) f) : R⟦X⟧)
            (↑((trunc (n + 1).succ : (a : R⟦X⟧) → R[X]) g) : R⟦X⟧)) :
        R)
      (HAdd.hAdd (α := R) (↑n : R) 1) =
    HAdd.hAdd (α := R) (β := R) ((coeff n : (a : R⟦X⟧) → R) (f • g.derivativeFun) : R)
      ((coeff n : (a : R⟦X⟧) → R) (g • f.derivativeFun) : R)
⊢ Eq (α := R) ((coeff n : (a : R⟦X⟧) → R) (f * g).derivativeFun : R)
    ((coeff n : (a : R⟦X⟧) → R) (f • g.derivativeFun + g • f.derivativeFun) : R)
have h₅ : HMul.hMul (α := R)
    ((coeff (n + 1) : (a : R⟦X⟧) → R)
        (HMul.hMul (α := R⟦X⟧) (↑((trunc (n + 1).succ : (a : R⟦X⟧) → R[X]) f) : R⟦X⟧)
          (↑((trunc (n + 1).succ : (a : R⟦X⟧) → R[X]) g) : R⟦X⟧)) :
      R)
    (HAdd.hAdd (α := R) (↑n : R) 1) =
  HAdd.hAdd (α := R) (β := R) ((coeff n : (a : R⟦X⟧) → R) (f * g.derivativeFun) : R)
    ((coeff n : (a : R⟦X⟧) → R) (g • f.derivativeFun) : R)
Tactic: rw [coeff_derivativeFun, map_add, coeff_mul_eq_coeff_trunc_mul_trunc _ _ (lt_succ_self _),
    smul_eq_mul, smul_eq_mul, coeff_mul_eq_coeff_trunc_mul_trunc₂ g f.derivativeFun h₂ h₁,
    coeff_mul_eq_coeff_trunc_mul_trunc₂ f g.derivativeFun h₂ h₁, trunc_derivativeFun,
    trunc_derivativeFun, ← map_add, ← derivativeFun_coe_mul_coe, coeff_derivativeFun]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Derivative (goal)
Goal:
R : Type u_1
inst : CommSemiring R
f g : R⟦X⟧
n : ℕ
h₁ : n < n + 1
h₂ : n < n + 1 + 1
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 • g.derivativeFun + g • f.derivativeFun)
h₃ :
  HMul.hMul (α := R) ((coeff (n + 1) : (a : R⟦X⟧) → R) (f * g) : R) (HAdd.hAdd (α := R) (↑n : R) 1) =
    HAdd.hAdd (α := R) (β := R) ((coeff n : (a : R⟦X⟧) → R) (f • g.derivativeFun) : R)
      ((coeff n : (a : R⟦X⟧) → R) (g • f.derivativeFun) : R)
h₄ :
  HMul.hMul (α := R)
      ((coeff (n + 1) : (a : R⟦X⟧) → R)
          (HMul.hMul (α := R⟦X⟧) (↑((trunc (n + 1).succ : (a : R⟦X⟧) → R[X]) f) : R⟦X⟧)
            (↑((trunc (n + 1).succ : (a : R⟦X⟧) → R[X]) g) : R⟦X⟧)) :
        R)
      (HAdd.hAdd (α := R) (↑n : R) 1) =
    HAdd.hAdd (α := R) (β := R) ((coeff n : (a : R⟦X⟧) → R) (f • g.derivativeFun) : R)
      ((coeff n : (a : R⟦X⟧) → R) (g • f.derivativeFun) : R)
h₅ :
  HMul.hMul (α := R)
      ((coeff (n + 1) : (a : R⟦X⟧) → R)
          (HMul.hMul (α := R⟦X⟧) (↑((trunc (n + 1).succ : (a : R⟦X⟧) → R[X]) f) : R⟦X⟧)
            (↑((trunc (n + 1).succ : (a : R⟦X⟧) → R[X]) g) : R⟦X⟧)) :
        R)
      (HAdd.hAdd (α := R) (↑n : R) 1) =
    HAdd.hAdd (α := R) (β := R) ((coeff n : (a : R⟦X⟧) → R) (f * g.derivativeFun) : R)
      ((coeff n : (a : R⟦X⟧) → R) (g • f.derivativeFun) : R)
⊢ Eq (α := R) ((coeff n : (a : R⟦X⟧) → R) (f * g).derivativeFun : R)
    ((coeff n : (a : R⟦X⟧) → R) (f • g.derivativeFun + g • f.derivativeFun) : R)
have h₆ : HMul.hMul (α := R)
    ((coeff (n + 1) : (a : R⟦X⟧) → R)
        (HMul.hMul (α := R⟦X⟧) (↑((trunc (n + 1).succ : (a : R⟦X⟧) → R[X]) f) : R⟦X⟧)
          (↑((trunc (n + 1).succ : (a : R⟦X⟧) → R[X]) g) : R⟦X⟧)) :
      R)
    (HAdd.hAdd (α := R) (↑n : R) 1) =
  HAdd.hAdd (α := R) (β := R) ((coeff n : (a : R⟦X⟧) → R) (f * g.derivativeFun) : R)
    ((coeff n : (a : R⟦X⟧) → R) (g * f.derivativeFun) : R)
Tactic: rw [coeff_derivativeFun, map_add, coeff_mul_eq_coeff_trunc_mul_trunc _ _ (lt_succ_self _),
    smul_eq_mul, smul_eq_mul, coeff_mul_eq_coeff_trunc_mul_trunc₂ g f.derivativeFun h₂ h₁,
    coeff_mul_eq_coeff_trunc_mul_trunc₂ f g.derivativeFun h₂ h₁, trunc_derivativeFun,
    trunc_derivativeFun, ← map_add, ← derivativeFun_coe_mul_coe, coeff_derivativeFun]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Derivative (goal)
Goal:
R : Type u_1
inst : CommSemiring R
f g : R⟦X⟧
n : ℕ
h₁ : n < n + 1
h₂ : n < n + 1 + 1
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 • g.derivativeFun + g • f.derivativeFun)
h₃ :
  HMul.hMul (α := R) ((coeff (n + 1) : (a : R⟦X⟧) → R) (f * g) : R) (HAdd.hAdd (α := R) (↑n : R) 1) =
    HAdd.hAdd (α := R) (β := R) ((coeff n : (a : R⟦X⟧) → R) (f • g.derivativeFun) : R)
      ((coeff n : (a : R⟦X⟧) → R) (g • f.derivativeFun) : R)
h₄ :
  HMul.hMul (α := R)
      ((coeff (n + 1) : (a : R⟦X⟧) → R)
          (HMul.hMul (α := R⟦X⟧) (↑((trunc (n + 1).succ : (a : R⟦X⟧) → R[X]) f) : R⟦X⟧)
            (↑((trunc (n + 1).succ : (a : R⟦X⟧) → R[X]) g) : R⟦X⟧)) :
        R)
      (HAdd.hAdd (α := R) (↑n : R) 1) =
    HAdd.hAdd (α := R) (β := R) ((coeff n : (a : R⟦X⟧) → R) (f • g.derivativeFun) : R)
      ((coeff n : (a : R⟦X⟧) → R) (g • f.derivativeFun) : R)
h₅ :
  HMul.hMul (α := R)
      ((coeff (n + 1) : (a : R⟦X⟧) → R)
          (HMul.hMul (α := R⟦X⟧) (↑((trunc (n + 1).succ : (a : R⟦X⟧) → R[X]) f) : R⟦X⟧)
            (↑((trunc (n + 1).succ : (a : R⟦X⟧) → R[X]) g) : R⟦X⟧)) :
        R)
      (HAdd.hAdd (α := R) (↑n : R) 1) =
    HAdd.hAdd (α := R) (β := R) ((coeff n : (a : R⟦X⟧) → R) (f * g.derivativeFun) : R)
      ((coeff n : (a : R⟦X⟧) → R) (g • f.derivativeFun) : R)
h₆ :
  HMul.hMul (α := R)
      ((coeff (n + 1) : (a : R⟦X⟧) → R)
          (HMul.hMul (α := R⟦X⟧) (↑((trunc (n + 1).succ : (a : R⟦X⟧) → R[X]) f) : R⟦X⟧)
            (↑((trunc (n + 1).succ : (a : R⟦X⟧) → R[X]) g) : R⟦X⟧)) :
        R)
      (HAdd.hAdd (α := R) (↑n : R) 1) =
    HAdd.hAdd (α := R) (β := R) ((coeff n : (a : R⟦X⟧) → R) (f * g.derivativeFun) : R)
      ((coeff n : (a : R⟦X⟧) → R) (g * f.derivativeFun) : R)
⊢ Eq (α := R) ((coeff n : (a : R⟦X⟧) → R) (f * g).derivativeFun : R)
    ((coeff n : (a : R⟦X⟧) → R) (f • g.derivativeFun + g • f.derivativeFun) : R)
have h₇ : HMul.hMul (α := R)
    ((coeff (n + 1) : (a : R⟦X⟧) → R)
        (HMul.hMul (α := R⟦X⟧) (↑((trunc (n + 1).succ : (a : R⟦X⟧) → R[X]) f) : R⟦X⟧)
          (↑((trunc (n + 1).succ : (a : R⟦X⟧) → R[X]) g) : R⟦X⟧)) :
      R)
    (HAdd.hAdd (α := R) (↑n : R) 1) =
  HAdd.hAdd (α := R) (β := R) ((coeff n : (a : R⟦X⟧) → R) (f * g.derivativeFun) : R)
    ((coeff n : (a : R⟦X⟧) → R)
        (HMul.hMul (α := R⟦X⟧) (↑((trunc (n + 1 + 1) : (a : R⟦X⟧) → R[X]) g) : R⟦X⟧)
          (↑((trunc (n + 1) : (a : R⟦X⟧) → R[X]) f.derivativeFun) : R⟦X⟧)) :
      R)
Tactic: rw [coeff_derivativeFun, map_add, coeff_mul_eq_coeff_trunc_mul_trunc _ _ (lt_succ_self _),
    smul_eq_mul, smul_eq_mul, coeff_mul_eq_coeff_trunc_mul_trunc₂ g f.derivativeFun h₂ h₁,
    coeff_mul_eq_coeff_trunc_mul_trunc₂ f g.derivativeFun h₂ h₁, trunc_derivativeFun,
    trunc_derivativeFun, ← map_add, ← derivativeFun_coe_mul_coe, coeff_derivativeFun]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Derivative (goal)
Goal:
R : Type u_1
inst : CommSemiring R
⊢ Eq.{u_1 + 1} (α := R⟦X⟧) (derivativeFun 1) 0
have rw : Eq.{u_1 + 1} (α := R⟦X⟧) (derivativeFun ((C : (a : R) → R⟦X⟧) 1)) 0
Tactic: rw [← map_one C, derivativeFun_C (1 : R)]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Derivative (goal)
Goal:
R : Type u_1
inst : CommSemiring R
rw : Eq.{u_1 + 1} (α := R⟦X⟧) (derivativeFun ((C : (a : R) → R⟦X⟧) 1)) 0
⊢ Eq.{u_1 + 1} (α := R⟦X⟧) (derivativeFun 1) 0
have rw₁ : Eq.{u_1 + 1} (α := R⟦X⟧) 0 0
Tactic: rw [← map_one C, derivativeFun_C (1 : R)]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Derivative (goal)
Goal:
R : Type u_1
inst : CommSemiring R
r : R
f : R⟦X⟧
⊢ (r • f).derivativeFun = r • f.derivativeFun
have rw : (HMul.hMul (α := R⟦X⟧) ((C : (a : R) → R⟦X⟧) r : R⟦X⟧) f).derivativeFun = r • f.derivativeFun
Tactic: rw [smul_eq_C_mul, smul_eq_C_mul, derivativeFun_mul, derivativeFun_C, smul_zero, add_zero,
    smul_eq_mul]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Derivative (goal)
Goal:
R : Type u_1
inst : CommSemiring R
r : R
f : R⟦X⟧
rw : (HMul.hMul (α := R⟦X⟧) ((C : (a : R) → R⟦X⟧) r : R⟦X⟧) f).derivativeFun = r • f.derivativeFun
⊢ (r • f).derivativeFun = r • f.derivativeFun
have rw₁ : (HMul.hMul (α := R⟦X⟧) ((C : (a : R) → R⟦X⟧) r : R⟦X⟧) f).derivativeFun =
  HMul.hMul (α := R⟦X⟧) ((C : (a : R) → R⟦X⟧) r : R⟦X⟧) f.derivativeFun
Tactic: rw [smul_eq_C_mul, smul_eq_C_mul, derivativeFun_mul, derivativeFun_C, smul_zero, add_zero,
    smul_eq_mul]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Derivative (goal)
Goal:
R : Type u_1
inst : CommSemiring R
r : R
f : R⟦X⟧
rw : (HMul.hMul (α := R⟦X⟧) ((C : (a : R) → R⟦X⟧) r : R⟦X⟧) f).derivativeFun = r • f.derivativeFun
rw₁ :
  (HMul.hMul (α := R⟦X⟧) ((C : (a : R) → R⟦X⟧) r : R⟦X⟧) f).derivativeFun =
    HMul.hMul (α := R⟦X⟧) ((C : (a : R) → R⟦X⟧) r : R⟦X⟧) f.derivativeFun
⊢ (r • f).derivativeFun = r • f.derivativeFun
have rw₂ : HSMul.hSMul (α := R⟦X⟧) ((C : (a : R) → R⟦X⟧) r : R⟦X⟧) f.derivativeFun +
    HSMul.hSMul (β := R⟦X⟧) f (derivativeFun ((C : (a : R) → R⟦X⟧) r)) =
  HMul.hMul (α := R⟦X⟧) ((C : (a : R) → R⟦X⟧) r : R⟦X⟧) f.derivativeFun
Tactic: rw [smul_eq_C_mul, smul_eq_C_mul, derivativeFun_mul, derivativeFun_C, smul_zero, add_zero,
    smul_eq_mul]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Derivative (goal)
Goal:
R : Type u_1
inst : CommSemiring R
r : R
f : R⟦X⟧
rw : (HMul.hMul (α := R⟦X⟧) ((C : (a : R) → R⟦X⟧) r : R⟦X⟧) f).derivativeFun = r • f.derivativeFun
rw₁ :
  (HMul.hMul (α := R⟦X⟧) ((C : (a : R) → R⟦X⟧) r : R⟦X⟧) f).derivativeFun =
    HMul.hMul (α := R⟦X⟧) ((C : (a : R) → R⟦X⟧) r : R⟦X⟧) f.derivativeFun
rw₂ :
  HSMul.hSMul (α := R⟦X⟧) ((C : (a : R) → R⟦X⟧) r : R⟦X⟧) f.derivativeFun +
      HSMul.hSMul (β := R⟦X⟧) f (derivativeFun ((C : (a : R) → R⟦X⟧) r)) =
    HMul.hMul (α := R⟦X⟧) ((C : (a : R) → R⟦X⟧) r : R⟦X⟧) f.derivativeFun
⊢ (r • f).derivativeFun = r • f.derivativeFun
have rw₃ : HSMul.hSMul (α := R⟦X⟧) ((C : (a : R) → R⟦X⟧) r : R⟦X⟧) f.derivativeFun + HSMul.hSMul (β := R⟦X⟧) f 0 =
  HMul.hMul (α := R⟦X⟧) ((C : (a : R) → R⟦X⟧) r : R⟦X⟧) f.derivativeFun
Tactic: rw [smul_eq_C_mul, smul_eq_C_mul, derivativeFun_mul, derivativeFun_C, smul_zero, add_zero,
    smul_eq_mul]