no goals
𝕂 : Type u_2
𝔸 : Type u_1
inst✝⁴ : Field 𝕂
inst✝³ : DivisionRing 𝔸
inst✝² : Algebra 𝕂 𝔸
inst✝¹ : TopologicalSpace 𝔸
inst✝ : TopologicalRing 𝔸
x : 𝔸
n : ℕ
⊢ (↑(expSeries 𝕂 𝔸 n) fun x_1 => x) = x ^ n / ↑n !
rw [div_eq_mul_inv, ← (Nat.cast_commute n ! (x ^ n)).inv_left₀.eq, ← smul_eq_mul,
  expSeries_apply_eq, inv_nat_cast_smul_eq 𝕂 𝔸]