chore: tidy various files (#7343)

Mathlib/Algebra/Order/LatticeGroup.lean

@@ -656,13 +656,13 @@ variable [Semiring α] [Invertible (2 : α)] [Lattice β] [AddCommGroup β] [Mod
   [CovariantClass β β (· + ·) (· ≤ ·)]
 
 lemma inf_eq_half_smul_add_sub_abs_sub (x y : β) :
-    x ⊓ y = (⅟2 : α) • (x + y - |y - x|) :=
-by rw [←LatticeOrderedCommGroup.two_inf_eq_add_sub_abs_sub x y, two_smul, ←two_smul α,
+    x ⊓ y = (⅟2 : α) • (x + y - |y - x|) := by
+  rw [←LatticeOrderedCommGroup.two_inf_eq_add_sub_abs_sub x y, two_smul, ←two_smul α,
     smul_smul, invOf_mul_self, one_smul]
 
 lemma sup_eq_half_smul_add_add_abs_sub (x y : β) :
-    x ⊔ y = (⅟2 : α) • (x + y + |y - x|) :=
-by rw [←LatticeOrderedCommGroup.two_sup_eq_add_add_abs_sub x y, two_smul, ←two_smul α,
+    x ⊔ y = (⅟2 : α) • (x + y + |y - x|) := by
+  rw [←LatticeOrderedCommGroup.two_sup_eq_add_add_abs_sub x y, two_smul, ←two_smul α,
     smul_smul, invOf_mul_self, one_smul]
 
 end invertible

Mathlib/Algebra/Order/Monoid/NatCast.lean

@@ -18,13 +18,13 @@ variable {α : Type*}
 open Function
 
 lemma lt_add_one [One α] [AddZeroClass α] [PartialOrder α] [ZeroLEOneClass α]
-  [NeZero (1 : α)] [CovariantClass α α (·+·) (·<·)] (a : α) : a < a + 1 :=
-lt_add_of_pos_right _ zero_lt_one
+    [NeZero (1 : α)] [CovariantClass α α (·+·) (·<·)] (a : α) : a < a + 1 :=
+  lt_add_of_pos_right _ zero_lt_one
 #align lt_add_one lt_add_one
 
 lemma lt_one_add [One α] [AddZeroClass α] [PartialOrder α] [ZeroLEOneClass α]
-  [NeZero (1 : α)] [CovariantClass α α (swap (·+·)) (·<·)] (a : α) : a < 1 + a :=
-lt_add_of_pos_left _ zero_lt_one
+    [NeZero (1 : α)] [CovariantClass α α (swap (·+·)) (·<·)] (a : α) : a < 1 + a :=
+  lt_add_of_pos_left _ zero_lt_one
 #align lt_one_add lt_one_add
 
 variable [AddMonoidWithOne α]
@@ -49,14 +49,14 @@ lemma zero_le_four [Preorder α] [ZeroLEOneClass α] [CovariantClass α α (·+
 
 lemma one_le_two [LE α] [ZeroLEOneClass α] [CovariantClass α α (·+·) (·≤·)] :
     (1 : α) ≤ 2 :=
-calc (1 : α) = 1 + 0 := (add_zero 1).symm
+  calc (1 : α) = 1 + 0 := (add_zero 1).symm
      _ ≤ 1 + 1 := add_le_add_left zero_le_one _
      _ = 2 := one_add_one_eq_two
 #align one_le_two one_le_two
 
 lemma one_le_two' [LE α] [ZeroLEOneClass α] [CovariantClass α α (swap (·+·)) (·≤·)] :
     (1 : α) ≤ 2 :=
-calc (1 : α) = 0 + 1 := (zero_add 1).symm
+  calc (1 : α) = 0 + 1 := (zero_add 1).symm
      _ ≤ 1 + 1 := add_le_add_right zero_le_one _
      _ = 2 := one_add_one_eq_two
 #align one_le_two' one_le_two'

Mathlib/Algebra/Ring/Basic.lean

@@ -156,46 +156,46 @@ variable (α)
 
 lemma IsLeftCancelMulZero.to_noZeroDivisors [Ring α] [IsLeftCancelMulZero α] :
     NoZeroDivisors α :=
-{ eq_zero_or_eq_zero_of_mul_eq_zero := @fun x y h ↦ by
-    by_cases hx : x = 0
-    { left
-      exact hx }
-    { right
-      rw [← sub_zero (x * y), ← mul_zero x, ← mul_sub] at h
-      have := (IsLeftCancelMulZero.mul_left_cancel_of_ne_zero) hx h
-      rwa [sub_zero] at this } }
+  { eq_zero_or_eq_zero_of_mul_eq_zero := fun {x y} h ↦ by
+      by_cases hx : x = 0
+      { left
+        exact hx }
+      { right
+        rw [← sub_zero (x * y), ← mul_zero x, ← mul_sub] at h
+        have := (IsLeftCancelMulZero.mul_left_cancel_of_ne_zero) hx h
+        rwa [sub_zero] at this } }
 #align is_left_cancel_mul_zero.to_no_zero_divisors IsLeftCancelMulZero.to_noZeroDivisors
 
 lemma IsRightCancelMulZero.to_noZeroDivisors [Ring α] [IsRightCancelMulZero α] :
     NoZeroDivisors α :=
-{ eq_zero_or_eq_zero_of_mul_eq_zero := @fun x y h ↦ by
-    by_cases hy : y = 0
-    { right
-      exact hy }
-    { left
-      rw [← sub_zero (x * y), ← zero_mul y, ← sub_mul] at h
-      have := (IsRightCancelMulZero.mul_right_cancel_of_ne_zero) hy h
-      rwa [sub_zero] at this } }
+  { eq_zero_or_eq_zero_of_mul_eq_zero := fun {x y} h ↦ by
+      by_cases hy : y = 0
+      { right
+        exact hy }
+      { left
+        rw [← sub_zero (x * y), ← zero_mul y, ← sub_mul] at h
+        have := (IsRightCancelMulZero.mul_right_cancel_of_ne_zero) hy h
+        rwa [sub_zero] at this } }
 #align is_right_cancel_mul_zero.to_no_zero_divisors IsRightCancelMulZero.to_noZeroDivisors
 
 instance (priority := 100) NoZeroDivisors.to_isCancelMulZero [Ring α] [NoZeroDivisors α] :
     IsCancelMulZero α :=
-{ mul_left_cancel_of_ne_zero := fun ha h ↦ by
-    rw [← sub_eq_zero, ← mul_sub] at h
-    exact sub_eq_zero.1 ((eq_zero_or_eq_zero_of_mul_eq_zero h).resolve_left ha)
-  mul_right_cancel_of_ne_zero := fun hb h ↦ by
-    rw [← sub_eq_zero, ← sub_mul] at h
-    exact sub_eq_zero.1 ((eq_zero_or_eq_zero_of_mul_eq_zero h).resolve_right hb) }
+  { mul_left_cancel_of_ne_zero := fun ha h ↦ by
+      rw [← sub_eq_zero, ← mul_sub] at h
+      exact sub_eq_zero.1 ((eq_zero_or_eq_zero_of_mul_eq_zero h).resolve_left ha)
+    mul_right_cancel_of_ne_zero := fun hb h ↦ by
+      rw [← sub_eq_zero, ← sub_mul] at h
+      exact sub_eq_zero.1 ((eq_zero_or_eq_zero_of_mul_eq_zero h).resolve_right hb) }
 #align no_zero_divisors.to_is_cancel_mul_zero NoZeroDivisors.to_isCancelMulZero
 
 lemma NoZeroDivisors.to_isDomain [Ring α] [h : Nontrivial α] [NoZeroDivisors α] :
     IsDomain α :=
-{ NoZeroDivisors.to_isCancelMulZero α, h with .. }
+  { NoZeroDivisors.to_isCancelMulZero α, h with .. }
 #align no_zero_divisors.to_is_domain NoZeroDivisors.to_isDomain
 
 instance (priority := 100) IsDomain.to_noZeroDivisors [Ring α] [IsDomain α] :
     NoZeroDivisors α :=
-IsRightCancelMulZero.to_noZeroDivisors α
+  IsRightCancelMulZero.to_noZeroDivisors α
 #align is_domain.to_no_zero_divisors IsDomain.to_noZeroDivisors
 
 end NoZeroDivisors

Mathlib/Analysis/Calculus/ContDiff.lean

@@ -84,7 +84,7 @@ theorem contDiff_zero_fun : ContDiff 𝕜 n fun _ : E => (0 : F) :=
 /-- Constants are `C^∞`.
 -/
 theorem contDiff_const {c : F} : ContDiff 𝕜 n fun _ : E => c := by
-  suffices h : ContDiff 𝕜 ∞ fun _ : E => c; · exact h.of_le le_top
+  suffices h : ContDiff 𝕜 ∞ fun _ : E => c from h.of_le le_top
   rw [contDiff_top_iff_fderiv]
   refine' ⟨differentiable_const c, _⟩
   rw [fderiv_const]
@@ -142,7 +142,7 @@ theorem iteratedFDeriv_const_of_ne {n : ℕ} (hn : n ≠ 0) (c : F) :
 /-- Unbundled bounded linear functions are `C^∞`.
 -/
 theorem IsBoundedLinearMap.contDiff (hf : IsBoundedLinearMap 𝕜 f) : ContDiff 𝕜 n f := by
-  suffices h : ContDiff 𝕜 ∞ f; · exact h.of_le le_top
+  suffices h : ContDiff 𝕜 ∞ f from h.of_le le_top
   rw [contDiff_top_iff_fderiv]
   refine' ⟨hf.differentiable, _⟩
   simp_rw [hf.fderiv]
@@ -186,7 +186,7 @@ theorem contDiffOn_id {s} : ContDiffOn 𝕜 n (id : E → E) s :=
 /-- Bilinear functions are `C^∞`.
 -/
 theorem IsBoundedBilinearMap.contDiff (hb : IsBoundedBilinearMap 𝕜 b) : ContDiff 𝕜 n b := by
-  suffices h : ContDiff 𝕜 ∞ b; · exact h.of_le le_top
+  suffices h : ContDiff 𝕜 ∞ b from h.of_le le_top
   rw [contDiff_top_iff_fderiv]
   refine' ⟨hb.differentiable, _⟩
   simp only [hb.fderiv]
@@ -429,8 +429,8 @@ theorem ContinuousLinearEquiv.iteratedFDerivWithin_comp_right (g : G ≃L[𝕜]
     simp only [ContinuousLinearMap.coe_comp', ContinuousLinearEquiv.coe_coe, comp_apply,
       ContinuousMultilinearMap.compContinuousLinearMapEquivL_apply,
       ContinuousMultilinearMap.compContinuousLinearMap_apply]
-    rw [ContinuousLinearEquiv.comp_right_fderivWithin _ (g.uniqueDiffOn_preimage_iff.2 hs x hx)]
-    rfl
+    rw [ContinuousLinearEquiv.comp_right_fderivWithin _ (g.uniqueDiffOn_preimage_iff.2 hs x hx),
+      ContinuousLinearMap.coe_comp', coe_coe, comp_apply, tail_def, tail_def]
 #align continuous_linear_equiv.iterated_fderiv_within_comp_right ContinuousLinearEquiv.iteratedFDerivWithin_comp_right
 
 /-- The iterated derivative of the composition with a linear map on the right is

Mathlib/Data/Countable/Defs.lean

@@ -38,7 +38,7 @@ class Countable (α : Sort u) : Prop where
 #align countable_iff_exists_injective countable_iff_exists_injective
 
 lemma Countable.exists_injective_nat (α : Sort u) [Countable α] : ∃ f : α → ℕ, Injective f :=
-Countable.exists_injective_nat'
+  Countable.exists_injective_nat'
 
 instance : Countable ℕ :=
   ⟨⟨id, injective_id⟩⟩

Mathlib/Data/List/Basic.lean

@@ -321,12 +321,12 @@ theorem subset_append_of_subset_right' (l l₁ l₂ : List α) : l ⊆ l₂ →
 
 theorem cons_subset_of_subset_of_mem {a : α} {l m : List α}
   (ainm : a ∈ m) (lsubm : l ⊆ m) : a::l ⊆ m :=
-cons_subset.2 ⟨ainm, lsubm⟩
+  cons_subset.2 ⟨ainm, lsubm⟩
 #align list.cons_subset_of_subset_of_mem List.cons_subset_of_subset_of_mem
 
 theorem append_subset_of_subset_of_subset {l₁ l₂ l : List α} (l₁subl : l₁ ⊆ l) (l₂subl : l₂ ⊆ l) :
     l₁ ++ l₂ ⊆ l :=
-fun _ h ↦ (mem_append.1 h).elim (@l₁subl _) (@l₂subl _)
+  fun _ h ↦ (mem_append.1 h).elim (@l₁subl _) (@l₂subl _)
 #align list.append_subset_of_subset_of_subset List.append_subset_of_subset_of_subset
 
 -- Porting note: in Std

Mathlib/Data/MvPolynomial/Basic.lean

@@ -336,8 +336,8 @@ theorem monomial_single_add : monomial (Finsupp.single n e + s) a = X n ^ e * mo
 #align mv_polynomial.monomial_single_add MvPolynomial.monomial_single_add
 
 theorem C_mul_X_pow_eq_monomial {s : σ} {a : R} {n : ℕ} :
-    C a * X s ^ n = monomial (Finsupp.single s n) a :=
-  by rw [← zero_add (Finsupp.single s n), monomial_add_single, C_apply]
+    C a * X s ^ n = monomial (Finsupp.single s n) a := by
+  rw [← zero_add (Finsupp.single s n), monomial_add_single, C_apply]
 #align mv_polynomial.C_mul_X_pow_eq_monomial MvPolynomial.C_mul_X_pow_eq_monomial
 
 theorem C_mul_X_eq_monomial {s : σ} {a : R} : C a * X s = monomial (Finsupp.single s 1) a := by

Mathlib/Data/Nat/ModEq.lean

@@ -302,12 +302,12 @@ lemma cancel_right_div_gcd (hm : 0 < m) (h : a * c ≡ b * c [MOD m]) : a ≡ b
 
 lemma cancel_left_div_gcd' (hm : 0 < m) (hcd : c ≡ d [MOD m]) (h : c * a ≡ d * b [MOD m]) :
     a ≡ b [MOD m / gcd m c] :=
-(h.trans $ hcd.symm.mul_right b).cancel_left_div_gcd hm
+  (h.trans $ hcd.symm.mul_right b).cancel_left_div_gcd hm
 #align nat.modeq.cancel_left_div_gcd' Nat.ModEq.cancel_left_div_gcd'
 
 lemma cancel_right_div_gcd' (hm : 0 < m) (hcd : c ≡ d [MOD m]) (h : a * c ≡ b * d [MOD m]) :
     a ≡ b [MOD m / gcd m c] :=
-(h.trans $ hcd.symm.mul_left b).cancel_right_div_gcd hm
+  (h.trans $ hcd.symm.mul_left b).cancel_right_div_gcd hm
 #align nat.modeq.cancel_right_div_gcd' Nat.ModEq.cancel_right_div_gcd'
 
 /-- A common factor that's coprime with the modulus can be cancelled from a `ModEq` -/

Mathlib/Logic/Relator.lean

@@ -74,68 +74,68 @@ def BiUnique : Prop := LeftUnique R ∧ RightUnique R
 variable {R}
 
 lemma RightTotal.rel_forall (h : RightTotal R) :
-    ((R ⇒ (· → ·)) ⇒ (· → ·)) (λ p => ∀i, p i) (λ q => ∀i, q i) :=
-λ _ _ Hrel H b => Exists.elim (h b) (λ _ Rab => Hrel Rab (H _))
+    ((R ⇒ (· → ·)) ⇒ (· → ·)) (fun p => ∀i, p i) (fun q => ∀i, q i) :=
+  fun _ _ Hrel H b => Exists.elim (h b) (fun _ Rab => Hrel Rab (H _))
 #align relator.right_total.rel_forall Relator.RightTotal.rel_forall
 
 lemma LeftTotal.rel_exists (h : LeftTotal R) :
-    ((R ⇒ (· → ·)) ⇒ (· → ·)) (λ p => ∃i, p i) (λ q => ∃i, q i) :=
-λ _ _ Hrel ⟨a, pa⟩ => (h a).imp $ λ _ Rab => Hrel Rab pa
+    ((R ⇒ (· → ·)) ⇒ (· → ·)) (fun p => ∃i, p i) (fun q => ∃i, q i) :=
+  fun _ _ Hrel ⟨a, pa⟩ => (h a).imp $ fun _ Rab => Hrel Rab pa
 #align relator.left_total.rel_exists Relator.LeftTotal.rel_exists
 
 lemma BiTotal.rel_forall (h : BiTotal R) :
-    ((R ⇒ Iff) ⇒ Iff) (λ p => ∀i, p i) (λ q => ∀i, q i) :=
-λ _ _ Hrel =>
-  ⟨λ H b => Exists.elim (h.right b) (λ _ Rab => (Hrel Rab).mp (H _)),
-    λ H a => Exists.elim (h.left a) (λ _ Rab => (Hrel Rab).mpr (H _))⟩
+    ((R ⇒ Iff) ⇒ Iff) (fun p => ∀i, p i) (fun q => ∀i, q i) :=
+  fun _ _ Hrel =>
+    ⟨fun H b => Exists.elim (h.right b) (fun _ Rab => (Hrel Rab).mp (H _)),
+      fun H a => Exists.elim (h.left a) (fun _ Rab => (Hrel Rab).mpr (H _))⟩
 #align relator.bi_total.rel_forall Relator.BiTotal.rel_forall
 
 lemma BiTotal.rel_exists (h : BiTotal R) :
-    ((R ⇒ Iff) ⇒ Iff) (λ p => ∃i, p i) (λ q => ∃i, q i) :=
-λ _ _ Hrel =>
-  ⟨λ ⟨a, pa⟩ => (h.left a).imp $ λ _ Rab => (Hrel Rab).1 pa,
-    λ ⟨b, qb⟩ => (h.right b).imp $ λ _ Rab => (Hrel Rab).2 qb⟩
+    ((R ⇒ Iff) ⇒ Iff) (fun p => ∃i, p i) (fun q => ∃i, q i) :=
+  fun _ _ Hrel =>
+    ⟨fun ⟨a, pa⟩ => (h.left a).imp $ fun _ Rab => (Hrel Rab).1 pa,
+      fun ⟨b, qb⟩ => (h.right b).imp $ fun _ Rab => (Hrel Rab).2 qb⟩
 #align relator.bi_total.rel_exists Relator.BiTotal.rel_exists
 
 lemma left_unique_of_rel_eq {eq' : β → β → Prop} (he : (R ⇒ (R ⇒ Iff)) Eq eq') : LeftUnique R :=
-λ a b c (ac : R a c) (bc : R b c) => (he ac bc).mpr ((he bc bc).mp rfl)
+  fun a b c (ac : R a c) (bc : R b c) => (he ac bc).mpr ((he bc bc).mp rfl)
 #align relator.left_unique_of_rel_eq Relator.left_unique_of_rel_eq
 
 end
 
 lemma rel_imp : (Iff ⇒ (Iff ⇒ Iff)) (· → ·) (· → ·) :=
-  λ _ _ h _ _ l => imp_congr h l
+  fun _ _ h _ _ l => imp_congr h l
 #align relator.rel_imp Relator.rel_imp
 
 lemma rel_not : (Iff ⇒ Iff) Not Not :=
-  λ _ _ h => not_congr h
+  fun _ _ h => not_congr h
 #align relator.rel_not Relator.rel_not
 
 lemma bi_total_eq {α : Type u₁} : Relator.BiTotal (@Eq α) :=
-  { left := λ a => ⟨a, rfl⟩, right := λ a => ⟨a, rfl⟩ }
+  { left := fun a => ⟨a, rfl⟩, right := fun a => ⟨a, rfl⟩ }
 #align relator.bi_total_eq Relator.bi_total_eq
 
 variable {α : Type*} {β : Type*} {γ : Type*} {δ : Type*}
 variable {r : α → β → Prop} {p : β → γ → Prop} {q : γ → δ → Prop}
 
 lemma LeftUnique.flip (h : LeftUnique r) : RightUnique (flip r) :=
-  λ _ _ _ h₁ h₂ => h h₁ h₂
+  fun _ _ _ h₁ h₂ => h h₁ h₂
 #align relator.left_unique.flip Relator.LeftUnique.flip
 
 lemma rel_and : ((·↔·) ⇒ (·↔·) ⇒ (·↔·)) (·∧·) (·∧·) :=
-  λ _ _ h₁ _ _ h₂ => and_congr h₁ h₂
+  fun _ _ h₁ _ _ h₂ => and_congr h₁ h₂
 #align relator.rel_and Relator.rel_and
 
 lemma rel_or : ((·↔·) ⇒ (·↔·) ⇒ (·↔·)) (·∨·) (·∨·) :=
-  λ _ _ h₁ _ _ h₂ => or_congr h₁ h₂
+  fun _ _ h₁ _ _ h₂ => or_congr h₁ h₂
 #align relator.rel_or Relator.rel_or
 
 lemma rel_iff : ((·↔·) ⇒ (·↔·) ⇒ (·↔·)) (·↔·) (·↔·) :=
-  λ _ _ h₁ _ _ h₂ => iff_congr h₁ h₂
+  fun _ _ h₁ _ _ h₂ => iff_congr h₁ h₂
 #align relator.rel_iff Relator.rel_iff
 
 lemma rel_eq {r : α → β → Prop} (hr : BiUnique r) : (r ⇒ r ⇒ (·↔·)) (·=·) (·=·) :=
-  λ _ _ h₁ _ _ h₂ => ⟨λ h => hr.right h₁ $ h.symm ▸ h₂, λ h => hr.left h₁ $ h.symm ▸ h₂⟩
+  fun _ _ h₁ _ _ h₂ => ⟨fun h => hr.right h₁ $ h.symm ▸ h₂, fun h => hr.left h₁ $ h.symm ▸ h₂⟩
 #align relator.rel_eq Relator.rel_eq
 
 open Function

Mathlib/MeasureTheory/Integral/SetIntegral.lean

@@ -45,7 +45,7 @@ We provide the following notations for expressing the integral of a function on
 * `∫ a in s, f a ∂μ` is `MeasureTheory.integral (μ.restrict s) f`
 * `∫ a in s, f a` is `∫ a in s, f a ∂volume`
 
-Note that the set notations are defined in the file `MeasureTheory/Integral/Bochner`,
+Note that the set notations are defined in the file `MeasureTheory/Integral/Bochner.lean`,
 but we reference them here because all theorems about set integrals are in this file.
 
 -/
@@ -955,10 +955,12 @@ open MeasureTheory Asymptotics Metric
 
 variable {ι : Type*} [NormedAddCommGroup E]
 
-/-- Fundamental theorem of calculus for set integrals: if `μ` is a measure that is finite at a
-filter `l` and `f` is a measurable function that has a finite limit `b` at `l ⊓ μ.ae`, then `∫ x in
-s i, f x ∂μ = μ (s i) • b + o(μ (s i))` at a filter `li` provided that `s i` tends to `l.small_sets`
-along `li`. Since `μ (s i)` is an `ℝ≥0∞` number, we use `(μ (s i)).toReal` in the actual statement.
+/-- Fundamental theorem of calculus for set integrals:
+if `μ` is a measure that is finite at a filter `l` and
+`f` is a measurable function that has a finite limit `b` at `l ⊓ μ.ae`, then
+`∫ x in s i, f x ∂μ = μ (s i) • b + o(μ (s i))` at a filter `li` provided that
+`s i` tends to `l.smallSets` along `li`.
+Since `μ (s i)` is an `ℝ≥0∞` number, we use `(μ (s i)).toReal` in the actual statement.
 
 Often there is a good formula for `(μ (s i)).toReal`, so the formalization can take an optional
 argument `m` with this formula and a proof of `(fun i => (μ (s i)).toReal) =ᶠ[li] m`. Without these
@@ -970,9 +972,10 @@ theorem Filter.Tendsto.integral_sub_linear_isLittleO_ae [NormedSpace ℝ E] [Com
     (m : ι → ℝ := fun i => (μ (s i)).toReal)
     (hsμ : (fun i => (μ (s i)).toReal) =ᶠ[li] m := by rfl) :
     (fun i => (∫ x in s i, f x ∂μ) - m i • b) =o[li] m := by
-  suffices : (fun s => (∫ x in s, f x ∂μ) - (μ s).toReal • b) =o[l.smallSets] fun s => (μ s).toReal
-  exact (this.comp_tendsto hs).congr'
-    (hsμ.mono fun a ha => by dsimp only [Function.comp_apply] at ha ⊢; rw [ha]) hsμ
+  suffices
+      (fun s => (∫ x in s, f x ∂μ) - (μ s).toReal • b) =o[l.smallSets] fun s => (μ s).toReal from
+    (this.comp_tendsto hs).congr'
+      (hsμ.mono fun a ha => by dsimp only [Function.comp_apply] at ha ⊢; rw [ha]) hsμ
   refine' isLittleO_iff.2 fun ε ε₀ => _
   have : ∀ᶠ s in l.smallSets, ∀ᶠ x in μ.ae, x ∈ s → f x ∈ closedBall b ε :=
     eventually_smallSets_eventually.2 (h.eventually <| closedBall_mem_nhds _ ε₀)

Mathlib/MeasureTheory/Measure/OuterMeasure.lean

@@ -940,7 +940,7 @@ def IsCaratheodory (s : Set α) : Prop :=
 
 theorem isCaratheodory_iff_le' {s : Set α} :
     IsCaratheodory m s ↔ ∀ t, m (t ∩ s) + m (t \ s) ≤ m t :=
-    forall_congr' fun _ => le_antisymm_iff.trans <| and_iff_right <| le_inter_add_diff _
+  forall_congr' fun _ => le_antisymm_iff.trans <| and_iff_right <| le_inter_add_diff _
 #align measure_theory.outer_measure.is_caratheodory_iff_le' MeasureTheory.OuterMeasure.isCaratheodory_iff_le'
 
 @[simp]
@@ -1624,14 +1624,14 @@ theorem trim_mono : Monotone (trim : OuterMeasure α → OuterMeasure α) := fun
 
 theorem le_trim_iff {m₁ m₂ : OuterMeasure α} :
     m₁ ≤ m₂.trim ↔ ∀ s, MeasurableSet s → m₁ s ≤ m₂ s := by
-    let me := extend (fun s (_p : MeasurableSet s) => measureOf m₂ s)
-    have me_empty : me ∅ = 0 := by apply extend_empty; simp; simp
-    have : m₁ ≤ OuterMeasure.ofFunction me me_empty ↔
-            (∀ (s : Set α), measureOf m₁ s ≤ me s) := le_ofFunction
-    apply this.trans
-    apply forall_congr'
-    intro s
-    apply le_iInf_iff
+  let me := extend (fun s (_p : MeasurableSet s) => measureOf m₂ s)
+  have me_empty : me ∅ = 0 := by apply extend_empty; simp; simp
+  have : m₁ ≤ OuterMeasure.ofFunction me me_empty ↔
+          (∀ (s : Set α), measureOf m₁ s ≤ me s) := le_ofFunction
+  apply this.trans
+  apply forall_congr'
+  intro s
+  apply le_iInf_iff
 #align measure_theory.outer_measure.le_trim_iff MeasureTheory.OuterMeasure.le_trim_iff
 
 theorem trim_le_trim_iff {m₁ m₂ : OuterMeasure α} :
@@ -1759,14 +1759,14 @@ theorem trim_sup (m₁ m₂ : OuterMeasure α) : (m₁ ⊔ m₂).trim = m₁.tri
 of the trimmed measures. -/
 theorem trim_iSup {ι} [Countable ι] (μ : ι → OuterMeasure α) :
     trim (⨆ i, μ i) = ⨆ i, trim (μ i) := by
-    simp_rw [← @iSup_plift_down _ ι]
-    ext1 s
-    obtain ⟨t, _, _, hμt⟩ :=
-      exists_measurable_superset_forall_eq_trim
-        (Option.elim' (⨆ i, μ (PLift.down i)) (μ ∘ PLift.down)) s
-    simp only [Option.forall, Option.elim'] at hμt
-    simp only [iSup_apply, ← hμt.1]
-    exact iSup_congr hμt.2
+  simp_rw [← @iSup_plift_down _ ι]
+  ext1 s
+  obtain ⟨t, _, _, hμt⟩ :=
+    exists_measurable_superset_forall_eq_trim
+      (Option.elim' (⨆ i, μ (PLift.down i)) (μ ∘ PLift.down)) s
+  simp only [Option.forall, Option.elim'] at hμt
+  simp only [iSup_apply, ← hμt.1]
+  exact iSup_congr hμt.2
 #align measure_theory.outer_measure.trim_supr MeasureTheory.OuterMeasure.trim_iSup
 
 /-- The trimmed property of a measure μ states that `μ.toOuterMeasure.trim = μ.toOuterMeasure`.