-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Exponential (goal)
Goal:
𝕂 : Type u_1
𝕊 : Type u_2
𝔸 : Type u_3
inst : NontriviallyNormedField 𝕂
inst_1 : CharZero 𝕂
inst_2 : NormedCommRing 𝕊
inst_3 : NormedRing 𝔸
inst_4 : NormedSpace 𝕂 𝕊
inst_5 : NormedAlgebra 𝕂 𝔸
inst_6 : Algebra 𝕊 𝔸
inst_7 : ContinuousSMul 𝕊 𝔸
inst_8 : IsScalarTower 𝕂 𝕊 𝔸
inst_9 : CompleteSpace 𝔸
x : 𝔸
t : 𝕊
htx :
  Membership.mem (γ := Set 𝔸)
    (Metric.eball 0 (FormalMultilinearSeries.radius.{u_1, u_3, u_3} (𝕜 := 𝕂) (E := 𝔸) (F := 𝔸) (expSeries 𝕂 𝔸))) (t • x)
this_1 : Tendsto.{u_2, u_3} (β := 𝔸) (fun (h : 𝕊) ↦ h • x) (𝓝 0) (𝓝 0)
this_2 :
  ∀ᶠ (h : 𝕊) in 𝓝 0,
    Membership.mem (γ := Set 𝔸)
      (Metric.eball 0 (FormalMultilinearSeries.radius.{u_1, u_3, u_3} (𝕜 := 𝕂) (E := 𝔸) (F := 𝔸) (expSeries 𝕂 𝔸)))
      (h • x)
h : 𝕊
hh :
  Membership.mem (γ := Set 𝔸)
    (Metric.eball 0 (FormalMultilinearSeries.radius.{u_1, u_3, u_3} (𝕜 := 𝕂) (E := 𝔸) (F := 𝔸) (expSeries 𝕂 𝔸))) (h • x)
this : Commute (t • x) (h • x)
h₁ :
  exp (t • x) *
      HSub.hSub (β := 𝔸) (exp ((0 + h) • x) - exp (HSMul.hSMul.{u_2, u_3, u_3} (α := 𝕊) 0 x))
        ((ContinuousLinearMap.smulRight (S := 𝕊) 1 x : (a : 𝕊) → 𝔸) h : 𝔸) =
    HSub.hSub (β := 𝔸) (exp (t • x + h • x) - exp (t • x))
      ((HSMul.hSMul (β := 𝕊 →L[𝕂] 𝔸) (exp (t • x)) (ContinuousLinearMap.smulRight (S := 𝕊) 1 x) : (a : 𝕊) → 𝔸) h : 𝔸)
h₂ :
  exp (t • x) *
      HSub.hSub (β := 𝔸) (exp ((0 + h) • x) - exp (HSMul.hSMul.{u_2, u_3, u_3} (α := 𝕊) 0 x))
        ((ContinuousLinearMap.smulRight (S := 𝕊) 1 x : (a : 𝕊) → 𝔸) h : 𝔸) =
    HSub.hSub (β := 𝔸) (exp (t • x) * exp (h • x) - exp (t • x))
      ((HSMul.hSMul (β := 𝕊 →L[𝕂] 𝔸) (exp (t • x)) (ContinuousLinearMap.smulRight (S := 𝕊) 1 x) : (a : 𝕊) → 𝔸) h : 𝔸)
h₃ :
  exp (t • x) *
      HSub.hSub (β := 𝔸) (exp (h • x) - exp (HSMul.hSMul.{u_2, u_3, u_3} (α := 𝕊) 0 x))
        ((ContinuousLinearMap.smulRight (S := 𝕊) 1 x : (a : 𝕊) → 𝔸) h : 𝔸) =
    HSub.hSub (β := 𝔸) (exp (t • x) * exp (h • x) - exp (t • x))
      ((HSMul.hSMul (β := 𝕊 →L[𝕂] 𝔸) (exp (t • x)) (ContinuousLinearMap.smulRight (S := 𝕊) 1 x) : (a : 𝕊) → 𝔸) h : 𝔸)
h₄ :
  exp (t • x) *
      HSub.hSub (β := 𝔸) (exp (h • x) - exp 0) ((ContinuousLinearMap.smulRight (S := 𝕊) 1 x : (a : 𝕊) → 𝔸) h : 𝔸) =
    HSub.hSub (β := 𝔸) (exp (t • x) * exp (h • x) - exp (t • x))
      ((HSMul.hSMul (β := 𝕊 →L[𝕂] 𝔸) (exp (t • x)) (ContinuousLinearMap.smulRight (S := 𝕊) 1 x) : (a : 𝕊) → 𝔸) h : 𝔸)
h₅ :
  exp (t • x) *
      HSub.hSub (β := 𝔸) (exp (h • x) - 1) ((ContinuousLinearMap.smulRight (S := 𝕊) 1 x : (a : 𝕊) → 𝔸) h : 𝔸) =
    HSub.hSub (β := 𝔸) (exp (t • x) * exp (h • x) - exp (t • x))
      ((HSMul.hSMul (β := 𝕊 →L[𝕂] 𝔸) (exp (t • x)) (ContinuousLinearMap.smulRight (S := 𝕊) 1 x) : (a : 𝕊) → 𝔸) h : 𝔸)
h₆ :
  exp (t • x) * (exp (h • x) - 1 - HSMul.hSMul (α := 𝕊) ((1 : (a : 𝕊) → 𝕊) h : 𝕊) x) =
    HSub.hSub (β := 𝔸) (exp (t • x) * exp (h • x) - exp (t • x))
      ((HSMul.hSMul (β := 𝕊 →L[𝕂] 𝔸) (exp (t • x)) (ContinuousLinearMap.smulRight (S := 𝕊) 1 x) : (a : 𝕊) → 𝔸) h : 𝔸)
⊢ exp (t • x) *
      HSub.hSub (β := 𝔸) (exp ((0 + h) • x) - exp (HSMul.hSMul.{u_2, u_3, u_3} (α := 𝕊) 0 x))
        ((ContinuousLinearMap.smulRight (S := 𝕊) 1 x : (a : 𝕊) → 𝔸) h : 𝔸) =
    HSub.hSub (β := 𝔸) (exp ((t + h) • x) - exp (t • x))
      ((HSMul.hSMul (β := 𝕊 →L[𝕂] 𝔸) (exp (t • x)) (ContinuousLinearMap.smulRight (S := 𝕊) 1 x) : (a : 𝕊) → 𝔸) h : 𝔸)
have h₇ : exp (t • x) * (exp (h • x) - 1 - h • x) =
  HSub.hSub (β := 𝔸) (exp (t • x) * exp (h • x) - exp (t • x))
    ((HSMul.hSMul (β := 𝕊 →L[𝕂] 𝔸) (exp (t • x)) (ContinuousLinearMap.smulRight (S := 𝕊) 1 x) : (a : 𝕊) → 𝔸) h : 𝔸)
Tactic: rw [add_smul t h, exp_add_of_commute_of_mem_ball this htx hh, zero_add, zero_smul, exp_zero,
    ContinuousLinearMap.smulRight_apply, ContinuousLinearMap.one_apply,
    ContinuousLinearMap.smul_apply, ContinuousLinearMap.smulRight_apply,
    ContinuousLinearMap.one_apply, smul_eq_mul, mul_sub_left_distrib, mul_sub_left_distrib, mul_one]