-- Module: Mathlib.Analysis.Normed.Algebra.TrivSqZeroExt
Goal:
𝕜 : Type u_1
R : Type u_3
M : Type u_4
inst : Field 𝕜
inst_1 : CharZero 𝕜
inst_2 : Ring R
inst_3 : AddCommGroup M
inst_4 : Algebra 𝕜 R
inst_5 : Module 𝕜 M
inst_6 : Module R M
inst_7 : Module.{u_3, u_4} Rᵐᵒᵖ M
inst_8 : SMulCommClass R Rᵐᵒᵖ M
inst_9 : IsScalarTower 𝕜 R M
inst_10 : IsScalarTower.{u_1, u_3, u_4} 𝕜 Rᵐᵒᵖ M
inst_11 : TopologicalSpace R
inst_12 : TopologicalSpace M
inst_13 : IsTopologicalRing R
inst_14 : IsTopologicalAddGroup M
inst_15 : ContinuousSMul R M
inst_16 : ContinuousSMul.{u_3, u_4} Rᵐᵒᵖ M
x : tsze R M
hx : MulOpposite.op x.fst • x.snd = x.fst • x.snd
n : ℕ
simp_rw :
  (HSMul.hSMul (α := 𝕜) (↑(n + 1).factorial : 𝕜)⁻¹ (x ^ (n + 1))).snd =
    HSMul.hSMul.{u_1, u_3, u_3} (α := 𝕜) (↑n.factorial : 𝕜)⁻¹ (x.fst ^ n) • x.snd
simp_rw₁ :
  HSMul.hSMul.{u_1, u_4, u_4} (α := 𝕜) (↑(n + 1).factorial : 𝕜)⁻¹ (x ^ (n + 1)).snd =
    HSMul.hSMul.{u_1, u_3, u_3} (α := 𝕜) (↑n.factorial : 𝕜)⁻¹ (x.fst ^ n) • x.snd
simp_rw₂ :
  HSMul.hSMul.{u_1, u_4, u_4} (α := 𝕜) (↑(n + 1).factorial : 𝕜)⁻¹ ((n + 1) • x.fst ^ (n + 1).pred • x.snd) =
    HSMul.hSMul.{u_1, u_3, u_3} (α := 𝕜) (↑n.factorial : 𝕜)⁻¹ (x.fst ^ n) • x.snd
simp_rw₃ :
  HSMul.hSMul.{u_1, u_4, u_4} (α := 𝕜) (↑(n + 1).factorial : 𝕜)⁻¹
      (HSMul.hSMul.{u_1, u_4, u_4} (α := 𝕜) (↑(n + 1) : 𝕜) (x.fst ^ (n + 1).pred • x.snd)) =
    HSMul.hSMul.{u_1, u_3, u_3} (α := 𝕜) (↑n.factorial : 𝕜)⁻¹ (x.fst ^ n) • x.snd
simp_rw₄ :
  HMul.hMul (α := 𝕜) (↑(n + 1).factorial : 𝕜)⁻¹ (↑(n + 1) : 𝕜) • x.fst ^ (n + 1).pred • x.snd =
    HSMul.hSMul.{u_1, u_3, u_3} (α := 𝕜) (↑n.factorial : 𝕜)⁻¹ (x.fst ^ n) • x.snd
simp_rw₅ :
  HMul.hMul (α := 𝕜) (↑(n + 1).factorial : 𝕜)⁻¹ (↑(n + 1) : 𝕜) • x.fst ^ (n + 1).pred • x.snd =
    HSMul.hSMul.{u_1, u_4, u_4} (α := 𝕜) (↑n.factorial : 𝕜)⁻¹ (x.fst ^ n • x.snd)
simp_rw₆ :
  HMul.hMul (α := 𝕜) (↑((n + 1) * n.factorial) : 𝕜)⁻¹ (↑(n + 1) : 𝕜) • x.fst ^ (n + 1).pred • x.snd =
    HSMul.hSMul.{u_1, u_4, u_4} (α := 𝕜) (↑n.factorial : 𝕜)⁻¹ (x.fst ^ n • x.snd)
simp_rw₇ :
  HMul.hMul (α := 𝕜) (↑((n + 1) * n.factorial) : 𝕜)⁻¹ (↑(n + 1) : 𝕜) • x.fst ^ n • x.snd =
    HSMul.hSMul.{u_1, u_4, u_4} (α := 𝕜) (↑n.factorial : 𝕜)⁻¹ (x.fst ^ n • x.snd)
simp_rw₈ :
  ((HMul.hMul (α := 𝕜) (↑(n + 1) : 𝕜) (↑n.factorial : 𝕜))⁻¹ * (↑(n + 1) : 𝕜)) • x.fst ^ n • x.snd =
    HSMul.hSMul.{u_1, u_4, u_4} (α := 𝕜) (↑n.factorial : 𝕜)⁻¹ (x.fst ^ n • x.snd)
simp_rw₉ :
  (HMul.hMul (α := 𝕜) (↑n.factorial : 𝕜)⁻¹ (↑(n + 1) : 𝕜)⁻¹ * (↑(n + 1) : 𝕜)) • x.fst ^ n • x.snd =
    HSMul.hSMul.{u_1, u_4, u_4} (α := 𝕜) (↑n.factorial : 𝕜)⁻¹ (x.fst ^ n • x.snd)
⊢ snd.{u_3, u_4} (R := R)
      ((expSeries 𝕜 (tsze R M) (n + 1) : (a : (i : Fin (n + 1)) → tsze R M) → tsze R M) fun (x_1 : Fin (n + 1)) ↦ x) =
    HSMul.hSMul (α := R) ((expSeries 𝕜 R n : (a : (i : Fin n) → R) → R) fun (x_1 : Fin n) ↦ x.fst : R) x.snd

Tactic:
simp_rw [expSeries_apply_eq, snd_smul, snd_pow_of_smul_comm _ _ hx,
    ← Nat.cast_smul_eq_nsmul 𝕜 (n + 1), smul_smul, smul_assoc, Nat.factorial_succ, Nat.pred_succ,
    Nat.cast_mul, mul_inv_rev,
    inv_mul_cancel_right₀ ((Nat.cast_ne_zero (R := 𝕜)).mpr <| Nat.succ_ne_zero n)]

Premises used: Iff.mpr, smul_assoc, Nat.factorial_succ, smul_smul, NormedSpace.expSeries_apply_eq, TrivSqZeroExt.snd_smul, TrivSqZeroExt.snd_pow_of_smul_comm, Nat.succ_ne_zero, Nat.cast_mul, HAdd.hAdd, Nat.pred_succ, Nat.cast_smul_eq_nsmul, mul_inv_rev, OfNat.ofNat, Nat.cast_ne_zero, inv_mul_cancel_right₀