chore: tidy various files (#12213)

Mathlib/Algebra/Category/ModuleCat/Free.lean

@@ -113,8 +113,8 @@ theorem span_exact {β : Type*} {u : ι ⊕ β → S.X₂} (huv : u ∘ Sum.inl
   rw [← sub_add_cancel m m', ← hnm,]
   simp only [map_smul]
   have hn' : (Finsupp.sum cn fun a b ↦ b • S.f (v a)) =
-      (Finsupp.sum cn fun a b ↦ b • u (Sum.inl a)) :=
-    by congr; ext a b; change b • (S.f ∘ v) a = _; rw [← huv]; rfl
+      (Finsupp.sum cn fun a b ↦ b • u (Sum.inl a)) := by
+    congr; ext a b; rw [← Function.comp_apply (f := S.f), ← huv, Function.comp_apply]
   rw [hn']
   apply add_mem
   · rw [Finsupp.mem_span_range_iff_exists_finsupp]

Mathlib/Algebra/Homology/ExactSequence.lean

@@ -250,10 +250,12 @@ lemma exact_iff_δlast {n : ℕ} (S : ComposableArrows C (n + 2)) :
       exact h.exact n (by omega)
   · rintro ⟨h, h'⟩
     refine' Exact.mk (IsComplex.mk (fun i hi => _)) (fun i hi => _)
-    · obtain hi | rfl := LE.le.lt_or_eq (show i ≤ n by omega)
+    · simp only [add_le_add_iff_right, ge_iff_le] at hi
+      obtain hi | rfl := hi.lt_or_eq
       · exact h.toIsComplex.zero i
       · exact h'.toIsComplex.zero 0
-    · obtain hi | rfl := LE.le.lt_or_eq (show i ≤ n by omega)
+    · simp only [add_le_add_iff_right, ge_iff_le] at hi
+      obtain hi | rfl := hi.lt_or_eq
       · exact h.exact i
       · exact h'.exact 0
 

Mathlib/Algebra/Homology/Localization.lean

@@ -46,9 +46,9 @@ variable (C c)
 
 lemma HomologicalComplex.homologyFunctor_inverts_quasiIso (i : ι) :
     (quasiIso C c).IsInvertedBy (homologyFunctor C c i) := fun _ _ _ hf => by
-      rw [mem_quasiIso_iff] at hf
-      dsimp
-      infer_instance
+  rw [mem_quasiIso_iff] at hf
+  dsimp
+  infer_instance
 
 namespace HomologicalComplexUpToQuasiIso
 

Mathlib/Analysis/Asymptotics/SpecificAsymptotics.lean

@@ -13,7 +13,7 @@ import Mathlib.Analysis.NormedSpace.Basic
 # A collection of specific asymptotic results
 
 This file contains specific lemmas about asymptotics which don't have their place in the general
-theory developed in `Analysis.Asymptotics.Asymptotics`.
+theory developed in `Mathlib.Analysis.Asymptotics.Asymptotics`.
 -/
 
 

Mathlib/Analysis/Fourier/FourierTransformDeriv.lean

@@ -417,7 +417,6 @@ theorem iteratedDeriv_fourierIntegral {f : ℝ → E} {N : ℕ∞} {n : ℕ}
   congr with y
   suffices (-(2 * π * I)) ^ n • y ^ n • f y = (-(2 * π * I * y)) ^ n • f y by
     simpa [innerSL_apply _]
-  have : y ^ n • f y = ((y ^ n : ℝ) : ℂ) • f y := rfl
-  simp only [← neg_mul, this, smul_smul, mul_pow, ofReal_pow, mul_assoc]
+  simp only [← neg_mul, ← coe_smul, smul_smul, mul_pow, ofReal_pow, mul_assoc]
 
 end Real

Mathlib/Analysis/SpecialFunctions/Trigonometric/Bounds.lean

@@ -200,7 +200,7 @@ theorem le_tan {x : ℝ} (h1 : 0 ≤ x) (h2 : x < π / 2) : x ≤ tan x := by
 
 theorem cos_lt_one_div_sqrt_sq_add_one {x : ℝ} (hx1 : -(3 * π / 2) ≤ x) (hx2 : x ≤ 3 * π / 2)
     (hx3 : x ≠ 0) : cos x < (1 / √(x ^ 2 + 1) : ℝ) := by
-  suffices ∀ {y : ℝ}, 0 < y → y ≤ 3 * π / 2 → cos y < ↑1 / sqrt (y ^ 2 + 1) by
+  suffices ∀ {y : ℝ}, 0 < y → y ≤ 3 * π / 2 → cos y < 1 / sqrt (y ^ 2 + 1) by
     rcases lt_or_lt_iff_ne.mpr hx3.symm with ⟨h⟩
     · exact this h hx2
     · convert this (by linarith : 0 < -x) (by linarith) using 1

Mathlib/Combinatorics/SimpleGraph/Basic.lean

@@ -453,7 +453,7 @@ variable {G₁ G₂ : SimpleGraph V}
 `G.Adj`. This is the order embedding; for the edge set of a particular graph, see
 `SimpleGraph.edgeSet`.
 
-The way `edgeSet` is defined is such that `mem_edgeSet` is proved by `refl`.
+The way `edgeSet` is defined is such that `mem_edgeSet` is proved by `Iff.rfl`.
 (That is, `s(v, w) ∈ G.edgeSet` is definitionally equal to `G.Adj v w`.)
 -/
 -- Porting note: We need a separate definition so that dot notation works.

Mathlib/Data/Complex/Order.lean

@@ -101,9 +101,7 @@ theorem not_lt_zero_iff {z : ℂ} : ¬z < 0 ↔ 0 ≤ z.re ∨ z.im ≠ 0 :=
 #align complex.not_lt_zero_iff Complex.not_lt_zero_iff
 
 theorem eq_re_of_ofReal_le {r : ℝ} {z : ℂ} (hz : (r : ℂ) ≤ z) : z = z.re := by
-  apply Complex.ext
-  rfl
-  simp only [← (Complex.le_def.1 hz).2, Complex.zero_im, Complex.ofReal_im]
+  rw [eq_comm, ← conj_eq_iff_re, conj_eq_iff_im, ← (Complex.le_def.1 hz).2, Complex.ofReal_im]
 #align complex.eq_re_of_real_le Complex.eq_re_of_ofReal_le
 
 @[simp]

Mathlib/Data/Finset/Card.lean

@@ -668,7 +668,7 @@ theorem one_lt_card_iff : 1 < s.card ↔ ∃ a b, a ∈ s ∧ b ∈ s ∧ a ≠
 
 theorem one_lt_card_iff_nontrivial : 1 < s.card ↔ s.Nontrivial := by
   rw [← not_iff_not, not_lt, Finset.Nontrivial, ← Set.nontrivial_coe_sort,
-      not_nontrivial_iff_subsingleton, card_le_one_iff_subsingleton_coe]; rfl
+    not_nontrivial_iff_subsingleton, card_le_one_iff_subsingleton_coe, coe_sort_coe]
 
 @[deprecated] alias one_lt_card_iff_nontrivial_coe := one_lt_card_iff_nontrivial
 

Mathlib/Data/Finsupp/Defs.lean

@@ -231,8 +231,6 @@ theorem finite_support (f : α →₀ M) : Set.Finite (Function.support f) :=
   f.fun_support_eq.symm ▸ f.support.finite_toSet
 #align finsupp.finite_support Finsupp.finite_support
 
-/- ./././Mathport/Syntax/Translate/Basic.lean:632:2:
-  warning: expanding binder collection (a «expr ∉ » s) -/
 theorem support_subset_iff {s : Set α} {f : α →₀ M} :
     ↑f.support ⊆ s ↔ ∀ a ∉ s, f a = 0 := by
   simp only [Set.subset_def, mem_coe, mem_support_iff]; exact forall_congr' fun a => not_imp_comm
@@ -463,8 +461,6 @@ theorem support_eq_singleton {f : α →₀ M} {a : α} :
     fun h => h.2.symm ▸ support_single_ne_zero _ h.1⟩
 #align finsupp.support_eq_singleton Finsupp.support_eq_singleton
 
-/- ./././Mathport/Syntax/Translate/Basic.lean:632:2:
-  warning: expanding binder collection (b «expr ≠ » 0) -/
 theorem support_eq_singleton' {f : α →₀ M} {a : α} :
     f.support = {a} ↔ ∃ b ≠ 0, f = single a b :=
   ⟨fun h =>
@@ -477,8 +473,6 @@ theorem card_support_eq_one {f : α →₀ M} : card f.support = 1 ↔ ∃ a, f
   by simp only [card_eq_one, support_eq_singleton]
 #align finsupp.card_support_eq_one Finsupp.card_support_eq_one
 
-/- ./././Mathport/Syntax/Translate/Basic.lean:632:2:
-  warning: expanding binder collection (b «expr ≠ » 0) -/
 theorem card_support_eq_one' {f : α →₀ M} :
     card f.support = 1 ↔ ∃ a, ∃ b ≠ 0, f = single a b := by
   simp only [card_eq_one, support_eq_singleton']

Mathlib/FieldTheory/PurelyInseparable.lean

@@ -594,13 +594,14 @@ theorem eq_separableClosure (L : IntermediateField F E)
     [IsSeparable F L] [IsPurelyInseparable L E] : L = separableClosure F E :=
   le_antisymm (le_separableClosure F E L) (separableClosure_le F E L)
 
+open separableClosure in
 /-- If `E / F` is algebraic, then an intermediate field of `E / F` is equal to the separable closure
 of `F` in `E` if and only if it is separable over `F`, and `E` is purely inseparable
 over it. -/
 theorem eq_separableClosure_iff (halg : Algebra.IsAlgebraic F E) (L : IntermediateField F E) :
     L = separableClosure F E ↔ IsSeparable F L ∧ IsPurelyInseparable L E :=
-  ⟨by rintro rfl; exact ⟨separableClosure.isSeparable F E,
-    separableClosure.isPurelyInseparable F E halg⟩, fun ⟨_, _⟩ ↦ eq_separableClosure F E L⟩
+  ⟨by rintro rfl; exact ⟨isSeparable F E, isPurelyInseparable F E halg⟩,
+   fun ⟨_, _⟩ ↦ eq_separableClosure F E L⟩
 
 -- TODO: prove it
 set_option linter.unusedVariables false in
@@ -635,8 +636,8 @@ theorem isPurelyInseparable_adjoin_simple_iff_pow_mem (q : ℕ) [hF : ExpChar F
 if and only if for any `x ∈ S`, `x ^ (q ^ n)` is contained in `F` for some `n : ℕ`. -/
 theorem isPurelyInseparable_adjoin_iff_pow_mem (q : ℕ) [hF : ExpChar F q] {S : Set E} :
     IsPurelyInseparable F (adjoin F S) ↔ ∀ x ∈ S, ∃ n : ℕ, x ^ q ^ n ∈ (algebraMap F E).range := by
-  simp_rw [← le_perfectClosure_iff, adjoin_le_iff, ← mem_perfectClosure_iff_pow_mem q]
-  rfl
+  simp_rw [← le_perfectClosure_iff, adjoin_le_iff, ← mem_perfectClosure_iff_pow_mem q,
+    Set.le_iff_subset, Set.subset_def, SetLike.mem_coe]
 
 /-- A compositum of two purely inseparable extensions is purely inseparable. -/
 instance isPurelyInseparable_sup (L1 L2 : IntermediateField F E)
@@ -873,7 +874,7 @@ theorem adjoin_eq_of_isAlgebraic (halg : Algebra.IsAlgebraic F E) :
   rw [lift_top, lift_adjoin] at h
   haveI : IsScalarTower F S K := IsScalarTower.of_algebraMap_eq (congrFun rfl)
   rw [← h, ← map_eq_of_separableClosure_eq_bot F (separableClosure_eq_bot E K)]
-  rfl
+  simp only [coe_map, IsScalarTower.coe_toAlgHom', IntermediateField.algebraMap_apply]
 
 end separableClosure
 

Mathlib/GroupTheory/Coxeter/Basic.lean

@@ -93,7 +93,7 @@ namespace Relations
 
 /-- The relations corresponding to a Coxeter matrix. -/
 def ofMatrix : B × B → FreeGroup B :=
- Function.uncurry fun b₁ b₂ => (FreeGroup.of b₁ * FreeGroup.of b₂) ^ M b₁ b₂
+  Function.uncurry fun b₁ b₂ => (FreeGroup.of b₁ * FreeGroup.of b₂) ^ M b₁ b₂
 
 /-- The set of relations corresponding to a Coxeter matrix. -/
 def toSet : Set (FreeGroup B) :=
@@ -135,8 +135,7 @@ structure CoxeterSystem (W : Type*) [Group W]  where
 
 /-- A group is a Coxeter group if it admits a Coxeter system for some Coxeter matrix `M`. -/
 class IsCoxeterGroup (W : Type u) [Group W] : Prop where
-  nonempty_system : ∃ (B : Type u), ∃ (M : Matrix B B ℕ),
-    M.IsCoxeter ∧ Nonempty (CoxeterSystem M W)
+  nonempty_system : ∃ B : Type u, ∃ M : Matrix B B ℕ, M.IsCoxeter ∧ Nonempty (CoxeterSystem M W)
 
 namespace CoxeterSystem
 
@@ -180,19 +179,16 @@ theorem ofCoxeterGroup_apply {X : Type*} (D : Matrix X X ℕ) (x : X) :
 theorem map_relations_eq_reindex_relations (e : B ≃ B') :
     (MulEquiv.toMonoidHom (FreeGroup.freeGroupCongr e)) '' CoxeterGroup.Relations.toSet M =
     CoxeterGroup.Relations.toSet (reindex e e M) := by
-  simp [CoxeterGroup.Relations.toSet, CoxeterGroup.Relations.ofMatrix]
-  apply le_antisymm
-  · rw [Set.le_iff_subset]; intro _
-    simp only [Set.mem_image, Set.mem_range, Prod.exists, Function.uncurry_apply_pair,
-      forall_exists_index, and_imp]
-    intro _ hb b _ heq; rw [← heq]
-    use (e hb); use (e b); aesop
-  · rw [Set.le_iff_subset]; intro hb'
-    simp only [Set.mem_range, Prod.exists, Function.uncurry_apply_pair, Set.mem_image,
-      forall_exists_index]
-    intro b1' b2' heq; rw [← heq]
-    use (FreeGroup.freeGroupCongr e).symm hb'
-    exact ⟨by use (e.symm b1'); use (e.symm b2'); aesop, by aesop⟩
+  simp only [MulEquiv.coe_toMonoidHom, FreeGroup.freeGroupCongr_apply, CoxeterGroup.Relations.toSet,
+    CoxeterGroup.Relations.ofMatrix, reindex_apply, submatrix_apply]
+  ext x
+  simp only [Set.mem_image, Set.mem_range, Prod.exists, Function.uncurry_apply_pair]
+  constructor
+  · rintro ⟨x, ⟨a, b, rfl⟩, rfl⟩
+    use e a, e b
+    simp
+  · rintro ⟨a, b, h⟩
+    refine ⟨(FreeGroup.freeGroupCongr e).symm x, ⟨e.symm a, e.symm b, ?_⟩, ?_⟩ <;> aesop
 
 /-- Coxeter groups of isomorphic types are isomorphic. -/
 def equivCoxeterGroup (e : B ≃ B') : CoxeterGroup M ≃* CoxeterGroup (reindex e e M) :=

Mathlib/GroupTheory/Coxeter/Matrix.lean

@@ -50,8 +50,7 @@ abbrev Aₙ : Matrix (Fin n) (Fin n) ℕ :=
       else (if (j : ℕ) + 1 = i ∨ (i : ℕ) + 1 = j then 3 else 2)
 
 theorem AₙIsCoxeter : IsCoxeter (Aₙ n) where
-  symmetric := by
-    simp [Matrix.IsSymm]; aesop
+  symmetric := by simp only [Matrix.IsSymm]; aesop
 
 /-- The Coxeter matrix of family Bₙ.
 
@@ -68,7 +67,7 @@ abbrev Bₙ : Matrix (Fin n) (Fin n) ℕ :=
         else (if (j : ℕ) + 1 = i ∨ (i : ℕ) + 1 = j then 3 else 2))
 
 theorem BₙIsCoxeter : IsCoxeter (Bₙ n) where
-  symmetric := by simp [Matrix.IsSymm]; aesop
+  symmetric := by simp only [Matrix.IsSymm]; aesop
 
 /-- The Coxeter matrix of family Dₙ.
 
@@ -88,7 +87,7 @@ abbrev Dₙ : Matrix (Fin n) (Fin n) ℕ :=
         else (if (j : ℕ) + 1 = i ∨ (i : ℕ) + 1 = j then 3 else 2))
 
 theorem DₙIsCoxeter : IsCoxeter (Dₙ n) where
-  symmetric := by simp [Matrix.IsSymm]; aesop
+  symmetric := by simp only [Matrix.IsSymm]; aesop
 
 /-- The Coxeter matrix of m-indexed family I₂(m).
 
@@ -102,7 +101,7 @@ abbrev I₂ₘ (m : ℕ) : Matrix (Fin 2) (Fin 2) ℕ :=
   Matrix.of fun i j => if i = j then 1 else m + 2
 
 theorem I₂ₘIsCoxeter (m : ℕ) : IsCoxeter (I₂ₘ m) where
-  symmetric := by simp [Matrix.IsSymm]; aesop
+  symmetric := by simp only [Matrix.IsSymm]; aesop
 
 /-- The Coxeter matrix of system E₆.
 

Mathlib/LinearAlgebra/AffineSpace/ContinuousAffineEquiv.lean

@@ -35,8 +35,9 @@ open Function
 /-- A continuous affine equivalence, denoted `P₁ ≃ᵃL[k] P₂`, between two affine topological spaces
 is an affine equivalence such that forward and inverse maps are continuous. -/
 structure ContinuousAffineEquiv (k P₁ P₂ : Type*) {V₁ V₂ : Type*} [Ring k]
-  [AddCommGroup V₁] [Module k V₁] [AddTorsor V₁ P₁] [TopologicalSpace P₁]
-  [AddCommGroup V₂] [Module k V₂] [AddTorsor V₂ P₂] [TopologicalSpace P₂] extends P₁ ≃ᵃ[k] P₂ where
+    [AddCommGroup V₁] [Module k V₁] [AddTorsor V₁ P₁] [TopologicalSpace P₁]
+    [AddCommGroup V₂] [Module k V₂] [AddTorsor V₂ P₂] [TopologicalSpace P₂]
+    extends P₁ ≃ᵃ[k] P₂ where
   continuous_toFun : Continuous toFun := by continuity
   continuous_invFun : Continuous invFun := by continuity
 

Mathlib/LinearAlgebra/Matrix/ToLin.lean

@@ -706,8 +706,9 @@ theorem LinearMap.toMatrix_mul (f g : M₁ →ₗ[R] M₁) :
 
 lemma LinearMap.toMatrix_pow (f : M₁ →ₗ[R] M₁) (k : ℕ) :
     (toMatrix v₁ v₁ f) ^ k = toMatrix v₁ v₁ (f ^ k) := by
-  induction' k with k ih; simp
-  rw [pow_succ, pow_succ, ih, ← toMatrix_mul]
+  induction k with
+  | zero => simp
+  | succ k ih => rw [pow_succ, pow_succ, ih, ← toMatrix_mul]
 
 theorem Matrix.toLin_mul [Finite l] [DecidableEq m] (A : Matrix l m R) (B : Matrix m n R) :
     Matrix.toLin v₁ v₃ (A * B) = (Matrix.toLin v₂ v₃ A).comp (Matrix.toLin v₁ v₂ B) := by

Mathlib/LinearAlgebra/RootSystem/Basic.lean

@@ -188,9 +188,10 @@ lemma eq_of_pairing_pairing_eq_two [NoZeroSMulDivisors ℤ M] (i j : ι)
   set f : ℕ → M := fun n ↦ β + (2 * n : ℤ) • (α - β)
   have hf : ∀ n : ℕ, (sαβ^[n]) β = f n := by
     intro n
-    induction' n with n ih
-    · simp [f]
-    · simp only [f, α, β, sα, sβ, sαβ, iterate_succ', ih, hα, hβ, two_smul, smul_add,
+    induction n with
+    | zero => simp [f]
+    | succ n ih =>
+      simp only [f, α, β, sα, sβ, sαβ, iterate_succ', ih, hα, hβ, two_smul, smul_add,
         mul_add, add_smul, comp_apply, map_zsmul, zsmul_sub, map_add, neg_sub, map_neg,
         smul_neg, map_sub, Nat.cast_succ, mul_one, LinearEquiv.trans_apply,
         reflection_apply_self] -- v4.7.0-rc1 issues

Mathlib/LinearAlgebra/Trace.lean

@@ -302,7 +302,7 @@ theorem trace_conj' (f : M →ₗ[R] M) (e : M ≃ₗ[R] N) : trace R N (e.conj
     haveI := (Module.free_def R N).mpr ⟨_, ⟨(b.map e).reindex (e.toEquiv.image _)⟩⟩
     rw [e.conj_apply, trace_comp_comm', ← comp_assoc, LinearEquiv.comp_coe,
       LinearEquiv.self_trans_symm, LinearEquiv.refl_toLinearMap, id_comp]
-  · rw [trace, trace, dif_neg hM, dif_neg]; rfl
+  · rw [trace, trace, dif_neg hM, dif_neg ?_, zero_apply, zero_apply]
     rintro ⟨s, ⟨b⟩⟩
     exact hM ⟨s.image e.symm, ⟨(b.map e.symm).reindex
       ((e.symm.toEquiv.image s).trans (Equiv.Set.ofEq Finset.coe_image.symm))⟩⟩

Mathlib/MeasureTheory/Function/EssSup.lean

@@ -15,12 +15,12 @@ We define the essential supremum and infimum of a function `f : α → β` with
 almost everywhere.
 
 TODO: The essential supremum of functions `α → ℝ≥0∞` is used in particular to define the norm in
-the `L∞` space (see `MeasureTheory.Function.LpSpace`).
+the `L∞` space (see `Mathlib.MeasureTheory.Function.LpSpace`).
 
 There is a different quantity which is sometimes also called essential supremum: the least
 upper-bound among measurable functions of a family of measurable functions (in an almost-everywhere
 sense). We do not define that quantity here, which is simply the supremum of a map with values in
-`α →ₘ[μ] β` (see `MeasureTheory.Function.AEEqFun`).
+`α →ₘ[μ] β` (see `Mathlib.MeasureTheory.Function.AEEqFun`).
 
 ## Main definitions
 

Mathlib/MeasureTheory/Function/L2Space.lean

@@ -12,7 +12,7 @@ import Mathlib.MeasureTheory.Integral.SetIntegral
 /-! # `L^2` space
 
 If `E` is an inner product space over `𝕜` (`ℝ` or `ℂ`), then `Lp E 2 μ`
-(defined in `MeasureTheory.Function.LpSpace`)
+(defined in `Mathlib.MeasureTheory.Function.LpSpace`)
 is also an inner product space, with inner product defined as `inner f g = ∫ a, ⟪f a, g a⟫ ∂μ`.
 
 ### Main results

Mathlib/MeasureTheory/Group/FundamentalDomain.lean

@@ -875,8 +875,7 @@ local notation "π" => @Quotient.mk _ α_mod_G
   `U` of the quotient, `μ U = ν ((π ⁻¹' U) ∩ t)`. -/
 class QuotientMeasureEqMeasurePreimage (ν : Measure α := by volume_tac)
     (μ : Measure (Quotient α_mod_G)) : Prop where
-  projection_respects_measure' : ∀ (t : Set α) (_ : IsFundamentalDomain G t ν),
-    μ = (ν.restrict t).map π
+  projection_respects_measure' (t : Set α) : IsFundamentalDomain G t ν → μ = (ν.restrict t).map π
 
 attribute [to_additive]
   MeasureTheory.QuotientMeasureEqMeasurePreimage
@@ -904,9 +903,7 @@ an artificial way to generate a measure downstairs such that the pair satisfies
 lemma IsFundamentalDomain.quotientMeasureEqMeasurePreimage_quotientMeasure
     {s : Set α} (fund_dom_s : IsFundamentalDomain G s ν) :
     QuotientMeasureEqMeasurePreimage ν ((ν.restrict s).map π) where
-  projection_respects_measure' := by
-    intro t fund_dom_t
-    rw [fund_dom_s.quotientMeasure_eq _ fund_dom_t]
+  projection_respects_measure' t fund_dom_t := by rw [fund_dom_s.quotientMeasure_eq _ fund_dom_t]
 
 /-- One can prove `QuotientMeasureEqMeasurePreimage` by checking behavior with respect to a single
 fundamental domain. -/
@@ -1019,8 +1016,8 @@ sigma-finite measure, then it is itself `SigmaFinite`. -/
 @[to_additive MeasureTheory.instSigmaFiniteAddQuotientOrbitRelInstMeasurableSpaceToMeasurableSpace]
 instance [SigmaFinite (volume : Measure α)] [HasFundamentalDomain G α]
     (μ : Measure (Quotient α_mod_G)) [QuotientMeasureEqMeasurePreimage volume μ] :
-    SigmaFinite μ := by
-  exact QuotientMeasureEqMeasurePreimage.sigmaFiniteQuotient (ν := (volume : Measure α)) (μ := μ)
+    SigmaFinite μ :=
+  QuotientMeasureEqMeasurePreimage.sigmaFiniteQuotient (ν := (volume : Measure α)) (μ := μ)
 
 end QuotientMeasureEqMeasurePreimage
 

Mathlib/MeasureTheory/Integral/IntegralEqImproper.lean

@@ -761,8 +761,7 @@ theorem tendsto_zero_of_hasDerivAt_of_integrableOn_Ioi
     apply IntegrableAtFilter.eq_zero_of_tendsto this ?_ A
     intro s hs
     rcases mem_atTop_sets.1 hs with ⟨b, hb⟩
-    apply le_antisymm (le_top)
-    rw [← volume_Ici (a := b)]
+    rw [← top_le_iff, ← volume_Ici (a := b)]
     exact measure_mono hb
   rwa [B, ← Embedding.tendsto_nhds_iff] at A
   exact (Completion.uniformEmbedding_coe E).embedding
@@ -938,8 +937,8 @@ theorem tendsto_limUnder_of_hasDerivAt_of_integrableOn_Iic [CompleteSpace E]
   suffices ∃ a, Tendsto f atBot (𝓝 a) from tendsto_nhds_limUnder this
   let g := f ∘ (fun x ↦ -x)
   have hdg : ∀ x ∈ Ioi (-a), HasDerivAt g (-f' (-x)) x := by
-    intro x (hx : -a < x)
-    have : -x ∈ Iic a := by simp; linarith
+    intro x hx
+    have : -x ∈ Iic a := by simp only [mem_Iic, mem_Ioi, neg_le] at *; exact hx.le
     simpa using HasDerivAt.scomp x (hderiv (-x) this) (hasDerivAt_neg' x)
   have L : Tendsto g atTop (𝓝 (limUnder atTop g)) := by
     apply tendsto_limUnder_of_hasDerivAt_of_integrableOn_Ioi hdg

Mathlib/MeasureTheory/Measure/Haar/Quotient.lean

@@ -135,12 +135,11 @@ lemma MeasureTheory.QuotientMeasureEqMeasurePreimage.mulInvariantMeasure_quotien
     [hasFun : HasFundamentalDomain Γ.op G ν] [QuotientMeasureEqMeasurePreimage ν μ] :
     μ.IsMulLeftInvariant where
   map_mul_left_eq_self x := by
-    apply Measure.ext
-    intro A hA
+    ext A hA
     obtain ⟨x₁, h⟩ := @Quotient.exists_rep _ (QuotientGroup.leftRel Γ) x
     convert measure_preimage_smul x₁ μ A using 1
     · rw [← h, Measure.map_apply (measurable_const_mul _) hA]
-      rfl
+      simp [← MulAction.Quotient.coe_smul_out', ← Quotient.mk''_eq_mk]
     exact smulInvariantMeasure_quotient ν
 
 variable [IsMulLeftInvariant μ] [SigmaFinite μ]
@@ -247,6 +246,7 @@ theorem MeasureTheory.QuotientMeasureEqMeasurePreimage.haarMeasure_quotient [Loc
       ← fund_dom_s.measure_zero_of_invariant _ (fun g ↦ QuotientGroup.sound _ _ g) h]
     apply measure_mono
     refine interior_subset.trans ?_
+    rw [QuotientGroup.coe_mk']
     show (K : Set G) ⊆ π ⁻¹' (π '' K)
     exact subset_preimage_image π K
   · show ν (π ⁻¹' (π '' K) ∩ s) ≠ ⊤