-- Module: Mathlib.RingTheory.PowerSeries.Derivative
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsAddTorsionFree R
f g : R⟦X⟧
hD : Eq (α := R⟦X⟧) ((d⁄dX R : (a : R⟦X⟧) → R⟦X⟧) f : R⟦X⟧) ((d⁄dX R : (a : R⟦X⟧) → R⟦X⟧) g : R⟦X⟧)
hc : Eq (α := R) ((constantCoeff : (a : R⟦X⟧) → R) f : R) ((constantCoeff : (a : R⟦X⟧) → R) g : R)
n : ℕ
equ :
  Eq (α := R) ((coeff n : (a : R⟦X⟧) → R) ((d⁄dX R : (a : R⟦X⟧) → R⟦X⟧) f : R⟦X⟧) : R)
    ((coeff n : (a : R⟦X⟧) → R) ((d⁄dX R : (a : R⟦X⟧) → R⟦X⟧) g : R⟦X⟧) : R)
h :
  ∀
    (equ :
      HMul.hMul (α := R) ((coeff (n + 1) : (a : R⟦X⟧) → R) f : R) (HAdd.hAdd (α := R) (↑n : R) 1) =
        (coeff n : (a : R⟦X⟧) → R) ((d⁄dX R : (a : R⟦X⟧) → R⟦X⟧) g : R⟦X⟧)),
    Eq (α := R) ((coeff (n + 1) : (a : R⟦X⟧) → R) f : R) ((coeff (n + 1) : (a : R⟦X⟧) → R) g : R)
h₁ :
  ∀
    (equ :
      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 + 1) : (a : R⟦X⟧) → R) f : R) ((coeff (n + 1) : (a : R⟦X⟧) → R) g : R)
h₂ :
  ∀
    (equ :
      HMul.hMul (α := R) (β := R) ((coeff (n + 1) : (a : R⟦X⟧) → R) f : R) ((↑n.succ : R) : R) =
        HMul.hMul (α := R) (β := R) ((coeff (n + 1) : (a : R⟦X⟧) → R) g : R) ((↑n.succ : R) : R)),
    Eq (α := R) ((coeff (n + 1) : (a : R⟦X⟧) → R) f : R) ((coeff (n + 1) : (a : R⟦X⟧) → R) g : R)
h₃ :
  ∀
    (equ :
      HMul.hMul (α := R) (β := R) ((↑n.succ : R) : R) ((coeff (n + 1) : (a : R⟦X⟧) → R) f : R) =
        HMul.hMul (α := R) (β := R) ((coeff (n + 1) : (a : R⟦X⟧) → R) g : R) ((↑n.succ : R) : R)),
    Eq (α := R) ((coeff (n + 1) : (a : R⟦X⟧) → R) f : R) ((coeff (n + 1) : (a : R⟦X⟧) → R) g : R)
h₄ :
  ∀
    (equ :
      HSMul.hSMul (β := R) n.succ ((coeff (n + 1) : (a : R⟦X⟧) → R) f : R) =
        HMul.hMul (α := R) (β := R) ((coeff (n + 1) : (a : R⟦X⟧) → R) g : R) ((↑n.succ : R) : R)),
    Eq (α := R) ((coeff (n + 1) : (a : R⟦X⟧) → R) f : R) ((coeff (n + 1) : (a : R⟦X⟧) → R) g : R)
h₅ :
  ∀
    (equ :
      HSMul.hSMul (β := R) n.succ ((coeff (n + 1) : (a : R⟦X⟧) → R) f : R) =
        HMul.hMul (α := R) (β := R) ((↑n.succ : R) : R) ((coeff (n + 1) : (a : R⟦X⟧) → R) g : R)),
    Eq (α := R) ((coeff (n + 1) : (a : R⟦X⟧) → R) f : R) ((coeff (n + 1) : (a : R⟦X⟧) → R) g : R)
h₆ :
  ∀
    (equ :
      HSMul.hSMul (β := R) n.succ ((coeff (n + 1) : (a : R⟦X⟧) → R) f : R) =
        HSMul.hSMul (β := R) n.succ ((coeff (n + 1) : (a : R⟦X⟧) → R) g : R)),
    Eq (α := R) ((coeff (n + 1) : (a : R⟦X⟧) → R) f : R) ((coeff (n + 1) : (a : R⟦X⟧) → R) g : R)
h₇ h₈ h₉ h₁₀ :
  ∀ (equ : Eq (α := R) ((coeff (n + 1) : (a : R⟦X⟧) → R) f : R) ((coeff (n + 1) : (a : R⟦X⟧) → R) g : R)),
    Eq (α := R) ((coeff (n + 1) : (a : R⟦X⟧) → R) f : R) ((coeff (n + 1) : (a : R⟦X⟧) → R) g : R)
⊢ Eq (α := R) ((coeff (n + 1) : (a : R⟦X⟧) → R) f : R) ((coeff (n + 1) : (a : R⟦X⟧) → R) g : R)

Tactic:
rwa [coeff_derivative, coeff_derivative, ← cast_succ, mul_comm, ← nsmul_eq_mul,
      mul_comm, ← nsmul_eq_mul, smul_right_inj n.succ_ne_zero] at equ

Premises used: Nat.cast_succ, Nat.succ_ne_zero, mul_comm, nsmul_eq_mul, PowerSeries.coeff_derivative, smul_right_inj