no goals
𝕂 : Type u_2
𝔸 : Type u_1
𝔹 : Type ?u.368109
inst✝⁷ : IsROrC 𝕂
inst✝⁶ : NormedRing 𝔸
inst✝⁵ : NormedAlgebra 𝕂 𝔸
inst✝⁴ : NormedRing 𝔹
inst✝³ : NormedAlgebra 𝕂 𝔹
inst✝² : CompleteSpace 𝔸
inst✝¹ : StarRing 𝔸
inst✝ : ContinuousStar 𝔸
x : 𝔸
h : x ∈ skewAdjoint 𝔸
⊢ exp 𝕂 x ∈ unitary 𝔸
rw [unitary.mem_iff, star_exp, skewAdjoint.mem_iff.mp h, ←
  exp_add_of_commute (Commute.refl x).neg_left, ← exp_add_of_commute (Commute.refl x).neg_right,
  add_left_neg, add_right_neg, exp_zero, and_self_iff]