chore(Analysis): golf Basic, Exponential, and ContinuousFunctionalCalculus/Unique (#38006)

Split from #37987 at reviewer request.

This PR contains only the golf changes to:
- `Mathlib/Analysis/CStarAlgebra/Basic.lean`
- `Mathlib/Analysis/CStarAlgebra/Exponential.lean`
- `Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Unique.lean`

Requested in: #37987 (comment)

Author: yuanyi-350

Mathlib/Analysis/CStarAlgebra/Basic.lean

@@ -224,17 +224,8 @@ theorem norm_of_mem_unitary [Nontrivial E] {U : E} (hU : U ∈ unitary E) : ‖U
 
 @[simp]
 theorem norm_coe_unitary_mul (U : unitary E) (A : E) : ‖(U : E) * A‖ = ‖A‖ := by
-  nontriviality E
-  refine le_antisymm ?_ ?_
-  · calc
-      _ ≤ ‖(U : E)‖ * ‖A‖ := norm_mul_le _ _
-      _ = ‖A‖ := by rw [norm_coe_unitary, one_mul]
-  · calc
-      _ = ‖(U : E)⋆ * U * A‖ := by rw [Unitary.coe_star_mul_self U, one_mul]
-      _ ≤ ‖(U : E)⋆‖ * ‖(U : E) * A‖ := by
-        rw [mul_assoc]
-        exact norm_mul_le _ _
-      _ = ‖(U : E) * A‖ := by rw [norm_star, norm_coe_unitary, one_mul]
+  rw [← sq_eq_sq₀ (norm_nonneg _) (norm_nonneg _)]
+  simp [sq, ← CStarRing.norm_star_mul_self, mul_assoc, ← mul_assoc (U : E)⋆]
 
 @[simp]
 theorem norm_unitary_smul (U : unitary E) (A : E) : ‖U • A‖ = ‖A‖ :=
@@ -244,12 +235,8 @@ theorem norm_mem_unitary_mul {U : E} (A : E) (hU : U ∈ unitary E) : ‖U * A
   norm_coe_unitary_mul ⟨U, hU⟩ A
 
 @[simp]
-theorem norm_mul_coe_unitary (A : E) (U : unitary E) : ‖A * U‖ = ‖A‖ :=
-  calc
-    _ = ‖((U : E)⋆ * A⋆)⋆‖ := by simp only [star_star, star_mul]
-    _ = ‖(U : E)⋆ * A⋆‖ := by rw [norm_star]
-    _ = ‖A⋆‖ := norm_mem_unitary_mul (star A) (Unitary.star_mem U.prop)
-    _ = ‖A‖ := norm_star _
+theorem norm_mul_coe_unitary (A : E) (U : unitary E) : ‖A * U‖ = ‖A‖ := by
+  simpa [← norm_star (A * U)] using norm_coe_unitary_mul (star U) (star A)
 
 theorem norm_mul_mem_unitary (A : E) {U : E} (hU : U ∈ unitary E) : ‖A * U‖ = ‖A‖ :=
   norm_mul_coe_unitary A ⟨U, hU⟩

Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Unique.lean

@@ -177,16 +177,7 @@ instance NNReal.instContinuousMap.UniqueHom [T2Space A] :
     ContinuousMap.UniqueHom ℝ≥0 A where
   eq_of_continuous_of_map_id s hs φ ψ hφ hψ h := by
     let s' : Set ℝ := (↑) '' s
-    let e : s ≃ₜ s' :=
-      { toFun := Subtype.map (↑) (by simp [s'])
-        invFun := Subtype.map Real.toNNReal (by simp [s'])
-        left_inv := fun _ ↦ by ext; simp
-        right_inv := fun x ↦ by
-          ext
-          obtain ⟨y, -, hy⟩ := x.2
-          simpa using hy ▸ NNReal.coe_nonneg y
-        continuous_toFun := continuous_coe.subtype_map (by simp [s'])
-        continuous_invFun := continuous_real_toNNReal.subtype_map (by simp [s']) }
+    let e : s ≃ₜ s' := NNReal.isEmbedding_coe.homeomorphImage s
     have (ξ : C(s, ℝ≥0) →⋆ₐ[ℝ≥0] A) (hξ : Continuous ξ) :
         (let ξ' := ξ.realContinuousMapOfNNReal.comp <| ContinuousMap.compStarAlgHom' ℝ ℝ e
         Continuous ξ' ∧ ξ' (.restrict s' <| .id ℝ) = ξ (.restrict s <| .id ℝ≥0)) := by
@@ -366,20 +357,10 @@ instance NNReal.instContinuousMapZero.UniqueHom
     ContinuousMapZero.UniqueHom ℝ≥0 A where
   eq_of_continuous_of_map_id s hs h0 φ ψ hφ hψ h := by
     let s' : Set ℝ := (↑) '' s
-    let e : s ≃ₜ s' :=
-      { toFun := Subtype.map (↑) (by simp [s'])
-        invFun := Subtype.map Real.toNNReal (by simp [s'])
-        left_inv := fun _ ↦ by ext; simp
-        right_inv := fun x ↦ by
-          ext
-          obtain ⟨y, -, hy⟩ := x.2
-          simpa using hy ▸ NNReal.coe_nonneg y
-        continuous_toFun := continuous_coe.subtype_map (by simp [s'])
-        continuous_invFun := continuous_real_toNNReal.subtype_map (by simp [s']) }
+    let e : s ≃ₜ s' := NNReal.isEmbedding_coe.homeomorphImage s
     have : Fact (0 ∈ s') := ⟨0, Fact.out, coe_zero⟩
-    have e0 : e 0 = 0 := by ext; simp [e]; rfl
-    have e0' : e.symm 0 = 0 := by
-      simpa only [Homeomorph.symm_apply_apply] using congr(e.symm $(e0)).symm
+    have e0 : e 0 = 0 := rfl
+    have e0' : e.symm 0 = 0 := e.symm_apply_eq.mpr e0
     have (ξ : C(s, ℝ≥0)₀ →⋆ₙₐ[ℝ≥0] A) (hξ : Continuous ξ) :
         (let ξ' := ξ.realContinuousMapZeroOfNNReal.comp <|
           ContinuousMapZero.nonUnitalStarAlgHom_precomp ℝ ⟨e, e0⟩;

Mathlib/Analysis/CStarAlgebra/Exponential.lean

@@ -55,17 +55,11 @@ lemma selfAdjoint.continuous_expUnitary : Continuous (expUnitary : selfAdjoint A
 theorem Commute.expUnitary_add {a b : selfAdjoint A} (h : Commute (a : A) (b : A)) :
     expUnitary (a + b) = expUnitary a * expUnitary b := by
   let +nondep : NormedAlgebra ℚ A := .restrictScalars ℚ ℂ A
-  ext
-  have hcomm : Commute (I • (a : A)) (I • (b : A)) := by
-    unfold Commute SemiconjBy
-    simp only [h.eq, Algebra.smul_mul_assoc, Algebra.mul_smul_comm]
-  simpa only [expUnitary_coe, AddSubgroup.coe_add, smul_add] using exp_add_of_commute hcomm
+  simpa only [Subtype.ext_iff, expUnitary_coe, AddSubgroup.coe_add, smul_add] using
+    exp_add_of_commute ((h.smul_left I).smul_right I)
 
 theorem Commute.expUnitary {a b : selfAdjoint A} (h : Commute (a : A) (b : A)) :
-    Commute (expUnitary a) (expUnitary b) :=
-  calc
-    selfAdjoint.expUnitary a * selfAdjoint.expUnitary b =
-        selfAdjoint.expUnitary b * selfAdjoint.expUnitary a := by
-      rw [← h.expUnitary_add, ← h.symm.expUnitary_add, add_comm]
+    Commute (expUnitary a) (expUnitary b) := by
+  rw [Commute, SemiconjBy, ← h.expUnitary_add, ← h.symm.expUnitary_add, add_comm]
 
 end Star