chore: fix whitespace

Author: harahu

Mathlib/Condensed/Basic.lean

@@ -49,10 +49,10 @@ instance {C : Type w} [Category.{v} C] : Category (Condensed.{u} C) :=
   show Category (Sheaf _ _) from inferInstance
 
 /--
-Condensed sets (types) with the appropriate universe levels, i.e. `Type (u+1)`-valued
+Condensed sets (types) with the appropriate universe levels, i.e. `Type (u + 1)`-valued
 sheaves on `CompHaus.{u}`.
 -/
-abbrev CondensedSet := Condensed.{u} (Type (u+1))
+abbrev CondensedSet := Condensed.{u} (Type (u + 1))
 
 namespace Condensed
 

Mathlib/Condensed/Functors.lean

@@ -34,7 +34,7 @@ section Universes
 
 /-- Increase the size of the target category of condensed sets. -/
 def Condensed.ulift : Condensed.{u} (Type u) ⥤ CondensedSet.{u} :=
-  sheafCompose (coherentTopology CompHaus) uliftFunctor.{u+1, u}
+  sheafCompose (coherentTopology CompHaus) uliftFunctor.{u + 1, u}
 
 instance : Condensed.ulift.Full := show (sheafCompose _ _).Full from inferInstance
 

Mathlib/Condensed/Light/TopCatAdjunction.lean

@@ -34,7 +34,7 @@ variable (X : LightCondSet.{u})
 private def coinducingCoprod :
     (Σ (i : (S : LightProfinite.{u}) × X.val.obj ⟨S⟩), i.fst) →
       X.val.obj ⟨LightProfinite.of PUnit⟩ :=
-  fun ⟨⟨_, i⟩, s⟩ ↦ X.val.map ((of PUnit.{u+1}).const s).op i
+  fun ⟨⟨_, i⟩, s⟩ ↦ X.val.map ((of PUnit.{u + 1}).const s).op i
 
 /-- Let `X` be a light condensed set. We define a topology on `X(*)` as the quotient topology of
 all the maps from light profinite sets `S` to `X(*)`, corresponding to elements of `X(S)`.
@@ -66,8 +66,8 @@ def toTopCatMap : X.toTopCat ⟶ Y.toTopCat :=
       apply continuous_sigma
       intro ⟨S, x⟩
       simp only [Function.comp_apply, coinducingCoprod]
-      rw [show (fun (a : S) ↦ f.val.app ⟨of PUnit⟩ (X.val.map ((of PUnit.{u+1}).const a).op x)) = _
-        from funext fun a ↦ NatTrans.naturality_apply f.val ((of PUnit.{u+1}).const a).op x]
+      rw [show (fun (a : S) ↦ f.val.app ⟨of PUnit⟩ (X.val.map ((of PUnit.{u + 1}).const a).op x)) = _
+        from funext fun a ↦ NatTrans.naturality_apply f.val ((of PUnit.{u + 1}).const a).op x]
       exact continuous_coinducingCoprod _ _ }
 
 /-- The functor `LightCondSet ⥤ TopCat` -/
@@ -100,7 +100,7 @@ lemma topCatAdjunctionCounit_bijective (X : TopCat.{u}) :
 noncomputable def topCatAdjunctionUnit (X : LightCondSet.{u}) : X ⟶ X.toTopCat.toLightCondSet where
   val := {
     app := fun S x ↦ {
-      toFun := fun s ↦ X.val.map ((of PUnit.{u+1}).const s).op x
+      toFun := fun s ↦ X.val.map ((of PUnit.{u + 1}).const s).op x
       continuous_toFun := by
         suffices ∀ (i : (T : LightProfinite.{u}) × X.val.obj ⟨T⟩),
           Continuous (fun (a : i.fst) ↦ X.coinducingCoprod ⟨i, a⟩) from this ⟨_, _⟩

Mathlib/Condensed/TopComparison.lean

@@ -19,7 +19,7 @@ nice properties, like preserving pullbacks and finite coproducts, then this Yone
 satisfies the sheaf condition for the regular and extensive topologies respectively.
 
 We apply this API to `CompHaus` and define the functor
-`topCatToCondensedSet : TopCat.{u+1} ⥤ CondensedSet.{u}`.
+`topCatToCondensedSet : TopCat.{u + 1} ⥤ CondensedSet.{u}`.
 
 -/
 
@@ -131,14 +131,14 @@ noncomputable def topCatToSheafCompHausLike :
 end
 
 /--
-Associate to a `(u+1)`-small topological space the corresponding condensed set, given by
+Associate to a `(u + 1)`-small topological space the corresponding condensed set, given by
 `yonedaPresheaf`.
 -/
 noncomputable abbrev TopCat.toCondensedSet (X : TopCat.{u + 1}) : CondensedSet.{u} :=
-  toSheafCompHausLike.{u+1} _ X (fun _ _ _ ↦ ((CompHaus.effectiveEpi_tfae _).out 0 2).mp)
+  toSheafCompHausLike.{u + 1} _ X (fun _ _ _ ↦ ((CompHaus.effectiveEpi_tfae _).out 0 2).mp)
 
 /--
-`TopCat.toCondensedSet` yields a functor from `TopCat.{u+1}` to `CondensedSet.{u}`.
+`TopCat.toCondensedSet` yields a functor from `TopCat.{u + 1}` to `CondensedSet.{u}`.
 -/
-noncomputable abbrev topCatToCondensedSet : TopCat.{u+1} ⥤ CondensedSet.{u} :=
-  topCatToSheafCompHausLike.{u+1} _ (fun _ _ _ ↦ ((CompHaus.effectiveEpi_tfae _).out 0 2).mp)
+noncomputable abbrev topCatToCondensedSet : TopCat.{u + 1} ⥤ CondensedSet.{u} :=
+  topCatToSheafCompHausLike.{u + 1} _ (fun _ _ _ ↦ ((CompHaus.effectiveEpi_tfae _).out 0 2).mp)

Mathlib/Deprecated/Sort.lean

@@ -47,16 +47,16 @@ theorem Sorted.tail (h : Sorted r l) : Sorted r l.tail := Pairwise.tail h
 
 @[deprecated rel_of_pairwise_cons (since := "2025-10-11")]
 theorem rel_of_sorted_cons (p : Sorted r (a :: l))
-  {a' : α} : a' ∈ l → r a a':= rel_of_pairwise_cons p
+  {a' : α} : a' ∈ l → r a a' := rel_of_pairwise_cons p
 
 @[deprecated pairwise_cons (since := "2025-10-11")]
 theorem sorted_cons : Sorted r (a :: l) ↔ (∀ a' ∈ l, r a a') ∧ Sorted r l := pairwise_cons
 
 @[deprecated Pairwise.filter (since := "2025-10-11")]
-theorem Sorted.filter (p : α → Bool) : Sorted r l →  Sorted r (filter p l) := Pairwise.filter p
+theorem Sorted.filter (p : α → Bool) : Sorted r l → Sorted r (filter p l) := Pairwise.filter p
 
 @[deprecated pairwise_singleton (since := "2025-10-11")]
-theorem sorted_singleton (r) (a : α) :  Sorted r [a] := pairwise_singleton r a
+theorem sorted_singleton (r) (a : α) : Sorted r [a] := pairwise_singleton r a
 
 @[deprecated Pairwise.rel_of_mem_take_of_mem_drop (since := "2025-10-11")]
 theorem Sorted.rel_of_mem_take_of_mem_drop {x y i} (h : Sorted r l)

Mathlib/Dynamics/Ergodic/Conservative.lean

@@ -161,8 +161,8 @@ theorem ae_mem_imp_frequently_image_mem (hf : Conservative f μ) (hs : NullMeasu
     ∀ᵐ x ∂μ, x ∈ s → ∃ᶠ n in atTop, f^[n] x ∈ s := by
   simp only [frequently_atTop, @forall_swap (_ ∈ s), ae_all_iff]
   intro n
-  filter_upwards [
-    measure_eq_zero_iff_ae_notMem.1 (hf.measure_mem_forall_ge_image_notMem_eq_zero hs n)]
+  filter_upwards
+    [measure_eq_zero_iff_ae_notMem.1 (hf.measure_mem_forall_ge_image_notMem_eq_zero hs n)]
   simp
 
 theorem inter_frequently_image_mem_ae_eq (hf : Conservative f μ) (hs : NullMeasurableSet s μ) :

Mathlib/Dynamics/Ergodic/MeasurePreserving.lean

@@ -197,7 +197,7 @@ lemma measure_symmDiff_preimage_iterate_le
   | zero => simp
   | succ n ih =>
     simp only [add_smul, one_smul]
-    grw [← ih, measure_symmDiff_le s (f^[n] ⁻¹' s) (f^[n+1] ⁻¹' s)]
+    grw [← ih, measure_symmDiff_le s (f^[n] ⁻¹' s) (f^[n + 1] ⁻¹' s)]
     replace hs : NullMeasurableSet (s ∆ (f ⁻¹' s)) μ :=
       hs.symmDiff <| hs.preimage hf.quasiMeasurePreserving
     rw [iterate_succ', preimage_comp, ← preimage_symmDiff, (hf.iterate n).measure_preimage hs]

Mathlib/Dynamics/PeriodicPts/Defs.lean

@@ -477,7 +477,7 @@ theorem periodicOrbit_apply_eq (hx : x ∈ periodicPts f) :
   periodicOrbit_apply_iterate_eq hx 1
 
 theorem periodicOrbit_chain (r : α → α → Prop) {f : α → α} {x : α} :
-    (periodicOrbit f x).Chain r ↔ ∀ n < minimalPeriod f x, r (f^[n] x) (f^[n+1] x) := by
+    (periodicOrbit f x).Chain r ↔ ∀ n < minimalPeriod f x, r (f^[n] x) (f^[n + 1] x) := by
   by_cases hx : x ∈ periodicPts f
   · have hx' := minimalPeriod_pos_of_mem_periodicPts hx
     have hM := Nat.sub_add_cancel (succ_le_iff.2 hx')
@@ -495,7 +495,7 @@ theorem periodicOrbit_chain (r : α → α → Prop) {f : α → α} {x : α} :
     simp
 
 theorem periodicOrbit_chain' (r : α → α → Prop) {f : α → α} {x : α} (hx : x ∈ periodicPts f) :
-    (periodicOrbit f x).Chain r ↔ ∀ n, r (f^[n] x) (f^[n+1] x) := by
+    (periodicOrbit f x).Chain r ↔ ∀ n, r (f^[n] x) (f^[n + 1] x) := by
   rw [periodicOrbit_chain r]
   refine ⟨fun H n => ?_, fun H n _ => H n⟩
   rw [iterate_succ_apply, ← iterate_mod_minimalPeriod_eq, ← iterate_mod_minimalPeriod_eq (n := n),

Mathlib/Dynamics/PeriodicPts/Lemmas.lean

@@ -69,8 +69,7 @@ theorem Commute.minimalPeriod_of_comp_eq_mul_of_coprime {g : α → α} (h : Com
     (hco : Coprime (minimalPeriod f x) (minimalPeriod g x)) :
     minimalPeriod (f ∘ g) x = minimalPeriod f x * minimalPeriod g x := by
   apply h.minimalPeriod_of_comp_dvd_mul.antisymm
-  suffices
-    ∀ {f g : α → α},
+  suffices ∀ {f g : α → α},
       Commute f g →
         Coprime (minimalPeriod f x) (minimalPeriod g x) →
           minimalPeriod f x ∣ minimalPeriod (f ∘ g) x from

Mathlib/Probability/ConditionalProbability.lean

@@ -18,18 +18,18 @@ the inverse of the measure of `s`: `cond μ s = (μ s)⁻¹ • μ.restrict s`.
 ensures that this is a probability measure (when `μ` is a finite measure).
 
 From this definition, we derive the "axiomatic" definition of conditional probability
-based on application: for any `s t : Set Ω`, we have `μ[t|s] = (μ s)⁻¹ * μ (s ∩ t)`.
+based on application: for any `s t : Set Ω`, we have `μ[t | s] = (μ s)⁻¹ * μ (s ∩ t)`.
 
 ## Main Statements
 
 * `cond_cond_eq_cond_inter`: conditioning on one set and then another is equivalent
   to conditioning on their intersection.
-* `cond_eq_inv_mul_cond_mul`: Bayes' Theorem, `μ[t|s] = (μ s)⁻¹ * μ[s|t] * (μ t)`.
+* `cond_eq_inv_mul_cond_mul`: Bayes' Theorem, `μ[t | s] = (μ s)⁻¹ * μ[s | t] * (μ t)`.
 
 ## Notation
 
 This file uses the notation `μ[|s]` the measure of `μ` conditioned on `s`,
-and `μ[t|s]` for the probability of `t` given `s` under `μ` (equivalent to the
+and `μ[t | s]` for the probability of `t` given `s` under `μ` (equivalent to the
 application `μ[|s] t`).
 
 These notations are contained in the scope `ProbabilityTheory`.
@@ -99,7 +99,7 @@ meta def condUnexpander : Lean.PrettyPrinter.Unexpander
 #guard_msgs in
 #check μ[|s]
 
-/-- Delaborator for `μ[t|s]` notation. -/
+/-- Delaborator for `μ[t | s]` notation. -/
 @[app_delab DFunLike.coe]
 meta def delabCondApplied : Delab :=
   whenNotPPOption getPPExplicit <| whenPPOption getPPNotation <| withOverApp 6 do
@@ -212,17 +212,17 @@ lemma cond_eq_zero_of_meas_eq_zero (hμs : μ s = 0) : μ[|s] = 0 := by simp [h
 
 /-- The axiomatic definition of conditional probability derived from a measure-theoretic one. -/
 theorem cond_apply (hms : MeasurableSet s) (μ : Measure Ω) (t : Set Ω) :
-    μ[t|s] = (μ s)⁻¹ * μ (s ∩ t) := by
+    μ[t | s] = (μ s)⁻¹ * μ (s ∩ t) := by
   rw [cond, Measure.smul_apply, Measure.restrict_apply' hms, Set.inter_comm, smul_eq_mul]
 
-theorem cond_apply' (ht : MeasurableSet t) (μ : Measure Ω) : μ[t|s] = (μ s)⁻¹ * μ (s ∩ t) := by
+theorem cond_apply' (ht : MeasurableSet t) (μ : Measure Ω) : μ[t | s] = (μ s)⁻¹ * μ (s ∩ t) := by
   rw [cond, Measure.smul_apply, Measure.restrict_apply ht, Set.inter_comm, smul_eq_mul]
 
-@[simp] lemma cond_apply_self (hs₀ : μ s ≠ 0) (hs : μ s ≠ ∞) : μ[s|s] = 1 := by
+@[simp] lemma cond_apply_self (hs₀ : μ s ≠ 0) (hs : μ s ≠ ∞) : μ[s | s] = 1 := by
   simpa [cond] using ENNReal.inv_mul_cancel hs₀ hs
 
 theorem cond_inter_self (hms : MeasurableSet s) (t : Set Ω) (μ : Measure Ω) :
-    μ[s ∩ t|s] = μ[t|s] := by
+    μ[s ∩ t | s] = μ[t | s] := by
   rw [cond_apply hms, ← Set.inter_assoc, Set.inter_self, ← cond_apply hms]
 
 theorem inter_pos_of_cond_ne_zero (hms : MeasurableSet s) (hcst : μ[t | s] ≠ 0) :
@@ -254,24 +254,24 @@ theorem cond_cond_eq_cond_inter (hms : MeasurableSet s) (hmt : MeasurableSet t)
   cond_cond_eq_cond_inter' hms hmt (measure_ne_top μ s)
 
 theorem cond_mul_eq_inter' (hms : MeasurableSet s) (hcs' : μ s ≠ ∞) (t : Set Ω) :
-    μ[t|s] * μ s = μ (s ∩ t) := by
+    μ[t | s] * μ s = μ (s ∩ t) := by
   obtain hcs | hcs := eq_or_ne (μ s) 0
   · simp [hcs, measure_inter_null_of_null_left]
   · rw [cond_apply hms, mul_comm, ← mul_assoc, ENNReal.mul_inv_cancel hcs hcs', one_mul]
 
 theorem cond_mul_eq_inter (hms : MeasurableSet s) (t : Set Ω) (μ : Measure Ω) [IsFiniteMeasure μ] :
-    μ[t|s] * μ s = μ (s ∩ t) := cond_mul_eq_inter' hms (measure_ne_top _ s) t
+    μ[t | s] * μ s = μ (s ∩ t) := cond_mul_eq_inter' hms (measure_ne_top _ s) t
 
 /-- A version of the law of total probability. -/
 theorem cond_add_cond_compl_eq (hms : MeasurableSet s) (μ : Measure Ω) [IsFiniteMeasure μ] :
-    μ[t|s] * μ s + μ[t|sᶜ] * μ sᶜ = μ t := by
+    μ[t | s] * μ s + μ[t | sᶜ] * μ sᶜ = μ t := by
   rw [cond_mul_eq_inter hms, cond_mul_eq_inter hms.compl, Set.inter_comm _ t,
     Set.inter_comm _ t]
   exact measure_inter_add_diff t hms
 
 /-- **Bayes' Theorem** -/
 theorem cond_eq_inv_mul_cond_mul (hms : MeasurableSet s) (hmt : MeasurableSet t) (μ : Measure Ω)
-    [IsFiniteMeasure μ] : μ[t|s] = (μ s)⁻¹ * μ[s|t] * μ t := by
+    [IsFiniteMeasure μ] : μ[t | s] = (μ s)⁻¹ * μ[s | t] * μ t := by
   rw [mul_assoc, cond_mul_eq_inter hmt s, Set.inter_comm, cond_apply hms]
 
 end Bayes