perf(Analysis/Normed/Group): lower instance priorities

Mathlib/Analysis/CStarAlgebra/CStarMatrix.lean

@@ -401,7 +401,6 @@ lemma reindexₗ_apply {l o : Type*} [Semiring R] [AddCommMonoid A] [Module R A]
     {eₘ : m ≃ l} {eₙ : n ≃ o} {M : CStarMatrix m n A} {i : l} {j : o} :
     reindexₗ R A eₘ eₙ M i j = Matrix.reindex eₘ eₙ M i j := rfl
 
-set_option backward.isDefEq.respectTransparency false in
 /-- The natural map that reindexes a matrix's rows and columns with equivalent types is an
 equivalence. -/
 def reindexₐ (R) (A) [Fintype m] [Fintype n] [Semiring R] [AddCommMonoid A] [Mul A] [Module R A]
@@ -418,7 +417,7 @@ def reindexₐ (R) (A) [Fintype m] [Fintype n] [Semiring R] [AddCommMonoid A] [M
       unfold reindexₗ
       dsimp only [Equiv.toFun_as_coe, Equiv.invFun_as_coe, Matrix.reindex_symm, AddHom.toFun_eq_coe,
         AddHom.coe_mk, Matrix.reindex_apply, Matrix.submatrix_apply]
-      rw [Matrix.star_apply, Matrix.star_apply]
+      rw [star_apply, star_apply]
       simp [Matrix.submatrix_apply] }
 
 @[simp]
@@ -474,7 +473,7 @@ def toOneByOne [Unique n] [Semiring R] [AddCommMonoid A] [Mul A] [Star A] [Modul
 
 end basic
 
-variable [Fintype m] [NonUnitalCStarAlgebra A] [PartialOrder A] [StarOrderedRing A]
+variable [Fintype m] [NonUnitalCStarAlgebra A]
 
 set_option backward.isDefEq.respectTransparency false in
 /-- Interpret a `CStarMatrix m n A` as a continuous linear map acting on `C⋆ᵐᵒᵈ (n → A)`. -/
@@ -537,23 +536,24 @@ open WithCStarModule in
 lemma toCLM_apply_single_apply [DecidableEq m] {M : CStarMatrix m n A} {i : m} {j : n} (a : A) :
     (toCLM M) (equiv _ _ |>.symm <| Pi.single i a) j = a * M i j := by simp
 
-open WithCStarModule in
-lemma mul_entry_mul_eq_inner_toCLM [Fintype n] [DecidableEq m] [DecidableEq n]
-    {M : CStarMatrix m n A} {i : m} {j : n} (a b : A) :
-    a * M i j * star b
-      = ⟪equiv _ _ |>.symm (Pi.single j b), toCLM M (equiv _ _ |>.symm <| Pi.single i a)⟫_A := by
-  simp [mul_assoc, inner_def]
-
-set_option backward.isDefEq.respectTransparency false in
 lemma toCLM_injective : Function.Injective (toCLM (A := A) (m := m) (n := n)) := by
   classical
   rw [injective_iff_map_eq_zero]
   intro M h
   ext i j
-  rw [Matrix.zero_apply, ← norm_eq_zero, ← sq_eq_zero_iff, sq, ← CStarRing.norm_star_mul_self,
+  rw [zero_apply, ← norm_eq_zero, ← sq_eq_zero_iff, sq, ← CStarRing.norm_star_mul_self,
     ← toCLM_apply_single_apply]
   simp [h]
 
+variable [PartialOrder A] [StarOrderedRing A]
+
+open WithCStarModule in
+lemma mul_entry_mul_eq_inner_toCLM [Fintype n] [DecidableEq m] [DecidableEq n]
+    {M : CStarMatrix m n A} {i : m} {j : n} (a b : A) :
+    a * M i j * star b
+      = ⟪equiv _ _ |>.symm (Pi.single j b), toCLM M (equiv _ _ |>.symm <| Pi.single i a)⟫_A := by
+  simp [mul_assoc, inner_def]
+
 variable [Fintype n]
 
 open WithCStarModule in

Mathlib/Analysis/Calculus/Deriv/Inv.lean

@@ -65,7 +65,8 @@ theorem differentiableAt_inv_iff : DifferentiableAt 𝕜 (fun x => x⁻¹) x ↔
 
 theorem deriv_inv : deriv (fun x => x⁻¹) x = -(x ^ 2)⁻¹ := by
   rcases eq_or_ne x 0 with (rfl | hne)
-  · simp [deriv_zero_of_not_differentiableAt (mt differentiableAt_inv_iff.1 (not_not.2 rfl))]
+  · rw [deriv_zero_of_not_differentiableAt (mt differentiableAt_inv_iff.1 (not_not.2 rfl))]
+    simp
   · exact (hasDerivAt_inv hne).deriv
 
 @[simp]

Mathlib/Analysis/Calculus/DiffContOnCl.lean

@@ -116,7 +116,7 @@ theorem smul_const {𝕜' : Type*} [NontriviallyNormedField 𝕜'] [NormedAlgebr
 
 theorem inv {f : E → 𝕜} (hf : DiffContOnCl 𝕜 f s) (h₀ : ∀ x ∈ closure s, f x ≠ 0) :
     DiffContOnCl 𝕜 f⁻¹ s :=
-  ⟨differentiableOn_inv.comp hf.1 fun _ hx => h₀ _ (subset_closure hx), hf.2.inv₀ h₀⟩
+  ⟨(differentiableOn_inv.comp hf.1 fun _ hx => h₀ _ (subset_closure hx) :), hf.2.inv₀ h₀⟩
 
 end DiffContOnCl
 

Mathlib/Analysis/Complex/Isometry.lean

@@ -8,6 +8,7 @@ module
 public import Mathlib.Analysis.Complex.Circle
 public import Mathlib.LinearAlgebra.Determinant
 public import Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Basic
+import Mathlib.Tactic.SuppressCompilation
 
 /-!
 # Isometries of the Complex Plane
@@ -32,6 +33,7 @@ The proof of `linear_isometry_complex_aux` is separated in the following parts:
 
 
 noncomputable section
+suppress_compilation -- needed to avoid a panic!
 
 open Complex
 

Mathlib/Analysis/Normed/Algebra/GelfandFormula.lean

@@ -67,7 +67,7 @@ theorem hasFDerivAt_resolvent {a : A} {k : 𝕜} (hk : k ∈ resolventSet 𝕜 a
   have H₁ : HasFDerivAt Ring.inverse _ (algebraMap 𝕜 A k - a) :=
     hasFDerivAt_ringInverse (𝕜 := 𝕜) hk.unit
   have H₂ : HasFDerivAt (fun a => algebraMap 𝕜 A k - a) (- .id 𝕜 A) a := by
-    simpa using (hasFDerivAt_const _ _).sub (hasFDerivAt_id (𝕜 := 𝕜) _)
+    simpa using (hasFDerivAt_const _ a).sub (hasFDerivAt_id a)
   simpa [resolvent_eq hk] using H₁.comp a H₂
 
 end NonTriviallyNormedField

Mathlib/Analysis/Normed/Group/Defs.lean

@@ -116,6 +116,9 @@ class ESeminormedAddMonoid (E : Type*) [TopologicalSpace E]
   enorm_zero : ‖(0 : E)‖ₑ = 0
   protected enorm_add_le : ∀ x y : E, ‖x + y‖ₑ ≤ ‖x‖ₑ + ‖y‖ₑ
 
+-- see Note [lower instance priority]
+attribute [instance 200] ESeminormedAddMonoid.toAddMonoid
+
 /-- An enormed monoid is an additive monoid endowed with a continuous enorm,
 which is positive definite: in other words, this is an `ESeminormedAddMonoid` with a positive
 definiteness condition added. -/
@@ -130,6 +133,9 @@ class ESeminormedMonoid (E : Type*) [TopologicalSpace E] extends ContinuousENorm
   enorm_zero : ‖(1 : E)‖ₑ = 0
   enorm_mul_le : ∀ x y : E, ‖x * y‖ₑ ≤ ‖x‖ₑ + ‖y‖ₑ
 
+-- see Note [lower instance priority]
+attribute [instance 200] ESeminormedMonoid.toMonoid
+
 /-- An enormed monoid is a monoid endowed with a continuous enorm,
 which is positive definite: in other words, this is an `ESeminormedMonoid` with a positive
 definiteness condition added. -/
@@ -146,6 +152,9 @@ the topology coming from `edist`. -/
 class ESeminormedAddCommMonoid (E : Type*) [TopologicalSpace E]
   extends ESeminormedAddMonoid E, AddCommMonoid E where
 
+-- see Note [lower instance priority]
+attribute [instance 200] ESeminormedAddCommMonoid.toAddCommMonoid
+
 /-- An enormed commutative monoid is an additive commutative monoid
 endowed with a continuous enorm which is positive definite.
 
@@ -160,6 +169,9 @@ class ENormedAddCommMonoid (E : Type*) [TopologicalSpace E]
 class ESeminormedCommMonoid (E : Type*) [TopologicalSpace E]
   extends ESeminormedMonoid E, CommMonoid E where
 
+-- see Note [lower instance priority]
+attribute [instance 200] ESeminormedCommMonoid.toCommMonoid
+
 /-- An enormed commutative monoid is a commutative monoid endowed with a continuous enorm
 which is positive definite. -/
 @[to_additive]
@@ -173,6 +185,9 @@ class SeminormedAddGroup (E : Type*) extends Norm E, AddGroup E, PseudoMetricSpa
   /-- The distance function is induced by the norm. -/
   dist_eq : ∀ x y, dist x y = ‖-x + y‖ := by aesop
 
+-- see Note [lower instance priority]
+attribute [instance 200] SeminormedAddGroup.toAddGroup
+
 /-- A seminormed group is a group endowed with a norm for which `dist x y = ‖x⁻¹ * y‖` defines a
 pseudometric space structure. -/
 @[to_additive]
@@ -181,13 +196,19 @@ class SeminormedGroup (E : Type*) extends Norm E, Group E, PseudoMetricSpace E w
   /-- The distance function is induced by the norm. -/
   dist_eq : ∀ x y, dist x y = ‖x⁻¹ * y‖ := by aesop
 
+-- see Note [lower instance priority]
+attribute [instance 200] SeminormedGroup.toGroup
+
 /-- A normed group is an additive group endowed with a norm for which `dist x y = ‖-x + y‖` defines
 a metric space structure. -/
 class NormedAddGroup (E : Type*) extends Norm E, AddGroup E, MetricSpace E where
   dist := fun x y => ‖-x + y‖
   /-- The distance function is induced by the norm. -/
   dist_eq : ∀ x y, dist x y = ‖-x + y‖ := by aesop
 
+-- see Note [lower instance priority]
+attribute [instance 200] NormedAddGroup.toAddGroup
+
 /-- A normed group is a group endowed with a norm for which `dist x y = ‖x⁻¹ * y‖` defines a metric
 space structure. -/
 @[to_additive]
@@ -196,6 +217,9 @@ class NormedGroup (E : Type*) extends Norm E, Group E, MetricSpace E where
   /-- The distance function is induced by the norm. -/
   dist_eq : ∀ x y, dist x y = ‖x⁻¹ * y‖ := by aesop
 
+-- see Note [lower instance priority]
+attribute [instance 200] NormedGroup.toGroup
+
 /-- A seminormed group is an additive group endowed with a norm for which `dist x y = ‖-x + y‖`
 defines a pseudometric space structure. -/
 class SeminormedAddCommGroup (E : Type*) extends Norm E, AddCommGroup E,
@@ -204,6 +228,9 @@ class SeminormedAddCommGroup (E : Type*) extends Norm E, AddCommGroup E,
   /-- The distance function is induced by the norm. -/
   dist_eq : ∀ x y, dist x y = ‖-x + y‖ := by aesop
 
+-- see Note [lower instance priority]
+attribute [instance 200] SeminormedAddCommGroup.toAddCommGroup
+
 /-- A seminormed group is a group endowed with a norm for which `dist x y = ‖x⁻¹ * y‖`
 defines a pseudometric space structure. -/
 @[to_additive]
@@ -212,13 +239,19 @@ class SeminormedCommGroup (E : Type*) extends Norm E, CommGroup E, PseudoMetricS
   /-- The distance function is induced by the norm. -/
   dist_eq : ∀ x y, dist x y = ‖x⁻¹ * y‖ := by aesop
 
+-- see Note [lower instance priority]
+attribute [instance 200] SeminormedCommGroup.toCommGroup
+
 /-- A normed group is an additive group endowed with a norm for which `dist x y = ‖-x + y‖` defines
 a metric space structure. -/
 class NormedAddCommGroup (E : Type*) extends Norm E, AddCommGroup E, MetricSpace E where
   dist := fun x y => ‖-x + y‖
   /-- The distance function is induced by the norm. -/
   dist_eq : ∀ x y, dist x y = ‖-x + y‖ := by aesop
 
+-- see Note [lower instance priority]
+attribute [instance 200] NormedAddCommGroup.toAddCommGroup
+
 /-- A normed group is a group endowed with a norm for which `dist x y = ‖x⁻¹ * y‖` defines a metric
 space structure. -/
 @[to_additive]
@@ -227,6 +260,9 @@ class NormedCommGroup (E : Type*) extends Norm E, CommGroup E, MetricSpace E whe
   /-- The distance function is induced by the norm. -/
   dist_eq : ∀ x y, dist x y = ‖x⁻¹ * y‖ := by aesop
 
+-- see Note [lower instance priority]
+attribute [instance 200] NormedCommGroup.toCommGroup
+
 -- See note [lower instance priority]
 @[to_additive]
 instance (priority := 100) NormedGroup.toSeminormedGroup [NormedGroup E] : SeminormedGroup E :=

Mathlib/Probability/Distributions/Gaussian/HasGaussianLaw/Basic.lean

@@ -218,12 +218,13 @@ lemma prodMk [Finite ι] (hX : HasGaussianLaw (fun ω ↦ (X · ω)) P) (i j : 
   letI := Fintype.ofFinite ι
   hX.map (.prod (.proj i) (.proj j))
 
-variable [Fintype ι]
-
-lemma toLp_pi (p : ℝ≥0∞) [Fact (1 ≤ p)] (hX : HasGaussianLaw (fun ω ↦ (X · ω)) P) :
+lemma toLp_pi [Finite ι] (p : ℝ≥0∞) [Fact (1 ≤ p)] (hX : HasGaussianLaw (fun ω ↦ (X · ω)) P) :
     HasGaussianLaw (fun ω ↦ toLp p (X · ω)) P :=
+  have := Fintype.ofFinite ι
   hX.map_equiv (PiLp.continuousLinearEquiv p ℝ E).symm
 
+variable [Fintype ι]
+
 lemma sum {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E] [MeasurableSpace E]
     [BorelSpace E] [SecondCountableTopology E]
     {X : ι → Ω → E} (hX : HasGaussianLaw (fun ω ↦ (X · ω)) P) :