chore: tidy various files (#34610)

Author: Ruben-VandeVelde

Archive/Examples/Kuratowski.lean

@@ -191,7 +191,7 @@ theorem kc_fourteenSet : k fourteenSetᶜ = (Ioo 0 1 ∪ Ioo 1 2)ᶜ := by
 
 theorem kck_fourteenSet : k (k fourteenSet)ᶜ = (Ioo 0 2 ∪ Ioo 4 5)ᶜ := by
   rw [closure_compl, k_fourteenSet,
-    interior_union_of_disjoint_closure, interior_union_of_disjoint_closure] <;>
+    interior_union_of_disjoint_closure, interior_union_of_disjoint_closure]
   all_goals
      simp [-union_singleton, disjoint_iff_inter_eq_empty, union_inter_distrib_right, Icc_inter_Icc]
   all_goals norm_num

Mathlib/Algebra/Algebra/Subalgebra/Directed.lean

@@ -29,23 +29,22 @@ variable (S : Subalgebra R A)
 
 variable {ι : Type*} [Nonempty ι] {K : ι → Subalgebra R A}
 
-theorem coe_iSup_of_directed (dir : Directed (· ≤ ·) K) : ↑(iSup K) = ⋃ i, (K i : Set A) :=
+theorem coe_iSup_of_directed (dir : Directed (· ≤ ·) K) : ↑(iSup K) = ⋃ i, (K i : Set A) := by
   let s : Subalgebra R A :=
     { __ := Subsemiring.copy _ _ (Subsemiring.coe_iSup_of_directed dir).symm
       algebraMap_mem' := fun _ ↦ Set.mem_iUnion.2
         ⟨Classical.arbitrary ι, Subalgebra.algebraMap_mem _ _⟩ }
   have : iSup K = s := le_antisymm
     (iSup_le fun i ↦ le_iSup (fun i ↦ (K i : Set A)) i) (Set.iUnion_subset fun _ ↦ le_iSup K _)
-  this.symm ▸ rfl
+  simp [this, s]
 
 variable (K)
 
 /-- Define an algebra homomorphism on a directed supremum of subalgebras by defining
 it on each subalgebra, and proving that it agrees on the intersection of subalgebras. -/
 noncomputable def iSupLift (dir : Directed (· ≤ ·) K) (f : ∀ i, K i →ₐ[R] B)
     (hf : ∀ (i j : ι) (h : K i ≤ K j), f i = (f j).comp (inclusion h))
-    (T : Subalgebra R A) (hT : T ≤ iSup K) : ↥T →ₐ[R] B :=
-by
+    (T : Subalgebra R A) (hT : T ≤ iSup K) : ↥T →ₐ[R] B := by
   let compat :
       ∀ (i j) (x : A) (hxi : x ∈ (K i : Set A)) (hxj : x ∈ (K j : Set A)),
         f i ⟨x, hxi⟩ = f j ⟨x, hxj⟩ := by
@@ -85,7 +84,7 @@ theorem iSupLift_inclusion {dir : Directed (· ≤ ·) K} {f : ∀ i, K i →ₐ
     iSupLift K dir f hf T hT (inclusion h x) = f i x := by
   dsimp [iSupLift, inclusion]
   rw [Set.iUnionLift_inclusion]
-  exact SetLike.coe_subset_coe.mpr fun ⦃x⦄ a ↦ hT (h a)
+  exact SetLike.coe_subset_coe.mpr <| h.trans hT
 
 @[simp]
 theorem iSupLift_comp_inclusion {dir : Directed (· ≤ ·) K} {f : ∀ i, K i →ₐ[R] B}

Mathlib/Algebra/Group/Irreducible/Indecomposable.lean

@@ -230,7 +230,6 @@ open Submonoid in
 lemma IsMulIndecomposable.apply_ne_one_iff_mem_closure
     [Finite ι] [InvolutiveInv ι] [CommGroup S] [IsOrderedMonoid S]
     (v : ι → G) (f : G →* S) (i : ι) (hi : v i ≠ 1) (hi' : v i⁻¹ = (v i)⁻¹) :
-    f (v i) ≠ 1 ↔ v i ∈ closure (v '' baseOf v f) ∨
-                 (v i)⁻¹ ∈ closure (v '' baseOf v f) :=
+    f (v i) ≠ 1 ↔ v i ∈ closure (v '' baseOf v f) ∨ (v i)⁻¹ ∈ closure (v '' baseOf v f) :=
   ⟨fun h ↦ mem_or_inv_mem_closure_baseOf v f i h hi',
     apply_ne_one_of_mem_or_inv_mem_closure v f (baseOf v f) (baseOf_subset_one_lt v f) i hi hi'⟩

Mathlib/Algebra/Module/FinitePresentation.lean

@@ -496,7 +496,7 @@ lemma Module.FinitePresentation.exists_notMem_bijective [Module.Finite R M]
     (hf : Function.Bijective (IsLocalizedModule.map p.primeCompl fM fN f)) :
     ∃ (g : R), g ∉ p ∧ Function.Bijective (LocalizedModule.map (Submonoid.powers g) f) := by
   obtain ⟨g, hg, h⟩ := exists_bijective_map_powers p.primeCompl fM fN f hf
-  exact ⟨g, hg, h g (by rfl)⟩
+  exact ⟨g, hg, h g dvd_rfl⟩
 
 open IsLocalizedModule in
 /--

Mathlib/Algebra/Module/Torsion/Basic.lean

@@ -165,8 +165,7 @@ variable (R M : Type*) [CommSemiring R] [AddCommMonoid M] [Module R M]
   `a • x = 0`. -/
 @[simps!]
 def torsionBy (a : R) : Submodule R M :=
-  -- Porting note (https://github.com/leanprover-community/mathlib4/issues/11036): broken dot notation on LinearMap.ker https://github.com/leanprover/lean4/issues/1629
-  LinearMap.ker (DistribSMul.toLinearMap R M a)
+  (DistribSMul.toLinearMap R M a).ker
 
 /-- The submodule containing all elements `x` of `M` such that `a • x = 0` for all `a` in `s`. -/
 @[simps!]
@@ -233,7 +232,7 @@ end Defs
 lemma isSMulRegular_iff_torsionBy_eq_bot {R} (M : Type*)
     [CommRing R] [AddCommGroup M] [Module R M] (r : R) :
     IsSMulRegular M r ↔ Submodule.torsionBy R M r = ⊥ :=
-  Iff.symm (DistribSMul.toLinearMap R M r).ker_eq_bot
+  (DistribSMul.toLinearMap R M r).ker_eq_bot.symm
 
 variable {R M : Type*}
 

Mathlib/Analysis/InnerProductSpace/Coalgebra.lean

@@ -121,7 +121,8 @@ noncomputable abbrev ringOfCoalgebra :
     simp_rw [AlgebraOfCoalgebra.mul_def, ← rTensor_tmul, ← comp_apply, ← adjoint_rTensor,
       ← adjoint_comp, ← coassoc_symm, adjoint_comp, adjoint_lTensor, comp_apply,
       ← toLinearEquiv_assocIsometry, ← toLinearEquiv_symm, adjoint_toLinearMap_eq_symm]
-    rfl
+    simp only [symm_symm, toLinearEquiv_assocIsometry, LinearEquiv.coe_coe, assoc_tmul,
+      lTensor_tmul]
   one := adjoint (counit (R := 𝕜) (A := E)) 1
   one_mul x := by
     dsimp [OfNat.ofNat]
@@ -164,13 +165,13 @@ noncomputable abbrev algebraOfCoalgebra : Algebra 𝕜 E where
       ← toLinearMap_symm_rid, ← toLinearMap_symm_lid, ← comm_trans_lid,
       ← toLinearEquiv_commIsometry, ← toLinearEquiv_lidIsometry, ← toLinearEquiv_trans,
       ← toLinearEquiv_symm, adjoint_toLinearMap_eq_symm]
-    rfl
+    simp
   smul_def' r x := by
     dsimp
     simp_rw [← rTensor_tmul, ← adjoint_rTensor, ← comp_apply, ← adjoint_comp,
       rTensor_counit_comp_comul, ← toLinearMap_symm_lid, ← toLinearEquiv_lidIsometry,
       ← toLinearEquiv_symm, adjoint_toLinearMap_eq_symm]
-    rfl
+    simp
 
 end algebraOfCoalgebra
 end InnerProductSpace

Mathlib/Analysis/InnerProductSpace/Orthogonal.lean

@@ -15,7 +15,7 @@ public import Mathlib.Topology.Algebra.Module.ClosedSubmodule
 In this file, the `orthogonal` complement of a submodule `K` is defined, and basic API established.
 We make duplicates for `Submodule` and `ClosedSubmodule`.
 Some of the more subtle results about the orthogonal complement are delayed to
-`Analysis.InnerProductSpace.Projection`.
+`Mathlib/Analysis/InnerProductSpace/Projection/`.
 
 See also `BilinForm.orthogonal` for orthogonality with respect to a general bilinear form.
 
@@ -125,11 +125,7 @@ lemma map_orthogonal (f : E →ₗᵢ[𝕜] F) :
   simp only [Submodule.ext_iff, mem_map, mem_orthogonal, forall_exists_index, and_imp,
     forall_apply_eq_imp_iff₂, mem_inf, mem_map, LinearMap.mem_range,
     LinearIsometry.coe_toLinearMap]
-  refine fun x ↦ ⟨?_, ?_⟩
-  · rintro ⟨x, hx, rfl⟩
-    refine ⟨by simpa using hx, x, rfl⟩
-  · rintro ⟨hx, x, rfl⟩
-    refine ⟨x, by simpa using hx, rfl⟩
+  grind [LinearIsometry.inner_map_map]
 
 lemma map_orthogonal_equiv (f : E ≃ₗᵢ[𝕜] F) :
     Kᗮ.map (f.toLinearEquiv : E →ₗ[𝕜] F) = (K.map (f.toLinearEquiv : E →ₗ[𝕜] F))ᗮ := by

Mathlib/Analysis/Meromorphic/Basic.lean

@@ -654,7 +654,7 @@ lemma zpow {f : 𝕜 → 𝕜'} {n : ℤ} (hf : Meromorphic f) : Meromorphic (f
 
 @[fun_prop]
 protected lemma deriv [CompleteSpace E] (hf : Meromorphic f) : Meromorphic (deriv f) :=
-    fun x ↦ (hf x).deriv
+  fun x ↦ (hf x).deriv
 
 @[fun_prop]
 lemma iterated_deriv [CompleteSpace E] {n : ℕ} (hf : Meromorphic f) :

Mathlib/Analysis/Normed/Operator/BoundedLinearMaps.lean

@@ -123,8 +123,7 @@ theorem snd : IsBoundedLinearMap 𝕜 fun x : E × F => x.2 := by
   exact le_max_right _ _
 
 theorem smul {𝕜' : Type*} (c : 𝕜') [SeminormedRing 𝕜'] [Module 𝕜' F] [IsBoundedSMul 𝕜' F]
-  [SMulCommClass 𝕜 𝕜' F]
-  (hf : IsBoundedLinearMap 𝕜 f) : IsBoundedLinearMap 𝕜 (c • f) :=
+    [SMulCommClass 𝕜 𝕜' F] (hf : IsBoundedLinearMap 𝕜 f) : IsBoundedLinearMap 𝕜 (c • f) :=
   let ⟨hlf, M, _, hM⟩ := hf
   (c • hlf.mk' f).isLinear.with_bound (‖c‖ * M) fun x =>
     calc
@@ -313,10 +312,9 @@ variable {f g : E → F}
 
 /-- A map between normed spaces is linear and continuous if and only if it is bounded. -/
 theorem isLinearMap_and_continuous_iff_isBoundedLinearMap (f : E → F) :
-    IsLinearMap 𝕜 f ∧ Continuous f ↔ IsBoundedLinearMap 𝕜 f :=
-  ⟨fun ⟨hlin, hcont⟩ ↦ ContinuousLinearMap.isBoundedLinearMap
-      ⟨⟨⟨f, IsLinearMap.map_add hlin⟩, IsLinearMap.map_smul hlin⟩, hcont⟩,
-        fun h_bdd ↦ ⟨h_bdd.toIsLinearMap, h_bdd.continuous⟩⟩
+    IsLinearMap 𝕜 f ∧ Continuous f ↔ IsBoundedLinearMap 𝕜 f where
+  mp | ⟨hlin, hcont⟩ => ContinuousLinearMap.isBoundedLinearMap ⟨hlin.mk' _, hcont⟩
+  mpr h_bdd := ⟨h_bdd.toIsLinearMap, h_bdd.continuous⟩
 
 end IsBoundedLinearMap
 

Mathlib/Analysis/SpecialFunctions/Gaussian/GaussianIntegral.lean

@@ -71,7 +71,7 @@ theorem integrableOn_rpow_mul_exp_neg_rpow {p s : ℝ} (hs : -1 < s) (hp : 1 ≤
       · refine (intervalIntegrable_iff_integrableOn_Icc_of_le zero_le_one).mp ?_
         exact intervalIntegral.intervalIntegrable_rpow' hs
       · intro x _
-        change ContinuousWithinAt ((fun x => exp (-x)) ∘ (fun x => x ^ p)) (Icc 0 1) x
+        rw [← Function.comp_def (fun x => exp (-x)) (· ^ p)]
         refine ContinuousAt.comp_continuousWithinAt (h_exp _) ?_
         exact continuousWithinAt_id.rpow_const (Or.inr (le_of_lt (lt_trans zero_lt_one hp)))
     · have h_rpow : ∀ (x r : ℝ), x ∈ Ici 1 → ContinuousWithinAt (fun x => x ^ r) (Ici 1) x := by
@@ -80,7 +80,7 @@ theorem integrableOn_rpow_mul_exp_neg_rpow {p s : ℝ} (hs : -1 < s) (hp : 1 ≤
         exact ne_of_gt (lt_of_lt_of_le zero_lt_one hx)
       refine integrable_of_isBigO_exp_neg (by simp : (0 : ℝ) < 1 / 2)
         (ContinuousOn.mul (fun x hx => h_rpow x s hx) (fun x hx => ?_)) (IsLittleO.isBigO ?_)
-      · change ContinuousWithinAt ((fun x => exp (-x)) ∘ (fun x => x ^ p)) (Ici 1) x
+      · rw [← Function.comp_def (fun x => exp (-x)) (· ^ p)]
         exact ContinuousAt.comp_continuousWithinAt (h_exp _) (h_rpow x p hx)
       · convert rpow_mul_exp_neg_mul_rpow_isLittleO_exp_neg s hp (by simp : (0 : ℝ) < 1) using 3
         rw [neg_mul, one_mul]