From 0bed1f91426f5b144646fca4cae6cd6e6bceff6d Mon Sep 17 00:00:00 2001
From: Matthew Robert Ballard <matt@mrb.email>
Date: Mon, 11 Mar 2024 18:02:30 +0000
Subject: [PATCH] perf(InnerProduct.Adjoint): speed up elaboration in two
 proofs (#11300)
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

For as yet un-completely diagnosed reasons, `unitary.star_mul_self_of_mem hu` for `(hu : u ∈ unitary (H →L[𝕜] H))` elaborates slowly thanks to `[1.068378s] ✅ ContinuousLinearMap.comp (ContinuousLinearMap.adjoint u) u =?= star ?a * ?b`. This PR pulls out the statements into `have`'s which speeds up the proofs significantly. #11299 documents the issue for future investigation.
---
 Mathlib/Analysis/InnerProductSpace/Adjoint.lean | 8 ++++++--
 1 file changed, 6 insertions(+), 2 deletions(-)

diff --git a/Mathlib/Analysis/InnerProductSpace/Adjoint.lean b/Mathlib/Analysis/InnerProductSpace/Adjoint.lean
index a617eb3d9f39f..c5ee2a27703cf 100644
--- a/Mathlib/Analysis/InnerProductSpace/Adjoint.lean
+++ b/Mathlib/Analysis/InnerProductSpace/Adjoint.lean
@@ -545,11 +545,15 @@ lemma _root_.LinearIsometryEquiv.star_eq_symm (e : H ≃ₗᵢ[𝕜] H) :
 
 theorem norm_map_of_mem_unitary {u : H →L[𝕜] H} (hu : u ∈ unitary (H →L[𝕜] H)) (x : H) :
     ‖u x‖ = ‖x‖ :=
-  u.norm_map_iff_adjoint_comp_self.mpr (unitary.star_mul_self_of_mem hu) x
+  -- Elaborates faster with this broken out #11299
+  have := unitary.star_mul_self_of_mem hu
+  u.norm_map_iff_adjoint_comp_self.mpr this x
 
 theorem inner_map_map_of_mem_unitary {u : H →L[𝕜] H} (hu : u ∈ unitary (H →L[𝕜] H)) (x y : H) :
     ⟪u x, u y⟫_𝕜 = ⟪x, y⟫_𝕜 :=
-  u.inner_map_map_iff_adjoint_comp_self.mpr (unitary.star_mul_self_of_mem hu) x y
+  -- Elaborates faster with this broken out #11299
+  have := unitary.star_mul_self_of_mem hu
+  u.inner_map_map_iff_adjoint_comp_self.mpr this x y
 
 end ContinuousLinearMap