From 7b1d45be99874ae55cd127da70d28e582cb0f073 Mon Sep 17 00:00:00 2001
From: Kevin Buzzard <k.buzzard@imperial.ac.uk>
Date: Tue, 14 Apr 2026 10:42:34 +0100
Subject: [PATCH 1/2] perf(Analysis/RCLike/Basic): move a section

---
 Mathlib/Analysis/RCLike/Basic.lean | 45 ++++++++++++++++++------------
 1 file changed, 27 insertions(+), 18 deletions(-)

diff --git a/Mathlib/Analysis/RCLike/Basic.lean b/Mathlib/Analysis/RCLike/Basic.lean
index 47383080dab471..d04dead62c88c0 100644
--- a/Mathlib/Analysis/RCLike/Basic.lean
+++ b/Mathlib/Analysis/RCLike/Basic.lean
@@ -662,24 +662,6 @@ variable (K) in
 lemma nnnorm_nsmul [NormedAddCommGroup E] [NormedSpace K E] (n : ℕ) (x : E) :
     ‖n • x‖₊ = n • ‖x‖₊ := by simpa [Nat.cast_smul_eq_nsmul] using nnnorm_smul (n : K) x
 
-section NormedField
-variable [NormedField E] [CharZero E] [NormedSpace K E]
-include K
-
-variable (K) in
-lemma norm_nnqsmul (q : ℚ≥0) (x : E) : ‖q • x‖ = q • ‖x‖ := by
-  simpa [NNRat.cast_smul_eq_nnqsmul] using norm_smul (q : K) x
-
-variable (K) in
-lemma nnnorm_nnqsmul (q : ℚ≥0) (x : E) : ‖q • x‖₊ = q • ‖x‖₊ := by
-  simpa [NNRat.cast_smul_eq_nnqsmul] using nnnorm_smul (q : K) x
-
-@[bound]
-lemma norm_expect_le {ι : Type*} {s : Finset ι} {f : ι → E} : ‖𝔼 i ∈ s, f i‖ ≤ 𝔼 i ∈ s, ‖f i‖ :=
-  Finset.le_expect_of_subadditive norm_zero norm_add_le fun _ _ ↦ by rw [norm_nnqsmul K]
-
-end NormedField
-
 theorem mul_self_norm (z : K) : ‖z‖ * ‖z‖ = normSq z := by rw [normSq_eq_def', sq]
 
 attribute [rclike_simps] norm_zero norm_one norm_eq_zero abs_norm norm_inv norm_div
@@ -788,6 +770,33 @@ end Instances
 
 namespace RCLike
 
+section NormedField
+variable [NormedField E] [CharZero E] [NormedSpace K E]
+include K
+
+set_option trace.profiler true
+set_option trace.profiler.useHeartbeats true
+
+-- [Elab.command] [728878.000000]
+-- [Elab.command] [220634.000000]
+variable (K) in
+lemma norm_nnqsmul (q : ℚ≥0) (x : E) : ‖q • x‖ = q • ‖x‖ := by
+  simpa [NNRat.cast_smul_eq_nnqsmul] using norm_smul (q : K) x
+
+-- [Elab.command] [183826.000000]
+-- [Elab.command] [183519.000000]
+variable (K) in
+lemma nnnorm_nnqsmul (q : ℚ≥0) (x : E) : ‖q • x‖₊ = q • ‖x‖₊ := by
+  simpa [NNRat.cast_smul_eq_nnqsmul] using nnnorm_smul (q : K) x
+
+-- [Elab.command] [1308705.000000]
+-- [Elab.command] [802785.000000]
+@[bound]
+lemma norm_expect_le {ι : Type*} {s : Finset ι} {f : ι → E} : ‖𝔼 i ∈ s, f i‖ ≤ 𝔼 i ∈ s, ‖f i‖ :=
+  Finset.le_expect_of_subadditive norm_zero norm_add_le fun _ _ ↦ by rw [norm_nnqsmul K]
+
+end NormedField
+
 section Order
 
 open scoped ComplexOrder

From 5a3bcef72b9ddca5b51c209cd469329ae14d2c9c Mon Sep 17 00:00:00 2001
From: Kevin Buzzard <k.buzzard@imperial.ac.uk>
Date: Tue, 14 Apr 2026 11:03:59 +0100
Subject: [PATCH 2/2] tidy up

---
 Mathlib/Analysis/RCLike/Basic.lean | 9 ---------
 1 file changed, 9 deletions(-)

diff --git a/Mathlib/Analysis/RCLike/Basic.lean b/Mathlib/Analysis/RCLike/Basic.lean
index d04dead62c88c0..6126e1b075c3a1 100644
--- a/Mathlib/Analysis/RCLike/Basic.lean
+++ b/Mathlib/Analysis/RCLike/Basic.lean
@@ -774,23 +774,14 @@ section NormedField
 variable [NormedField E] [CharZero E] [NormedSpace K E]
 include K
 
-set_option trace.profiler true
-set_option trace.profiler.useHeartbeats true
-
--- [Elab.command] [728878.000000]
--- [Elab.command] [220634.000000]
 variable (K) in
 lemma norm_nnqsmul (q : ℚ≥0) (x : E) : ‖q • x‖ = q • ‖x‖ := by
   simpa [NNRat.cast_smul_eq_nnqsmul] using norm_smul (q : K) x
 
--- [Elab.command] [183826.000000]
--- [Elab.command] [183519.000000]
 variable (K) in
 lemma nnnorm_nnqsmul (q : ℚ≥0) (x : E) : ‖q • x‖₊ = q • ‖x‖₊ := by
   simpa [NNRat.cast_smul_eq_nnqsmul] using nnnorm_smul (q : K) x
 
--- [Elab.command] [1308705.000000]
--- [Elab.command] [802785.000000]
 @[bound]
 lemma norm_expect_le {ι : Type*} {s : Finset ι} {f : ι → E} : ‖𝔼 i ∈ s, f i‖ ≤ 𝔼 i ∈ s, ‖f i‖ :=
   Finset.le_expect_of_subadditive norm_zero norm_add_le fun _ _ ↦ by rw [norm_nnqsmul K]