chore: tidy various files (#11490)

Mathlib/Algebra/Algebra/Hom.lean

@@ -73,10 +73,10 @@ instance (priority := 100) linearMapClass [AlgHomClass F R A B] : LinearMapClass
 /-- Turn an element of a type `F` satisfying `AlgHomClass F α β` into an actual
 `AlgHom`. This is declared as the default coercion from `F` to `α →+* β`. -/
 @[coe]
-def toAlgHom {F : Type*} [FunLike F A B] [AlgHomClass F R A B] (f : F) : A →ₐ[R] B :=
-  { (f : A →+* B) with
-      toFun := f
-      commutes' := AlgHomClass.commutes f }
+def toAlgHom {F : Type*} [FunLike F A B] [AlgHomClass F R A B] (f : F) : A →ₐ[R] B where
+  __ := (f : A →+* B)
+  toFun := f
+  commutes' := AlgHomClass.commutes f
 
 instance coeTC {F : Type*} [FunLike F A B] [AlgHomClass F R A B] : CoeTC F (A →ₐ[R] B) :=
   ⟨AlgHomClass.toAlgHom⟩

Mathlib/Algebra/Algebra/Subalgebra/Basic.lean

@@ -620,14 +620,12 @@ def rangeRestrict (f : A →ₐ[R] B) : A →ₐ[R] f.range :=
   f.codRestrict f.range f.mem_range_self
 #align alg_hom.range_restrict AlgHom.rangeRestrict
 
-theorem rangeRestrict_surjective (f : A →ₐ[R] B):
-    Function.Surjective (f.rangeRestrict) :=
+theorem rangeRestrict_surjective (f : A →ₐ[R] B) : Function.Surjective (f.rangeRestrict) :=
   fun ⟨_y, hy⟩ =>
-  let ⟨x, hx⟩ := hy
-  ⟨x, SetCoe.ext hx⟩
+    let ⟨x, hx⟩ := hy
+    ⟨x, SetCoe.ext hx⟩
 
-theorem ker_rangeRestrict (f : A →ₐ[R] B) :
-    RingHom.ker f.rangeRestrict = RingHom.ker f :=
+theorem ker_rangeRestrict (f : A →ₐ[R] B) : RingHom.ker f.rangeRestrict = RingHom.ker f :=
   Ideal.ext fun _ ↦ Subtype.ext_iff
 
 /-- The equalizer of two R-algebra homomorphisms -/

Mathlib/Algebra/Module/CharacterModule.lean

@@ -153,8 +153,10 @@ by the ideal generated by the order of `a`. -/
     (ℤ ∙ a) ≃ₗ[ℤ] ℤ ⧸ Ideal.span {(addOrderOf a : ℤ)} :=
   LinearEquiv.ofEq _ _ (LinearMap.span_singleton_eq_range ℤ A a) ≪≫ₗ
   (LinearMap.quotKerEquivRange <| LinearMap.toSpanSingleton ℤ A a).symm ≪≫ₗ
-  Submodule.quotEquivOfEq _ _
-    (by ext1 x; rw [Ideal.mem_span_singleton, addOrderOf_dvd_iff_zsmul_eq_zero]; rfl)
+  Submodule.quotEquivOfEq _ _ (by
+    ext1 x
+    rw [Ideal.mem_span_singleton, addOrderOf_dvd_iff_zsmul_eq_zero, LinearMap.mem_ker,
+      LinearMap.toSpanSingleton_apply])
 
 lemma intSpanEquivQuotAddOrderOf_apply_self (a : A) :
     intSpanEquivQuotAddOrderOf a ⟨a, Submodule.mem_span_singleton_self a⟩ =

Mathlib/Algebra/Order/Nonneg/Ring.lean

@@ -220,7 +220,7 @@ instance addMonoidWithOne [OrderedSemiring α] : AddMonoidWithOne { x : α // 0
     Nonneg.orderedAddCommMonoid with
     natCast := fun n => ⟨n, Nat.cast_nonneg n⟩
     natCast_zero := by simp
-    natCast_succ := fun _ => by simp only [Nat.cast_add, Nat.cast_one]; rfl }
+    natCast_succ := fun _ => by ext; simp }
 #align nonneg.add_monoid_with_one Nonneg.addMonoidWithOne
 
 @[simp, norm_cast]

Mathlib/AlgebraicGeometry/ProjectiveSpectrum/Scheme.lean

@@ -685,7 +685,7 @@ lemma fromSpec_toSpec {f : A} {m : ℕ} (hm : 0 < m) (f_deg : f ∈ 𝒜 m) (x :
   · intro i
     erw [ToSpec.mem_carrier_iff, HomogeneousLocalization.val_mk'']
     dsimp only [GradedAlgebra.proj_apply]
-    rw [show (mk (decompose 𝒜 z i ^ m) ⟨f^i, ⟨i, rfl⟩⟩: Away f) =
+    rw [show (mk (decompose 𝒜 z i ^ m) ⟨f^i, ⟨i, rfl⟩⟩ : Away f) =
       (decompose 𝒜 z i ^ m : A) • (mk 1 ⟨f^i, ⟨i, rfl⟩⟩ : Away f) by
       · rw [smul_mk, smul_eq_mul, mul_one], Algebra.smul_def]
     exact Ideal.mul_mem_right _ _ <|

Mathlib/Analysis/Asymptotics/Asymptotics.lean

@@ -1984,7 +1984,7 @@ theorem isBigOWith_of_eq_mul {u v : α → R} (φ : α → R) (hφ : ∀ᶠ x in
 #align asymptotics.is_O_with_of_eq_mul Asymptotics.isBigOWith_of_eq_mul
 
 theorem isBigOWith_iff_exists_eq_mul (hc : 0 ≤ c) :
-    IsBigOWith c l u v ↔ ∃ (φ : α → 𝕜) (_hφ : ∀ᶠ x in l, ‖φ x‖ ≤ c), u =ᶠ[l] φ * v := by
+    IsBigOWith c l u v ↔ ∃ φ : α → 𝕜, (∀ᶠ x in l, ‖φ x‖ ≤ c) ∧ u =ᶠ[l] φ * v := by
   constructor
   · intro h
     use fun x => u x / v x
@@ -1995,12 +1995,12 @@ theorem isBigOWith_iff_exists_eq_mul (hc : 0 ≤ c) :
 #align asymptotics.is_O_with_iff_exists_eq_mul Asymptotics.isBigOWith_iff_exists_eq_mul
 
 theorem IsBigOWith.exists_eq_mul (h : IsBigOWith c l u v) (hc : 0 ≤ c) :
-    ∃ (φ : α → 𝕜) (_hφ : ∀ᶠ x in l, ‖φ x‖ ≤ c), u =ᶠ[l] φ * v :=
+    ∃ φ : α → 𝕜, (∀ᶠ x in l, ‖φ x‖ ≤ c) ∧ u =ᶠ[l] φ * v :=
   (isBigOWith_iff_exists_eq_mul hc).mp h
 #align asymptotics.is_O_with.exists_eq_mul Asymptotics.IsBigOWith.exists_eq_mul
 
 theorem isBigO_iff_exists_eq_mul :
-    u =O[l] v ↔ ∃ (φ : α → 𝕜) (_hφ : l.IsBoundedUnder (· ≤ ·) (norm ∘ φ)), u =ᶠ[l] φ * v := by
+    u =O[l] v ↔ ∃ φ : α → 𝕜, l.IsBoundedUnder (· ≤ ·) (norm ∘ φ) ∧ u =ᶠ[l] φ * v := by
   constructor
   · rintro h
     rcases h.exists_nonneg with ⟨c, hnnc, hc⟩
@@ -2014,7 +2014,7 @@ alias ⟨IsBigO.exists_eq_mul, _⟩ := isBigO_iff_exists_eq_mul
 #align asymptotics.is_O.exists_eq_mul Asymptotics.IsBigO.exists_eq_mul
 
 theorem isLittleO_iff_exists_eq_mul :
-    u =o[l] v ↔ ∃ (φ : α → 𝕜) (_hφ : Tendsto φ l (𝓝 0)), u =ᶠ[l] φ * v := by
+    u =o[l] v ↔ ∃ φ : α → 𝕜, Tendsto φ l (𝓝 0) ∧ u =ᶠ[l] φ * v := by
   constructor
   · exact fun h => ⟨fun x => u x / v x, h.tendsto_div_nhds_zero, h.eventually_mul_div_cancel.symm⟩
   · simp only [IsLittleO_def]

Mathlib/Analysis/Fourier/RiemannLebesgueLemma.lean

@@ -151,15 +151,10 @@ theorem tendsto_integral_exp_inner_smul_cocompact_of_continuous_compact_support
     rw [norm_smul, norm_div, Real.norm_of_nonneg (mul_nonneg two_pos.le <| sq_nonneg _), norm_one,
       sq, ← div_div, ← div_div, ← div_div, div_mul_cancel _ (norm_eq_zero.not.mpr hw_ne)]
   --* Rewrite integral in terms of `f v - f (v + w')`.
-  -- Porting note: this was
-  -- rw [norm_eq_abs, ← Complex.ofReal_one, ← ofReal_bit0, ← of_real_div,
-  --   Complex.abs_of_nonneg one_half_pos.le]
-  have : ‖(1 / 2 : ℂ)‖ = 1 / 2 := by norm_num
+  have : ‖(1 / 2 : ℂ)‖ = 2⁻¹ := by norm_num
   rw [fourier_integral_eq_half_sub_half_period_translate hw_ne
       (hf1.integrable_of_hasCompactSupport hf2),
-    norm_smul, this]
-  have : ε = 1 / 2 * (2 * ε) := by field_simp; rw [mul_comm]
-  rw [this, mul_lt_mul_left (one_half_pos : (0 : ℝ) < 1 / 2)]
+    norm_smul, this, inv_mul_eq_div, div_lt_iff' two_pos]
   refine' lt_of_le_of_lt (norm_integral_le_integral_norm _) _
   simp_rw [norm_smul, norm_eq_abs, abs_coe_circle, one_mul]
   --* Show integral can be taken over A only.
@@ -176,7 +171,7 @@ theorem tendsto_integral_exp_inner_smul_cocompact_of_continuous_compact_support
       refine' (div_le_one <| norm_pos_iff.mpr hw_ne).mpr _
       refine' le_trans (le_add_of_nonneg_right <| one_div_nonneg.mpr <| _) hw_bd
       exact (mul_pos (zero_lt_two' ℝ) hδ1).le
-    · exact ((le_add_iff_nonneg_right _).mpr zero_le_one).trans hv.le
+    · exact (le_add_of_nonneg_right zero_le_one).trans hv.le
   rw [int_A]; clear int_A
   --* Bound integral using fact that `‖f v - f (v + w')‖` is small.
   have bdA : ∀ v : V, v ∈ A → ‖‖f v - f (v + i w)‖‖ ≤ ε / B := by
@@ -185,10 +180,9 @@ theorem tendsto_integral_exp_inner_smul_cocompact_of_continuous_compact_support
     refine' fun x _ => (hδ2 _).le
     rw [sub_add_cancel', norm_neg, hw'_nm, ← div_div, div_lt_iff (norm_pos_iff.mpr hw_ne), ←
       div_lt_iff' hδ1, div_div]
-    refine' (lt_add_of_pos_left _ _).trans_le hw_bd
-    exact one_half_pos
+    exact (lt_add_of_pos_left _ one_half_pos).trans_le hw_bd
   have bdA2 := norm_set_integral_le_of_norm_le_const (hB_vol.trans_lt ENNReal.coe_lt_top) bdA ?_
-  swap;
+  swap
   · apply Continuous.aestronglyMeasurable
     exact
       continuous_norm.comp <|

Mathlib/Analysis/SpecialFunctions/Trigonometric/Bounds.lean

@@ -62,10 +62,12 @@ lemma one_sub_sq_div_two_le_cos : 1 - x ^ 2 / 2 ≤ cos x := by
   · simpa using this $ neg_nonneg.2 $ le_of_not_le hx₀
   suffices MonotoneOn (fun x ↦ cos x + x ^ 2 / 2) (Ici 0) by
     simpa using this left_mem_Ici hx₀ hx₀
-  refine monotoneOn_of_hasDerivWithinAt_nonneg (convex_Ici _) (Continuous.continuousOn $ by
-    continuity) (fun x _ ↦
-    ((hasDerivAt_cos ..).add $ (hasDerivAt_pow ..).div_const _).hasDerivWithinAt) fun x hx ↦ ?_
-  simpa [mul_div_cancel_left] using sin_le $ interior_subset hx
+  refine monotoneOn_of_hasDerivWithinAt_nonneg
+    (convex_Ici _)
+    (Continuous.continuousOn <| by continuity)
+    (fun x _ ↦ ((hasDerivAt_cos ..).add <| (hasDerivAt_pow ..).div_const _).hasDerivWithinAt)
+    fun x hx ↦ ?_
+  simpa [mul_div_cancel_left] using sin_le <| interior_subset hx
 
 /-- **Jordan's inequality**. -/
 lemma two_div_pi_mul_le_sin (hx₀ : 0 ≤ x) (hx : x ≤ π / 2) : 2 / π * x ≤ sin x := by
@@ -98,8 +100,11 @@ lemma cos_quadratic_upper_bound (hx : |x| ≤ π) : cos x ≤ 1 - 2 / π ^ 2 * x
   simp only [Nat.cast_ofNat, Nat.succ_sub_succ_eq_sub, tsub_zero, pow_one, ← neg_sub', neg_sub,
     ← mul_assoc] at hderiv
   have hmono : MonotoneOn (fun x ↦ 1 - 2 / π ^ 2 * x ^ 2 - cos x) (Icc 0 (π / 2)) := by
-    refine monotoneOn_of_hasDerivWithinAt_nonneg (convex_Icc ..) (Continuous.continuousOn $
-      by continuity) (fun x _ ↦ (hderiv _).hasDerivWithinAt) fun x hx ↦ sub_nonneg.2 ?_
+    refine monotoneOn_of_hasDerivWithinAt_nonneg
+      (convex_Icc ..)
+      (Continuous.continuousOn $ by continuity)
+      (fun x _ ↦ (hderiv _).hasDerivWithinAt)
+      fun x hx ↦ sub_nonneg.2 ?_
     have ⟨hx₀, hx⟩ := interior_subset hx
     calc 2 / π ^ 2 * 2 * x
         = 2 / π * (2 / π * x) := by ring

Mathlib/Combinatorics/SetFamily/Shadow.lean

@@ -105,7 +105,7 @@ lemma mem_shadow_iff_exists_sdiff : t ∈ ∂ 𝒜 ↔ ∃ s ∈ 𝒜, t ⊆ s 
 
 /-- `t` is in the shadow of `𝒜` iff we can add an element to it so that the resulting finset is in
 `𝒜`. -/
-lemma mem_shadow_iff_insert_mem : t ∈ ∂ 𝒜 ↔ ∃ a, a ∉ t ∧ insert a t ∈ 𝒜 := by
+lemma mem_shadow_iff_insert_mem : t ∈ ∂ 𝒜 ↔ ∃ a ∉ t, insert a t ∈ 𝒜 := by
   simp_rw [mem_shadow_iff_exists_sdiff, ← covBy_iff_card_sdiff_eq_one, covBy_iff_exists_insert]
   aesop
 #align finset.mem_shadow_iff_insert_mem Finset.mem_shadow_iff_insert_mem

Mathlib/Data/Finset/Preimage.lean

@@ -113,7 +113,7 @@ theorem preimage_subset {f : α ↪ β} {s : Finset β} {t : Finset α} (hs : s
 #align finset.preimage_subset Finset.preimage_subset
 
 theorem subset_map_iff {f : α ↪ β} {s : Finset β} {t : Finset α} :
-    s ⊆ t.map f ↔ ∃ u, u ⊆ t ∧ s = u.map f := by
+    s ⊆ t.map f ↔ ∃ u ⊆ t, s = u.map f := by
   classical
   simp_rw [← coe_subset, coe_map, subset_image_iff, map_eq_image, eq_comm]
 #align finset.subset_map_iff Finset.subset_map_iff

Mathlib/Data/Int/Order/Basic.lean

@@ -61,8 +61,8 @@ theorem abs_eq_natAbs : ∀ a : ℤ, |a| = natAbs a
 @[simp, norm_cast] lemma coe_natAbs (n : ℤ) : (n.natAbs : ℤ) = |n| := n.abs_eq_natAbs.symm
 #align int.coe_nat_abs Int.coe_natAbs
 
-lemma _root_.Nat.cast_natAbs {α : Type*} [AddGroupWithOne α] (n : ℤ) : (n.natAbs : α) = |n| :=
-  by rw [← coe_natAbs, Int.cast_ofNat]
+lemma _root_.Nat.cast_natAbs {α : Type*} [AddGroupWithOne α] (n : ℤ) : (n.natAbs : α) = |n| := by
+  rw [← coe_natAbs, Int.cast_ofNat]
 #align nat.cast_nat_abs Nat.cast_natAbs
 
 theorem natAbs_abs (a : ℤ) : natAbs |a| = natAbs a := by rw [abs_eq_natAbs]; rfl

Mathlib/Data/SetLike/Basic.lean

@@ -187,7 +187,7 @@ theorem coe_eq_coe {x y : p} : (x : B) = y ↔ x = y :=
 #align set_like.coe_eq_coe SetLike.coe_eq_coe
 
 -- Porting note: this is not necessary anymore due to the way coercions work
- #noalign set_like.coe_mk
+#noalign set_like.coe_mk
 
 @[simp]
 theorem coe_mem (x : p) : (x : B) ∈ p :=

Mathlib/FieldTheory/PurelyInseparable.lean

@@ -1005,8 +1005,8 @@ theorem IntermediateField.sepDegree_adjoin_eq_of_isAlgebraic_of_isPurelyInsepara
     rintro x ⟨y, hy⟩
     obtain ⟨n, z, hz⟩ := IsPurelyInseparable.pow_mem F q y
     refine ⟨n, algebraMap F M z, ?_⟩
-    rw [← IsScalarTower.algebraMap_apply, IsScalarTower.algebraMap_apply F E K, hz, ← hy, map_pow]
-    rfl
+    rw [← IsScalarTower.algebraMap_apply, IsScalarTower.algebraMap_apply F E K, hz, ← hy, map_pow,
+      AlgHom.toRingHom_eq_coe, IsScalarTower.coe_toAlgHom]
   have h := lift_sepDegree_mul_lift_sepDegree_of_isAlgebraic F E L
     (IsPurelyInseparable.isAlgebraic F E)
   rw [IsPurelyInseparable.sepDegree_eq_one F E, Cardinal.lift_one, one_mul] at h

Mathlib/GroupTheory/Perm/Basic.lean

@@ -630,8 +630,8 @@ variable [AddGroup α] (a b : α)
 #align equiv.zpow_add_left Equiv.zpow_addLeft
 
 @[simp] lemma zpow_addRight : ∀ (n : ℤ), Equiv.addRight a ^ n = Equiv.addRight (n • a)
-  | (Int.ofNat n) => by simp
-  | (Int.negSucc n) => by simp
+  | Int.ofNat n => by simp
+  | Int.negSucc n => by simp
 #align equiv.zpow_add_right Equiv.zpow_addRight
 
 end AddGroup
@@ -683,8 +683,8 @@ lemma zpow_mulLeft (n : ℤ) : Equiv.mulLeft a ^ n = Equiv.mulLeft (a ^ n) :=
 
 @[to_additive existing (attr := simp) zpow_addRight]
 lemma zpow_mulRight : ∀ n : ℤ, Equiv.mulRight a ^ n = Equiv.mulRight (a ^ n)
-  | (Int.ofNat n) => by simp
-  | (Int.negSucc n) => by simp
+  | Int.ofNat n => by simp
+  | Int.negSucc n => by simp
 #align equiv.zpow_mul_right Equiv.zpow_mulRight
 
 end Group
@@ -709,8 +709,8 @@ lemma BijOn.perm_pow : BijOn f s s → ∀ n : ℕ, BijOn (f ^ n) s s := by
 #align set.bij_on.perm_pow Set.BijOn.perm_pow
 
 lemma BijOn.perm_zpow (hf : BijOn f s s) : ∀ n : ℤ, BijOn (f ^ n) s s
-  | (Int.ofNat n) => hf.perm_pow n
-  | (Int.negSucc n) => (hf.perm_pow (n + 1)).perm_inv
+  | Int.ofNat n => hf.perm_pow n
+  | Int.negSucc n => (hf.perm_pow (n + 1)).perm_inv
 #align set.bij_on.perm_zpow Set.BijOn.perm_zpow
 
 end Set

Mathlib/Logic/Function/Basic.lean

@@ -596,18 +596,18 @@ lemma forall_update_iff (f : ∀a, β a) {a : α} {b : β a} (p : ∀a, β a →
 #align function.forall_update_iff Function.forall_update_iff
 
 theorem exists_update_iff (f : ∀ a, β a) {a : α} {b : β a} (p : ∀ a, β a → Prop) :
-    (∃ x, p x (update f a b x)) ↔ p a b ∨ ∃ (x : _) (_ : x ≠ a), p x (f x) := by
+    (∃ x, p x (update f a b x)) ↔ p a b ∨ ∃ x ≠ a, p x (f x) := by
   rw [← not_forall_not, forall_update_iff f fun a b ↦ ¬p a b]
   simp [-not_and, not_and_or]
 #align function.exists_update_iff Function.exists_update_iff
 
 theorem update_eq_iff {a : α} {b : β a} {f g : ∀ a, β a} :
-    update f a b = g ↔ b = g a ∧ ∀ (x) (_ : x ≠ a), f x = g x :=
+    update f a b = g ↔ b = g a ∧ ∀ x ≠ a, f x = g x :=
   funext_iff.trans <| forall_update_iff _ fun x y ↦ y = g x
 #align function.update_eq_iff Function.update_eq_iff
 
 theorem eq_update_iff {a : α} {b : β a} {f g : ∀ a, β a} :
-    g = update f a b ↔ g a = b ∧ ∀ (x) (_ : x ≠ a), g x = f x :=
+    g = update f a b ↔ g a = b ∧ ∀ x ≠ a, g x = f x :=
   funext_iff.trans <| forall_update_iff _ fun x y ↦ g x = y
 #align function.eq_update_iff Function.eq_update_iff
 

Mathlib/MeasureTheory/Integral/DominatedConvergence.lean

@@ -145,7 +145,7 @@ lemma hasSum_integral_of_summable_integral_norm {ι} [Countable ι] {F : ι →
   have (i : ι) : ∫⁻ (a : α), ‖F i a‖₊ ∂μ = ‖(∫ a : α, ‖F i a‖ ∂μ)‖₊ := by
     rw [lintegral_coe_eq_integral _ (hF_int i).norm, coe_nnreal_eq, coe_nnnorm,
       Real.norm_of_nonneg (integral_nonneg (fun a ↦ norm_nonneg (F i a)))]
-    rfl
+    simp only [coe_nnnorm]
   rw [funext this, ← ENNReal.coe_tsum]
   · apply coe_ne_top
   · simp_rw [← NNReal.summable_coe, coe_nnnorm]

Mathlib/MeasureTheory/Measure/NullMeasurable.lean

@@ -225,7 +225,7 @@ protected theorem insert [MeasurableSingletonClass (NullMeasurableSpace α μ)]
 #align measure_theory.null_measurable_set.insert MeasureTheory.NullMeasurableSet.insert
 
 theorem exists_measurable_superset_ae_eq (h : NullMeasurableSet s μ) :
-    ∃ t, t ⊇ s ∧ MeasurableSet t ∧ t =ᵐ[μ] s := by
+    ∃ t ⊇ s, MeasurableSet t ∧ t =ᵐ[μ] s := by
   rcases h with ⟨t, htm, hst⟩
   refine' ⟨t ∪ toMeasurable μ (s \ t), _, htm.union (measurableSet_toMeasurable _ _), _⟩
   · exact diff_subset_iff.1 (subset_toMeasurable _ _)
@@ -243,7 +243,7 @@ theorem compl_toMeasurable_compl_ae_eq (h : NullMeasurableSet s μ) : (toMeasura
 #align measure_theory.null_measurable_set.compl_to_measurable_compl_ae_eq MeasureTheory.NullMeasurableSet.compl_toMeasurable_compl_ae_eq
 
 theorem exists_measurable_subset_ae_eq (h : NullMeasurableSet s μ) :
-    ∃ t, t ⊆ s ∧ MeasurableSet t ∧ t =ᵐ[μ] s :=
+    ∃ t ⊆ s, MeasurableSet t ∧ t =ᵐ[μ] s :=
   ⟨(toMeasurable μ sᶜ)ᶜ, compl_subset_comm.2 <| subset_toMeasurable _ _,
     (measurableSet_toMeasurable _ _).compl, compl_toMeasurable_compl_ae_eq h⟩
 #align measure_theory.null_measurable_set.exists_measurable_subset_ae_eq MeasureTheory.NullMeasurableSet.exists_measurable_subset_ae_eq

Mathlib/MeasureTheory/Measure/Regular.lean

@@ -418,7 +418,7 @@ lemma of_restrict [OpensMeasurableSpace α] {μ : Measure α} {s : ℕ → Set 
     rw [← inter_iUnion, iUnion_disjointed, univ_subset_iff.mp h'', inter_univ]
   rcases ENNReal.exists_pos_sum_of_countable' (tsub_pos_iff_lt.2 hr).ne' ℕ with ⟨δ, δ0, hδε⟩
   rw [lt_tsub_iff_right, add_comm] at hδε
-  have : ∀ n, ∃ (U : _) (_ : U ⊇ A n), IsOpen U ∧ μ U < μ (A n) + δ n := by
+  have : ∀ n, ∃ U ⊇ A n, IsOpen U ∧ μ U < μ (A n) + δ n := by
     intro n
     have H₁ : ∀ t, μ.restrict (s n) t = μ (t ∩ s n) := fun t => restrict_apply' (hm n)
     have Ht : μ.restrict (s n) (A n) ≠ ∞ := by
@@ -470,7 +470,7 @@ theorem measurableSet_of_isOpen [OuterRegular μ] (H : InnerRegularWRT μ p IsOp
     have : 0 < μ univ := (bot_le.trans_lt hr).trans_le (measure_mono (subset_univ _))
     obtain ⟨K, -, hK, -⟩ : ∃ K, K ⊆ univ ∧ p K ∧ 0 < μ K := H isOpen_univ _ this
     simpa using hd hK isOpen_univ
-  obtain ⟨ε, hε, hεs, rfl⟩ : ∃ (ε : _) (_ : ε ≠ 0), ε + ε ≤ μ s ∧ r = μ s - (ε + ε) := by
+  obtain ⟨ε, hε, hεs, rfl⟩ : ∃ ε ≠ 0, ε + ε ≤ μ s ∧ r = μ s - (ε + ε) := by
     use (μ s - r) / 2
     simp [*, hr.le, ENNReal.add_halves, ENNReal.sub_sub_cancel, le_add_right, tsub_eq_zero_iff_le]
   rcases hs.exists_isOpen_diff_lt hμs hε with ⟨U, hsU, hUo, hUt, hμU⟩

Mathlib/MeasureTheory/Measure/Typeclasses.lean

@@ -1425,7 +1425,7 @@ variable [TopologicalSpace α] [MeasurableSpace α] {μ : Measure α} {s : Set 
 /-- If `s` is a compact set and `μ` is finite at `𝓝 x` for every `x ∈ s`, then `s` admits an open
 superset of finite measure. -/
 theorem exists_open_superset_measure_lt_top' (h : IsCompact s)
-    (hμ : ∀ x ∈ s, μ.FiniteAtFilter (𝓝 x)) : ∃ (U : _) (_ : U ⊇ s), IsOpen U ∧ μ U < ∞ := by
+    (hμ : ∀ x ∈ s, μ.FiniteAtFilter (𝓝 x)) : ∃ U ⊇ s, IsOpen U ∧ μ U < ∞ := by
   refine' IsCompact.induction_on h _ _ _ _
   · use ∅
     simp [Superset]
@@ -1443,7 +1443,7 @@ theorem exists_open_superset_measure_lt_top' (h : IsCompact s)
 /-- If `s` is a compact set and `μ` is a locally finite measure, then `s` admits an open superset of
 finite measure. -/
 theorem exists_open_superset_measure_lt_top (h : IsCompact s) (μ : Measure α)
-    [IsLocallyFiniteMeasure μ] : ∃ (U : _) (_ : U ⊇ s), IsOpen U ∧ μ U < ∞ :=
+    [IsLocallyFiniteMeasure μ] : ∃ U ⊇ s, IsOpen U ∧ μ U < ∞ :=
   h.exists_open_superset_measure_lt_top' fun x _ => μ.finiteAt_nhds x
 #align is_compact.exists_open_superset_measure_lt_top IsCompact.exists_open_superset_measure_lt_top
 
@@ -1493,13 +1493,13 @@ def MeasureTheory.Measure.finiteSpanningSetsInOpen [TopologicalSpace α] [SigmaC
     μ.FiniteSpanningSetsIn { K | IsOpen K } where
   set n := ((isCompact_compactCovering α n).exists_open_superset_measure_lt_top μ).choose
   set_mem n :=
-    ((isCompact_compactCovering α n).exists_open_superset_measure_lt_top μ).choose_spec.snd.1
+    ((isCompact_compactCovering α n).exists_open_superset_measure_lt_top μ).choose_spec.2.1
   finite n :=
-    ((isCompact_compactCovering α n).exists_open_superset_measure_lt_top μ).choose_spec.snd.2
+    ((isCompact_compactCovering α n).exists_open_superset_measure_lt_top μ).choose_spec.2.2
   spanning :=
     eq_univ_of_subset
       (iUnion_mono fun n =>
-        ((isCompact_compactCovering α n).exists_open_superset_measure_lt_top μ).choose_spec.fst)
+        ((isCompact_compactCovering α n).exists_open_superset_measure_lt_top μ).choose_spec.1)
       (iUnion_compactCovering α)
 #align measure_theory.measure.finite_spanning_sets_in_open MeasureTheory.Measure.finiteSpanningSetsInOpen