-- 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)
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)
⊢ 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)
        (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)
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]