chore: tidy various files (#17095)

Mathlib/Algebra/Algebra/Basic.lean

@@ -185,8 +185,7 @@ theorem End_algebraMap_isUnit_inv_apply_eq_iff {x : R}
     mpr := fun H =>
       H.symm ▸ by
         apply_fun ⇑h.unit.val using ((Module.End_isUnit_iff _).mp h).injective
-        erw [End_isUnit_apply_inv_apply_of_isUnit]
-        rfl }
+        simpa using End_isUnit_apply_inv_apply_of_isUnit h (x • m') }
 
 theorem End_algebraMap_isUnit_inv_apply_eq_iff' {x : R}
     (h : IsUnit (algebraMap R (Module.End S M) x)) (m m' : M) :
@@ -195,8 +194,7 @@ theorem End_algebraMap_isUnit_inv_apply_eq_iff' {x : R}
     mpr := fun H =>
       H.symm ▸ by
         apply_fun (↑h.unit : M → M) using ((Module.End_isUnit_iff _).mp h).injective
-        erw [End_isUnit_apply_inv_apply_of_isUnit]
-        rfl }
+        simpa using End_isUnit_apply_inv_apply_of_isUnit h (x • m') |>.symm }
 
 end
 

Mathlib/Algebra/Group/Subgroup/Basic.lean

@@ -69,7 +69,7 @@ Definitions in the file:
 * `MonoidHom.ker f` : the kernel of a group homomorphism `f` is the subgroup of elements `x : G`
   such that `f x = 1`
 
-* `MonoidHom.eq_locus f g` : given group homomorphisms `f`, `g`, the elements of `G` such that
+* `MonoidHom.eqLocus f g` : given group homomorphisms `f`, `g`, the elements of `G` such that
   `f x = g x` form a subgroup of `G`
 
 ## Implementation notes

Mathlib/Algebra/Lie/Subalgebra.lean

@@ -224,7 +224,7 @@ variable [Module R M]
 `L`, we may regard `M` as a Lie module of `L'` by restriction. -/
 instance lieModule [LieModule R L M] : LieModule R L' M where
   smul_lie t x m := by
-    rw [coe_bracket_of_module]; erw [smul_lie]; simp only [coe_bracket_of_module]
+    rw [coe_bracket_of_module, Submodule.coe_smul_of_tower, smul_lie, coe_bracket_of_module]
   lie_smul t x m := by simp only [coe_bracket_of_module, lie_smul]
 
 /-- An `L`-equivariant map of Lie modules `M → N` is `L'`-equivariant for any Lie subalgebra

Mathlib/Algebra/Module/Equiv/Basic.lean

@@ -122,7 +122,7 @@ protected theorem smul_def (f : M ≃ₗ[R] M) (a : M) : f • a = f a :=
 
 /-- `LinearEquiv.applyDistribMulAction` is faithful. -/
 instance apply_faithfulSMul : FaithfulSMul (M ≃ₗ[R] M) M :=
-  ⟨@fun _ _ ↦ LinearEquiv.ext⟩
+  ⟨LinearEquiv.ext⟩
 
 instance apply_smulCommClass [SMul S R] [SMul S M] [IsScalarTower S R M] :
     SMulCommClass S (M ≃ₗ[R] M) M where

Mathlib/Analysis/SpecialFunctions/Gamma/Basic.lean

@@ -553,8 +553,7 @@ lemma integral_rpow_mul_exp_neg_mul_Ioi {a r : ℝ} (ha : 0 < a) (hr : 0 < r) :
   convert integral_cpow_mul_exp_neg_mul_Ioi (by rwa [ofReal_re] : 0 < (a : ℂ).re) hr
   refine _root_.integral_ofReal.symm.trans <| setIntegral_congr measurableSet_Ioi (fun t ht ↦ ?_)
   norm_cast
-  rw [← ofReal_cpow (le_of_lt ht), RCLike.ofReal_mul]
-  rfl
+  simp_rw [← ofReal_cpow ht.le, RCLike.ofReal_mul, coe_algebraMap]
 
 open Lean.Meta Qq Mathlib.Meta.Positivity in
 /-- The `positivity` extension which identifies expressions of the form `Gamma a`. -/

Mathlib/Analysis/SpecialFunctions/Trigonometric/Bounds.lean

@@ -173,11 +173,9 @@ theorem lt_tan {x : ℝ} (h1 : 0 < x) (h2 : x < π / 2) : x < tan x := by
   let U := Ico 0 (π / 2)
   have intU : interior U = Ioo 0 (π / 2) := interior_Ico
   have half_pi_pos : 0 < π / 2 := div_pos pi_pos two_pos
-  have cos_pos : ∀ {y : ℝ}, y ∈ U → 0 < cos y := by
-    intro y hy
+  have cos_pos {y : ℝ} (hy : y ∈ U) : 0 < cos y := by
     exact cos_pos_of_mem_Ioo (Ico_subset_Ioo_left (neg_lt_zero.mpr half_pi_pos) hy)
-  have sin_pos : ∀ {y : ℝ}, y ∈ interior U → 0 < sin y := by
-    intro y hy
+  have sin_pos {y : ℝ} (hy : y ∈ interior U) : 0 < sin y := by
     rw [intU] at hy
     exact sin_pos_of_mem_Ioo (Ioo_subset_Ioo_right (div_le_self pi_pos.le one_le_two) hy)
   have tan_cts_U : ContinuousOn tan U := by
@@ -186,8 +184,7 @@ theorem lt_tan {x : ℝ} (h1 : 0 < x) (h2 : x < π / 2) : x < tan x := by
     simp only [mem_setOf_eq]
     exact (cos_pos hz).ne'
   have tan_minus_id_cts : ContinuousOn (fun y : ℝ => tan y - y) U := tan_cts_U.sub continuousOn_id
-  have deriv_pos : ∀ y : ℝ, y ∈ interior U → 0 < deriv (fun y' : ℝ => tan y' - y') y := by
-    intro y hy
+  have deriv_pos (y : ℝ) (hy : y ∈ interior U) : 0 < deriv (fun y' : ℝ => tan y' - y') y := by
     have := cos_pos (interior_subset hy)
     simp only [deriv_tan_sub_id y this.ne', one_div, gt_iff_lt, sub_pos]
     norm_cast

Mathlib/FieldTheory/Finiteness.lean

@@ -72,7 +72,7 @@ theorem coeSort_finsetBasisIndex [IsNoetherian K V] :
 /-- In a noetherian module over a division ring, there exists a finite basis.
 This is indexed by the `Finset` `IsNoetherian.finsetBasisIndex`.
 This is in contrast to the result `finite_basis_index (Basis.ofVectorSpace K V)`,
-which provides a set and a `Set.finite`.
+which provides a set and a `Set.Finite`.
 -/
 noncomputable def finsetBasis [IsNoetherian K V] : Basis (finsetBasisIndex K V) K V :=
   (Basis.ofVectorSpace K V).reindex (by rw [coeSort_finsetBasisIndex])

Mathlib/FieldTheory/Galois/Basic.lean

@@ -24,7 +24,7 @@ In this file we define Galois extensions as extensions which are both separable
 
 - `IntermediateField.fixingSubgroup_fixedField` : If `E/F` is finite dimensional (but not
   necessarily Galois) then `fixingSubgroup (fixedField H) = H`
-- `IntermediateField.fixedField_fixingSubgroup`: If `E/F` is finite dimensional and Galois
+- `IsGalois.fixedField_fixingSubgroup`: If `E/F` is finite dimensional and Galois
   then `fixedField (fixingSubgroup K) = K`
 
 Together, these two results prove the Galois correspondence.

Mathlib/GroupTheory/MonoidLocalization/Basic.lean

@@ -548,7 +548,7 @@ theorem mk'_spec' (x) (y : S) : f.toMap y * f.mk' x y = f.toMap x := by rw [mul_
 
 @[to_additive]
 theorem eq_mk'_iff_mul_eq {x} {y : S} {z} : z = f.mk' x y ↔ z * f.toMap y = f.toMap x :=
-  ⟨fun H ↦ by rw [H, mk'_spec], fun H ↦ by erw [mul_inv_right, H]⟩
+  ⟨fun H ↦ by rw [H, mk'_spec], fun H ↦ by rw [mk', mul_inv_right, H]⟩
 
 @[to_additive]
 theorem mk'_eq_iff_eq_mul {x} {y : S} {z} : f.mk' x y = z ↔ f.toMap x = z * f.toMap y := by
@@ -773,9 +773,7 @@ theorem lift_comp : (f.lift hg).comp f.toMap = g := by ext; exact f.lift_eq hg _
 @[to_additive (attr := simp)]
 theorem lift_of_comp (j : N →* P) : f.lift (f.isUnit_comp j) = j := by
   ext
-  rw [lift_spec]
-  show j _ = j _ * _
-  erw [← j.map_mul, sec_spec']
+  simp_rw [lift_spec, MonoidHom.comp_apply, ← j.map_mul, sec_spec']
 
 @[to_additive]
 theorem epic_of_localizationMap {j k : N →* P} (h : ∀ a, j.comp f.toMap a = k.comp f.toMap a) :
@@ -834,8 +832,8 @@ theorem lift_surjective_iff :
     obtain ⟨z, hz⟩ := H v
     obtain ⟨x, hx⟩ := f.surj z
     use x
-    rw [← hz, f.eq_mk'_iff_mul_eq.2 hx, lift_mk', mul_assoc, mul_comm _ (g ↑x.2)]
-    erw [IsUnit.mul_liftRight_inv (g.restrict S) hg, mul_one]
+    rw [← hz, f.eq_mk'_iff_mul_eq.2 hx, lift_mk', mul_assoc, mul_comm _ (g ↑x.2),
+      ← MonoidHom.restrict_apply, IsUnit.mul_liftRight_inv (g.restrict S) hg, mul_one]
   · intro H v
     obtain ⟨x, hx⟩ := H v
     use f.mk' x.1 x.2
@@ -1131,9 +1129,9 @@ of `AddCommMonoid`s, `k ∘ f` is a Localization map for `M` at `S`."]
 def ofMulEquivOfLocalizations (k : N ≃* P) : LocalizationMap S P :=
   (k.toMonoidHom.comp f.toMap).toLocalizationMap (fun y ↦ isUnit_comp f k.toMonoidHom y)
     (fun v ↦
-      let ⟨z, hz⟩ := k.toEquiv.surjective v
+      let ⟨z, hz⟩ := k.surjective v
       let ⟨x, hx⟩ := f.surj z
-      ⟨x, show v * k _ = k _ by rw [← hx, map_mul, ← hz]; rfl⟩)
+      ⟨x, show v * k _ = k _ by rw [← hx, map_mul, ← hz]⟩)
     fun x y ↦ (k.apply_eq_iff_eq.trans f.eq_iff_exists).1
 
 @[to_additive (attr := simp)]
@@ -1203,18 +1201,17 @@ def ofMulEquivOfDom {k : P ≃* M} (H : T.map k.toMonoidHom = S) : LocalizationM
       ⟨z, hz⟩)
     (fun z ↦
       let ⟨x, hx⟩ := f.surj z
-      let ⟨v, hv⟩ := k.toEquiv.surjective x.1
-      let ⟨w, hw⟩ := k.toEquiv.surjective x.2
-      ⟨(v, ⟨w, H' ▸ show k w ∈ S from hw.symm ▸ x.2.2⟩),
-        show z * f.toMap (k.toEquiv w) = f.toMap (k.toEquiv v) by erw [hv, hw, hx]⟩)
-    fun x y ↦
-    show f.toMap _ = f.toMap _ → _ by
-      erw [f.eq_iff_exists]
-      exact
-        fun ⟨c, hc⟩ ↦
-          let ⟨d, hd⟩ := k.toEquiv.surjective c
-          ⟨⟨d, H' ▸ show k d ∈ S from hd.symm ▸ c.2⟩, by
-            erw [← hd, ← map_mul k, ← map_mul k] at hc; exact k.toEquiv.injective hc⟩
+      let ⟨v, hv⟩ := k.surjective x.1
+      let ⟨w, hw⟩ := k.surjective x.2
+      ⟨(v, ⟨w, H' ▸ show k w ∈ S from hw.symm ▸ x.2.2⟩), by
+        simp_rw [MonoidHom.comp_apply, MulEquiv.toMonoidHom_eq_coe, MonoidHom.coe_coe, hv, hw, hx]⟩)
+    fun x y ↦ by
+      rw [MonoidHom.comp_apply, MonoidHom.comp_apply, MulEquiv.toMonoidHom_eq_coe,
+        MonoidHom.coe_coe, f.eq_iff_exists]
+      rintro ⟨c, hc⟩
+      let ⟨d, hd⟩ := k.surjective c
+      refine ⟨⟨d, H' ▸ show k d ∈ S from hd.symm ▸ c.2⟩, ?_⟩
+      rw [← hd, ← map_mul k, ← map_mul k] at hc; exact k.injective hc
 
 @[to_additive (attr := simp)]
 theorem ofMulEquivOfDom_apply {k : P ≃* M} (H : T.map k.toMonoidHom = S) (x) :

Mathlib/LinearAlgebra/LinearIndependent.lean

@@ -591,8 +591,7 @@ theorem LinearIndependent.units_smul {v : ι → M} (hv : LinearIndependent R v)
     exact (hgs i hi).symm ▸ zero_smul _ _
   · rw [← hsum, Finset.sum_congr rfl _]
     intros
-    erw [Pi.smul_apply, smul_assoc]
-    rfl
+    rw [Pi.smul_apply', smul_assoc, Units.smul_def]
 
 lemma LinearIndependent.eq_of_pair {x y : M} (h : LinearIndependent R ![x, y])
     {s t s' t' : R} (h' : s • x + t • y = s' • x + t' • y) : s = s' ∧ t = t' := by

Mathlib/Logic/Function/FiberPartition.lean

@@ -62,7 +62,7 @@ lemma fiber_nonempty (f : Y → Z) (a : Fiber f) : Set.Nonempty a.val := by
   rw [mem_iff_eq_image, ← map_preimage_eq_image]
 
 lemma map_preimage_eq_image_map {W : Type*} (f : Y → Z) (g : Z → W) (a : Fiber (g ∘ f)) :
-    g (f a.preimage) = a.image := by rw [← map_preimage_eq_image]; rfl
+    g (f a.preimage) = a.image := by rw [← map_preimage_eq_image, comp_apply]
 
 lemma image_eq_image_mk (f : Y → Z) (g : X → Y) (a : Fiber (f ∘ g)) :
     a.image = (Fiber.mk f (g (a.preimage _))).image := by

Mathlib/MeasureTheory/Function/LocallyIntegrable.lean

@@ -127,10 +127,10 @@ theorem LocallyIntegrableOn.aestronglyMeasurable [SecondCountableTopology X]
   rw [this, aestronglyMeasurable_iUnion_iff]
   exact fun i : ℕ => (hu i).aestronglyMeasurable
 
-/-- If `s` is either open, or closed, then `f` is locally integrable on `s` iff it is integrable on
-every compact subset contained in `s`. -/
+/-- If `s` is locally closed (e.g. open or closed), then `f` is locally integrable on `s` iff it is
+integrable on every compact subset contained in `s`. -/
 theorem locallyIntegrableOn_iff [LocallyCompactSpace X] (hs : IsLocallyClosed s) :
-    LocallyIntegrableOn f s μ ↔ ∀ (k : Set X), k ⊆ s → (IsCompact k → IntegrableOn f k μ) := by
+    LocallyIntegrableOn f s μ ↔ ∀ (k : Set X), k ⊆ s → IsCompact k → IntegrableOn f k μ := by
   refine ⟨fun hf k hk ↦ hf.integrableOn_compact_subset hk, fun hf x hx ↦ ?_⟩
   rcases hs with ⟨U, Z, hU, hZ, rfl⟩
   rcases exists_compact_subset hU hx.1 with ⟨K, hK, hxK, hKU⟩

Mathlib/MeasureTheory/Measure/SeparableMeasure.lean

@@ -32,7 +32,7 @@ of separability in the metric space made by constant indicators equipped with th
 
 ## Main definitions
 
-* `MeasureTheory.Measure.μ.MeasureDense 𝒜`: `𝒜` is a measure-dense family if it only contains
+* `MeasureTheory.Measure.MeasureDense μ 𝒜`: `𝒜` is a measure-dense family if it only contains
   measurable sets and if the following condition is satisfied: if `s` is measurable with finite
   measure, then for any `ε > 0` there exists `t ∈ 𝒜` such that `μ (s ∆ t) < ε `.
 * `MeasureTheory.IsSeparable`: A measure is separable if there exists a countable and
@@ -87,8 +87,7 @@ structure Measure.MeasureDense (μ : Measure X) (𝒜 : Set (Set X)) : Prop :=
   /-- Each set has to be measurable. -/
   measurable : ∀ s ∈ 𝒜, MeasurableSet s
   /-- Any measurable set can be approximated by sets in the family. -/
-  approx : ∀ s, MeasurableSet s → μ s ≠ ∞ → ∀ (ε : ℝ),
-    0 < ε → ∃ t ∈ 𝒜, μ (s ∆ t) < ENNReal.ofReal ε
+  approx : ∀ s, MeasurableSet s → μ s ≠ ∞ → ∀ ε : ℝ, 0 < ε → ∃ t ∈ 𝒜, μ (s ∆ t) < ENNReal.ofReal ε
 
 theorem Measure.MeasureDense.nonempty (h𝒜 : μ.MeasureDense 𝒜) : 𝒜.Nonempty := by
   rcases h𝒜.approx ∅ MeasurableSet.empty (by simp) 1 (by norm_num) with ⟨t, ht, -⟩
@@ -103,8 +102,8 @@ theorem Measure.MeasureDense.nonempty' (h𝒜 : μ.MeasureDense 𝒜) :
 
 /-- The set of measurable sets is measure-dense. -/
 theorem measureDense_measurableSet : μ.MeasureDense {s | MeasurableSet s} where
-  measurable := fun _ h ↦ h
-  approx := fun s hs _ ε ε_pos ↦ ⟨s, hs, by simpa⟩
+  measurable _ h := h
+  approx s hs _ ε ε_pos := ⟨s, hs, by simpa⟩
 
 /-- If a family of sets `𝒜` is measure-dense in `X`, then any measurable set with finite measure
 can be approximated by sets in `𝒜` with finite measure. -/
@@ -155,22 +154,20 @@ theorem Measure.MeasureDense.indicatorConstLp_subset_closure (h𝒜 : μ.Measure
 with finite measure. -/
 theorem Measure.MeasureDense.fin_meas (h𝒜 : μ.MeasureDense 𝒜) :
     μ.MeasureDense {s | s ∈ 𝒜 ∧ μ s ≠ ∞} where
-  measurable := fun s h ↦ h𝒜.measurable s h.1
-  approx := by
-    intro s ms hμs ε ε_pos
+  measurable s h := h𝒜.measurable s h.1
+  approx s ms hμs ε ε_pos := by
     rcases Measure.MeasureDense.fin_meas_approx h𝒜 ms hμs ε ε_pos with ⟨t, t_mem, hμt, hμst⟩
     exact ⟨t, ⟨t_mem, hμt⟩, hμst⟩
 
 /-- If a measurable space equipped with a finite measure is generated by an algebra of sets, then
 this algebra of sets is measure-dense. -/
 theorem Measure.MeasureDense.of_generateFrom_isSetAlgebra_finite [IsFiniteMeasure μ]
     (h𝒜 : IsSetAlgebra 𝒜) (hgen : m = MeasurableSpace.generateFrom 𝒜) : μ.MeasureDense 𝒜 where
-  measurable := fun s hs ↦ hgen ▸ measurableSet_generateFrom hs
-  approx := by
+  measurable s hs := hgen ▸ measurableSet_generateFrom hs
+  approx s ms := by
     -- We want to show that any measurable set can be approximated by sets in `𝒜`. To do so, it is
     -- enough to show that such sets constitute a `σ`-algebra containing `𝒜`. This is contained in
     -- the theorem `generateFrom_induction`.
-    intro s ms
     have : MeasurableSet s ∧ ∀ (ε : ℝ), 0 < ε → ∃ t ∈ 𝒜, (μ (s ∆ t)).toReal < ε := by
       apply generateFrom_induction
         (p := fun s ↦ MeasurableSet s ∧ ∀ (ε : ℝ), 0 < ε → ∃ t ∈ 𝒜, (μ (s ∆ t)).toReal < ε)
@@ -220,14 +217,14 @@ theorem Measure.MeasureDense.of_generateFrom_isSetAlgebra_finite [IsFiniteMeasur
                 apply _root_.add_lt_add
                 · rw [measure_diff (h_fin := measure_ne_top _ _),
                     toReal_sub_of_le (ha := measure_ne_top _ _)]
-                  apply lt_of_le_of_lt (sub_le_dist ..)
-                  simp only [Finset.mem_range, Nat.lt_add_one_iff]
-                  exact (dist_comm (α := ℝ) .. ▸ hN N (le_refl N))
-                  exact (measure_mono <| iUnion_subset <|
-                    fun i ↦ iUnion_subset (fun _ ↦ subset_iUnion f i))
-                  exact iUnion_subset <| fun i ↦ iUnion_subset (fun _ ↦ subset_iUnion f i)
-                  exact MeasurableSet.biUnion (countable_coe_iff.1 inferInstance)
-                    (fun n _ ↦ (hf n).1.nullMeasurableSet)
+                  · apply lt_of_le_of_lt (sub_le_dist ..)
+                    simp only [Finset.mem_range, Nat.lt_add_one_iff]
+                    exact (dist_comm (α := ℝ) .. ▸ hN N (le_refl N))
+                  · exact measure_mono <| iUnion_subset <|
+                      fun i ↦ iUnion_subset fun _ ↦ subset_iUnion f i
+                  · exact iUnion_subset <| fun i ↦ iUnion_subset (fun _ ↦ subset_iUnion f i)
+                  · exact MeasurableSet.biUnion (countable_coe_iff.1 inferInstance)
+                      (fun n _ ↦ (hf n).1.nullMeasurableSet)
                 · calc
                     (μ ((⋃ n ∈ (Finset.range (N + 1)), f n) ∆
                     (⋃ n ∈ (Finset.range (N + 1)), g ↑n))).toReal
@@ -257,18 +254,17 @@ theorem Measure.MeasureDense.of_generateFrom_isSetAlgebra_sigmaFinite (h𝒜 : I
     (S : μ.FiniteSpanningSetsIn 𝒜) (hgen : m = MeasurableSpace.generateFrom 𝒜) :
     μ.MeasureDense 𝒜 where
   measurable s hs := hgen ▸ measurableSet_generateFrom hs
-  approx := by
+  approx s ms hμs ε ε_pos := by
     -- We use partial unions of (Sₙ) to get a monotone family spanning `X`.
     let T := Accumulate S.set
-    have T_mem : ∀ n, T n ∈ 𝒜 := fun n ↦ by
+    have T_mem (n) : T n ∈ 𝒜 := by
       simpa using h𝒜.biUnion_mem {k | k ≤ n}.toFinset (fun k _ ↦ S.set_mem k)
-    have T_finite : ∀ n, μ (T n) < ∞ := fun n ↦ by
+    have T_finite (n) : μ (T n) < ∞ := by
       simpa using measure_biUnion_lt_top {k | k ≤ n}.toFinset.finite_toSet
         (fun k _ ↦ S.finite k)
     have T_spanning : ⋃ n, T n = univ := S.spanning ▸ iUnion_accumulate
     -- We use the fact that we already know this is true for finite measures. As `⋃ n, T n = X`,
     -- we have that `μ ((T n) ∩ s) ⟶ μ s`.
-    intro s ms hμs ε ε_pos
     have mono : Monotone (fun n ↦ (T n) ∩ s) := fun m n hmn ↦ inter_subset_inter_left s
         (biUnion_subset_biUnion_left fun k hkm ↦ Nat.le_trans hkm hmn)
     have := tendsto_measure_iUnion_atTop (μ := μ) mono
@@ -423,15 +419,14 @@ instance Lp.SecondCountableTopology [IsSeparable μ] [TopologicalSpace.Separable
   -- constant indicators with support in `𝒜₀`, and is denoted `D`. To make manipulations easier,
   -- we define the function `key` which given an integer `n` and two families of `n` elements
   -- in `u` and `𝒜₀` associates the corresponding sum.
-  let key : (n : ℕ) → (Fin n → u) → (Fin n → 𝒜₀) → (Lp E p μ) :=
-    fun n d s ↦ ∑ i, indicatorConstLp p (h𝒜₀.measurable (s i) (Subtype.mem (s i)))
-      (s i).2.2 (d i : E)
+  let key (n : ℕ) (d : Fin n → u) (s : Fin n → 𝒜₀) : (Lp E p μ) :=
+    ∑ i, indicatorConstLp p (h𝒜₀.measurable (s i) (Subtype.mem (s i))) (s i).2.2 (d i : E)
   let D := {s : Lp E p μ | ∃ n d t, s = key n d t}
   refine ⟨D, ?_, ?_⟩
   · -- Countability directly follows from countability of `u` and `𝒜₀`. The function `f` below
     -- is the uncurryfied version of `key`, which is easier to manipulate as countability of the
     -- domain is automatically infered.
-    let f : (Σ n : ℕ, (Fin n → u) × (Fin n → 𝒜₀)) → Lp E p μ := fun nds ↦ key nds.1 nds.2.1 nds.2.2
+    let f (nds : Σ n : ℕ, (Fin n → u) × (Fin n → 𝒜₀)) : Lp E p μ := key nds.1 nds.2.1 nds.2.2
     have := count_𝒜₀.to_subtype
     have := countable_u.to_subtype
     have : D ⊆ range f := by

Mathlib/NumberTheory/NumberField/CanonicalEmbedding/Basic.lean

@@ -613,7 +613,7 @@ theorem mem_span_latticeBasis (x : (mixedSpace K)) :
   rfl
 
 theorem span_latticeBasis :
-    (Submodule.span ℤ (Set.range (latticeBasis K))) = (mixedEmbedding.integerLattice K) :=
+    Submodule.span ℤ (Set.range (latticeBasis K)) = mixedEmbedding.integerLattice K :=
   Submodule.ext_iff.mpr (mem_span_latticeBasis K)
 
 instance : DiscreteTopology (mixedEmbedding.integerLattice K) := by