no goals
𝕜 : Type u_2
R : Type u_1
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedCommRing R
inst✝³ : NormedAlgebra 𝕜 R
inst✝² : TopologicalRing R
inst✝¹ : CompleteSpace R
inst✝ : T2Space R
r : R
⊢ exp 𝕜 (r • ε) = ↑1 + r • ε
rw [eps, ← inr_smul, exp_inr, Nat.cast_one]