fix: change compl precedence (#5586)

Co-authored-by: Yury G. Kudryashov <urkud@urkud.name>

Archive/Wiedijk100Theorems/BallotProblem.lean

@@ -261,9 +261,9 @@ theorem headI_mem_of_nonempty {α : Type _} [Inhabited α] : ∀ {l : List α} (
 #align ballot.head_mem_of_nonempty Ballot.headI_mem_of_nonempty
 
 theorem first_vote_neg (p q : ℕ) (h : 0 < p + q) :
-    condCount (countedSequence p q) ({l | l.headI = 1}ᶜ) = q / (p + q) := by
+    condCount (countedSequence p q) {l | l.headI = 1}ᶜ = q / (p + q) := by
   have := condCount_compl
-    ({l : List ℤ | l.headI = 1}ᶜ) (countedSequence_finite p q) (countedSequence_nonempty p q)
+    {l : List ℤ | l.headI = 1}ᶜ (countedSequence_finite p q) (countedSequence_nonempty p q)
   rw [compl_compl, first_vote_pos _ _ h] at this
   rw [(_ : (q / (p + q) : ENNReal) = 1 - p / (p + q)), ← this, ENNReal.add_sub_cancel_right]
   · simp only [Ne.def, ENNReal.div_eq_top, Nat.cast_eq_zero, add_eq_zero_iff, ENNReal.nat_ne_top,

Mathlib/Algebra/Algebra/Spectrum.lean

@@ -70,7 +70,7 @@ algebra `A`.
 
 The spectrum is simply the complement of the resolvent set.  -/
 def spectrum (a : A) : Set R :=
-  resolventSet R aᶜ
+  (resolventSet R a)ᶜ
 #align spectrum spectrum
 
 variable {R}

Mathlib/Algebra/BigOperators/Basic.lean

@@ -2026,7 +2026,7 @@ theorem prod_subtype_mul_prod_subtype {α β : Type _} [Fintype α] [CommMonoid
     ((∏ i : { x // p x }, f i) * ∏ i : { x // ¬p x }, f i) = ∏ i, f i := by
   classical
     let s := { x | p x }.toFinset
-    rw [← Finset.prod_subtype s, ← Finset.prod_subtype (sᶜ)]
+    rw [← Finset.prod_subtype s, ← Finset.prod_subtype sᶜ]
     · exact Finset.prod_mul_prod_compl _ _
     · simp
     · simp

Mathlib/Algebra/IndicatorFunction.lean

@@ -415,28 +415,28 @@ theorem mulIndicator_mul' (s : Set α) (f g : α → M) :
 
 @[to_additive (attr := simp)]
 theorem mulIndicator_compl_mul_self_apply (s : Set α) (f : α → M) (a : α) :
-    mulIndicator (sᶜ) f a * mulIndicator s f a = f a :=
+    mulIndicator sᶜ f a * mulIndicator s f a = f a :=
   by_cases (fun ha : a ∈ s => by simp [ha]) fun ha => by simp [ha]
 #align set.mul_indicator_compl_mul_self_apply Set.mulIndicator_compl_mul_self_apply
 #align set.indicator_compl_add_self_apply Set.indicator_compl_add_self_apply
 
 @[to_additive (attr := simp)]
 theorem mulIndicator_compl_mul_self (s : Set α) (f : α → M) :
-    mulIndicator (sᶜ) f * mulIndicator s f = f :=
+    mulIndicator sᶜ f * mulIndicator s f = f :=
   funext <| mulIndicator_compl_mul_self_apply s f
 #align set.mul_indicator_compl_mul_self Set.mulIndicator_compl_mul_self
 #align set.indicator_compl_add_self Set.indicator_compl_add_self
 
 @[to_additive (attr := simp)]
 theorem mulIndicator_self_mul_compl_apply (s : Set α) (f : α → M) (a : α) :
-    mulIndicator s f a * mulIndicator (sᶜ) f a = f a :=
+    mulIndicator s f a * mulIndicator sᶜ f a = f a :=
   by_cases (fun ha : a ∈ s => by simp [ha]) fun ha => by simp [ha]
 #align set.mul_indicator_self_mul_compl_apply Set.mulIndicator_self_mul_compl_apply
 #align set.indicator_self_add_compl_apply Set.indicator_self_add_compl_apply
 
 @[to_additive (attr := simp)]
 theorem mulIndicator_self_mul_compl (s : Set α) (f : α → M) :
-    mulIndicator s f * mulIndicator (sᶜ) f = f :=
+    mulIndicator s f * mulIndicator sᶜ f = f :=
   funext <| mulIndicator_self_mul_compl_apply s f
 #align set.mul_indicator_self_mul_compl Set.mulIndicator_self_mul_compl
 #align set.indicator_self_add_compl Set.indicator_self_add_compl
@@ -546,13 +546,13 @@ theorem mulIndicator_div' (s : Set α) (f g : α → G) :
 
 @[to_additive indicator_compl']
 theorem mulIndicator_compl (s : Set α) (f : α → G) :
-    mulIndicator (sᶜ) f = f * (mulIndicator s f)⁻¹ :=
+    mulIndicator sᶜ f = f * (mulIndicator s f)⁻¹ :=
   eq_mul_inv_of_mul_eq <| s.mulIndicator_compl_mul_self f
 #align set.mul_indicator_compl Set.mulIndicator_compl
 #align set.indicator_compl' Set.indicator_compl'
 
 theorem indicator_compl {G} [AddGroup G] (s : Set α) (f : α → G) :
-    indicator (sᶜ) f = f - indicator s f := by rw [sub_eq_add_neg, indicator_compl']
+    indicator sᶜ f = f - indicator s f := by rw [sub_eq_add_neg, indicator_compl']
 #align set.indicator_compl Set.indicator_compl
 
 @[to_additive indicator_diff']

Mathlib/Algebra/Ring/BooleanRing.lean

@@ -300,7 +300,7 @@ theorem ofBoolAlg_inf (a b : AsBoolAlg α) : ofBoolAlg (a ⊓ b) = ofBoolAlg a *
 #align of_boolalg_inf ofBoolAlg_inf
 
 @[simp]
-theorem ofBoolAlg_compl (a : AsBoolAlg α) : ofBoolAlg (aᶜ) = 1 + ofBoolAlg a :=
+theorem ofBoolAlg_compl (a : AsBoolAlg α) : ofBoolAlg aᶜ = 1 + ofBoolAlg a :=
   rfl
 #align of_boolalg_compl ofBoolAlg_compl
 

Mathlib/Algebra/Ring/Idempotents.lean

@@ -122,7 +122,7 @@ instance : HasCompl { p : R // IsIdempotentElem p } :=
   ⟨fun p => ⟨1 - p, p.prop.one_sub⟩⟩
 
 @[simp]
-theorem coe_compl (p : { p : R // IsIdempotentElem p }) : ↑(pᶜ) = (1 : R) - ↑p :=
+theorem coe_compl (p : { p : R // IsIdempotentElem p }) : ↑pᶜ = (1 : R) - ↑p :=
   rfl
 #align is_idempotent_elem.coe_compl IsIdempotentElem.coe_compl
 

Mathlib/Algebra/Star/Pointwise.lean

@@ -94,7 +94,7 @@ theorem iUnion_star {ι : Sort _} [Star α] (s : ι → Set α) : (⋃ i, s i)
 #align set.Union_star Set.iUnion_star
 
 @[simp]
-theorem compl_star [Star α] : (sᶜ)⋆ = s⋆ᶜ := preimage_compl
+theorem compl_star [Star α] : sᶜ⋆ = s⋆ᶜ := preimage_compl
 #align set.compl_star Set.compl_star
 
 @[simp]

Mathlib/Algebra/Support.lean

@@ -60,7 +60,7 @@ theorem nmem_mulSupport {f : α → M} {x : α} : x ∉ mulSupport f ↔ f x = 1
 #align function.nmem_support Function.nmem_support
 
 @[to_additive]
-theorem compl_mulSupport {f : α → M} : mulSupport fᶜ = { x | f x = 1 } :=
+theorem compl_mulSupport {f : α → M} : (mulSupport f)ᶜ = { x | f x = 1 } :=
   ext fun _ => nmem_mulSupport
 #align function.compl_mul_support Function.compl_mulSupport
 #align function.compl_support Function.compl_support

Mathlib/AlgebraicGeometry/PrimeSpectrum/Basic.lean

@@ -415,7 +415,7 @@ instance zariskiTopology : TopologicalSpace (PrimeSpectrum R) :=
 #align prime_spectrum.zariski_topology PrimeSpectrum.zariskiTopology
 
 theorem isOpen_iff (U : Set (PrimeSpectrum R)) : IsOpen U ↔ ∃ s, Uᶜ = zeroLocus s := by
-  simp only [@eq_comm _ (Uᶜ)] ; rfl
+  simp only [@eq_comm _ Uᶜ] ; rfl
 #align prime_spectrum.is_open_iff PrimeSpectrum.isOpen_iff
 
 theorem isClosed_iff_zeroLocus (Z : Set (PrimeSpectrum R)) : IsClosed Z ↔ ∃ s, Z = zeroLocus s := by
@@ -778,7 +778,7 @@ theorem isOpen_basicOpen {a : R} : IsOpen (basicOpen a : Set (PrimeSpectrum R))
 
 @[simp]
 theorem basicOpen_eq_zeroLocus_compl (r : R) :
-    (basicOpen r : Set (PrimeSpectrum R)) = zeroLocus {r}ᶜ :=
+    (basicOpen r : Set (PrimeSpectrum R)) = (zeroLocus {r})ᶜ :=
   Set.ext fun x => by simp only [SetLike.mem_coe, mem_basicOpen, Set.mem_compl_iff, mem_zeroLocus,
     Set.singleton_subset_iff]
 #align prime_spectrum.basic_open_eq_zero_locus_compl PrimeSpectrum.basicOpen_eq_zeroLocus_compl
@@ -853,7 +853,7 @@ theorem isCompact_basicOpen (f : R) : IsCompact (basicOpen f : Set (PrimeSpectru
     rcases Submodule.exists_finset_of_mem_iSup I hn with ⟨s, hs⟩
     use s
     -- Using simp_rw here, because `hI` and `zero_locus_supr` need to be applied underneath binders
-    simp_rw [basicOpen_eq_zeroLocus_compl f, Set.inter_comm (zeroLocus {f}ᶜ), ← Set.diff_eq,
+    simp_rw [basicOpen_eq_zeroLocus_compl f, Set.inter_comm (zeroLocus {f})ᶜ, ← Set.diff_eq,
       Set.diff_eq_empty]
     rw [show (Set.iInter fun i => Set.iInter fun (_ : i ∈ s) => Z i) =
       Set.iInter fun i => Set.iInter fun (_ : i ∈ s) => zeroLocus (I i) from congr_arg _

Mathlib/AlgebraicGeometry/PrimeSpectrum/IsOpenComapC.lean

@@ -55,7 +55,7 @@ theorem comap_C_mem_imageOfDf {I : PrimeSpectrum R[X]}
 /-- The open set `imageOfDf f` coincides with the image of `basicOpen f` under the
 morphism `C⁺ : Spec R[x] → Spec R`. -/
 theorem imageOfDf_eq_comap_C_compl_zeroLocus :
-    imageOfDf f = PrimeSpectrum.comap (C : R →+* R[X]) '' zeroLocus {f}ᶜ := by
+    imageOfDf f = PrimeSpectrum.comap (C : R →+* R[X]) '' (zeroLocus {f})ᶜ := by
   ext x
   refine' ⟨fun hx => ⟨⟨map C x.asIdeal, isPrime_map_C_of_isPrime x.IsPrime⟩, ⟨_, _⟩⟩, _⟩
   · rw [mem_compl_iff, mem_zeroLocus, singleton_subset_iff]

Mathlib/AlgebraicGeometry/ProjectiveSpectrum/Topology.lean

@@ -348,7 +348,7 @@ set_option linter.uppercaseLean3 false in
 #align projective_spectrum.Top ProjectiveSpectrum.top
 
 theorem isOpen_iff (U : Set (ProjectiveSpectrum 𝒜)) : IsOpen U ↔ ∃ s, Uᶜ = zeroLocus 𝒜 s := by
-  simp only [@eq_comm _ (Uᶜ)] ; rfl
+  simp only [@eq_comm _ Uᶜ] ; rfl
 #align projective_spectrum.is_open_iff ProjectiveSpectrum.isOpen_iff
 
 theorem isClosed_iff_zeroLocus (Z : Set (ProjectiveSpectrum 𝒜)) :
@@ -405,7 +405,7 @@ theorem isOpen_basicOpen {a : A} : IsOpen (basicOpen 𝒜 a : Set (ProjectiveSpe
 
 @[simp]
 theorem basicOpen_eq_zeroLocus_compl (r : A) :
-    (basicOpen 𝒜 r : Set (ProjectiveSpectrum 𝒜)) = zeroLocus 𝒜 {r}ᶜ :=
+    (basicOpen 𝒜 r : Set (ProjectiveSpectrum 𝒜)) = (zeroLocus 𝒜 {r})ᶜ :=
   Set.ext fun x => by simp only [Set.mem_compl_iff, mem_zeroLocus, Set.singleton_subset_iff] ; rfl
 #align projective_spectrum.basic_open_eq_zero_locus_compl ProjectiveSpectrum.basicOpen_eq_zeroLocus_compl
 

Mathlib/Analysis/Calculus/ContDiff.lean

@@ -1688,7 +1688,7 @@ theorem contDiffAt_inv {x : 𝕜'} (hx : x ≠ 0) {n} : ContDiffAt 𝕜 n Inv.in
   simpa only [Ring.inverse_eq_inv'] using contDiffAt_ring_inverse 𝕜 (Units.mk0 x hx)
 #align cont_diff_at_inv contDiffAt_inv
 
-theorem contDiffOn_inv {n} : ContDiffOn 𝕜 n (Inv.inv : 𝕜' → 𝕜') ({0}ᶜ) := fun _ hx =>
+theorem contDiffOn_inv {n} : ContDiffOn 𝕜 n (Inv.inv : 𝕜' → 𝕜') {0}ᶜ := fun _ hx =>
   (contDiffAt_inv 𝕜 hx).contDiffWithinAt
 #align cont_diff_on_inv contDiffOn_inv
 

Mathlib/Analysis/Calculus/Deriv/Slope.lean

@@ -59,17 +59,17 @@ variable {L L₁ L₂ : Filter 𝕜}
 definition with a limit. In this version we have to take the limit along the subset `-{x}`,
 because for `y=x` the slope equals zero due to the convention `0⁻¹=0`. -/
 theorem hasDerivAtFilter_iff_tendsto_slope {x : 𝕜} {L : Filter 𝕜} :
-    HasDerivAtFilter f f' x L ↔ Tendsto (slope f x) (L ⊓ 𝓟 ({x}ᶜ)) (𝓝 f') :=
+    HasDerivAtFilter f f' x L ↔ Tendsto (slope f x) (L ⊓ 𝓟 {x}ᶜ) (𝓝 f') :=
   calc HasDerivAtFilter f f' x L
     ↔ Tendsto (fun y ↦ slope f x y - (y - x)⁻¹ • (y - x) • f') L (𝓝 0) := by
         simp only [hasDerivAtFilter_iff_tendsto, ← norm_inv, ← norm_smul,
           ← tendsto_zero_iff_norm_tendsto_zero, slope_def_module, smul_sub]
-  _ ↔ Tendsto (fun y ↦ slope f x y - (y - x)⁻¹ • (y - x) • f') (L ⊓ 𝓟 ({x}ᶜ)) (𝓝 0) :=
+  _ ↔ Tendsto (fun y ↦ slope f x y - (y - x)⁻¹ • (y - x) • f') (L ⊓ 𝓟 {x}ᶜ) (𝓝 0) :=
         .symm <| tendsto_inf_principal_nhds_iff_of_forall_eq <| by simp
-  _ ↔ Tendsto (fun y ↦ slope f x y - f') (L ⊓ 𝓟 ({x}ᶜ)) (𝓝 0) := tendsto_congr' <| by
+  _ ↔ Tendsto (fun y ↦ slope f x y - f') (L ⊓ 𝓟 {x}ᶜ) (𝓝 0) := tendsto_congr' <| by
         refine (EqOn.eventuallyEq fun y hy ↦ ?_).filter_mono inf_le_right
         rw [inv_smul_smul₀ (sub_ne_zero.2 hy) f']
-  _ ↔ Tendsto (slope f x) (L ⊓ 𝓟 ({x}ᶜ)) (𝓝 f') :=
+  _ ↔ Tendsto (slope f x) (L ⊓ 𝓟 {x}ᶜ) (𝓝 f') :=
         by rw [← nhds_translation_sub f', tendsto_comap_iff]; rfl
 #align has_deriv_at_filter_iff_tendsto_slope hasDerivAtFilter_iff_tendsto_slope
 

Mathlib/Analysis/Calculus/Dslope.lean

@@ -55,7 +55,7 @@ theorem ContinuousLinearMap.dslope_comp {F : Type _} [NormedAddCommGroup F] [Nor
   · simpa only [dslope_of_ne _ hne] using f.toLinearMap.slope_comp g a b
 #align continuous_linear_map.dslope_comp ContinuousLinearMap.dslope_comp
 
-theorem eqOn_dslope_slope (f : 𝕜 → E) (a : 𝕜) : EqOn (dslope f a) (slope f a) ({a}ᶜ) := fun _ =>
+theorem eqOn_dslope_slope (f : 𝕜 → E) (a : 𝕜) : EqOn (dslope f a) (slope f a) {a}ᶜ := fun _ =>
   dslope_of_ne f
 #align eq_on_dslope_slope eqOn_dslope_slope
 
@@ -78,7 +78,7 @@ theorem dslope_sub_smul_of_ne (f : 𝕜 → E) (h : b ≠ a) :
 #align dslope_sub_smul_of_ne dslope_sub_smul_of_ne
 
 theorem eqOn_dslope_sub_smul (f : 𝕜 → E) (a : 𝕜) :
-    EqOn (dslope (fun x => (x - a) • f x) a) f ({a}ᶜ) := fun _ => dslope_sub_smul_of_ne f
+    EqOn (dslope (fun x => (x - a) • f x) a) f {a}ᶜ := fun _ => dslope_sub_smul_of_ne f
 #align eq_on_dslope_sub_smul eqOn_dslope_sub_smul
 
 theorem dslope_sub_smul [DecidableEq 𝕜] (f : 𝕜 → E) (a : 𝕜) :

Mathlib/Analysis/Convex/Integral.lean

@@ -237,13 +237,13 @@ theorem ConcaveOn.le_map_integral [IsProbabilityMeasure μ] (hg : ConcaveOn ℝ
 values of `f` over `t` and `tᶜ` are different. -/
 theorem ae_eq_const_or_exists_average_ne_compl [IsFiniteMeasure μ] (hfi : Integrable f μ) :
     f =ᵐ[μ] const α (⨍ x, f x ∂μ) ∨
-      ∃ t, MeasurableSet t ∧ μ t ≠ 0 ∧ μ (tᶜ) ≠ 0 ∧ (⨍ x in t, f x ∂μ) ≠ ⨍ x in tᶜ, f x ∂μ := by
+      ∃ t, MeasurableSet t ∧ μ t ≠ 0 ∧ μ tᶜ ≠ 0 ∧ (⨍ x in t, f x ∂μ) ≠ ⨍ x in tᶜ, f x ∂μ := by
   refine' or_iff_not_imp_right.mpr fun H => _; push_neg at H
   refine' hfi.ae_eq_of_forall_set_integral_eq _ _ (integrable_const _) fun t ht ht' => _; clear ht'
   simp only [const_apply, set_integral_const]
   by_cases h₀ : μ t = 0
   · rw [restrict_eq_zero.2 h₀, integral_zero_measure, h₀, ENNReal.zero_toReal, zero_smul]
-  by_cases h₀' : μ (tᶜ) = 0
+  by_cases h₀' : μ tᶜ = 0
   · rw [← ae_eq_univ] at h₀'
     rw [restrict_congr_set h₀', restrict_univ, measure_congr h₀', measure_smul_average]
   have := average_mem_openSegment_compl_self ht.nullMeasurableSet h₀ h₀' hfi
@@ -258,7 +258,7 @@ theorem Convex.average_mem_interior_of_set [IsFiniteMeasure μ] (hs : Convex ℝ
     (hfs : ∀ᵐ x ∂μ, f x ∈ s) (hfi : Integrable f μ) (ht : (⨍ x in t, f x ∂μ) ∈ interior s) :
     (⨍ x, f x ∂μ) ∈ interior s := by
   rw [← measure_toMeasurable] at h0 ; rw [← restrict_toMeasurable (measure_ne_top μ t)] at ht
-  by_cases h0' : μ (toMeasurable μ tᶜ) = 0
+  by_cases h0' : μ (toMeasurable μ t)ᶜ = 0
   · rw [← ae_eq_univ] at h0'
     rwa [restrict_congr_set h0', restrict_univ] at ht
   exact

Mathlib/Analysis/Convex/StoneSeparation.lean

@@ -84,7 +84,7 @@ theorem not_disjoint_segment_convexHull_triple {p q u v x y z : E} (hz : z ∈ s
 
 /-- **Stone's Separation Theorem** -/
 theorem exists_convex_convex_compl_subset (hs : Convex 𝕜 s) (ht : Convex 𝕜 t) (hst : Disjoint s t) :
-    ∃ C : Set E, Convex 𝕜 C ∧ Convex 𝕜 (Cᶜ) ∧ s ⊆ C ∧ t ⊆ Cᶜ := by
+    ∃ C : Set E, Convex 𝕜 C ∧ Convex 𝕜 Cᶜ ∧ s ⊆ C ∧ t ⊆ Cᶜ := by
   let S : Set (Set E) := { C | Convex 𝕜 C ∧ Disjoint C t }
   obtain ⟨C, hC, hsC, hCmax⟩ :=
     zorn_subset_nonempty S

Mathlib/Analysis/NormedSpace/FiniteDimension.lean

@@ -621,7 +621,7 @@ instance (priority := 900) FiniteDimensional.proper_real (E : Type u) [NormedAdd
 `IsCompact.exists_mem_frontier_infDist_compl_eq_dist`. -/
 theorem exists_mem_frontier_infDist_compl_eq_dist {E : Type _} [NormedAddCommGroup E]
     [NormedSpace ℝ E] [FiniteDimensional ℝ E] {x : E} {s : Set E} (hx : x ∈ s) (hs : s ≠ univ) :
-    ∃ y ∈ frontier s, Metric.infDist x (sᶜ) = dist x y := by
+    ∃ y ∈ frontier s, Metric.infDist x sᶜ = dist x y := by
   rcases Metric.exists_mem_closure_infDist_eq_dist (nonempty_compl.2 hs) x with ⟨y, hys, hyd⟩
   rw [closure_compl] at hys
   refine'
@@ -638,7 +638,7 @@ theorem exists_mem_frontier_infDist_compl_eq_dist {E : Type _} [NormedAddCommGro
 nonrec theorem IsCompact.exists_mem_frontier_infDist_compl_eq_dist {E : Type _}
     [NormedAddCommGroup E] [NormedSpace ℝ E] [Nontrivial E] {x : E} {K : Set E} (hK : IsCompact K)
     (hx : x ∈ K) :
-    ∃ y ∈ frontier K, Metric.infDist x (Kᶜ) = dist x y := by
+    ∃ y ∈ frontier K, Metric.infDist x Kᶜ = dist x y := by
   obtain hx' | hx' : x ∈ interior K ∪ frontier K := by
     rw [← closure_eq_interior_union_frontier]
     exact subset_closure hx

Mathlib/Analysis/NormedSpace/MStructure.lean

@@ -177,7 +177,7 @@ instance Subtype.hasCompl : HasCompl { f : M // IsLprojection X f } :=
   ⟨fun P => ⟨1 - P, P.prop.Lcomplement⟩⟩
 
 @[simp]
-theorem coe_compl (P : { P : M // IsLprojection X P }) : ↑(Pᶜ) = (1 : M) - ↑P :=
+theorem coe_compl (P : { P : M // IsLprojection X P }) : ↑Pᶜ = (1 : M) - ↑P :=
   rfl
 #align is_Lprojection.coe_compl IsLprojection.coe_compl
 
@@ -260,22 +260,22 @@ theorem coe_top [FaithfulSMul M X] :
   rfl
 #align is_Lprojection.coe_top IsLprojection.coe_top
 
-theorem compl_mul {P : { P : M // IsLprojection X P }} {Q : M} : ↑(Pᶜ) * Q = Q - ↑P * Q := by
+theorem compl_mul {P : { P : M // IsLprojection X P }} {Q : M} : ↑Pᶜ * Q = Q - ↑P * Q := by
   rw [coe_compl, sub_mul, one_mul]
 #align is_Lprojection.compl_mul IsLprojection.compl_mul
 
-theorem mul_compl_self {P : { P : M // IsLprojection X P }} : (↑P : M) * ↑(Pᶜ) = 0 := by
+theorem mul_compl_self {P : { P : M // IsLprojection X P }} : (↑P : M) * ↑Pᶜ = 0 := by
   rw [coe_compl, mul_sub, mul_one, P.prop.proj.eq, sub_self]
 #align is_Lprojection.mul_compl_self IsLprojection.mul_compl_self
 
 theorem distrib_lattice_lemma [FaithfulSMul M X] {P Q R : { P : M // IsLprojection X P }} :
-    ((↑P : M) + ↑(Pᶜ) * R) * (↑P + ↑Q * ↑R * ↑(Pᶜ)) = ↑P + ↑Q * ↑R * ↑(Pᶜ) := by
-  rw [add_mul, mul_add, mul_add, (mul_assoc _ (R : M) (↑Q * ↑R * ↑(Pᶜ))),
+    ((↑P : M) + ↑Pᶜ * R) * (↑P + ↑Q * ↑R * ↑Pᶜ) = ↑P + ↑Q * ↑R * ↑Pᶜ := by
+  rw [add_mul, mul_add, mul_add, (mul_assoc _ (R : M) (↑Q * ↑R * ↑Pᶜ)),
     ← mul_assoc (R : M) (↑Q * ↑R) _, ← coe_inf Q, (Pᶜ.prop.commute R.prop).eq,
-    ((Q ⊓ R).prop.commute (Pᶜ).prop).eq, (R.prop.commute (Q ⊓ R).prop).eq, coe_inf Q,
+    ((Q ⊓ R).prop.commute Pᶜ.prop).eq, (R.prop.commute (Q ⊓ R).prop).eq, coe_inf Q,
     mul_assoc (Q : M), ←mul_assoc, mul_assoc (R : M), (Pᶜ.prop.commute P.prop).eq, mul_compl_self,
     MulZeroClass.zero_mul, MulZeroClass.mul_zero, zero_add, add_zero, ← mul_assoc, P.prop.proj.eq,
-    R.prop.proj.eq, ←coe_inf Q, mul_assoc, ((Q ⊓ R).prop.commute (Pᶜ).prop).eq, ← mul_assoc,
+    R.prop.proj.eq, ←coe_inf Q, mul_assoc, ((Q ⊓ R).prop.commute Pᶜ.prop).eq, ← mul_assoc,
     Pᶜ.prop.proj.eq]
 #align is_Lprojection.distrib_lattice_lemma IsLprojection.distrib_lattice_lemma
 
@@ -307,15 +307,15 @@ instance [FaithfulSMul M X] : Lattice { P : M // IsLprojection X P } where
 instance Subtype.distribLattice [FaithfulSMul M X] :
     DistribLattice { P : M // IsLprojection X P } where
   le_sup_inf P Q R := by
-    have e₁ : ↑((P ⊔ Q) ⊓ (P ⊔ R)) = ↑P + ↑Q * (R : M) * ↑(Pᶜ) := by
+    have e₁ : ↑((P ⊔ Q) ⊓ (P ⊔ R)) = ↑P + ↑Q * (R : M) * ↑Pᶜ := by
       rw [coe_inf, coe_sup, coe_sup, ← add_sub, ← add_sub, ← compl_mul, ← compl_mul, add_mul,
-        mul_add, ((Pᶜ).prop.commute Q.prop).eq, mul_add, ← mul_assoc, mul_assoc (Q: M),
-        ((Pᶜ).prop.commute P.prop).eq, mul_compl_self, MulZeroClass.zero_mul, MulZeroClass.mul_zero,
-        zero_add, add_zero, ← mul_assoc, mul_assoc (Q : M), P.prop.proj.eq, (Pᶜ).prop.proj.eq,
-        mul_assoc, ((Pᶜ).prop.commute R.prop).eq, ← mul_assoc]
-    have e₂ : ↑((P ⊔ Q) ⊓ (P ⊔ R)) * ↑(P ⊔ Q ⊓ R) = (P : M) + ↑Q * ↑R * ↑(Pᶜ) := by
+        mul_add, (Pᶜ.prop.commute Q.prop).eq, mul_add, ← mul_assoc, mul_assoc (Q: M),
+        (Pᶜ.prop.commute P.prop).eq, mul_compl_self, MulZeroClass.zero_mul, MulZeroClass.mul_zero,
+        zero_add, add_zero, ← mul_assoc, mul_assoc (Q : M), P.prop.proj.eq, Pᶜ.prop.proj.eq,
+        mul_assoc, (Pᶜ.prop.commute R.prop).eq, ← mul_assoc]
+    have e₂ : ↑((P ⊔ Q) ⊓ (P ⊔ R)) * ↑(P ⊔ Q ⊓ R) = (P : M) + ↑Q * ↑R * ↑Pᶜ := by
       rw [coe_inf, coe_sup, coe_sup, coe_sup, ← add_sub, ← add_sub, ← add_sub, ← compl_mul, ←
-        compl_mul, ← compl_mul, ((Pᶜ).prop.commute (Q ⊓ R).prop).eq, coe_inf, mul_assoc,
+        compl_mul, ← compl_mul, (Pᶜ.prop.commute (Q ⊓ R).prop).eq, coe_inf, mul_assoc,
         distrib_lattice_lemma, (Q.prop.commute R.prop).eq, distrib_lattice_lemma]
     rw [le_def, e₁, coe_inf, e₂]
 

Mathlib/Analysis/NormedSpace/Multilinear.lean

@@ -270,7 +270,7 @@ theorem restr_norm_le {k n : ℕ} (f : (MultilinearMap 𝕜 (fun _ : Fin n => G)
   rw [mul_right_comm, mul_assoc]
   convert H _ using 2
   simp only [apply_dite norm, Fintype.prod_dite, prod_const ‖z‖, Finset.card_univ,
-    Fintype.card_of_subtype (sᶜ) fun _ => mem_compl, card_compl, Fintype.card_fin, hk, mk_coe, ←
+    Fintype.card_of_subtype sᶜ fun _ => mem_compl, card_compl, Fintype.card_fin, hk, mk_coe, ←
     (s.orderIsoOfFin hk).symm.bijective.prod_comp fun x => ‖v x‖]
   convert rfl
 #align multilinear_map.restr_norm_le MultilinearMap.restr_norm_le