-- Module: Mathlib.RingTheory.PowerSeries.Derivative
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)
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)
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)
          (HMul.hMul (α := R⟦X⟧) (↑((trunc (n + 1 + 1) : (a : R⟦X⟧) → R[X]) f) : R⟦X⟧)
            (↑((trunc (n + 1) : (a : R⟦X⟧) → R[X]) g.derivativeFun) : R⟦X⟧)) :
        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)
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)
          (HMul.hMul (α := R⟦X⟧) (↑((trunc (n + 1 + 1) : (a : R⟦X⟧) → R[X]) f) : R⟦X⟧)
            (↑((derivative : (a : R[X]) → R[X]) ((trunc (n + 1 + 1) : (a : R⟦X⟧) → R[X]) g)) : R⟦X⟧)) :
        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)
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)
          (HMul.hMul (α := R⟦X⟧) (↑((trunc (n + 1 + 1) : (a : R⟦X⟧) → R[X]) f) : R⟦X⟧)
            (↑((derivative : (a : R[X]) → R[X]) ((trunc (n + 1 + 1) : (a : R⟦X⟧) → R[X]) g)) : R⟦X⟧)) :
        R)
      ((coeff n : (a : R⟦X⟧) → R)
          (HMul.hMul (α := R⟦X⟧) (↑((trunc (n + 1 + 1) : (a : R⟦X⟧) → R[X]) g) : R⟦X⟧)
            (↑((derivative : (a : R[X]) → R[X]) ((trunc (n + 1 + 1) : (a : R⟦X⟧) → R[X]) f)) : R⟦X⟧)) :
        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) =
    (coeff n : (a : R⟦X⟧) → R)
      (HMul.hMul (α := R⟦X⟧) (↑((trunc (n + 1 + 1) : (a : R⟦X⟧) → R[X]) f) : R⟦X⟧)
          (↑((derivative : (a : R[X]) → R[X]) ((trunc (n + 1 + 1) : (a : R⟦X⟧) → R[X]) g)) : R⟦X⟧) +
        HMul.hMul (α := R⟦X⟧) (↑((trunc (n + 1 + 1) : (a : R⟦X⟧) → R[X]) g) : R⟦X⟧)
          (↑((derivative : (a : R[X]) → R[X]) ((trunc (n + 1 + 1) : (a : R⟦X⟧) → R[X]) f)) : R⟦X⟧))
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) =
    (coeff n : (a : R⟦X⟧) → R)
      (HMul.hMul (α := R⟦X⟧) (↑((trunc (n + 1 + 1) : (a : R⟦X⟧) → R[X]) f) : R⟦X⟧)
          (↑((trunc (n + 1 + 1) : (a : R⟦X⟧) → R[X]) g) : R⟦X⟧)).derivativeFun
h₁₃ 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) =
    HMul.hMul (α := R)
      ((coeff (n + 1) : (a : R⟦X⟧) → R)
          (HMul.hMul (α := R⟦X⟧) (↑((trunc (n + 1 + 1) : (a : R⟦X⟧) → R[X]) f) : R⟦X⟧)
            (↑((trunc (n + 1 + 1) : (a : R⟦X⟧) → R[X]) g) : R⟦X⟧)) :
        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 • g.derivativeFun + 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]

Premises used: PowerSeries.coeff_mul_eq_coeff_trunc_mul_trunc₂, PowerSeries.coeff_derivativeFun, Nat.lt_succ_self, map_add, _private.0.PowerSeries.derivativeFun_coe_mul_coe, PowerSeries.coeff_mul_eq_coeff_trunc_mul_trunc, smul_eq_mul, PowerSeries.trunc_derivativeFun, PowerSeries.derivativeFun