∀ {𝔸 : Type u_1} {𝔹 : Type u_2} [inst : NormedRing 𝔸] [NormedAlgebra ℚ 𝔸] [CompleteSpace 𝔸] [inst_3 : NormedRing 𝔹]
  [NormedAlgebra ℚ 𝔹] [CompleteSpace 𝔹] (x : 𝔸 × 𝔹), (NormedSpace.exp x).1 = NormedSpace.exp x.1