diff --git a/Mathlib.lean b/Mathlib.lean
index 2291d8b5abd02..34323cf452fa0 100644
--- a/Mathlib.lean
+++ b/Mathlib.lean
@@ -362,6 +362,7 @@ import Mathlib.Algebra.Module.Bimodule
 import Mathlib.Algebra.Module.CharacterModule
 import Mathlib.Algebra.Module.DedekindDomain
 import Mathlib.Algebra.Module.Equiv
+import Mathlib.Algebra.Module.FinitePresentation
 import Mathlib.Algebra.Module.GradedModule
 import Mathlib.Algebra.Module.Hom
 import Mathlib.Algebra.Module.Injective
@@ -1130,6 +1131,7 @@ import Mathlib.CategoryTheory.Adjunction.Mates
 import Mathlib.CategoryTheory.Adjunction.Opposites
 import Mathlib.CategoryTheory.Adjunction.Over
 import Mathlib.CategoryTheory.Adjunction.Reflective
+import Mathlib.CategoryTheory.Adjunction.Restrict
 import Mathlib.CategoryTheory.Adjunction.Whiskering
 import Mathlib.CategoryTheory.Balanced
 import Mathlib.CategoryTheory.Bicategory.Adjunction
diff --git a/Mathlib/Algebra/BigOperators/Associated.lean b/Mathlib/Algebra/BigOperators/Associated.lean
index a7fd5512244e4..46a96e3979ff3 100644
--- a/Mathlib/Algebra/BigOperators/Associated.lean
+++ b/Mathlib/Algebra/BigOperators/Associated.lean
@@ -91,15 +91,15 @@ theorem Multiset.prod_primes_dvd [CancelCommMonoidWithZero α]
     apply mul_dvd_mul_left a
     refine induct _ (fun a ha => h a (Multiset.mem_cons_of_mem ha)) (fun b b_in_s => ?_)
       fun a => (Multiset.countP_le_of_le _ (Multiset.le_cons_self _ _)).trans (uniq a)
-    · have b_div_n := div b (Multiset.mem_cons_of_mem b_in_s)
-      have a_prime := h a (Multiset.mem_cons_self a s)
-      have b_prime := h b (Multiset.mem_cons_of_mem b_in_s)
-      refine' (b_prime.dvd_or_dvd b_div_n).resolve_left fun b_div_a => _
-      have assoc := b_prime.associated_of_dvd a_prime b_div_a
-      have := uniq a
-      rw [Multiset.countP_cons_of_pos _ (Associated.refl _), Nat.succ_le_succ_iff, ← not_lt,
-        Multiset.countP_pos] at this
-      exact this ⟨b, b_in_s, assoc.symm⟩
+    have b_div_n := div b (Multiset.mem_cons_of_mem b_in_s)
+    have a_prime := h a (Multiset.mem_cons_self a s)
+    have b_prime := h b (Multiset.mem_cons_of_mem b_in_s)
+    refine' (b_prime.dvd_or_dvd b_div_n).resolve_left fun b_div_a => _
+    have assoc := b_prime.associated_of_dvd a_prime b_div_a
+    have := uniq a
+    rw [Multiset.countP_cons_of_pos _ (Associated.refl _), Nat.succ_le_succ_iff, ← not_lt,
+      Multiset.countP_pos] at this
+    exact this ⟨b, b_in_s, assoc.symm⟩
 #align multiset.prod_primes_dvd Multiset.prod_primes_dvd
 
 theorem Finset.prod_primes_dvd [CancelCommMonoidWithZero α] [Unique αˣ] {s : Finset α} (n : α)
diff --git a/Mathlib/Algebra/BigOperators/Basic.lean b/Mathlib/Algebra/BigOperators/Basic.lean
index 5a51fe6edf8ca..15ea60d67ee31 100644
--- a/Mathlib/Algebra/BigOperators/Basic.lean
+++ b/Mathlib/Algebra/BigOperators/Basic.lean
@@ -2075,8 +2075,8 @@ theorem mem_sum {f : α → Multiset β} (s : Finset α) (b : β) :
     (b ∈ ∑ x in s, f x) ↔ ∃ a ∈ s, b ∈ f a := by
   classical
     refine' s.induction_on (by simp) _
-    · intro a t hi ih
-      simp [sum_insert hi, ih, or_and_right, exists_or]
+    intro a t hi ih
+    simp [sum_insert hi, ih, or_and_right, exists_or]
 #align finset.mem_sum Finset.mem_sum
 
 section ProdEqZero
diff --git a/Mathlib/Algebra/BigOperators/Intervals.lean b/Mathlib/Algebra/BigOperators/Intervals.lean
index 9acda0db6e337..2b96ec12d198c 100644
--- a/Mathlib/Algebra/BigOperators/Intervals.lean
+++ b/Mathlib/Algebra/BigOperators/Intervals.lean
@@ -295,7 +295,7 @@ lemma prod_range_diag_flip (n : ℕ) (f : ℕ → ℕ → M) :
       Nat.lt_succ_iff, le_add_iff_nonneg_right, Nat.zero_le, and_true, and_imp, imp_self,
       implies_true, Sigma.forall, forall_const, add_tsub_cancel_of_le, Sigma.mk.inj_iff,
       add_tsub_cancel_left, heq_eq_eq]
-  · exact fun a b han hba ↦ lt_of_le_of_lt hba han
+  exact fun a b han hba ↦ lt_of_le_of_lt hba han
 #align sum_range_diag_flip Finset.sum_range_diag_flip
 
 end Generic
diff --git a/Mathlib/Algebra/Category/ModuleCat/Monoidal/Basic.lean b/Mathlib/Algebra/Category/ModuleCat/Monoidal/Basic.lean
index 67a4b7948e785..16d02a65f304d 100644
--- a/Mathlib/Algebra/Category/ModuleCat/Monoidal/Basic.lean
+++ b/Mathlib/Algebra/Category/ModuleCat/Monoidal/Basic.lean
@@ -138,7 +138,7 @@ private theorem pentagon_aux (W X Y Z : Type*) [AddCommMonoid W] [AddCommMonoid
     [AddCommMonoid Y] [AddCommMonoid Z] [Module R W] [Module R X] [Module R Y] [Module R Z] :
     (((assoc R X Y Z).toLinearMap.lTensor W).comp
             (assoc R W (X ⊗[R] Y) Z).toLinearMap).comp
-        ((assoc R W X Y).rTensor Z) =
+        ((assoc R W X Y).toLinearMap.rTensor Z) =
       (assoc R W X (Y ⊗[R] Z)).toLinearMap.comp (assoc R (W ⊗[R] X) Y Z).toLinearMap := by
   apply TensorProduct.ext_fourfold
   intro w x y z
diff --git a/Mathlib/Algebra/CharP/Basic.lean b/Mathlib/Algebra/CharP/Basic.lean
index f4b7930de46e6..a74bdba2f3672 100644
--- a/Mathlib/Algebra/CharP/Basic.lean
+++ b/Mathlib/Algebra/CharP/Basic.lean
@@ -466,8 +466,9 @@ section NonAssocSemiring
 
 variable {R} [NonAssocSemiring R]
 
--- see Note [lower instance priority]
-instance (priority := 100) CharOne.subsingleton [CharP R 1] : Subsingleton R :=
+-- This lemma is not an instance, to make sure that trying to prove `α` is a subsingleton does
+-- not try to find a ring structure on `α`, which can be expensive.
+lemma CharOne.subsingleton [CharP R 1] : Subsingleton R :=
   Subsingleton.intro <|
     suffices ∀ r : R, r = 0 from fun a b => show a = b by rw [this a, this b]
     fun r =>
@@ -477,8 +478,9 @@ instance (priority := 100) CharOne.subsingleton [CharP R 1] : Subsingleton R :=
       _ = 0 * r := by rw [CharP.cast_eq_zero]
       _ = 0 := by rw [zero_mul]
 
-theorem false_of_nontrivial_of_char_one [Nontrivial R] [CharP R 1] : False :=
-  false_of_nontrivial_of_subsingleton R
+theorem false_of_nontrivial_of_char_one [Nontrivial R] [CharP R 1] : False := by
+  have : Subsingleton R := CharOne.subsingleton
+  exact false_of_nontrivial_of_subsingleton R
 #align char_p.false_of_nontrivial_of_char_one CharP.false_of_nontrivial_of_char_one
 
 theorem ringChar_ne_one [Nontrivial R] : ringChar R ≠ 1 := by
diff --git a/Mathlib/Algebra/Lie/Derivation/AdjointAction.lean b/Mathlib/Algebra/Lie/Derivation/AdjointAction.lean
index e073356e666b1..583a328e27056 100644
--- a/Mathlib/Algebra/Lie/Derivation/AdjointAction.lean
+++ b/Mathlib/Algebra/Lie/Derivation/AdjointAction.lean
@@ -53,6 +53,10 @@ variable {R L}
 /-- The definitions `LieDerivation.ad` and `LieAlgebra.ad` agree. -/
 @[simp] lemma coe_ad_apply_eq_ad_apply (x : L) : ad R L x = LieAlgebra.ad R L x := by ext; simp
 
+lemma ad_apply_lieDerivation (x : L) (D : LieDerivation R L L) : ad R L (D x) = - ⁅x, D⁆ := rfl
+
+lemma lie_ad (x : L) (D : LieDerivation R L L) : ⁅ad R L x, D⁆ = ⁅x, D⁆ := by ext; simp
+
 variable (R L) in
 /-- The kernel of the adjoint action on a Lie algebra is equal to its center. -/
 lemma ad_ker_eq_center : (ad R L).ker = LieAlgebra.center R L := by
@@ -67,9 +71,7 @@ lemma injective_ad_of_center_eq_bot (h : LieAlgebra.center R L = ⊥) :
 
 /-- The commutator of a derivation `D` and a derivation of the form `ad x` is `ad (D x)`. -/
 lemma lie_der_ad_eq_ad_der (D : LieDerivation R L L) (x : L) : ⁅D, ad R L x⁆ = ad R L (D x) := by
-  ext a
-  rw [commutator_apply, ad_apply_apply, ad_apply_apply, ad_apply_apply, apply_lie_eq_add,
-    add_sub_cancel_left]
+  rw [ad_apply_lieDerivation, ← lie_ad, lie_skew]
 
 variable (R L) in
 /-- The range of the adjoint action homomorphism from a Lie algebra `L` to the Lie algebra of its
@@ -84,6 +86,15 @@ lemma mem_ad_idealRange_iff {D : LieDerivation R L L} :
     D ∈ (ad R L).idealRange ↔ ∃ x : L, ad R L x = D :=
   (ad R L).mem_idealRange_iff (ad_isIdealMorphism R L)
 
+lemma maxTrivSubmodule_eq_bot_of_center_eq_bot (h : LieAlgebra.center R L = ⊥) :
+    LieModule.maxTrivSubmodule R L (LieDerivation R L L) = ⊥ := by
+  refine (LieSubmodule.eq_bot_iff _).mpr fun D hD ↦ ext fun x ↦ ?_
+  have : ad R L (D x) = 0 := by
+    rw [LieModule.mem_maxTrivSubmodule] at hD
+    simp [ad_apply_lieDerivation, hD]
+  rw [← LieHom.mem_ker, ad_ker_eq_center, h, LieSubmodule.mem_bot] at this
+  simp [this]
+
 end AdjointAction
 
 end LieDerivation
diff --git a/Mathlib/Algebra/Lie/Derivation/Basic.lean b/Mathlib/Algebra/Lie/Derivation/Basic.lean
index 9ccdc096e2825..d5d085f21677c 100644
--- a/Mathlib/Algebra/Lie/Derivation/Basic.lean
+++ b/Mathlib/Algebra/Lie/Derivation/Basic.lean
@@ -291,6 +291,10 @@ instance : LieRing (LieDerivation R L L) where
 instance instLieAlgebra : LieAlgebra R (LieDerivation R L L) where
   lie_smul := fun r d e => by ext a; simp only [commutator_apply, map_smul, smul_sub, smul_apply]
 
+@[simp] lemma lie_apply (D₁ D₂ : LieDerivation R L L) (x : L) :
+    ⁅D₁, D₂⁆ x = D₁ (D₂ x) - D₂ (D₁ x) :=
+  rfl
+
 end
 
 section
@@ -328,6 +332,29 @@ def inner : M →ₗ[R] LieDerivation R L M where
   map_add' m n := by ext; simp
   map_smul' t m := by ext; simp
 
+instance instLieRingModule : LieRingModule L (LieDerivation R L M) where
+  bracket x D := inner R L M (D x)
+  add_lie x y D := by simp
+  lie_add x D₁ D₂ := by simp
+  leibniz_lie x y D := by simp
+
+@[simp] lemma lie_lieDerivation_apply (x y : L) (D : LieDerivation R L M) :
+    ⁅x, D⁆ y = ⁅y, D x⁆ :=
+  rfl
+
+@[simp] lemma lie_coe_lieDerivation_apply (x : L) (D : LieDerivation R L M) :
+    ⁅x, (D : L →ₗ[R] M)⁆ = ⁅x, D⁆ := by
+  ext; simp
+
+instance instLieModule : LieModule R L (LieDerivation R L M) where
+  smul_lie t x D := by ext; simp
+  lie_smul t x D := by ext; simp
+
+protected lemma leibniz_lie (x : L) (D₁ D₂ : LieDerivation R L L) :
+    ⁅x, ⁅D₁, D₂⁆⁆ = ⁅⁅x, D₁⁆, D₂⁆ + ⁅D₁, ⁅x, D₂⁆⁆ := by
+  ext y
+  simp [-lie_skew, ← lie_skew (D₁ x) (D₂ y), ← lie_skew (D₂ x) (D₁ y), sub_eq_neg_add]
+
 end Inner
 
 end LieDerivation
diff --git a/Mathlib/Algebra/Lie/Derivation/Killing.lean b/Mathlib/Algebra/Lie/Derivation/Killing.lean
index 14c2e769486c3..90f42918b89f8 100644
--- a/Mathlib/Algebra/Lie/Derivation/Killing.lean
+++ b/Mathlib/Algebra/Lie/Derivation/Killing.lean
@@ -42,17 +42,26 @@ lemma killingForm_restrict_range_ad : (killingForm R 𝔻).restrict 𝕀 = killi
   rw [← (ad_isIdealMorphism R L).eq, ← LieIdeal.killingForm_eq]
   rfl
 
+/-- The orthogonal complement of the inner derivations is a Lie submodule of all derivations. -/
+@[simps!] noncomputable def rangeAdOrthogonal : LieSubmodule R L (LieDerivation R L L) where
+  __ := 𝕀ᗮ
+  lie_mem := by
+    intro x D hD
+    have : 𝕀ᗮ = (ad R L).idealRange.killingCompl := by simp [← (ad_isIdealMorphism R L).eq]
+    change D ∈ 𝕀ᗮ at hD
+    change ⁅x, D⁆ ∈ 𝕀ᗮ
+    rw [this] at hD ⊢
+    rw [← lie_ad]
+    exact lie_mem_right _ _ (ad R L).idealRange.killingCompl _ _ hD
+
 variable {R L}
 
 /-- If a derivation `D` is in the Killing orthogonal of the range of the adjoint action, then, for
 any `x : L`, `ad (D x)` is also in this orthogonal. -/
 lemma ad_mem_orthogonal_of_mem_orthogonal {D : LieDerivation R L L} (hD : D ∈ 𝕀ᗮ) (x : L) :
     ad R L (D x) ∈ 𝕀ᗮ := by
-  have : 𝕀ᗮ = (ad R L).idealRange.killingCompl := by
-    simp [← (ad_isIdealMorphism R L).eq]
-  rw [this] at hD ⊢
-  rw [← lie_der_ad_eq_ad_der]
-  exact lie_mem_left _ _ (ad R L).idealRange.killingCompl _ _ hD
+  simp only [ad_apply_lieDerivation, LieHom.range_coeSubmodule, neg_mem_iff]
+  exact (rangeAdOrthogonal R L).lie_mem hD
 
 lemma ad_mem_ker_killingForm_ad_range_of_mem_orthogonal
     {D : LieDerivation R L L} (hD : D ∈ 𝕀ᗮ) (x : L) :
diff --git a/Mathlib/Algebra/Module/FinitePresentation.lean b/Mathlib/Algebra/Module/FinitePresentation.lean
new file mode 100644
index 0000000000000..c7938924b0ffa
--- /dev/null
+++ b/Mathlib/Algebra/Module/FinitePresentation.lean
@@ -0,0 +1,301 @@
+/-
+Copyright (c) 2024 Andrew Yang. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Andrew Yang
+-/
+import Mathlib.RingTheory.Noetherian
+import Mathlib.Algebra.Module.LocalizedModule
+import Mathlib.LinearAlgebra.Isomorphisms
+import Mathlib.LinearAlgebra.FreeModule.Finite.Basic
+/-!
+
+# Finitely Presented Modules
+
+## Main definition
+
+- `Module.FinitePresentation`: A module is finitely presented if it is generated by some
+  finite set `s` and the kernel of the presentation `Rˢ → M` is also finitely generated.
+
+## Main results
+
+- `Module.finitePresentation_iff_finite`: If `R` is noetherian, then f.p. iff f.g. on `R`-modules.
+
+Suppose `0 → K → M → N → 0` is an exact sequence of `R`-modules.
+
+- `Module.finitePresentation_of_surjective`: If `M` is f.p., `K` is f.g., then `N` is f.p.
+
+- `Module.FinitePresentation.fg_ker`: If `M` is f.g., `N` is f.p., then `K` is f.g.
+
+- `Module.finitePresentation_of_ker`: If `N` and `K` is f.p., then `M` is also f.p.
+
+- `Module.FinitePresentation.isLocalizedModule_map`: If `M` and `N` are `R`-modules and `M` is f.p.,
+  and `S` is a submonoid of `R`, then `Hom(Mₛ, Nₛ)` is the localization of `Hom(M, N)`.
+
+
+Also the instances finite + free => f.p. => finite are also provided
+
+## TODO
+Suppose `S` is an `R`-algebra, `M` is an `S`-module. Then
+1. If `S` is f.p., then `M` is `R`-f.p. implies `M` is `S`-f.p.
+2. If `S` is both f.p. (as an algebra) and finite (as a module),
+  then `M` is `S`-fp implies that `M` is `R`-f.p.
+3. If `S` is f.p. as a module, then `S` is f.p. as an algebra.
+In particular,
+4. `S` is f.p. as an `R`-module iff it is f.p. as an algebra and is finite as a module.
+
+
+For finitely presented algebras, see `Algebra.FinitePresentation`
+in file `RingTheory/FinitePresentation`.
+-/
+
+section Semiring
+variable (R M) [Semiring R] [AddCommMonoid M] [Module R M]
+
+/--
+A module is finitely presented if it is finitely generated by some set `s`
+and the kernel of the presentation `Rˢ → M` is also finitely generated.
+-/
+class Module.FinitePresentation : Prop where
+  out : ∃ (s : Finset M), Submodule.span R (s : Set M) = ⊤ ∧
+    (LinearMap.ker (Finsupp.total s M R Subtype.val)).FG
+
+instance (priority := 100) [h : Module.FinitePresentation R M] : Module.Finite R M := by
+  obtain ⟨s, hs₁, _⟩ := h
+  exact ⟨s, hs₁⟩
+
+end Semiring
+
+section Ring
+
+variable (R M N) [Ring R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N]
+
+-- Ideally this should be an instance but it makes mathlib much slower.
+lemma Module.finitePresentation_of_finite [IsNoetherianRing R] [h : Module.Finite R M] :
+    Module.FinitePresentation R M := by
+  obtain ⟨s, hs⟩ := h
+  exact ⟨s, hs, IsNoetherian.noetherian _⟩
+
+lemma Module.finitePresentation_iff_finite [IsNoetherianRing R] :
+    Module.FinitePresentation R M ↔ Module.Finite R M :=
+  ⟨fun _ ↦ inferInstance, fun _ ↦ finitePresentation_of_finite R M⟩
+
+variable {R M N}
+
+lemma Module.finitePresentation_of_free_of_surjective [Module.Free R M] [Module.Finite R M]
+    (l : M →ₗ[R] N)
+    (hl : Function.Surjective l) (hl' : (LinearMap.ker l).FG) :
+    Module.FinitePresentation R N := by
+  classical
+  let b := Module.Free.chooseBasis R M
+  let π : Free.ChooseBasisIndex R M → (Set.finite_range (l ∘ b)).toFinset :=
+    fun i ↦ ⟨l (b i), by simp⟩
+  have : π.Surjective := fun ⟨x, hx⟩ ↦ by
+    obtain ⟨y, rfl⟩ : ∃ a, l (b a) = x := by simpa using hx
+    exact ⟨y, rfl⟩
+  choose σ hσ using this
+  have hπ : Subtype.val ∘ π = l ∘ b := rfl
+  have hσ₁ : π ∘ σ = id := by ext i; exact congr_arg Subtype.val (hσ i)
+  have hσ₂ : l ∘ b ∘ σ = Subtype.val := by ext i; exact congr_arg Subtype.val (hσ i)
+  refine ⟨(Set.finite_range (l ∘ b)).toFinset,
+    by simpa [Set.range_comp, LinearMap.range_eq_top], ?_⟩
+  let f : M →ₗ[R] (Set.finite_range (l ∘ b)).toFinset →₀ R :=
+    Finsupp.lmapDomain _ _ π ∘ₗ b.repr.toLinearMap
+  convert hl'.map f
+  ext x; simp only [LinearMap.mem_ker, Submodule.mem_map]
+  constructor
+  · intro hx
+    refine ⟨b.repr.symm (x.mapDomain σ), ?_, ?_⟩
+    · simp [Finsupp.apply_total, hσ₂, hx]
+    · simp only [f, LinearMap.comp_apply, b.repr.apply_symm_apply,
+        LinearEquiv.coe_toLinearMap, Finsupp.lmapDomain_apply]
+      rw [← Finsupp.mapDomain_comp, hσ₁, Finsupp.mapDomain_id]
+  · rintro ⟨y, hy, rfl⟩
+    simp [f, hπ, ← Finsupp.apply_total, hy]
+
+-- Ideally this should be an instance but it makes mathlib much slower.
+variable (R M) in
+lemma Module.finitePresentation_of_free [Module.Free R M] [Module.Finite R M] :
+    Module.FinitePresentation R M :=
+  Module.finitePresentation_of_free_of_surjective LinearMap.id (⟨·, rfl⟩)
+    (by simpa using Submodule.fg_bot)
+
+variable {ι} [_root_.Finite ι]
+
+instance : Module.FinitePresentation R R := Module.finitePresentation_of_free _ _
+instance : Module.FinitePresentation R (ι →₀ R) := Module.finitePresentation_of_free _ _
+instance : Module.FinitePresentation R (ι → R) := Module.finitePresentation_of_free _ _
+
+lemma Module.finitePresentation_of_surjective [h : Module.FinitePresentation R M] (l : M →ₗ[R] N)
+    (hl : Function.Surjective l) (hl' : (LinearMap.ker l).FG) :
+    Module.FinitePresentation R N := by
+  classical
+  obtain ⟨s, hs, hs'⟩ := h
+  obtain ⟨t, ht⟩ := hl'
+  have H : Function.Surjective (Finsupp.total s M R Subtype.val) :=
+    LinearMap.range_eq_top.mp (by rw [Finsupp.range_total, Subtype.range_val, ← hs]; rfl)
+  apply Module.finitePresentation_of_free_of_surjective (l ∘ₗ Finsupp.total s M R Subtype.val)
+    (hl.comp H)
+  choose σ hσ using (show _ from H)
+  have : Finsupp.total s M R Subtype.val '' (σ '' t) = t := by
+    simp only [Set.image_image, hσ, Set.image_id']
+  rw [LinearMap.ker_comp, ← ht, ← this, ← Submodule.map_span, Submodule.comap_map_eq,
+    ← Finset.coe_image]
+  exact Submodule.FG.sup ⟨_, rfl⟩ hs'
+
+lemma Module.FinitePresentation.fg_ker [Module.Finite R M]
+    [h : Module.FinitePresentation R N] (l : M →ₗ[R] N) (hl : Function.Surjective l) :
+    (LinearMap.ker l).FG := by
+  classical
+  obtain ⟨s, hs, hs'⟩ := h
+  have H : Function.Surjective (Finsupp.total s N R Subtype.val) :=
+    LinearMap.range_eq_top.mp (by rw [Finsupp.range_total, Subtype.range_val, ← hs]; rfl)
+  obtain ⟨f, hf⟩ : ∃ f : (s →₀ R) →ₗ[R] M, l ∘ₗ f = (Finsupp.total s N R Subtype.val) := by
+    choose f hf using show _ from hl
+    exact ⟨Finsupp.total s M R (fun i ↦ f i), by ext; simp [hf]⟩
+  have : (LinearMap.ker l).map (LinearMap.range f).mkQ = ⊤ := by
+    rw [← top_le_iff]
+    rintro x -
+    obtain ⟨x, rfl⟩ := Submodule.mkQ_surjective _ x
+    obtain ⟨y, hy⟩ := H (l x)
+    rw [← hf, LinearMap.comp_apply, eq_comm, ← sub_eq_zero, ← map_sub] at hy
+    exact ⟨_, hy, by simp⟩
+  apply Submodule.fg_of_fg_map_of_fg_inf_ker f.range.mkQ
+  · rw [this]
+    exact Module.Finite.out
+  · rw [Submodule.ker_mkQ, inf_comm, ← Submodule.map_comap_eq, ← LinearMap.ker_comp, hf]
+    exact hs'.map f
+
+lemma Module.FinitePresentation.fg_ker_iff [Module.FinitePresentation R M]
+    (l : M →ₗ[R] N) (hl : Function.Surjective l) :
+    Submodule.FG (LinearMap.ker l) ↔ Module.FinitePresentation R N :=
+  ⟨finitePresentation_of_surjective l hl, fun _ ↦ fg_ker l hl⟩
+
+lemma Module.finitePresentation_of_ker [Module.FinitePresentation R N]
+    (l : M →ₗ[R] N) (hl : Function.Surjective l) [Module.FinitePresentation R (LinearMap.ker l)] :
+    Module.FinitePresentation R M := by
+  obtain ⟨s, hs⟩ : (⊤ : Submodule R M).FG := by
+    apply Submodule.fg_of_fg_map_of_fg_inf_ker l
+    · rw [Submodule.map_top, LinearMap.range_eq_top.mpr hl]; exact Module.Finite.out
+    · rw [top_inf_eq, ← Submodule.fg_top]; exact Module.Finite.out
+  refine ⟨s, hs, ?_⟩
+  let π := Finsupp.total s M R Subtype.val
+  have H : Function.Surjective π :=
+    LinearMap.range_eq_top.mp (by rw [Finsupp.range_total, Subtype.range_val, ← hs]; rfl)
+  have inst : Module.Finite R (LinearMap.ker (l ∘ₗ π)) := by
+    constructor
+    rw [Submodule.fg_top]; exact Module.FinitePresentation.fg_ker _ (hl.comp H)
+  letI : AddCommGroup (LinearMap.ker (l ∘ₗ π)) := inferInstance
+  let f : LinearMap.ker (l ∘ₗ π) →ₗ[R] LinearMap.ker l := LinearMap.restrict π (fun x ↦ id)
+  have e : π ∘ₗ Submodule.subtype _ = Submodule.subtype _ ∘ₗ f := by ext; rfl
+  have hf : Function.Surjective f := by
+    rw [← LinearMap.range_eq_top]
+    apply Submodule.map_injective_of_injective (Submodule.injective_subtype _)
+    rw [Submodule.map_top, Submodule.range_subtype, ← LinearMap.range_comp, ← e,
+      LinearMap.range_comp, Submodule.range_subtype, LinearMap.ker_comp,
+      Submodule.map_comap_eq_of_surjective H]
+  show (LinearMap.ker π).FG
+  have : LinearMap.ker π ≤ LinearMap.ker (l ∘ₗ π) :=
+    Submodule.comap_mono (f := π) (bot_le (a := LinearMap.ker l))
+  rw [← inf_eq_right.mpr this, ← Submodule.range_subtype (LinearMap.ker _),
+    ← Submodule.map_comap_eq, ← LinearMap.ker_comp, e, LinearMap.ker_comp f,
+    LinearMap.ker_eq_bot.mpr (Submodule.injective_subtype _), Submodule.comap_bot]
+  exact (Module.FinitePresentation.fg_ker f hf).map (Submodule.subtype _)
+
+end Ring
+
+section CommRing
+open BigOperators
+variable {R M N N'} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N]
+variable [AddCommGroup N'] [Module R N'] (S : Submonoid R) (f : N →ₗ[R] N') [IsLocalizedModule S f]
+
+
+lemma Module.FinitePresentation.exists_lift_of_isLocalizedModule
+    [h : Module.FinitePresentation R M] (g : M →ₗ[R] N') :
+    ∃ (h : M →ₗ[R] N) (s : S), f ∘ₗ h = s • g := by
+  obtain ⟨σ, hσ, τ, hτ⟩ := h
+  let π := Finsupp.total σ M R Subtype.val
+  have hπ : Function.Surjective π :=
+    LinearMap.range_eq_top.mp (by rw [Finsupp.range_total, Subtype.range_val, ← hσ]; rfl)
+  classical
+  choose s hs using IsLocalizedModule.surj S f
+  let i : σ → N :=
+    fun x ↦ (∏ j in σ.erase x.1, (s (g j)).2) • (s (g x)).1
+  let s₀ := ∏ j in σ, (s (g j)).2
+  have hi : f ∘ₗ Finsupp.total σ N R i = (s₀ • g) ∘ₗ π := by
+    ext j
+    simp only [LinearMap.coe_comp, Function.comp_apply, Finsupp.lsingle_apply, Finsupp.total_single,
+      one_smul, LinearMap.map_smul_of_tower, ← hs, LinearMap.smul_apply, i, s₀, π]
+    rw [← mul_smul, Finset.prod_erase_mul]
+    exact j.prop
+  have : ∀ x : τ, ∃ s : S, s • (Finsupp.total σ N R i x) = 0 := by
+    intros x
+    convert_to ∃ s : S, s • (Finsupp.total σ N R i x) = s • 0
+    · simp only [smul_zero]
+    apply IsLocalizedModule.exists_of_eq (S := S) (f := f)
+    rw [← LinearMap.comp_apply, map_zero, hi, LinearMap.comp_apply]
+    convert map_zero (s₀ • g)
+    rw [← LinearMap.mem_ker, ← hτ]
+    exact Submodule.subset_span x.prop
+  choose s' hs' using this
+  let s₁ := ∏ i : τ, s' i
+  have : LinearMap.ker π ≤ LinearMap.ker (s₁ • Finsupp.total σ N R i) := by
+    rw [← hτ, Submodule.span_le]
+    intro x hxσ
+    simp only [s₁]
+    rw [SetLike.mem_coe, LinearMap.mem_ker, LinearMap.smul_apply,
+      ← Finset.prod_erase_mul _ _ (Finset.mem_univ ⟨x, hxσ⟩), mul_smul]
+    convert smul_zero _
+    exact hs' ⟨x, hxσ⟩
+  refine ⟨Submodule.liftQ _ _ this ∘ₗ
+    (LinearMap.quotKerEquivOfSurjective _ hπ).symm.toLinearMap, s₁ * s₀, ?_⟩
+  ext x
+  obtain ⟨x, rfl⟩ := hπ x
+  rw [← LinearMap.comp_apply, ← LinearMap.comp_apply, mul_smul, LinearMap.smul_comp, ← hi,
+    ← LinearMap.comp_smul, LinearMap.comp_assoc, LinearMap.comp_assoc]
+  congr 2
+  convert Submodule.liftQ_mkQ _ _ this using 2
+  ext x
+  apply (LinearMap.quotKerEquivOfSurjective _ hπ).injective
+  simp [LinearMap.quotKerEquivOfSurjective]
+
+lemma Module.Finite.exists_smul_of_comp_eq_of_isLocalizedModule
+    [hM : Module.Finite R M] (g₁ g₂ : M →ₗ[R] N) (h : f.comp g₁ = f.comp g₂) :
+    ∃ (s : S), s • g₁ = s • g₂ := by
+  classical
+  have : ∀ x, ∃ s : S, s • g₁ x = s • g₂ x := fun x ↦
+    IsLocalizedModule.exists_of_eq (S := S) (f := f) (LinearMap.congr_fun h x)
+  choose s hs using this
+  obtain ⟨σ, hσ⟩ := hM
+  use σ.prod s
+  rw [← sub_eq_zero, ← LinearMap.ker_eq_top, ← top_le_iff, ← hσ, Submodule.span_le]
+  intro x hx
+  simp only [SetLike.mem_coe, LinearMap.mem_ker, LinearMap.sub_apply, LinearMap.smul_apply,
+    sub_eq_zero, ← Finset.prod_erase_mul σ s hx, mul_smul, hs]
+
+lemma Module.FinitePresentation.isLocalizedModule_map
+    {M' : Type*} [AddCommGroup M'] [Module R M'] (f : M →ₗ[R] M') [IsLocalizedModule S f]
+    {N' : Type*} [AddCommGroup N'] [Module R N'] (g : N →ₗ[R] N') [IsLocalizedModule S g]
+    [Module.FinitePresentation R M] :
+      IsLocalizedModule S (IsLocalizedModule.map S f g) := by
+  constructor
+  · intro s
+    rw [Module.End_isUnit_iff]
+    have := (Module.End_isUnit_iff _).mp (IsLocalizedModule.map_units (S := S) (f := g) s)
+    constructor
+    · exact fun _ _ e ↦ LinearMap.ext fun m ↦ this.left (LinearMap.congr_fun e m)
+    · intro h;
+      use ((IsLocalizedModule.map_units (S := S) (f := g) s).unit⁻¹).1 ∘ₗ h
+      ext x
+      exact Module.End_isUnit_apply_inv_apply_of_isUnit
+        (IsLocalizedModule.map_units (S := S) (f := g) s) (h x)
+  · intro h
+    obtain ⟨h', s, e⟩ := Module.FinitePresentation.exists_lift_of_isLocalizedModule S g (h ∘ₗ f)
+    refine ⟨⟨h', s⟩, ?_⟩
+    apply IsLocalizedModule.ringHom_ext S f (IsLocalizedModule.map_units g)
+    refine e.symm.trans (by ext; simp)
+  · intro h₁ h₂ e
+    apply Module.Finite.exists_smul_of_comp_eq_of_isLocalizedModule S g
+    ext x
+    simpa using LinearMap.congr_fun e (f x)
+
+end CommRing
diff --git a/Mathlib/Algebra/Module/LocalizedModule.lean b/Mathlib/Algebra/Module/LocalizedModule.lean
index fd750ef877afe..d7845676024d3 100644
--- a/Mathlib/Algebra/Module/LocalizedModule.lean
+++ b/Mathlib/Algebra/Module/LocalizedModule.lean
@@ -900,6 +900,10 @@ theorem lift_comp (g : M →ₗ[R] M'') (h : ∀ x : S, IsUnit ((algebraMap R (M
   rw [LinearMap.comp_assoc, iso_symm_comp, LocalizedModule.lift_comp S g h]
 #align is_localized_module.lift_comp IsLocalizedModule.lift_comp
 
+@[simp]
+theorem lift_apply (g : M →ₗ[R] M'') (h) (x) :
+    lift S f g h (f x) = g x := LinearMap.congr_fun (lift_comp S f g h) x
+
 theorem lift_unique (g : M →ₗ[R] M'') (h : ∀ x : S, IsUnit ((algebraMap R (Module.End R M'')) x))
     (l : M' →ₗ[R] M'') (hl : l.comp f = g) : lift S f g h = l := by
   dsimp only [IsLocalizedModule.lift]
@@ -1102,6 +1106,28 @@ theorem mk'_surjective : Function.Surjective (Function.uncurry <| mk' f : M × S
   exact ⟨⟨m, s⟩, mk'_eq_iff.mpr e.symm⟩
 #align is_localized_module.mk'_surjective IsLocalizedModule.mk'_surjective
 
+variable {N N'} [AddCommGroup N] [AddCommGroup N'] [Module R N] [Module R N']
+variable (g : N →ₗ[R] N') [IsLocalizedModule S g]
+
+/-- A linear map `M →ₗ[R] N` gives a map between localized modules `Mₛ →ₗ[R] Nₛ`. -/
+noncomputable
+def map : (M →ₗ[R] N) →ₗ[R] (M' →ₗ[R] N') where
+  toFun h := lift S f (g ∘ₗ h) (IsLocalizedModule.map_units g)
+  map_add' h₁ h₂ := by
+    apply IsLocalizedModule.ringHom_ext S f (IsLocalizedModule.map_units g)
+    simp only [lift_comp, LinearMap.add_comp, LinearMap.comp_add]
+  map_smul' r h := by
+    apply IsLocalizedModule.ringHom_ext S f (IsLocalizedModule.map_units g)
+    simp only [lift_comp, LinearMap.add_comp, LinearMap.comp_add, LinearMap.smul_comp,
+      LinearMap.comp_smul, RingHom.id_apply]
+
+lemma map_comp (h : M →ₗ[R] N) : (map S f g h) ∘ₗ f = g ∘ₗ h :=
+  lift_comp S f (g ∘ₗ h) (IsLocalizedModule.map_units g)
+
+@[simp]
+lemma map_apply (h : M →ₗ[R] N) (x) : map S f g h (f x) = g (h x) :=
+  lift_apply S f (g ∘ₗ h) (IsLocalizedModule.map_units g) x
+
 section Algebra
 
 theorem mkOfAlgebra {R S S' : Type*} [CommRing R] [CommRing S] [CommRing S'] [Algebra R S]
diff --git a/Mathlib/Algebra/Polynomial/Degree/TrailingDegree.lean b/Mathlib/Algebra/Polynomial/Degree/TrailingDegree.lean
index a043c4e997de7..9f7a1a10ca9ac 100644
--- a/Mathlib/Algebra/Polynomial/Degree/TrailingDegree.lean
+++ b/Mathlib/Algebra/Polynomial/Degree/TrailingDegree.lean
@@ -562,15 +562,28 @@ lemma natTrailingDegree_eq_zero_of_constantCoeff_ne_zero (h : constantCoeff p 
     p.natTrailingDegree = 0 :=
   le_antisymm (natTrailingDegree_le_of_ne_zero h) zero_le'
 
-lemma Monic.eq_X_pow_of_natTrailingDegree_eq_natDegree
-    (h₁ : p.Monic) (h₂ : p.natTrailingDegree = p.natDegree) :
-    p = X ^ p.natDegree := by
-  ext n
-  rw [coeff_X_pow]
-  obtain hn | rfl | hn := lt_trichotomy n p.natDegree
-  · rw [if_neg hn.ne, coeff_eq_zero_of_lt_natTrailingDegree (h₂ ▸ hn)]
-  · simpa only [if_pos rfl] using h₁.leadingCoeff
-  · rw [if_neg hn.ne', coeff_eq_zero_of_natDegree_lt hn]
+namespace Monic
+
+lemma eq_X_pow_iff_natDegree_le_natTrailingDegree (h₁ : p.Monic) :
+    p = X ^ p.natDegree ↔ p.natDegree ≤ p.natTrailingDegree := by
+  refine ⟨fun h => ?_, fun h => ?_⟩
+  · nontriviality R
+    rw [h, natTrailingDegree_X_pow, ← h]
+  · ext n
+    rw [coeff_X_pow]
+    obtain hn | rfl | hn := lt_trichotomy n p.natDegree
+    · rw [if_neg hn.ne, coeff_eq_zero_of_lt_natTrailingDegree (hn.trans_le h)]
+    · simpa only [if_pos rfl] using h₁.leadingCoeff
+    · rw [if_neg hn.ne', coeff_eq_zero_of_natDegree_lt hn]
+
+lemma eq_X_pow_iff_natTrailingDegree_eq_natDegree (h₁ : p.Monic) :
+    p = X ^ p.natDegree ↔ p.natTrailingDegree = p.natDegree :=
+  h₁.eq_X_pow_iff_natDegree_le_natTrailingDegree.trans (natTrailingDegree_le_natDegree p).ge_iff_eq
+
+@[deprecated] -- 2024-04-26
+alias ⟨_, eq_X_pow_of_natTrailingDegree_eq_natDegree⟩ := eq_X_pow_iff_natTrailingDegree_eq_natDegree
+
+end Monic
 
 end Semiring
 
diff --git a/Mathlib/Analysis/NormedSpace/PiLp.lean b/Mathlib/Analysis/NormedSpace/PiLp.lean
index 6bf0ff1ca9eef..168dd399ebc39 100644
--- a/Mathlib/Analysis/NormedSpace/PiLp.lean
+++ b/Mathlib/Analysis/NormedSpace/PiLp.lean
@@ -679,8 +679,8 @@ instance normedSpace [NormedField 𝕜] [∀ i, SeminormedAddCommGroup (β i)]
 #align pi_Lp.normed_space PiLp.normedSpace
 
 variable {𝕜 p α}
-variable [SeminormedRing 𝕜] [∀ i, SeminormedAddCommGroup (β i)]
-variable [∀ i, Module 𝕜 (β i)] [∀ i, BoundedSMul 𝕜 (β i)] (c : 𝕜)
+variable [Semiring 𝕜] [∀ i, SeminormedAddCommGroup (α i)] [∀ i, SeminormedAddCommGroup (β i)]
+variable [∀ i, Module 𝕜 (α i)] [∀ i, Module 𝕜 (β i)] (c : 𝕜)
 
 /-- The canonical map `WithLp.equiv` between `PiLp ∞ β` and `Π i, β i` as a linear isometric
 equivalence. -/
@@ -691,10 +691,11 @@ def equivₗᵢ : PiLp ∞ β ≃ₗᵢ[𝕜] ∀ i, β i :=
     norm_map' := norm_equiv }
 #align pi_Lp.equivₗᵢ PiLp.equivₗᵢ
 
+section piLpCongrLeft
 variable {ι' : Type*}
 variable [Fintype ι']
 variable (p 𝕜)
-variable (E : Type*) [NormedAddCommGroup E] [Module 𝕜 E] [BoundedSMul 𝕜 E]
+variable (E : Type*) [SeminormedAddCommGroup E] [Module 𝕜 E]
 
 /-- An equivalence of finite domains induces a linearly isometric equivalence of finitely supported
 functions-/
@@ -741,6 +742,58 @@ theorem _root_.LinearIsometryEquiv.piLpCongrLeft_single [DecidableEq ι] [Decida
     Pi.single, Function.update, Equiv.symm_apply_eq]
 #align linear_isometry_equiv.pi_Lp_congr_left_single LinearIsometryEquiv.piLpCongrLeft_single
 
+end piLpCongrLeft
+
+section piLpCongrRight
+variable {β}
+
+variable (p) in
+/-- A family of linearly isometric equivalences in the codomain induces an isometric equivalence
+between Pi types with the Lp norm.
+
+This is the isometry version of `LinearEquiv.piCongrRight`. -/
+protected def _root_.LinearIsometryEquiv.piLpCongrRight (e : ∀ i, α i ≃ₗᵢ[𝕜] β i) :
+    PiLp p α ≃ₗᵢ[𝕜] PiLp p β where
+  toLinearEquiv :=
+    WithLp.linearEquiv _ _ _
+      ≪≫ₗ (LinearEquiv.piCongrRight fun i => (e i).toLinearEquiv)
+      ≪≫ₗ (WithLp.linearEquiv _ _ _).symm
+  norm_map' := (WithLp.linearEquiv p 𝕜 _).symm.surjective.forall.2 fun x => by
+    simp only [LinearEquiv.trans_apply, LinearEquiv.piCongrRight_apply,
+      Equiv.apply_symm_apply, WithLp.linearEquiv_symm_apply, WithLp.linearEquiv_apply]
+    obtain rfl | hp := p.dichotomy
+    · simp_rw [PiLp.norm_equiv_symm, Pi.norm_def, LinearEquiv.piCongrRight_apply,
+        LinearIsometryEquiv.coe_toLinearEquiv, LinearIsometryEquiv.nnnorm_map]
+    · have : 0 < p.toReal := zero_lt_one.trans_le <| by norm_cast
+      simp only [PiLp.norm_eq_sum this, WithLp.equiv_symm_pi_apply, LinearEquiv.piCongrRight_apply,
+        LinearIsometryEquiv.coe_toLinearEquiv, LinearIsometryEquiv.norm_map]
+
+@[simp]
+theorem _root_.LinearIsometryEquiv.piLpCongrRight_apply (e : ∀ i, α i ≃ₗᵢ[𝕜] β i) (x : PiLp p α) :
+    LinearIsometryEquiv.piLpCongrRight p e x =
+      (WithLp.equiv p _).symm (fun i => e i (x i)) :=
+  rfl
+
+@[simp]
+theorem _root_.LinearIsometryEquiv.piLpCongrRight_refl :
+    LinearIsometryEquiv.piLpCongrRight p (fun i => .refl 𝕜 (α i)) = .refl _ _ :=
+  rfl
+
+@[simp]
+theorem _root_.LinearIsometryEquiv.piLpCongrRight_symm (e : ∀ i, α i ≃ₗᵢ[𝕜] β i) :
+    (LinearIsometryEquiv.piLpCongrRight p e).symm =
+      LinearIsometryEquiv.piLpCongrRight p (fun i => (e i).symm) :=
+  rfl
+
+@[simp high]
+theorem _root_.LinearIsometryEquiv.piLpCongrRight_single (e : ∀ i, α i ≃ₗᵢ[𝕜] β i) [DecidableEq ι]
+    (i : ι) (v : α i) :
+    LinearIsometryEquiv.piLpCongrRight p e ((WithLp.equiv p (∀ i, α i)).symm <| Pi.single i v) =
+      (WithLp.equiv p (∀ i, β i)).symm (Pi.single i (e _ v)) :=
+  funext <| Pi.apply_single (e ·) (fun _ => map_zero _) _ _
+
+end piLpCongrRight
+
 section Single
 
 variable (p)
diff --git a/Mathlib/CategoryTheory/Adjunction/FullyFaithful.lean b/Mathlib/CategoryTheory/Adjunction/FullyFaithful.lean
index 086d0c8dca81b..da30b40e13012 100644
--- a/Mathlib/CategoryTheory/Adjunction/FullyFaithful.lean
+++ b/Mathlib/CategoryTheory/Adjunction/FullyFaithful.lean
@@ -3,7 +3,6 @@ Copyright (c) 2019 Scott Morrison. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Scott Morrison
 -/
-import Mathlib.CategoryTheory.Conj
 import Mathlib.CategoryTheory.MorphismProperty
 
 #align_import category_theory.adjunction.fully_faithful from "leanprover-community/mathlib"@"9e7c80f638149bfb3504ba8ff48dfdbfc949fb1a"
@@ -14,9 +13,6 @@ import Mathlib.CategoryTheory.MorphismProperty
 A left adjoint is fully faithful, if and only if the unit is an isomorphism
 (and similarly for right adjoints and the counit).
 
-`Adjunction.restrictFullyFaithful` shows that an adjunction can be restricted along fully faithful
-inclusions.
-
 ## Future work
 
 The statements from Riehl 4.5.13 for adjoints which are either full, or faithful.
@@ -210,40 +206,4 @@ lemma isIso_unit_app_of_iso [R.Faithful] [R.Full] {X : D} {Y : C} (e : Y ≅ R.o
     IsIso (h.unit.app Y) :=
   (isIso_unit_app_iff_mem_essImage h).mpr ⟨X, ⟨e.symm⟩⟩
 
--- TODO also do the statements from Riehl 4.5.13 for full and faithful separately?
-universe v₃ v₄ u₃ u₄
-
-variable {C' : Type u₃} [Category.{v₃} C']
-variable {D' : Type u₄} [Category.{v₄} D']
-
--- TODO: This needs some lemmas describing the produced adjunction, probably in terms of `adj`,
--- `iC` and `iD`.
-/-- If `C` is a full subcategory of `C'` and `D` is a full subcategory of `D'`, then we can restrict
-an adjunction `L' ⊣ R'` where `L' : C' ⥤ D'` and `R' : D' ⥤ C'` to `C` and `D`.
-The construction here is slightly more general, in that `C` is required only to have a full and
-faithful "inclusion" functor `iC : C ⥤ C'` (and similarly `iD : D ⥤ D'`) which commute (up to
-natural isomorphism) with the proposed restrictions.
--/
-def Adjunction.restrictFullyFaithful (iC : C ⥤ C') (iD : D ⥤ D') {L' : C' ⥤ D'} {R' : D' ⥤ C'}
-    (adj : L' ⊣ R') {L : C ⥤ D} {R : D ⥤ C} (comm1 : iC ⋙ L' ≅ L ⋙ iD) (comm2 : iD ⋙ R' ≅ R ⋙ iC)
-    [iC.Full] [iC.Faithful] [iD.Full] [iD.Faithful] : L ⊣ R :=
-  Adjunction.mkOfHomEquiv
-    { homEquiv := fun X Y =>
-        calc
-          (L.obj X ⟶ Y) ≃ (iD.obj (L.obj X) ⟶ iD.obj Y) := equivOfFullyFaithful iD
-          _ ≃ (L'.obj (iC.obj X) ⟶ iD.obj Y) := Iso.homCongr (comm1.symm.app X) (Iso.refl _)
-          _ ≃ (iC.obj X ⟶ R'.obj (iD.obj Y)) := adj.homEquiv _ _
-          _ ≃ (iC.obj X ⟶ iC.obj (R.obj Y)) := Iso.homCongr (Iso.refl _) (comm2.app Y)
-          _ ≃ (X ⟶ R.obj Y) := (equivOfFullyFaithful iC).symm
-
-      homEquiv_naturality_left_symm := fun {X' X Y} f g => by
-        apply iD.map_injective
-        simpa [Trans.trans] using (comm1.inv.naturality_assoc f _).symm
-      homEquiv_naturality_right := fun {X Y' Y} f g => by
-        apply iC.map_injective
-        suffices R'.map (iD.map g) ≫ comm2.hom.app Y = comm2.hom.app Y' ≫ iC.map (R.map g) by
-          simp [Trans.trans, this]
-        apply comm2.hom.naturality g }
-#align category_theory.adjunction.restrict_fully_faithful CategoryTheory.Adjunction.restrictFullyFaithful
-
 end CategoryTheory
diff --git a/Mathlib/CategoryTheory/Adjunction/Reflective.lean b/Mathlib/CategoryTheory/Adjunction/Reflective.lean
index e487a9ba6bee8..b22c920d61a1d 100644
--- a/Mathlib/CategoryTheory/Adjunction/Reflective.lean
+++ b/Mathlib/CategoryTheory/Adjunction/Reflective.lean
@@ -4,8 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Bhavik Mehta
 -/
 import Mathlib.CategoryTheory.Adjunction.FullyFaithful
-import Mathlib.CategoryTheory.Functor.ReflectsIso
-import Mathlib.CategoryTheory.EpiMono
+import Mathlib.CategoryTheory.Conj
 
 #align_import category_theory.adjunction.reflective from "leanprover-community/mathlib"@"239d882c4fb58361ee8b3b39fb2091320edef10a"
 
diff --git a/Mathlib/CategoryTheory/Adjunction/Restrict.lean b/Mathlib/CategoryTheory/Adjunction/Restrict.lean
new file mode 100644
index 0000000000000..1c8cb4ecf114f
--- /dev/null
+++ b/Mathlib/CategoryTheory/Adjunction/Restrict.lean
@@ -0,0 +1,69 @@
+/-
+Copyright (c) 2019 Scott Morrison. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Scott Morrison
+-/
+import Mathlib.CategoryTheory.Conj
+import Mathlib.CategoryTheory.Adjunction.Basic
+/-!
+
+# Restricting adjunctions
+
+`Adjunction.restrictFullyFaithful` shows that an adjunction can be restricted along fully faithful
+inclusions.
+-/
+
+namespace CategoryTheory.Adjunction
+
+universe v₁ v₂ u₁ u₂ v₃ v₄ u₃ u₄
+
+open Category Opposite
+
+variable {C : Type u₁} [Category.{v₁} C]
+variable {D : Type u₂} [Category.{v₂} D]
+variable {C' : Type u₃} [Category.{v₃} C']
+variable {D' : Type u₄} [Category.{v₄} D']
+variable (iC : C ⥤ C') (iD : D ⥤ D') {L' : C' ⥤ D'} {R' : D' ⥤ C'} (adj : L' ⊣ R')
+variable {L : C ⥤ D} {R : D ⥤ C} (comm1 : iC ⋙ L' ≅ L ⋙ iD) (comm2 : iD ⋙ R' ≅ R ⋙ iC)
+variable [iC.Full] [iC.Faithful] [iD.Full] [iD.Faithful]
+
+/-- If `C` is a full subcategory of `C'` and `D` is a full subcategory of `D'`, then we can restrict
+an adjunction `L' ⊣ R'` where `L' : C' ⥤ D'` and `R' : D' ⥤ C'` to `C` and `D`.
+The construction here is slightly more general, in that `C` is required only to have a full and
+faithful "inclusion" functor `iC : C ⥤ C'` (and similarly `iD : D ⥤ D'`) which commute (up to
+natural isomorphism) with the proposed restrictions.
+-/
+def restrictFullyFaithful : L ⊣ R :=
+  Adjunction.mkOfHomEquiv
+    { homEquiv := fun X Y =>
+        calc
+          (L.obj X ⟶ Y) ≃ (iD.obj (L.obj X) ⟶ iD.obj Y) := equivOfFullyFaithful iD
+          _ ≃ (L'.obj (iC.obj X) ⟶ iD.obj Y) := Iso.homCongr (comm1.symm.app X) (Iso.refl _)
+          _ ≃ (iC.obj X ⟶ R'.obj (iD.obj Y)) := adj.homEquiv _ _
+          _ ≃ (iC.obj X ⟶ iC.obj (R.obj Y)) := Iso.homCongr (Iso.refl _) (comm2.app Y)
+          _ ≃ (X ⟶ R.obj Y) := (equivOfFullyFaithful iC).symm
+
+      homEquiv_naturality_left_symm := fun {X' X Y} f g => by
+        apply iD.map_injective
+        simpa [Trans.trans] using (comm1.inv.naturality_assoc f _).symm
+      homEquiv_naturality_right := fun {X Y' Y} f g => by
+        apply iC.map_injective
+        suffices R'.map (iD.map g) ≫ comm2.hom.app Y = comm2.hom.app Y' ≫ iC.map (R.map g) by
+          simp [Trans.trans, this]
+        apply comm2.hom.naturality g }
+#align category_theory.adjunction.restrict_fully_faithful CategoryTheory.Adjunction.restrictFullyFaithful
+
+@[simp, reassoc]
+lemma map_restrictFullyFaithful_unit_app (X : C) :
+    iC.map ((restrictFullyFaithful iC iD adj comm1 comm2).unit.app X) =
+    adj.unit.app (iC.obj X) ≫ R'.map (comm1.hom.app X) ≫ comm2.hom.app (L.obj X) := by
+  simp [restrictFullyFaithful]
+
+@[simp, reassoc]
+lemma map_restrictFullyFaithful_counit_app (X : D) :
+    iD.map ((restrictFullyFaithful iC iD adj comm1 comm2).counit.app X) =
+    comm1.inv.app (R.obj X) ≫ L'.map (comm2.inv.app X) ≫ adj.counit.app (iD.obj X) := by
+  dsimp [restrictFullyFaithful]
+  simp
+
+end CategoryTheory.Adjunction
diff --git a/Mathlib/CategoryTheory/Bicategory/Coherence.lean b/Mathlib/CategoryTheory/Bicategory/Coherence.lean
index 1ffceaac2c20b..c2586df37b007 100644
--- a/Mathlib/CategoryTheory/Bicategory/Coherence.lean
+++ b/Mathlib/CategoryTheory/Bicategory/Coherence.lean
@@ -80,13 +80,13 @@ See `inclusion`.
 -/
 def preinclusion (B : Type u) [Quiver.{v + 1} B] :
     PrelaxFunctor (LocallyDiscrete (Paths B)) (FreeBicategory B) where
-  obj := id
-  map := @fun a b => (@inclusionPath B _ a b).obj
+  obj a := a.as
+  map := @fun a b f => (@inclusionPath B _ a.as b.as).obj f
   map₂ η := (inclusionPath _ _).map η
 #align category_theory.free_bicategory.preinclusion CategoryTheory.FreeBicategory.preinclusion
 
 @[simp]
-theorem preinclusion_obj (a : B) : (preinclusion B).obj a = a :=
+theorem preinclusion_obj (a : B) : (preinclusion B).obj ⟨a⟩ = a :=
   rfl
 #align category_theory.free_bicategory.preinclusion_obj CategoryTheory.FreeBicategory.preinclusion_obj
 
@@ -196,7 +196,7 @@ theorem normalizeAux_nil_comp {a b c : B} (f : Hom a b) (g : Hom b c) :
 /-- The normalization pseudofunctor for the free bicategory on a quiver `B`. -/
 def normalize (B : Type u) [Quiver.{v + 1} B] :
     Pseudofunctor (FreeBicategory B) (LocallyDiscrete (Paths B)) where
-  obj := id
+  obj a := ⟨a⟩
   map f := ⟨normalizeAux nil f⟩
   map₂ η := eqToHom <| Discrete.ext _ _ <| normalizeAux_congr nil η
   mapId a := eqToIso <| Discrete.ext _ _ rfl
@@ -250,7 +250,7 @@ def inclusion (B : Type u) [Quiver.{v + 1} B] :
     Pseudofunctor (LocallyDiscrete (Paths B)) (FreeBicategory B) :=
   { -- All the conditions for 2-morphisms are trivial thanks to the coherence theorem!
     preinclusion B with
-    mapId := fun a : FreeBicategory B => Iso.refl (𝟙 a)
+    mapId := fun a => Iso.refl _
     mapComp := fun f g => inclusionMapCompAux f.as g.as }
 #align category_theory.free_bicategory.inclusion CategoryTheory.FreeBicategory.inclusion
 
diff --git a/Mathlib/CategoryTheory/Bicategory/LocallyDiscrete.lean b/Mathlib/CategoryTheory/Bicategory/LocallyDiscrete.lean
index fb7a0950c6394..f6e0c09bba0b1 100644
--- a/Mathlib/CategoryTheory/Bicategory/LocallyDiscrete.lean
+++ b/Mathlib/CategoryTheory/Bicategory/LocallyDiscrete.lean
@@ -1,7 +1,7 @@
 /-
 Copyright (c) 2022 Yuma Mizuno. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Yuma Mizuno
+Authors: Yuma Mizuno, Calle Sönne
 -/
 import Mathlib.CategoryTheory.DiscreteCategory
 import Mathlib.CategoryTheory.Bicategory.Functor
@@ -19,49 +19,69 @@ other words, the category consisting of the 1-morphisms between each pair of obj
 in `LocallyDiscrete C` is defined as the discrete category associated with the type `X ⟶ Y`.
 -/
 
-
 namespace CategoryTheory
 
 open Bicategory Discrete
 
 open Bicategory
 
+
 universe w₂ v v₁ v₂ u u₁ u₂
 
 variable {C : Type u}
 
-/-- A type synonym for promoting any type to a category,
-with the only morphisms being equalities.
+/-- A wrapper for promoting any category to a bicategory,
+with the only 2-morphisms being equalities.
 -/
-def LocallyDiscrete (C : Type u) :=
-  C
-#align category_theory.locally_discrete CategoryTheory.LocallyDiscrete
+@[ext]
+structure LocallyDiscrete (C : Type u) where
+  /-- A wrapper for promoting any category to a bicategory,
+  with the only 2-morphisms being equalities.
+  -/
+  as : C
 
 namespace LocallyDiscrete
 
-instance [Inhabited C] : Inhabited (LocallyDiscrete C) := ⟨(default : C)⟩
+@[simp]
+theorem mk_as (a : LocallyDiscrete C) : mk a.as = a := rfl
+
+/-- `LocallyDiscrete C` is equivalent to the original type `C`. -/
+@[simps]
+def locallyDiscreteEquiv : LocallyDiscrete C ≃ C where
+  toFun := LocallyDiscrete.as
+  invFun := LocallyDiscrete.mk
+  left_inv := by aesop_cat
+  right_inv := by aesop_cat
 
-instance [CategoryStruct.{v} C] : CategoryStruct (LocallyDiscrete C)
+instance [DecidableEq C] : DecidableEq (LocallyDiscrete C) :=
+  locallyDiscreteEquiv.decidableEq
+
+instance [Inhabited C] : Inhabited (LocallyDiscrete C) :=
+  ⟨⟨default⟩⟩
+
+instance categoryStruct [CategoryStruct.{v} C] : CategoryStruct (LocallyDiscrete C)
     where
-  Hom := fun X Y : C => Discrete (X ⟶ Y)
-  id := fun X : C => ⟨𝟙 X⟩
+  Hom := fun a b => Discrete (a.as ⟶ b.as)
+  id := fun a => ⟨𝟙 a.as⟩
   comp f g := ⟨f.as ≫ g.as⟩
 
 variable [CategoryStruct.{v} C]
 
-instance (priority := 900) homSmallCategory (X Y : LocallyDiscrete C) : SmallCategory (X ⟶ Y) :=
-  let X' : C := X
-  let Y' : C := Y
-  CategoryTheory.discreteCategory (X' ⟶ Y')
+@[simp]
+lemma id_as (a : LocallyDiscrete C) : (𝟙 a : Discrete (a.as ⟶ a.as)).as = 𝟙 a.as :=
+  rfl
+
+@[simp]
+lemma comp_as {a b c : LocallyDiscrete C} (f : a ⟶ b) (g : b ⟶ c) : (f ≫ g).as = f.as ≫ g.as :=
+  rfl
+
+instance (priority := 900) homSmallCategory (a b : LocallyDiscrete C) : SmallCategory (a ⟶ b) :=
+  CategoryTheory.discreteCategory (a.as ⟶ b.as)
 #align category_theory.locally_discrete.hom_small_category CategoryTheory.LocallyDiscrete.homSmallCategory
 
 -- Porting note: Manually adding this instance (inferInstance doesn't work)
-instance subsingleton2Hom {X Y : LocallyDiscrete C} (f g : X ⟶ Y) : Subsingleton (f ⟶ g) :=
-  let X' : C := X
-  let Y' : C := Y
-  let f' : Discrete (X' ⟶ Y') := f
-  let g' : Discrete (X' ⟶ Y') := g
-  show Subsingleton (f' ⟶ g') from inferInstance
+instance subsingleton2Hom {a b : LocallyDiscrete C} (f g : a ⟶ b) : Subsingleton (f ⟶ g) :=
+  instSubsingletonDiscreteHom f g
 
 /-- Extract the equation from a 2-morphism in a locally discrete 2-category. -/
 theorem eq_of_hom {X Y : LocallyDiscrete C} {f g : X ⟶ Y} (η : f ⟶ g) : f = g :=
@@ -70,7 +90,8 @@ theorem eq_of_hom {X Y : LocallyDiscrete C} {f g : X ⟶ Y} (η : f ⟶ g) : f =
 
 end LocallyDiscrete
 
-variable (C) [Category.{v} C]
+variable (C)
+variable [Category.{v} C]
 
 /-- The locally discrete bicategory on a category is a bicategory in which the objects and the
 1-morphisms are the same as those in the underlying category, and the 2-morphisms are the
@@ -80,42 +101,33 @@ instance locallyDiscreteBicategory : Bicategory (LocallyDiscrete C)
     where
   whiskerLeft f g h η := eqToHom (congr_arg₂ (· ≫ ·) rfl (LocallyDiscrete.eq_of_hom η))
   whiskerRight η h := eqToHom (congr_arg₂ (· ≫ ·) (LocallyDiscrete.eq_of_hom η) rfl)
-  associator f g h :=
-    eqToIso <| by
-      apply Discrete.ext
-      change (f.as ≫ g.as) ≫ h.as = f.as ≫ (g.as ≫ h.as)
-      rw [Category.assoc]
-  leftUnitor f :=
-    eqToIso <| by
-      apply Discrete.ext
-      change 𝟙 _ ≫ _ = _
-      rw [Category.id_comp]
-  rightUnitor f :=
-    eqToIso <| by
-      apply Discrete.ext
-      change _ ≫ 𝟙 _ = _
-      rw [Category.comp_id]
+  associator f g h := eqToIso <| by apply Discrete.ext; simp
+  leftUnitor f := eqToIso <| by apply Discrete.ext; simp
+  rightUnitor f := eqToIso <| by apply Discrete.ext; simp
 #align category_theory.locally_discrete_bicategory CategoryTheory.locallyDiscreteBicategory
 
 /-- A locally discrete bicategory is strict. -/
-instance locallyDiscreteBicategory.strict : Strict (LocallyDiscrete C)
-    where
-  id_comp := by
-    intros
-    apply Discrete.ext
-    apply Category.id_comp
-  comp_id := by
-    intros
-    apply Discrete.ext
-    apply Category.comp_id
-  assoc := by
-    intros
-    apply Discrete.ext
-    apply Category.assoc
+instance locallyDiscreteBicategory.strict : Strict (LocallyDiscrete C) where
+  id_comp f := Discrete.ext _ _ (Category.id_comp _)
+  comp_id f := Discrete.ext _ _ (Category.comp_id _)
+  assoc f g h := Discrete.ext _ _ (Category.assoc _ _ _)
 #align category_theory.locally_discrete_bicategory.strict CategoryTheory.locallyDiscreteBicategory.strict
 
 variable {I : Type u₁} [Category.{v₁} I] {B : Type u₂} [Bicategory.{w₂, v₂} B] [Strict B]
 
+/--
+If `B` is a strict bicategory and `I` is a (1-)category, any functor (of 1-categories) `I ⥤ B` can
+be promoted to a pseudofunctor from `LocallyDiscrete I` to `B`.
+-/
+@[simps]
+def Functor.toPseudoFunctor (F : I ⥤ B) : Pseudofunctor (LocallyDiscrete I) B
+    where
+  obj i := F.obj i.as
+  map f := F.map f.as
+  map₂ η := eqToHom (congr_arg _ (LocallyDiscrete.eq_of_hom η))
+  mapId i := eqToIso (F.map_id i.as)
+  mapComp f g := eqToIso (F.map_comp f.as g.as)
+
 /--
 If `B` is a strict bicategory and `I` is a (1-)category, any functor (of 1-categories) `I ⥤ B` can
 be promoted to an oplax functor from `LocallyDiscrete I` to `B`.
@@ -123,11 +135,35 @@ be promoted to an oplax functor from `LocallyDiscrete I` to `B`.
 @[simps]
 def Functor.toOplaxFunctor (F : I ⥤ B) : OplaxFunctor (LocallyDiscrete I) B
     where
-  obj := F.obj
+  obj i := F.obj i.as
   map f := F.map f.as
   map₂ η := eqToHom (congr_arg _ (LocallyDiscrete.eq_of_hom η))
-  mapId i := eqToHom (F.map_id i)
+  mapId i := eqToHom (F.map_id i.as)
   mapComp f g := eqToHom (F.map_comp f.as g.as)
 #align category_theory.functor.to_oplax_functor CategoryTheory.Functor.toOplaxFunctor
 
 end CategoryTheory
+
+section Quiver
+
+open CategoryTheory LocallyDiscrete
+
+universe v u
+
+variable {C : Type u} [CategoryStruct.{v} C]
+
+/-- The 1-morphism in `LocallyDiscrete C` associated to a given morphism `f : a ⟶ b` in `C` -/
+@[simps]
+def Quiver.Hom.toLoc {a b : C} (f : a ⟶ b) : LocallyDiscrete.mk a ⟶ LocallyDiscrete.mk b :=
+  ⟨f⟩
+
+@[simp]
+lemma Quiver.Hom.id_toLoc (a : C) : (𝟙 a).toLoc = 𝟙 (LocallyDiscrete.mk a) :=
+  rfl
+
+@[simp]
+lemma Quiver.Hom.comp_toLoc {a b c : C} (f : a ⟶ b) (g : b ⟶ c) :
+    (f ≫ g).toLoc = f.toLoc ≫ g.toLoc :=
+  rfl
+
+end Quiver
diff --git a/Mathlib/CategoryTheory/Groupoid/Subgroupoid.lean b/Mathlib/CategoryTheory/Groupoid/Subgroupoid.lean
index 49998783436ad..4eeb0822e2bf5 100644
--- a/Mathlib/CategoryTheory/Groupoid/Subgroupoid.lean
+++ b/Mathlib/CategoryTheory/Groupoid/Subgroupoid.lean
@@ -94,7 +94,7 @@ theorem mul_mem_cancel_left {c d e : C} {f : c ⟶ d} {g : d ⟶ e} (hf : f ∈
   · rintro h
     suffices Groupoid.inv f ≫ f ≫ g ∈ S.arrows d e by
       simpa only [inv_eq_inv, IsIso.inv_hom_id_assoc] using this
-    · apply S.mul (S.inv hf) h
+    apply S.mul (S.inv hf) h
   · apply S.mul hf
 #align category_theory.subgroupoid.mul_mem_cancel_left CategoryTheory.Subgroupoid.mul_mem_cancel_left
 
@@ -104,7 +104,7 @@ theorem mul_mem_cancel_right {c d e : C} {f : c ⟶ d} {g : d ⟶ e} (hg : g ∈
   · rintro h
     suffices (f ≫ g) ≫ Groupoid.inv g ∈ S.arrows c d by
       simpa only [inv_eq_inv, IsIso.hom_inv_id, Category.comp_id, Category.assoc] using this
-    · apply S.mul h (S.inv hg)
+    apply S.mul h (S.inv hg)
   · exact fun hf => S.mul hf hg
 #align category_theory.subgroupoid.mul_mem_cancel_right CategoryTheory.Subgroupoid.mul_mem_cancel_right
 
@@ -590,7 +590,7 @@ theorem isNormal_map (hφ : Function.Injective φ.obj) (hφ' : im φ hφ = ⊤)
       simp only [eqToHom_refl, Category.comp_id, Category.id_comp, inv_eq_inv]
       suffices Map.Arrows φ hφ S (φ.obj c') (φ.obj c') (φ.map <| Groupoid.inv f ≫ γ ≫ f) by
         simp only [inv_eq_inv, Functor.map_comp, Functor.map_inv] at this; exact this
-      · constructor; apply Sn.conj f γS }
+      constructor; apply Sn.conj f γS }
 #align category_theory.subgroupoid.is_normal_map CategoryTheory.Subgroupoid.isNormal_map
 
 end Hom
diff --git a/Mathlib/CategoryTheory/Limits/Preserves/Basic.lean b/Mathlib/CategoryTheory/Limits/Preserves/Basic.lean
index af05eeaa71d2c..7d9758ccc36b7 100644
--- a/Mathlib/CategoryTheory/Limits/Preserves/Basic.lean
+++ b/Mathlib/CategoryTheory/Limits/Preserves/Basic.lean
@@ -271,8 +271,8 @@ def preservesLimitsOfShapeOfEquiv {J' : Type w₂} [Category.{w₂'} J'] (e : J
         have := (isLimitOfPreserves F (t.whiskerEquivalence e)).whiskerEquivalence e.symm
         apply ((IsLimit.postcomposeHomEquiv equ _).symm this).ofIsoLimit
         refine' Cones.ext (Iso.refl _) fun j => _
-        · dsimp
-          simp [equ, ← Functor.map_comp] }
+        dsimp
+        simp [equ, ← Functor.map_comp] }
 #align category_theory.limits.preserves_limits_of_shape_of_equiv CategoryTheory.Limits.preservesLimitsOfShapeOfEquiv
 
 /-- A functor preserving larger limits also preserves smaller limits. -/
@@ -340,8 +340,8 @@ def preservesColimitsOfShapeOfEquiv {J' : Type w₂} [Category.{w₂'} J'] (e :
         have := (isColimitOfPreserves F (t.whiskerEquivalence e)).whiskerEquivalence e.symm
         apply ((IsColimit.precomposeInvEquiv equ _).symm this).ofIsoColimit
         refine' Cocones.ext (Iso.refl _) fun j => _
-        · dsimp
-          simp [equ, ← Functor.map_comp] }
+        dsimp
+        simp [equ, ← Functor.map_comp] }
 #align category_theory.limits.preserves_colimits_of_shape_of_equiv CategoryTheory.Limits.preservesColimitsOfShapeOfEquiv
 
 /-- A functor preserving larger colimits also preserves smaller colimits. -/
diff --git a/Mathlib/CategoryTheory/Limits/Shapes/BinaryProducts.lean b/Mathlib/CategoryTheory/Limits/Shapes/BinaryProducts.lean
index b0c5d6cf6cf9f..bb4bd23dba8b9 100644
--- a/Mathlib/CategoryTheory/Limits/Shapes/BinaryProducts.lean
+++ b/Mathlib/CategoryTheory/Limits/Shapes/BinaryProducts.lean
@@ -1441,13 +1441,13 @@ def Over.coprod [HasBinaryCoproducts C] {A : C} : Over A ⥤ Over A ⥤ Over A w
         dsimp; rw [coprod.map_desc, Category.id_comp, Over.w k])
       naturality := fun f g k => by
         ext;
-          · dsimp; simp }
+        dsimp; simp }
   map_id X := by
     ext
-    · dsimp; simp
+    dsimp; simp
   map_comp f g := by
     ext
-    · dsimp; simp
+    dsimp; simp
 #align category_theory.over.coprod CategoryTheory.Over.coprod
 
 end CategoryTheory
diff --git a/Mathlib/CategoryTheory/Limits/Shapes/FiniteLimits.lean b/Mathlib/CategoryTheory/Limits/Shapes/FiniteLimits.lean
index ced0dfbdbaf96..55aa2b5a679a7 100644
--- a/Mathlib/CategoryTheory/Limits/Shapes/FiniteLimits.lean
+++ b/Mathlib/CategoryTheory/Limits/Shapes/FiniteLimits.lean
@@ -146,7 +146,7 @@ instance instFintypeWalkingParallelPairHom (j j' : WalkingParallelPair) :
       (WalkingParallelPair.recOn j' ∅ [WalkingParallelPairHom.id one].toFinset)
   complete := by
     rintro (_|_) <;> simp
-    · cases j <;> simp
+    cases j <;> simp
 end
 
 instance : FinCategory WalkingParallelPair where
diff --git a/Mathlib/CategoryTheory/Limits/Shapes/Images.lean b/Mathlib/CategoryTheory/Limits/Shapes/Images.lean
index 4c20abc48ac8e..b758b784c505b 100644
--- a/Mathlib/CategoryTheory/Limits/Shapes/Images.lean
+++ b/Mathlib/CategoryTheory/Limits/Shapes/Images.lean
@@ -110,8 +110,8 @@ theorem ext {F F' : MonoFactorisation f} (hI : F.I = F'.I)
   cases' hI
   simp? at hm says simp only [eqToHom_refl, Category.id_comp] at hm
   congr
-  · apply (cancel_mono Fm).1
-    rw [Ffac, hm, Ffac']
+  apply (cancel_mono Fm).1
+  rw [Ffac, hm, Ffac']
 #align category_theory.limits.mono_factorisation.ext CategoryTheory.Limits.MonoFactorisation.ext
 
 /-- Any mono factorisation of `f` gives a mono factorisation of `f ≫ g` when `g` is a mono. -/
diff --git a/Mathlib/CategoryTheory/Limits/Shapes/WidePullbacks.lean b/Mathlib/CategoryTheory/Limits/Shapes/WidePullbacks.lean
index 16ff8ee3919fa..d994d30869cef 100644
--- a/Mathlib/CategoryTheory/Limits/Shapes/WidePullbacks.lean
+++ b/Mathlib/CategoryTheory/Limits/Shapes/WidePullbacks.lean
@@ -243,7 +243,7 @@ def wideSpan (B : C) (objs : J → C) (arrows : ∀ j : J, B ⟶ objs j) : WideP
     cases f
     · simp only [Eq.ndrec, hom_id, eq_rec_constant, Category.id_comp]; congr
     · cases g
-      · simp only [Eq.ndrec, hom_id, eq_rec_constant, Category.comp_id]; congr
+      simp only [Eq.ndrec, hom_id, eq_rec_constant, Category.comp_id]; congr
 #align category_theory.limits.wide_pushout_shape.wide_span CategoryTheory.Limits.WidePushoutShape.wideSpan
 
 /-- Every diagram is naturally isomorphic (actually, equal) to a `wideSpan` -/
diff --git a/Mathlib/CategoryTheory/Sites/Pullback.lean b/Mathlib/CategoryTheory/Sites/Pullback.lean
index 2d5160bffbd5c..61b243b44626d 100644
--- a/Mathlib/CategoryTheory/Sites/Pullback.lean
+++ b/Mathlib/CategoryTheory/Sites/Pullback.lean
@@ -3,6 +3,7 @@ Copyright (c) 2021 Andrew Yang. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Andrew Yang
 -/
+import Mathlib.CategoryTheory.Adjunction.Restrict
 import Mathlib.CategoryTheory.Sites.CoverPreserving
 import Mathlib.CategoryTheory.Sites.LeftExact
 
diff --git a/Mathlib/CategoryTheory/Subobject/MonoOver.lean b/Mathlib/CategoryTheory/Subobject/MonoOver.lean
index 8215e9bd2bd85..57aaef261f6b1 100644
--- a/Mathlib/CategoryTheory/Subobject/MonoOver.lean
+++ b/Mathlib/CategoryTheory/Subobject/MonoOver.lean
@@ -4,8 +4,8 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Bhavik Mehta, Scott Morrison
 -/
 import Mathlib.CategoryTheory.Limits.Over
-import Mathlib.CategoryTheory.Limits.Shapes.Images
 import Mathlib.CategoryTheory.Adjunction.Reflective
+import Mathlib.CategoryTheory.Adjunction.Restrict
 
 #align_import category_theory.subobject.mono_over from "leanprover-community/mathlib"@"70fd9563a21e7b963887c9360bd29b2393e6225a"
 
diff --git a/Mathlib/Combinatorics/SimpleGraph/Connectivity.lean b/Mathlib/Combinatorics/SimpleGraph/Connectivity.lean
index 91679e173a76e..8c85659b32099 100644
--- a/Mathlib/Combinatorics/SimpleGraph/Connectivity.lean
+++ b/Mathlib/Combinatorics/SimpleGraph/Connectivity.lean
@@ -1944,9 +1944,9 @@ abbrev toDeleteEdge (e : Sym2 V) (p : G.Walk v w) (hp : e ∉ p.edges) :
 theorem map_toDeleteEdges_eq (s : Set (Sym2 V)) {p : G.Walk v w} (hp) :
     Walk.map (Hom.mapSpanningSubgraphs (G.deleteEdges_le s)) (p.toDeleteEdges s hp) = p := by
   rw [← transfer_eq_map_of_le, transfer_transfer, transfer_self]
-  · intros e
-    rw [edges_transfer]
-    apply edges_subset_edgeSet p
+  intros e
+  rw [edges_transfer]
+  apply edges_subset_edgeSet p
 #align simple_graph.walk.map_to_delete_edges_eq SimpleGraph.Walk.map_toDeleteEdges_eq
 
 protected theorem IsPath.toDeleteEdges (s : Set (Sym2 V))
diff --git a/Mathlib/Computability/Halting.lean b/Mathlib/Computability/Halting.lean
index abd70a07a11fe..297a11ae8f03d 100644
--- a/Mathlib/Computability/Halting.lean
+++ b/Mathlib/Computability/Halting.lean
@@ -252,11 +252,11 @@ theorem computable_iff_re_compl_re {p : α → Prop} [DecidablePred p] :
           simp only [Part.mem_map_iff, Part.mem_assert_iff, Part.mem_some_iff, exists_prop,
             and_true, exists_const] at hx hy
           cases hy.1 hx.1)
-      · refine' Partrec.of_eq pk fun n => Part.eq_some_iff.2 _
-        rw [hk]
-        simp only [Part.mem_map_iff, Part.mem_assert_iff, Part.mem_some_iff, exists_prop, and_true,
-          true_eq_decide_iff, and_self, exists_const, false_eq_decide_iff]
-        apply Decidable.em⟩⟩
+      refine' Partrec.of_eq pk fun n => Part.eq_some_iff.2 _
+      rw [hk]
+      simp only [Part.mem_map_iff, Part.mem_assert_iff, Part.mem_some_iff, exists_prop, and_true,
+        true_eq_decide_iff, and_self, exists_const, false_eq_decide_iff]
+      apply Decidable.em⟩⟩
 #align computable_pred.computable_iff_re_compl_re ComputablePred.computable_iff_re_compl_re
 
 theorem computable_iff_re_compl_re' {p : α → Prop} :
diff --git a/Mathlib/Computability/Partrec.lean b/Mathlib/Computability/Partrec.lean
index 0f978e483e9b0..524a26a43cd9f 100644
--- a/Mathlib/Computability/Partrec.lean
+++ b/Mathlib/Computability/Partrec.lean
@@ -835,10 +835,10 @@ theorem fix_aux {α σ} (f : α →. Sum σ α) (a : α) (b : σ) :
         exact Or.inr ⟨_, hk, h₂⟩
       · rwa [le_antisymm (Nat.le_of_lt_succ mk) km]
     · rcases IH _ am₃ k.succ (by simp [F]; exact ⟨_, hk, am₃⟩) with ⟨n, hn₁, hn₂⟩
-      · refine' ⟨n, hn₁, fun m mn km => _⟩
-        cases' km.lt_or_eq_dec with km km
-        · exact hn₂ _ mn km
-        · exact km ▸ ⟨_, hk⟩
+      refine' ⟨n, hn₁, fun m mn km => _⟩
+      cases' km.lt_or_eq_dec with km km
+      · exact hn₂ _ mn km
+      · exact km ▸ ⟨_, hk⟩
 #align partrec.fix_aux Partrec.fix_aux
 
 theorem fix {f : α →. Sum σ α} (hf : Partrec f) : Partrec (PFun.fix f) := by
diff --git a/Mathlib/Computability/TMToPartrec.lean b/Mathlib/Computability/TMToPartrec.lean
index 117b2f67ac835..26716f56a3632 100644
--- a/Mathlib/Computability/TMToPartrec.lean
+++ b/Mathlib/Computability/TMToPartrec.lean
@@ -666,10 +666,10 @@ theorem cont_eval_fix {f k v} (fok : Code.Ok f) :
         obtain ⟨v₁, hv₁, v₂, hv₂, h₃⟩ :=
           IH (stepRet (k₀.then (Cont.fix f k)) v₀) (by rw [stepRet, if_neg he, e₁]; rfl)
             v'.tail _ stepRet_then (by apply ReflTransGen.single; rw [e₀]; rfl)
-        · refine' ⟨_, PFun.mem_fix_iff.2 _, h₃⟩
-          simp only [Part.eq_some_iff.2 hv₁, Part.map_some, Part.mem_some_iff]
-          split_ifs at hv₂ ⊢ <;> [exact Or.inl (congr_arg Sum.inl (Part.mem_some_iff.1 hv₂));
-            exact Or.inr ⟨_, rfl, hv₂⟩]
+        refine' ⟨_, PFun.mem_fix_iff.2 _, h₃⟩
+        simp only [Part.eq_some_iff.2 hv₁, Part.map_some, Part.mem_some_iff]
+        split_ifs at hv₂ ⊢ <;> [exact Or.inl (congr_arg Sum.inl (Part.mem_some_iff.1 hv₂));
+          exact Or.inr ⟨_, rfl, hv₂⟩]
     · exact IH _ rfl _ _ stepRet_then (ReflTransGen.tail hr rfl)
   · rintro ⟨v', he, hr⟩
     rw [reaches_eval] at hr
@@ -1344,8 +1344,8 @@ theorem move_ok {p k₁ k₂ q s L₁ o L₂} {S : K' → List Γ'} (h₁ : k₁
     simp only [splitAtPred, Option.elim, List.head?, List.tail_cons, Option.iget_some] at e ⊢
     revert e; cases p a <;> intro e <;>
       simp only [cond_false, cond_true, Prod.mk.injEq, true_and, false_and] at e ⊢
-    · simp only [e]
-      rfl
+    simp only [e]
+    rfl
   · refine' TransGen.head rfl _
     simp only [TM2.step, Option.mem_def, TM2.stepAux, Option.elim, ne_eq, List.reverseAux_cons]
     cases' e₁ : S k₁ with a' Sk <;> rw [e₁, splitAtPred] at e
@@ -1402,8 +1402,8 @@ theorem clear_ok {p k q s L₁ o L₂} {S : K' → List Γ'} (e : splitAtPred p
     simp only [splitAtPred, Option.elim, List.head?, List.tail_cons] at e ⊢
     revert e; cases p a <;> intro e <;>
       simp only [cond_false, cond_true, Prod.mk.injEq, true_and, false_and] at e ⊢
-    · rcases e with ⟨e₁, e₂⟩
-      rw [e₁, e₂]
+    rcases e with ⟨e₁, e₂⟩
+    rw [e₁, e₂]
   · refine' TransGen.head rfl _
     simp only [TM2.step, Option.mem_def, TM2.stepAux, Option.elim]
     cases' e₁ : S k with a' Sk <;> rw [e₁, splitAtPred] at e
diff --git a/Mathlib/Data/FP/Basic.lean b/Mathlib/Data/FP/Basic.lean
index 8fc937bb7548e..5c8af52cfe045 100644
--- a/Mathlib/Data/FP/Basic.lean
+++ b/Mathlib/Data/FP/Basic.lean
@@ -155,7 +155,7 @@ unsafe def ofPosRatDn (n : ℕ+) (d : ℕ+) : Float × Bool := by
   let r := mkRat n₂ d₂
   let m := r.floor
   refine' (Float.finite Bool.false e₃ (Int.toNat m) _, r.den = 1)
-  · exact lcProof
+  exact lcProof
 #align fp.of_pos_rat_dn FP.ofPosRatDn
 
 -- Porting note: remove this line when you dropped 'lcProof'
diff --git a/Mathlib/Data/Finset/Lattice.lean b/Mathlib/Data/Finset/Lattice.lean
index ecd0ea13977f4..2489f2658be2a 100644
--- a/Mathlib/Data/Finset/Lattice.lean
+++ b/Mathlib/Data/Finset/Lattice.lean
@@ -1768,7 +1768,7 @@ theorem min_erase_ne_self {s : Finset α} : (s.erase x).min ≠ x := by
   convert @max_erase_ne_self αᵒᵈ _ (toDual x) (s.map toDual.toEmbedding) using 1
   apply congr_arg -- Porting note: forces unfolding to see `Finset.min` is `Finset.max`
   congr!
-  · ext; simp only [mem_map_equiv]; exact Iff.rfl
+  ext; simp only [mem_map_equiv]; exact Iff.rfl
 #align finset.min_erase_ne_self Finset.min_erase_ne_self
 
 theorem exists_next_right {x : α} {s : Finset α} (h : ∃ y ∈ s, x < y) :
diff --git a/Mathlib/Data/Finset/NatAntidiagonal.lean b/Mathlib/Data/Finset/NatAntidiagonal.lean
index ed7cc5f1ecd65..f6f0e0abff046 100644
--- a/Mathlib/Data/Finset/NatAntidiagonal.lean
+++ b/Mathlib/Data/Finset/NatAntidiagonal.lean
@@ -72,7 +72,7 @@ theorem antidiagonal_succ (n : ℕ) :
         (by simp) := by
   apply eq_of_veq
   rw [cons_val, map_val]
-  · apply Multiset.Nat.antidiagonal_succ
+  apply Multiset.Nat.antidiagonal_succ
 #align finset.nat.antidiagonal_succ Finset.Nat.antidiagonal_succ
 
 theorem antidiagonal_succ' (n : ℕ) :
diff --git a/Mathlib/Data/Finset/Powerset.lean b/Mathlib/Data/Finset/Powerset.lean
index a1e8bda09004d..b5a373cb7dbce 100644
--- a/Mathlib/Data/Finset/Powerset.lean
+++ b/Mathlib/Data/Finset/Powerset.lean
@@ -320,9 +320,9 @@ theorem powersetCard_sup [DecidableEq α] (u : Finset α) (n : ℕ) (hn : n < u.
     simp only [mem_biUnion, exists_prop, id]
     obtain ⟨t, ht⟩ : ∃ t, t ∈ powersetCard n (u.erase x) := powersetCard_nonempty.2
       (le_trans (Nat.le_sub_one_of_lt hn) pred_card_le_card_erase)
-    · refine' ⟨insert x t, _, mem_insert_self _ _⟩
-      rw [← insert_erase hx, powersetCard_succ_insert (not_mem_erase _ _)]
-      exact mem_union_right _ (mem_image_of_mem _ ht)
+    refine' ⟨insert x t, _, mem_insert_self _ _⟩
+    rw [← insert_erase hx, powersetCard_succ_insert (not_mem_erase _ _)]
+    exact mem_union_right _ (mem_image_of_mem _ ht)
 #align finset.powerset_len_sup Finset.powersetCard_sup
 
 theorem powersetCard_map {β : Type*} (f : α ↪ β) (n : ℕ) (s : Finset α) :
diff --git a/Mathlib/Data/Finsupp/AList.lean b/Mathlib/Data/Finsupp/AList.lean
index a38cd81a1005e..e210c37b6d545 100644
--- a/Mathlib/Data/Finsupp/AList.lean
+++ b/Mathlib/Data/Finsupp/AList.lean
@@ -127,10 +127,10 @@ theorem _root_.Finsupp.toAList_lookupFinsupp (f : α →₀ M) : f.toAList.looku
   classical
     by_cases h : f a = 0
     · suffices f.toAList.lookup a = none by simp [h, this]
-      · simp [lookup_eq_none, h]
+      simp [lookup_eq_none, h]
     · suffices f.toAList.lookup a = some (f a) by simp [h, this]
-      · apply mem_lookup_iff.2
-        simpa using h
+      apply mem_lookup_iff.2
+      simpa using h
 #align finsupp.to_alist_lookup_finsupp Finsupp.toAList_lookupFinsupp
 
 theorem lookupFinsupp_surjective : Function.Surjective (@lookupFinsupp α M _) := fun f =>
diff --git a/Mathlib/Data/Finsupp/Basic.lean b/Mathlib/Data/Finsupp/Basic.lean
index 5b0ff8720d4fc..431c75bdecbe7 100644
--- a/Mathlib/Data/Finsupp/Basic.lean
+++ b/Mathlib/Data/Finsupp/Basic.lean
@@ -481,7 +481,7 @@ theorem mapDomain_comp {f : α → β} {g : β → γ} :
   · intro
     exact single_add _
   refine' sum_congr fun _ _ => sum_single_index _
-  · exact single_zero _
+  exact single_zero _
 #align finsupp.map_domain_comp Finsupp.mapDomain_comp
 
 @[simp]
diff --git a/Mathlib/Data/Finsupp/BigOperators.lean b/Mathlib/Data/Finsupp/BigOperators.lean
index 0ff1c8db46bab..2dad3a837817b 100644
--- a/Mathlib/Data/Finsupp/BigOperators.lean
+++ b/Mathlib/Data/Finsupp/BigOperators.lean
@@ -88,12 +88,12 @@ theorem List.support_sum_eq [AddMonoid M] (l : List (ι →₀ M))
     rw [Finsupp.support_add_eq, IH hl.right, Finset.sup_eq_union]
     suffices _root_.Disjoint hd.support (tl.foldr (fun x y ↦ (Finsupp.support x ⊔ y)) ∅) by
       exact Finset.disjoint_of_subset_right (List.support_sum_subset _) this
-    · rw [← List.foldr_map, ← Finset.bot_eq_empty, List.foldr_sup_eq_sup_toFinset,
-        Finset.disjoint_sup_right]
-      intro f hf
-      simp only [List.mem_toFinset, List.mem_map] at hf
-      obtain ⟨f, hf, rfl⟩ := hf
-      exact hl.left _ hf
+    rw [← List.foldr_map, ← Finset.bot_eq_empty, List.foldr_sup_eq_sup_toFinset,
+      Finset.disjoint_sup_right]
+    intro f hf
+    simp only [List.mem_toFinset, List.mem_map] at hf
+    obtain ⟨f, hf, rfl⟩ := hf
+    exact hl.left _ hf
 #align list.support_sum_eq List.support_sum_eq
 
 theorem Multiset.support_sum_eq [AddCommMonoid M] (s : Multiset (ι →₀ M))
diff --git a/Mathlib/Data/Fintype/Card.lean b/Mathlib/Data/Fintype/Card.lean
index 6d0130052044d..d456a6eae6856 100644
--- a/Mathlib/Data/Fintype/Card.lean
+++ b/Mathlib/Data/Fintype/Card.lean
@@ -1251,13 +1251,13 @@ theorem List.exists_pw_disjoint_with_card {α : Type*} [Fintype α]
     exact ranges_nodup hu
   · -- pairwise disjoint
     refine Pairwise.map _ (fun s t ↦ disjoint_map (Equiv.injective _)) ?_
-    · -- List.Pairwise List.disjoint l
-      apply Pairwise.pmap (List.ranges_disjoint c)
-      intro u hu v hv huv
-      apply disjoint_pmap
-      · intro a a' ha ha' h
-        simpa only [klift, Fin.mk_eq_mk] using h
-      exact huv
+    -- List.Pairwise List.disjoint l
+    apply Pairwise.pmap (List.ranges_disjoint c)
+    intro u hu v hv huv
+    apply disjoint_pmap
+    · intro a a' ha ha' h
+      simpa only [klift, Fin.mk_eq_mk] using h
+    exact huv
 
 end Ranges
 
diff --git a/Mathlib/Data/Fintype/Option.lean b/Mathlib/Data/Fintype/Option.lean
index 7dbd2ca61726e..d97ab98814426 100644
--- a/Mathlib/Data/Fintype/Option.lean
+++ b/Mathlib/Data/Fintype/Option.lean
@@ -101,7 +101,7 @@ theorem induction_empty_option {P : ∀ (α : Type u) [Fintype α], Prop}
       convert h_option α (Pα _)
     @truncRecEmptyOption (fun α => ∀ h, @P α h) (@fun α β e hα hβ => @of_equiv α β hβ e (hα _))
       f_empty h_option α _ (Classical.decEq α)
-  · exact p _
+  exact p _
   -- ·
 #align fintype.induction_empty_option Fintype.induction_empty_option
 
diff --git a/Mathlib/Data/Fintype/Pi.lean b/Mathlib/Data/Fintype/Pi.lean
index 8ba109b91693b..32bcb195258d2 100644
--- a/Mathlib/Data/Fintype/Pi.lean
+++ b/Mathlib/Data/Fintype/Pi.lean
@@ -125,7 +125,7 @@ theorem Fintype.piFinset_univ {α : Type*} {β : α → Type*} [DecidableEq α]
 -- but those don't work with subsingletons in lean4 as-is so we cannot do this here.
 noncomputable instance _root_.Function.Embedding.fintype {α β} [Fintype α] [Fintype β] :
   Fintype (α ↪ β) :=
-  by classical. exact Fintype.ofEquiv _ (Equiv.subtypeInjectiveEquivEmbedding α β)
+  by classical exact Fintype.ofEquiv _ (Equiv.subtypeInjectiveEquivEmbedding α β)
 #align function.embedding.fintype Function.Embedding.fintype
 
 @[simp]
diff --git a/Mathlib/Data/LazyList/Basic.lean b/Mathlib/Data/LazyList/Basic.lean
index 1a0b28a3a2fca..de5f89f72448e 100644
--- a/Mathlib/Data/LazyList/Basic.lean
+++ b/Mathlib/Data/LazyList/Basic.lean
@@ -84,7 +84,7 @@ instance : LawfulTraversable LazyList := by
     · simp only [List.traverse, map_pure]; rfl
     · replace ih : tl.get.traverse f = ofList <$> tl.get.toList.traverse f := ih
       simp only [traverse._eq_2, ih, Functor.map_map, seq_map_assoc, toList, List.traverse, map_seq]
-      · rfl
+      rfl
     · apply ih
 
 /-- `init xs`, if `xs` non-empty, drops the last element of the list.
diff --git a/Mathlib/Data/List/NodupEquivFin.lean b/Mathlib/Data/List/NodupEquivFin.lean
index b7d5e3f6818c6..2f7d31f6bed30 100644
--- a/Mathlib/Data/List/NodupEquivFin.lean
+++ b/Mathlib/Data/List/NodupEquivFin.lean
@@ -220,7 +220,7 @@ theorem duplicate_iff_exists_distinct_get {l : List α} {x : α} :
     · rintro ⟨f, hf⟩
       refine' ⟨f ⟨0, by simp⟩, f ⟨1, by simp⟩,
         f.lt_iff_lt.2 (show (0 : ℕ) < 1 from zero_lt_one), _⟩
-      · rw [← hf, ← hf]; simp
+      rw [← hf, ← hf]; simp
     · rintro ⟨n, m, hnm, h, h'⟩
       refine' ⟨OrderEmbedding.ofStrictMono (fun i => if (i : ℕ) = 0 then n else m) _, _⟩
       · rintro ⟨⟨_ | i⟩, hi⟩ ⟨⟨_ | j⟩, hj⟩
diff --git a/Mathlib/Data/Matroid/Dual.lean b/Mathlib/Data/Matroid/Dual.lean
index 5ec190e9ec961..2e8ebf2590aff 100644
--- a/Mathlib/Data/Matroid/Dual.lean
+++ b/Mathlib/Data/Matroid/Dual.lean
@@ -13,18 +13,18 @@ collection of bases of another matroid on `E` called the 'dual' of `M`.
 The map from `M` to its dual is an involution, interacts nicely with minors,
 and preserves many important matroid properties such as representability and connectivity.
 
-This file defines the dual matroid `M﹡` of `M`, and gives associated API. The definition
+This file defines the dual matroid `M✶` of `M`, and gives associated API. The definition
 is in terms of its independent sets, using `IndepMatroid.matroid`.
 
 We also define 'Co-independence' (independence in the dual) of a set as a predicate `M.Coindep X`.
-This is an abbreviation for `M﹡.Indep X`, but has its own name for the sake of dot notation.
+This is an abbreviation for `M✶.Indep X`, but has its own name for the sake of dot notation.
 
 ## Main Definitions
 
-* `M.Dual`, written `M﹡`, is the matroid in which a set `B` is a base if and only if `B ⊆ M.E`
+* `M.Dual`, written `M✶`, is the matroid in which a set `B` is a base if and only if `B ⊆ M.E`
   and `M.E \ B` is a base for `M`.
 
-* `M.Coindep X` means `M﹡.Indep X`, or equivalently that `X` is contained in `M.E \ B` for some
+* `M.Coindep X` means `M✶.Indep X`, or equivalently that `X` is contained in `M.E \ B` for some
   base `B` of `M`.
 -/
 
@@ -115,46 +115,46 @@ section dual
 /-- The dual of a matroid; the bases are the complements (w.r.t `M.E`) of the bases of `M`. -/
 def dual (M : Matroid α) : Matroid α := M.dualIndepMatroid.matroid
 
-/-- The `﹡` symbol, which denotes matroid duality.
+/-- The `✶` symbol, which denotes matroid duality.
   (This is distinct from the usual `*` symbol for multiplication, due to precedence issues. )-/
-postfix:max "﹡" => Matroid.dual
+postfix:max "✶" => Matroid.dual
 
-theorem dual_indep_iff_exists' : (M﹡.Indep I) ↔ I ⊆ M.E ∧ (∃ B, M.Base B ∧ Disjoint I B) := by
+theorem dual_indep_iff_exists' : (M✶.Indep I) ↔ I ⊆ M.E ∧ (∃ B, M.Base B ∧ Disjoint I B) := by
   simp [dual]
 
-@[simp] theorem dual_ground : M﹡.E = M.E := rfl
+@[simp] theorem dual_ground : M✶.E = M.E := rfl
 
 @[simp] theorem dual_indep_iff_exists (hI : I ⊆ M.E := by aesop_mat) :
-    M﹡.Indep I ↔ (∃ B, M.Base B ∧ Disjoint I B) := by
+    M✶.Indep I ↔ (∃ B, M.Base B ∧ Disjoint I B) := by
   rw [dual_indep_iff_exists', and_iff_right hI]
 
-theorem dual_dep_iff_forall : (M﹡.Dep I) ↔ (∀ B, M.Base B → (I ∩ B).Nonempty) ∧ I ⊆ M.E := by
+theorem dual_dep_iff_forall : (M✶.Dep I) ↔ (∀ B, M.Base B → (I ∩ B).Nonempty) ∧ I ⊆ M.E := by
   simp_rw [dep_iff, dual_indep_iff_exists', dual_ground, and_congr_left_iff, not_and,
     not_exists, not_and, not_disjoint_iff_nonempty_inter, imp_iff_right_iff, iff_true_intro Or.inl]
 
-instance dual_finite [M.Finite] : M﹡.Finite :=
+instance dual_finite [M.Finite] : M✶.Finite :=
   ⟨M.ground_finite⟩
 
-instance dual_nonempty [M.Nonempty] : M﹡.Nonempty :=
+instance dual_nonempty [M.Nonempty] : M✶.Nonempty :=
   ⟨M.ground_nonempty⟩
 
-@[simp] theorem dual_base_iff (hB : B ⊆ M.E := by aesop_mat) : M﹡.Base B ↔ M.Base (M.E \ B) := by
+@[simp] theorem dual_base_iff (hB : B ⊆ M.E := by aesop_mat) : M✶.Base B ↔ M.Base (M.E \ B) := by
   rw [base_compl_iff_mem_maximals_disjoint_base, base_iff_maximal_indep, dual_indep_iff_exists',
     mem_maximals_setOf_iff]
   simp [dual_indep_iff_exists']
 
-theorem dual_base_iff' : M﹡.Base B ↔ M.Base (M.E \ B) ∧ B ⊆ M.E :=
+theorem dual_base_iff' : M✶.Base B ↔ M.Base (M.E \ B) ∧ B ⊆ M.E :=
   (em (B ⊆ M.E)).elim (fun h ↦ by rw [dual_base_iff, and_iff_left h])
     (fun h ↦ iff_of_false (h ∘ (fun h' ↦ h'.subset_ground)) (h ∘ And.right))
 
-theorem setOf_dual_base_eq : {B | M﹡.Base B} = (fun X ↦ M.E \ X) '' {B | M.Base B} := by
+theorem setOf_dual_base_eq : {B | M✶.Base B} = (fun X ↦ M.E \ X) '' {B | M.Base B} := by
   ext B
   simp only [mem_setOf_eq, mem_image, dual_base_iff']
   refine' ⟨fun h ↦ ⟨_, h.1, diff_diff_cancel_left h.2⟩,
     fun ⟨B', hB', h⟩ ↦ ⟨_,h.symm.trans_subset (diff_subset _ _)⟩⟩
   rwa [← h, diff_diff_cancel_left hB'.subset_ground]
 
-@[simp] theorem dual_dual (M : Matroid α) : M﹡﹡ = M :=
+@[simp] theorem dual_dual (M : Matroid α) : M✶✶ = M :=
   eq_of_base_iff_base_forall rfl (fun B (h : B ⊆ M.E) ↦
     by rw [dual_base_iff, dual_base_iff, dual_ground, diff_diff_cancel_left h])
 
@@ -163,23 +163,23 @@ theorem dual_involutive : Function.Involutive (dual : Matroid α → Matroid α)
 theorem dual_injective : Function.Injective (dual : Matroid α → Matroid α) :=
   dual_involutive.injective
 
-@[simp] theorem dual_inj {M₁ M₂ : Matroid α} : M₁﹡ = M₂﹡ ↔ M₁ = M₂ :=
+@[simp] theorem dual_inj {M₁ M₂ : Matroid α} : M₁✶ = M₂✶ ↔ M₁ = M₂ :=
   dual_injective.eq_iff
 
-theorem eq_dual_comm {M₁ M₂ : Matroid α} : M₁ = M₂﹡ ↔ M₂ = M₁﹡ := by
+theorem eq_dual_comm {M₁ M₂ : Matroid α} : M₁ = M₂✶ ↔ M₂ = M₁✶ := by
   rw [← dual_inj, dual_dual, eq_comm]
 
-theorem eq_dual_iff_dual_eq {M₁ M₂ : Matroid α} : M₁ = M₂﹡ ↔ M₁﹡ = M₂ :=
+theorem eq_dual_iff_dual_eq {M₁ M₂ : Matroid α} : M₁ = M₂✶ ↔ M₁✶ = M₂ :=
   dual_involutive.eq_iff.symm
 
-theorem Base.compl_base_of_dual (h : M﹡.Base B) : M.Base (M.E \ B) :=
+theorem Base.compl_base_of_dual (h : M✶.Base B) : M.Base (M.E \ B) :=
   (dual_base_iff'.1 h).1
 
-theorem Base.compl_base_dual (h : M.Base B) : M﹡.Base (M.E \ B) := by
+theorem Base.compl_base_dual (h : M.Base B) : M✶.Base (M.E \ B) := by
   rwa [dual_base_iff, diff_diff_cancel_left h.subset_ground]
 
 theorem Base.compl_inter_basis_of_inter_basis (hB : M.Base B) (hBX : M.Basis (B ∩ X) X) :
-    M﹡.Basis ((M.E \ B) ∩ (M.E \ X)) (M.E \ X) := by
+    M✶.Basis ((M.E \ B) ∩ (M.E \ X)) (M.E \ X) := by
   refine' Indep.basis_of_forall_insert _ (inter_subset_right _ _) (fun e he ↦ _)
   · rw [dual_indep_iff_exists]
     exact ⟨B, hB, disjoint_of_subset_left (inter_subset_left _ _) disjoint_sdiff_left⟩
@@ -200,37 +200,37 @@ theorem Base.compl_inter_basis_of_inter_basis (hB : M.Base B) (hBX : M.Basis (B
   exact hfb.2 (hBX.mem_of_insert_indep (Or.elim (hem.1 hfb.1) (False.elim ∘ hfb.2) id) hi).1
 
 theorem Base.inter_basis_iff_compl_inter_basis_dual (hB : M.Base B) (hX : X ⊆ M.E := by aesop_mat):
-    M.Basis (B ∩ X) X ↔ M﹡.Basis ((M.E \ B) ∩ (M.E \ X)) (M.E \ X) := by
+    M.Basis (B ∩ X) X ↔ M✶.Basis ((M.E \ B) ∩ (M.E \ X)) (M.E \ X) := by
   refine' ⟨hB.compl_inter_basis_of_inter_basis, fun h ↦ _⟩
   simpa [inter_eq_self_of_subset_right hX, inter_eq_self_of_subset_right hB.subset_ground] using
     hB.compl_base_dual.compl_inter_basis_of_inter_basis h
 
 theorem base_iff_dual_base_compl (hB : B ⊆ M.E := by aesop_mat) :
-    M.Base B ↔ M﹡.Base (M.E \ B) := by
+    M.Base B ↔ M✶.Base (M.E \ B) := by
   rw [dual_base_iff, diff_diff_cancel_left hB]
 
-theorem ground_not_base (M : Matroid α) [h : RkPos M﹡] : ¬M.Base M.E := by
+theorem ground_not_base (M : Matroid α) [h : RkPos M✶] : ¬M.Base M.E := by
   rwa [rkPos_iff_empty_not_base, dual_base_iff, diff_empty] at h
 
-theorem Base.ssubset_ground [h : RkPos M﹡] (hB : M.Base B) : B ⊂ M.E :=
+theorem Base.ssubset_ground [h : RkPos M✶] (hB : M.Base B) : B ⊂ M.E :=
   hB.subset_ground.ssubset_of_ne (by rintro rfl; exact M.ground_not_base hB)
 
-theorem Indep.ssubset_ground [h : RkPos M﹡] (hI : M.Indep I) : I ⊂ M.E := by
+theorem Indep.ssubset_ground [h : RkPos M✶] (hI : M.Indep I) : I ⊂ M.E := by
   obtain ⟨B, hB⟩ := hI.exists_base_superset; exact hB.2.trans_ssubset hB.1.ssubset_ground
 
-/-- A coindependent set of `M` is an independent set of the dual of `M﹡`. we give it a separate
+/-- A coindependent set of `M` is an independent set of the dual of `M✶`. we give it a separate
   definition to enable dot notation. Which spelling is better depends on context. -/
-abbrev Coindep (M : Matroid α) (I : Set α) : Prop := M﹡.Indep I
+abbrev Coindep (M : Matroid α) (I : Set α) : Prop := M✶.Indep I
 
-theorem coindep_def : M.Coindep X ↔ M﹡.Indep X := Iff.rfl
+theorem coindep_def : M.Coindep X ↔ M✶.Indep X := Iff.rfl
 
-theorem Coindep.indep (hX : M.Coindep X) : M﹡.Indep X :=
+theorem Coindep.indep (hX : M.Coindep X) : M✶.Indep X :=
   hX
 
-@[simp] theorem dual_coindep_iff : M﹡.Coindep X ↔ M.Indep X := by
+@[simp] theorem dual_coindep_iff : M✶.Coindep X ↔ M.Indep X := by
   rw [Coindep, dual_dual]
 
-theorem Indep.coindep (hI : M.Indep I) : M﹡.Coindep I :=
+theorem Indep.coindep (hI : M.Indep I) : M✶.Coindep I :=
   dual_coindep_iff.2 hI
 
 theorem coindep_iff_exists' : M.Coindep X ↔ (∃ B, M.Base B ∧ B ⊆ M.E \ X) ∧ X ⊆ M.E := by
diff --git a/Mathlib/Data/Matroid/Restrict.lean b/Mathlib/Data/Matroid/Restrict.lean
index 6b126a9e3dcfa..ba1d94175fcfc 100644
--- a/Mathlib/Data/Matroid/Restrict.lean
+++ b/Mathlib/Data/Matroid/Restrict.lean
@@ -88,7 +88,7 @@ section restrict
       rw [union_subset_iff, and_iff_left (subset_union_right _ _), union_comm]
       exact hBIB'.trans (union_subset_union_left _ (subset_inter hIY hI.subset_ground))
 
-    have hi : M﹡.Indep (M.E \ (B ∪ (R ∩ M.E))) := by
+    have hi : M✶.Indep (M.E \ (B ∪ (R ∩ M.E))) := by
       rw [dual_indep_iff_exists]
       exact ⟨B, hB, disjoint_of_subset_right (subset_union_left _ _) disjoint_sdiff_left⟩
 
diff --git a/Mathlib/Data/Nat/Digits.lean b/Mathlib/Data/Nat/Digits.lean
index 8b9c8373430eb..7d93b83232bd4 100644
--- a/Mathlib/Data/Nat/Digits.lean
+++ b/Mathlib/Data/Nat/Digits.lean
@@ -244,8 +244,8 @@ theorem digits_ofDigits (b : ℕ) (h : 1 < b) (L : List ℕ) (w₁ : ∀ l ∈ L
         apply w₁
         exact List.mem_cons_of_mem _ m
       · intro h
-        · rw [List.getLast_cons h] at w₂
-          convert w₂
+        rw [List.getLast_cons h] at w₂
+        convert w₂
     · exact w₁ d (List.mem_cons_self _ _)
     · by_cases h' : L = []
       · rcases h' with rfl
@@ -366,8 +366,8 @@ theorem getLast_digit_ne_zero (b : ℕ) {m : ℕ} (hm : m ≠ 0) :
   · simpa only [digits_of_lt (b + 2) n hn hnb]
   · rw [digits_getLast n (le_add_left 2 b)]
     refine' IH _ (Nat.div_lt_self hn.bot_lt (one_lt_succ_succ b)) _
-    · rw [← pos_iff_ne_zero]
-      exact Nat.div_pos (le_of_not_lt hnb) (zero_lt_succ (succ b))
+    rw [← pos_iff_ne_zero]
+    exact Nat.div_pos (le_of_not_lt hnb) (zero_lt_succ (succ b))
 #align nat.last_digit_ne_zero Nat.getLast_digit_ne_zero
 
 /-- The digits in the base b+2 expansion of n are all less than b+2 -/
diff --git a/Mathlib/Data/Nat/Interval.lean b/Mathlib/Data/Nat/Interval.lean
index a8daa1300d0e7..43b1da7251df7 100644
--- a/Mathlib/Data/Nat/Interval.lean
+++ b/Mathlib/Data/Nat/Interval.lean
@@ -259,10 +259,10 @@ theorem Ico_image_const_sub_eq_Ico (hac : a ≤ c) :
     rw [lt_tsub_iff_left, Nat.lt_succ_iff] at ha
     have hx : x ≤ c := (Nat.le_add_left _ _).trans ha
     refine' ⟨c - x, _, tsub_tsub_cancel_of_le hx⟩
-    · rw [mem_Ico]
-      exact
-        ⟨le_tsub_of_add_le_right ha,
-          (tsub_lt_iff_left hx).2 <| succ_le_iff.1 <| tsub_le_iff_right.1 hb⟩
+    rw [mem_Ico]
+    exact
+      ⟨le_tsub_of_add_le_right ha,
+        (tsub_lt_iff_left hx).2 <| succ_le_iff.1 <| tsub_le_iff_right.1 hb⟩
 #align nat.Ico_image_const_sub_eq_Ico Nat.Ico_image_const_sub_eq_Ico
 
 theorem Ico_succ_left_eq_erase_Ico : Ico a.succ b = erase (Ico a b) a := by
diff --git a/Mathlib/Data/Nat/Pairing.lean b/Mathlib/Data/Nat/Pairing.lean
index 2e29c77bd2030..205bb2516bbac 100644
--- a/Mathlib/Data/Nat/Pairing.lean
+++ b/Mathlib/Data/Nat/Pairing.lean
@@ -130,10 +130,10 @@ theorem pair_lt_pair_left {a₁ a₂} (b) (h : a₁ < a₂) : pair a₁ b < pair
     · exact Nat.mul_self_le_mul_self h₂
     · exact Nat.lt_add_right _ h
   · simp at h₁
-    · simp only [not_lt_of_gt (lt_of_le_of_lt h₁ h), ite_false]
-      apply add_lt_add
-      · exact Nat.mul_self_lt_mul_self h
-      · apply Nat.add_lt_add_right; assumption
+    simp only [not_lt_of_gt (lt_of_le_of_lt h₁ h), ite_false]
+    apply add_lt_add
+    · exact Nat.mul_self_lt_mul_self h
+    · apply Nat.add_lt_add_right; assumption
 #align nat.mkpair_lt_mkpair_left Nat.pair_lt_pair_left
 
 theorem pair_lt_pair_right (a) {b₁ b₂} (h : b₁ < b₂) : pair a b₁ < pair a b₂ := by
diff --git a/Mathlib/Data/Ordmap/Ordset.lean b/Mathlib/Data/Ordmap/Ordset.lean
index c4c5a71d6a2fc..00405ab65d5ab 100644
--- a/Mathlib/Data/Ordmap/Ordset.lean
+++ b/Mathlib/Data/Ordmap/Ordset.lean
@@ -1479,7 +1479,7 @@ theorem Valid'.merge_aux₁ {o₁ o₂ ls ll lx lr rs rl rx rr t}
           size_balance' v.2 hr.2.2.2, e, hl.2.1, hr.2.1]
         abel
     · rw [e, add_right_comm]; rintro ⟨⟩
-  · intro _ _; rw [e]; unfold delta at hr₂ ⊢; omega
+  intro _ _; rw [e]; unfold delta at hr₂ ⊢; omega
 #align ordnode.valid'.merge_aux₁ Ordnode.Valid'.merge_aux₁
 
 theorem Valid'.merge_aux {l r o₁ o₂} (hl : Valid' o₁ l o₂) (hr : Valid' o₁ r o₂)
@@ -1528,14 +1528,14 @@ theorem insertWith.valid_aux [IsTotal α (· ≤ ·)] [@DecidableRel α (· ≤
         refine' ⟨vl.balanceL h.right H, _⟩
         rw [size_balanceL vl.3 h.3.2.2 vl.2 h.2.2.2 H, h.2.size_eq]
         exact (e.add_right _).add_right _
-      · exact Or.inl ⟨_, e, h.3.1⟩
+      exact Or.inl ⟨_, e, h.3.1⟩
     · have : y < x := lt_of_le_not_le ((total_of (· ≤ ·) _ _).resolve_left h_1) h_1
       rcases insertWith.valid_aux f x hf h.right this br with ⟨vr, e⟩
       suffices H : _ by
         refine' ⟨h.left.balanceR vr H, _⟩
         rw [size_balanceR h.3.2.1 vr.3 h.2.2.1 vr.2 H, h.2.size_eq]
         exact (e.add_left _).add_right _
-      · exact Or.inr ⟨_, e, h.3.1⟩
+      exact Or.inr ⟨_, e, h.3.1⟩
 #align ordnode.insert_with.valid_aux Ordnode.insertWith.valid_aux
 
 theorem insertWith.valid [IsTotal α (· ≤ ·)] [@DecidableRel α (· ≤ ·)] (f : α → α) (x : α)
@@ -1622,7 +1622,7 @@ theorem Valid'.erase_aux [@DecidableRel α (· ≤ ·)] (x : α) {t a₁ a₂} (
         · rw [size_balanceR t_l_valid.bal h.right.bal t_l_valid.sz h.right.sz h_balanceable]
           repeat apply Raised.add_right
           exact t_l_size
-      · left; exists t_l.size; exact And.intro t_l_size h.bal.1
+      left; exists t_l.size; exact And.intro t_l_size h.bal.1
     · have h_glue := Valid'.glue h.left h.right h.bal.1
       cases' h_glue with h_glue_valid h_glue_sized
       constructor
@@ -1635,7 +1635,7 @@ theorem Valid'.erase_aux [@DecidableRel α (· ≤ ·)] (x : α) {t a₁ a₂} (
           apply Raised.add_right
           apply Raised.add_left
           exact t_r_size
-      · right; exists t_r.size; exact And.intro t_r_size h.bal.1
+      right; exists t_r.size; exact And.intro t_r_size h.bal.1
 #align ordnode.valid'.erase_aux Ordnode.Valid'.erase_aux
 
 theorem erase.valid [@DecidableRel α (· ≤ ·)] (x : α) {t} (h : Valid t) : Valid (erase x t) :=
diff --git a/Mathlib/Data/PFunctor/Univariate/M.lean b/Mathlib/Data/PFunctor/Univariate/M.lean
index d91a380ab6d62..742b20c90db18 100644
--- a/Mathlib/Data/PFunctor/Univariate/M.lean
+++ b/Mathlib/Data/PFunctor/Univariate/M.lean
@@ -347,15 +347,15 @@ theorem mk_dest (x : M F) : M.mk (dest x) = x := by
   rw [h']
   intros ch h
   congr
-  · ext a
-    dsimp only [children]
-    generalize hh : cast _ a = a''
-    rw [cast_eq_iff_heq] at hh
-    revert a''
-    rw [h]
-    intros _ hh
-    cases hh
-    rfl
+  ext a
+  dsimp only [children]
+  generalize hh : cast _ a = a''
+  rw [cast_eq_iff_heq] at hh
+  revert a''
+  rw [h]
+  intros _ hh
+  cases hh
+  rfl
 set_option linter.uppercaseLean3 false in
 #align pfunctor.M.mk_dest PFunctor.M.mk_dest
 
@@ -404,7 +404,7 @@ theorem agree_iff_agree' {n : ℕ} (x y : M F) :
     Agree (x.approx n) (y.approx <| n + 1) ↔ Agree' n x y := by
   constructor <;> intro h
   · induction' n with _ n_ih generalizing x y
-    constructor
+    · constructor
     · induction x using PFunctor.M.casesOn'
       induction y using PFunctor.M.casesOn'
       simp only [approx_mk] at h
@@ -414,7 +414,7 @@ theorem agree_iff_agree' {n : ℕ} (x y : M F) :
       apply n_ih
       apply hagree
   · induction' n with _ n_ih generalizing x y
-    constructor
+    · constructor
     · cases' h with _ _ _ a x' y'
       induction' x using PFunctor.M.casesOn' with x_a x_f
       induction' y using PFunctor.M.casesOn' with y_a y_f
diff --git a/Mathlib/Data/Set/Pointwise/Basic.lean b/Mathlib/Data/Set/Pointwise/Basic.lean
index f5da1d1e2b12e..098f454a99d7e 100644
--- a/Mathlib/Data/Set/Pointwise/Basic.lean
+++ b/Mathlib/Data/Set/Pointwise/Basic.lean
@@ -1389,12 +1389,12 @@ theorem card_pow_eq_card_pow_card_univ_aux {f : ℕ → ℕ} (h1 : Monotone f) {
           lt_of_le_of_lt (ih (n.le_succ.trans h))
             (lt_of_le_of_ne (h1 n.le_succ) (h2 n (Nat.succ_le_succ_iff.mp h))))
         n
-  · obtain ⟨n, hn1, hn2⟩ := key
-    replace key : ∀ k : ℕ, f (n + k) = f (n + k + 1) ∧ f (n + k) = f n := fun k =>
-      Nat.rec ⟨hn2, rfl⟩ (fun k ih => ⟨h3 _ ih.1, ih.1.symm.trans ih.2⟩) k
-    replace key : ∀ k : ℕ, n ≤ k → f k = f n := fun k hk =>
-      (congr_arg f (add_tsub_cancel_of_le hk)).symm.trans (key (k - n)).2
-    exact fun k hk => (key k (hn1.trans hk)).trans (key B hn1).symm
+  obtain ⟨n, hn1, hn2⟩ := key
+  replace key : ∀ k : ℕ, f (n + k) = f (n + k + 1) ∧ f (n + k) = f n := fun k =>
+    Nat.rec ⟨hn2, rfl⟩ (fun k ih => ⟨h3 _ ih.1, ih.1.symm.trans ih.2⟩) k
+  replace key : ∀ k : ℕ, n ≤ k → f k = f n := fun k hk =>
+    (congr_arg f (add_tsub_cancel_of_le hk)).symm.trans (key (k - n)).2
+  exact fun k hk => (key k (hn1.trans hk)).trans (key B hn1).symm
 #align group.card_pow_eq_card_pow_card_univ_aux Group.card_pow_eq_card_pow_card_univ_aux
 #align add_group.card_nsmul_eq_card_nsmul_card_univ_aux AddGroup.card_nsmul_eq_card_nsmul_card_univ_aux
 
diff --git a/Mathlib/Data/Sign.lean b/Mathlib/Data/Sign.lean
index cc6f977794dc6..307425aa7da4f 100644
--- a/Mathlib/Data/Sign.lean
+++ b/Mathlib/Data/Sign.lean
@@ -361,7 +361,7 @@ theorem sign_eq_neg_one_iff : sign a = -1 ↔ a < 0 := by
   refine' ⟨fun h => _, fun h => sign_neg h⟩
   rw [sign_apply] at h
   split_ifs at h
-  · assumption
+  assumption
 #align sign_eq_neg_one_iff sign_eq_neg_one_iff
 
 end Preorder
diff --git a/Mathlib/Data/Sym/Sym2.lean b/Mathlib/Data/Sym/Sym2.lean
index d40341a1d1773..0d2bc2b7b0edc 100644
--- a/Mathlib/Data/Sym/Sym2.lean
+++ b/Mathlib/Data/Sym/Sym2.lean
@@ -617,16 +617,16 @@ def sym2EquivSym' : Equiv (Sym2 α) (Sym' α 2)
   left_inv := by apply Sym2.ind; aesop (add norm unfold [Sym2.fromVector])
   right_inv x := by
     refine' x.recOnSubsingleton fun x => _
-    · cases' x with x hx
-      cases' x with _ x
-      · simp at hx
-      cases' x with _ x
-      · simp at hx
-      cases' x with _ x
-      swap
-      · exfalso
-        simp at hx
-      rfl
+    cases' x with x hx
+    cases' x with _ x
+    · simp at hx
+    cases' x with _ x
+    · simp at hx
+    cases' x with _ x
+    swap
+    · exfalso
+      simp at hx
+    rfl
 #align sym2.sym2_equiv_sym' Sym2.sym2EquivSym'
 
 /-- The symmetric square is equivalent to the second symmetric power. -/
diff --git a/Mathlib/Data/ZMod/Basic.lean b/Mathlib/Data/ZMod/Basic.lean
index ee051be4841e5..8fe8bb4a8a994 100644
--- a/Mathlib/Data/ZMod/Basic.lean
+++ b/Mathlib/Data/ZMod/Basic.lean
@@ -297,6 +297,7 @@ theorem cast_one (h : m ∣ n) : (cast (1 : ZMod n) : R) = 1 := by
   cases n;
   · rw [Nat.dvd_one] at h
     subst m
+    have : Subsingleton R := CharP.CharOne.subsingleton
     apply Subsingleton.elim
   rw [Nat.mod_eq_of_lt]
   · exact Nat.cast_one
diff --git a/Mathlib/GroupTheory/Commutator.lean b/Mathlib/GroupTheory/Commutator.lean
index 54baea071bc37..7397ab18af2da 100644
--- a/Mathlib/GroupTheory/Commutator.lean
+++ b/Mathlib/GroupTheory/Commutator.lean
@@ -227,17 +227,17 @@ theorem commutator_pi_pi_of_finite {η : Type*} [Finite η] {Gs : η → Type*}
     Subgroup.pi Set.univ fun i => ⁅H i, K i⁆ := by
   classical
     apply le_antisymm (commutator_pi_pi_le H K)
-    · rw [pi_le_iff]
-      intro i hi
-      rw [map_commutator]
-      apply commutator_mono <;>
-        · rw [le_pi_iff]
-          intro j _hj
-          rintro _ ⟨_, ⟨x, hx, rfl⟩, rfl⟩
-          by_cases h : j = i
-          · subst h
-            simpa using hx
-          · simp [h, one_mem]
+    rw [pi_le_iff]
+    intro i hi
+    rw [map_commutator]
+    apply commutator_mono <;>
+      · rw [le_pi_iff]
+        intro j _hj
+        rintro _ ⟨_, ⟨x, hx, rfl⟩, rfl⟩
+        by_cases h : j = i
+        · subst h
+          simpa using hx
+        · simp [h, one_mem]
 #align subgroup.commutator_pi_pi_of_finite Subgroup.commutator_pi_pi_of_finite
 
 end Subgroup
diff --git a/Mathlib/GroupTheory/CoprodI.lean b/Mathlib/GroupTheory/CoprodI.lean
index ae826483ed8fe..839f581902ea4 100644
--- a/Mathlib/GroupTheory/CoprodI.lean
+++ b/Mathlib/GroupTheory/CoprodI.lean
@@ -758,7 +758,7 @@ theorem of_word (w : Word M) (h : w ≠ empty) : ∃ (i j : _) (w' : NeWord M i
       obtain ⟨i, j, w', hw' : w'.toList = y::l⟩ := hi
       obtain rfl : y = ⟨i, w'.head⟩ := by simpa [hw'] using w'.toList_head?
       refine' ⟨x.1, j, append (singleton x.2 hnot1.1) hchain.1 w', _⟩
-      · simpa [toWord] using hw'
+      simpa [toWord] using hw'
 #align free_product.neword.of_word Monoid.CoprodI.NeWord.of_word
 
 /-- A non-empty reduced word determines an element of the free product, given by multiplication. -/
@@ -986,10 +986,10 @@ theorem lift_injective_of_ping_pong : Function.Injective (lift f) := by
   classical
     apply (injective_iff_map_eq_one (lift f)).mpr
     rw [(CoprodI.Word.equiv).forall_congr_left']
-    · intro w Heq
-      dsimp [Word.equiv] at *
-      · rw [empty_of_word_prod_eq_one f hcard X hXnonempty hXdisj hpp Heq]
-        rfl
+    intro w Heq
+    dsimp [Word.equiv] at *
+    rw [empty_of_word_prod_eq_one f hcard X hXnonempty hXdisj hpp Heq]
+    rfl
 #align free_product.lift_injective_of_ping_pong Monoid.CoprodI.lift_injective_of_ping_pong
 
 end PingPongLemma
@@ -1134,13 +1134,13 @@ theorem _root_.FreeGroup.injective_lift_of_ping_pong : Function.Injective (FreeG
               _ ⊆ Y i := hi
         _ ⊆ X' i := Set.subset_union_right _ _
   show _ ∨ ∃ i, 3 ≤ #(H i)
-  · inhabit ι
-    right
-    use Inhabited.default
-    simp only [H]
-    rw [FreeGroup.freeGroupUnitEquivInt.cardinal_eq, Cardinal.mk_denumerable]
-    apply le_of_lt
-    exact nat_lt_aleph0 3
+  inhabit ι
+  right
+  use Inhabited.default
+  simp only [H]
+  rw [FreeGroup.freeGroupUnitEquivInt.cardinal_eq, Cardinal.mk_denumerable]
+  apply le_of_lt
+  exact nat_lt_aleph0 3
 #align free_group.injective_lift_of_ping_pong FreeGroup.injective_lift_of_ping_pong
 
 end PingPongLemma
diff --git a/Mathlib/GroupTheory/Coxeter/Basic.lean b/Mathlib/GroupTheory/Coxeter/Basic.lean
index 1cb35022bf3d4..16e152dd54e3c 100644
--- a/Mathlib/GroupTheory/Coxeter/Basic.lean
+++ b/Mathlib/GroupTheory/Coxeter/Basic.lean
@@ -25,6 +25,14 @@ is a Coxeter group (`IsCoxeterGroup`), and we may speak of the simple reflection
 (`CoxeterSystem.simple`). We state all of our results about Coxeter groups in terms of Coxeter
 systems where possible.
 
+Let $W$ be a group equipped with a Coxeter system. For all monoids $G$ and all functions
+$f \colon B \to G$ whose values satisfy the Coxeter relations, we may lift $f$ to a multiplicative
+homomorphism $W \to G$ (`CoxeterSystem.lift`) in a unique way.
+
+A *word* is a sequence of elements of $B$. The word $(i_1, \ldots, i_\ell)$ has a corresponding
+product $s_{i_1} \cdots s_{i_\ell} \in W$ (`CoxeterSystem.wordProd`). Every element of $W$ is the
+product of some word (`CoxeterSystem.wordProd_surjective`).
+
 ## Implementation details
 
 Much of the literature on Coxeter groups conflates the set $S = \{s_i : i \in B\} \subseteq W$ of
@@ -35,11 +43,14 @@ reflections unless necessary; instead, we state our results in terms of $B$ wher
 
 ## Main definitions
 
-* `CoxeterMatrix.group`
+* `CoxeterMatrix.Group`
 * `CoxeterSystem`
 * `IsCoxeterGroup`
 * `CoxeterSystem.simple` : If `cs` is a Coxeter system on the group `W`, then `cs.simple i` is the
   simple reflection of `W` at the index `i`.
+* `CoxeterSystem.lift` : Extend a function `f : B → G` to a monoid homomorphism `f' : W → G`
+  satisfying `f' (cs.simple i) = f i` for all `i`.
+* `CoxeterSystem.wordProd`
 
 ## References
 
@@ -51,6 +62,14 @@ reflections unless necessary; instead, we state our results in terms of $B$ wher
 ## TODO
 
 * The simple reflections of a Coxeter system are distinct.
+* Introduce some ways to actually construct some Coxeter groups. For example, given a Coxeter matrix
+$M : B \times B \to \mathbb{N}$, a real vector space $V$, a basis $\{\alpha_i : i \in B\}$
+and a bilinear form $\langle \cdot, \cdot \rangle \colon V \times V \to \mathbb{R}$ satisfying
+$$\langle \alpha_i, \alpha_{i'}\rangle = - \cos(\pi / M_{i,i'}),$$ one can form the subgroup of
+$GL(V)$ generated by the reflections in the $\alpha_i$, and it is a Coxeter group. We can use this
+to combinatorially describe the Coxeter groups of type $A$, $B$, $D$, and $I$.
+* State and prove Matsumoto's theorem.
+* Classify the finite Coxeter groups.
 
 ## Tags
 
@@ -58,7 +77,7 @@ coxeter system, coxeter group
 
 -/
 
-open Function
+open Function Set List
 
 /-! ### Coxeter groups -/
 
@@ -74,7 +93,7 @@ $s_i$ and $s_{i'}$. -/
 def relation (i i' : B) : FreeGroup B := (FreeGroup.of i * FreeGroup.of i') ^ M i i'
 
 /-- The set of all Coxeter relations associated to the Coxeter matrix $M$. -/
-def relationsSet : Set (FreeGroup B) := Set.range <| uncurry M.relation
+def relationsSet : Set (FreeGroup B) := range <| uncurry M.relation
 
 /-- The Coxeter group associated to a Coxeter matrix $M$; that is, the group
 $$\langle \{s_i\}_{i \in B} \vert \{(s_i s_{i'})^{M_{i, i'}}\}_{i, i' \in B} \rangle.$$ -/
@@ -151,7 +170,8 @@ protected def reindex (e : B ≃ B') : CoxeterSystem (M.reindex e) W :=
   ⟨cs.mulEquiv.trans (M.reindexGroupEquiv e).symm⟩
 
 /-- Push a Coxeter system through a group isomorphism. -/
-@[simps] protected def map (e : W ≃* H) : CoxeterSystem M H := ⟨e.symm.trans cs.mulEquiv⟩
+@[simps]
+protected def map (e : W ≃* H) : CoxeterSystem M H := ⟨e.symm.trans cs.mulEquiv⟩
 
 /-! ### Simple reflections -/
 
@@ -166,4 +186,192 @@ theorem _root_.CoxeterMatrix.toCoxeterSystem_simple (M : CoxeterMatrix B) :
 
 @[simp] theorem map_simple (e : W ≃* H) (i : B) : (cs.map e).simple i = e (cs.simple i) := rfl
 
+local prefix:100 "s" => cs.simple
+
+@[simp]
+theorem simple_mul_simple_self (i : B) : s i * s i = 1 := by
+  have : (FreeGroup.of i) * (FreeGroup.of i) ∈ M.relationsSet := ⟨(i, i), by simp [relation]⟩
+  have : (QuotientGroup.mk (FreeGroup.of i * FreeGroup.of i) : M.Group) = 1 :=
+    (QuotientGroup.eq_one_iff _).mpr (Subgroup.subset_normalClosure this)
+  unfold simple
+  rw [← map_mul, PresentedGroup.of, ← QuotientGroup.mk_mul, this, map_one]
+
+@[simp]
+theorem simple_mul_simple_cancel_right {w : W} (i : B) : w * s i * s i = w := by
+  simp [mul_assoc]
+
+@[simp]
+theorem simple_mul_simple_cancel_left {w : W} (i : B) : s i * (s i * w) = w := by
+  simp [← mul_assoc]
+
+@[simp] theorem simple_sq (i : B) : s i ^ 2 = 1 := pow_two (s i) ▸ cs.simple_mul_simple_self i
+
+@[simp]
+theorem inv_simple (i : B) : (s i)⁻¹ = s i :=
+  (eq_inv_of_mul_eq_one_right (cs.simple_mul_simple_self i)).symm
+
+@[simp]
+theorem simple_mul_simple_pow (i i' : B) : (s i * s i') ^ M i i' = 1 := by
+  have : (FreeGroup.of i * FreeGroup.of i') ^ M i i' ∈ M.relationsSet := ⟨(i, i'), rfl⟩
+  have : (QuotientGroup.mk ((FreeGroup.of i * FreeGroup.of i') ^ M i i') : M.Group) = 1 :=
+    (QuotientGroup.eq_one_iff _).mpr (Subgroup.subset_normalClosure this)
+  unfold simple
+  rw [← map_mul, ← map_pow, PresentedGroup.of, PresentedGroup.of,
+      ← QuotientGroup.mk_mul, ← QuotientGroup.mk_pow, this, map_one]
+
+@[simp] theorem simple_mul_simple_pow' (i i' : B) : (s i' * s i) ^ M i i' = 1 :=
+  M.symmetric i' i ▸ cs.simple_mul_simple_pow i' i
+
+/-- The simple reflections of `W` generate `W` as a group. -/
+theorem subgroup_closure_range_simple : Subgroup.closure (range cs.simple) = ⊤ := by
+  have : cs.simple = cs.mulEquiv.symm ∘ PresentedGroup.of := rfl
+  rw [this, Set.range_comp, ← MulEquiv.coe_toMonoidHom, ← MonoidHom.map_closure,
+    PresentedGroup.closure_range_of, ← MonoidHom.range_eq_map]
+  exact MonoidHom.range_top_of_surjective _ (MulEquiv.surjective _)
+
+/-- The simple reflections of `W` generate `W` as a monoid. -/
+theorem submonoid_closure_range_simple : Submonoid.closure (range cs.simple) = ⊤ := by
+  have : range cs.simple = range cs.simple ∪ (range cs.simple)⁻¹ := by
+    simp_rw [inv_range, inv_simple, union_self]
+  rw [this, ← Subgroup.closure_toSubmonoid, subgroup_closure_range_simple, Subgroup.top_toSubmonoid]
+
+/-! ### Induction principles for Coxeter systems -/
+
+/-- If `p : W → Prop` holds for all simple reflections, it holds for the identity, and it is
+preserved under multiplication, then it holds for all elements of `W`. -/
+theorem simple_induction {p : W → Prop} (w : W) (simple : ∀ i : B, p (s i)) (one : p 1)
+    (mul : ∀ w w' : W, p w → p w' → p (w * w')) : p w := by
+  have := cs.submonoid_closure_range_simple.symm ▸ Submonoid.mem_top w
+  exact Submonoid.closure_induction this (fun x ⟨i, hi⟩ ↦ hi ▸ simple i) one mul
+
+/-- If `p : W → Prop` holds for the identity and it is preserved under multiplying on the left
+by a simple reflection, then it holds for all elements of `W`. -/
+theorem simple_induction_left {p : W → Prop} (w : W) (one : p 1)
+    (mul_simple_left : ∀ (w : W) (i : B), p w → p (s i * w)) : p w := by
+  let p' : (w : W) → w ∈ Submonoid.closure (Set.range cs.simple) → Prop :=
+    fun w _ ↦ p w
+  have := cs.submonoid_closure_range_simple.symm ▸ Submonoid.mem_top w
+  apply Submonoid.closure_induction_left (p := p')
+  · exact one
+  · rintro _ ⟨i, rfl⟩ y _
+    exact mul_simple_left y i
+  · exact this
+
+/-- If `p : W → Prop` holds for the identity and it is preserved under multiplying on the right
+by a simple reflection, then it holds for all elements of `W`. -/
+theorem simple_induction_right {p : W → Prop} (w : W) (one : p 1)
+    (mul_simple_right : ∀ (w : W) (i : B), p w → p (w * s i)) : p w := by
+  let p' : ((w : W) → w ∈ Submonoid.closure (Set.range cs.simple) → Prop) :=
+    fun w _ ↦ p w
+  have := cs.submonoid_closure_range_simple.symm ▸ Submonoid.mem_top w
+  apply Submonoid.closure_induction_right (p := p')
+  · exact one
+  · rintro x _ _ ⟨i, rfl⟩
+    exact mul_simple_right x i
+  · exact this
+
+/-! ### Homomorphisms from a Coxeter group -/
+
+/-- If two homomorphisms with domain `W` agree on all simple reflections, then they are equal. -/
+theorem ext_simple {G : Type*} [Monoid G] {φ₁ φ₂ : W →* G} (h : ∀ i : B, φ₁ (s i) = φ₂ (s i)) :
+    φ₁ = φ₂ :=
+  MonoidHom.eq_of_eqOn_denseM cs.submonoid_closure_range_simple (fun _ ⟨i, hi⟩ ↦ hi ▸ h i)
+
+/-- The proposition that the values of the function `f : B → G` satisfy the Coxeter relations
+corresponding to the matrix `M`. -/
+def _root_.CoxeterMatrix.IsLiftable {G : Type*} [Monoid G] (M : CoxeterMatrix B) (f : B → G) :
+    Prop := ∀ i i', (f i * f i') ^ M i i' = 1
+
+private theorem relations_liftable {G : Type*} [Group G] {f : B → G} (hf : IsLiftable M f)
+    (r : FreeGroup B) (hr : r ∈ M.relationsSet) : (FreeGroup.lift f) r = 1 := by
+  rcases hr with ⟨⟨i, i'⟩, rfl⟩
+  rw [uncurry, relation, map_pow, _root_.map_mul, FreeGroup.lift.of, FreeGroup.lift.of]
+  exact hf i i'
+
+private def groupLift {G : Type*} [Group G] {f : B → G} (hf : IsLiftable M f) : W →* G :=
+  (PresentedGroup.toGroup (relations_liftable hf)).comp cs.mulEquiv.toMonoidHom
+
+private def restrictUnit {G : Type*} [Monoid G] {f : B → G} (hf : IsLiftable M f) (i : B) :
+    Gˣ where
+  val := f i
+  inv := f i
+  val_inv := pow_one (f i * f i) ▸ M.diagonal i ▸ hf i i
+  inv_val := pow_one (f i * f i) ▸ M.diagonal i ▸ hf i i
+
+private theorem toMonoidHom_apply_symm_apply (a : PresentedGroup (M.relationsSet)):
+    (MulEquiv.toMonoidHom cs.mulEquiv : W →* PresentedGroup (M.relationsSet))
+    ((MulEquiv.symm cs.mulEquiv) a) = a := calc
+  _ = cs.mulEquiv ((MulEquiv.symm cs.mulEquiv) a) := by rfl
+  _ = _                                           := by rw [MulEquiv.apply_symm_apply]
+
+/-- The universal mapping property of Coxeter systems. For any monoid `G`,
+functions `f : B → G` whose values satisfy the Coxeter relations are equivalent to
+monoid homomorphisms `f' : W → G`. -/
+def lift {G : Type*} [Monoid G] : {f : B → G // IsLiftable M f} ≃ (W →* G) where
+  toFun f := MonoidHom.comp (Units.coeHom G) (cs.groupLift
+    (show ∀ i i', ((restrictUnit f.property) i * (restrictUnit f.property) i') ^ M i i' = 1 from
+      fun i i' ↦ Units.ext (f.property i i')))
+  invFun ι := ⟨ι ∘ cs.simple, fun i i' ↦ by
+    rw [comp_apply, comp_apply, ← map_mul, ← map_pow, simple_mul_simple_pow, map_one]⟩
+  left_inv f := by
+    ext i
+    simp only [MonoidHom.comp_apply, comp_apply, mem_setOf_eq, groupLift, simple]
+    rw [← MonoidHom.toFun_eq_coe, toMonoidHom_apply_symm_apply, PresentedGroup.toGroup.of,
+      OneHom.toFun_eq_coe, MonoidHom.toOneHom_coe, Units.coeHom_apply]
+    rfl
+  right_inv ι := by
+    apply cs.ext_simple
+    intro i
+    dsimp only
+    rw [groupLift, simple, MonoidHom.comp_apply, MonoidHom.comp_apply, toMonoidHom_apply_symm_apply,
+      PresentedGroup.toGroup.of, CoxeterSystem.restrictUnit, Units.coeHom_apply]
+    rfl
+
+@[simp]
+theorem lift_apply_simple {G : Type*} [Monoid G] {f : B → G} (hf : IsLiftable M f) (i : B) :
+    cs.lift ⟨f, hf⟩ (s i) = f i := congrFun (congrArg Subtype.val (cs.lift.left_inv ⟨f, hf⟩)) i
+
+/-- If two Coxeter systems on the same group `W` have the same Coxeter matrix `M : Matrix B B ℕ`
+and the same simple reflection map `B → W`, then they are identical. -/
+theorem simple_determines_coxeterSystem :
+    Injective (simple : CoxeterSystem M W → B → W) := by
+  intro cs1 cs2 h
+  apply CoxeterSystem.ext
+  apply MulEquiv.toMonoidHom_injective
+  apply cs1.ext_simple
+  intro i
+  nth_rw 2 [h]
+  simp [simple]
+
+/-! ### Words -/
+
+/-- The product of the simple reflections of `W` corresponding to the indices in `ω`. -/
+def wordProd (ω : List B) : W := prod (map cs.simple ω)
+
+local prefix:100 "π" => cs.wordProd
+
+@[simp] theorem wordProd_nil : π [] = 1 := by simp [wordProd]
+
+theorem wordProd_cons (i : B) (ω : List B) : π (i :: ω) = s i * π ω := by simp [wordProd]
+
+@[simp] theorem wordProd_singleton (i : B) : π ([i]) = s i := by simp [wordProd]
+
+theorem wordProd_concat (i : B) (ω : List B) : π (ω.concat i) = π ω * s i := by simp [wordProd]
+
+theorem wordProd_append (ω ω' : List B) : π (ω ++ ω') = π ω * π ω' := by simp [wordProd]
+
+@[simp] theorem wordProd_reverse (ω : List B) : π (reverse ω) = (π ω)⁻¹ := by
+  induction' ω with x ω' ih
+  · simp
+  · simpa [wordProd_cons, wordProd_append] using ih
+
+theorem wordProd_surjective : Surjective cs.wordProd := by
+  intro w
+  apply cs.simple_induction_left w
+  · use []
+    rw [wordProd_nil]
+  · rintro _ i ⟨ω, rfl⟩
+    use i :: ω
+    rw [wordProd_cons]
+
 end CoxeterSystem
diff --git a/Mathlib/GroupTheory/MonoidLocalization.lean b/Mathlib/GroupTheory/MonoidLocalization.lean
index fc3e43b53270f..f9990e1c26446 100644
--- a/Mathlib/GroupTheory/MonoidLocalization.lean
+++ b/Mathlib/GroupTheory/MonoidLocalization.lean
@@ -1192,9 +1192,9 @@ theorem map_comp : (f.map hy k).comp f.toMap = k.toMap.comp g :=
 @[to_additive]
 theorem map_mk' (x) (y : S) : f.map hy k (f.mk' x y) = k.mk' (g x) ⟨g y, hy y⟩ := by
   rw [map, lift_mk', mul_inv_left]
-  · show k.toMap (g x) = k.toMap (g y) * _
-    rw [mul_mk'_eq_mk'_of_mul]
-    exact (k.mk'_mul_cancel_left (g x) ⟨g y, hy y⟩).symm
+  show k.toMap (g x) = k.toMap (g y) * _
+  rw [mul_mk'_eq_mk'_of_mul]
+  exact (k.mk'_mul_cancel_left (g x) ⟨g y, hy y⟩).symm
 #align submonoid.localization_map.map_mk' Submonoid.LocalizationMap.map_mk'
 #align add_submonoid.localization_map.map_mk' AddSubmonoid.LocalizationMap.map_mk'
 
diff --git a/Mathlib/GroupTheory/Subgroup/Basic.lean b/Mathlib/GroupTheory/Subgroup/Basic.lean
index 797267b66f7ac..51d36fa2d3b05 100644
--- a/Mathlib/GroupTheory/Subgroup/Basic.lean
+++ b/Mathlib/GroupTheory/Subgroup/Basic.lean
@@ -3512,8 +3512,8 @@ theorem subgroupOf_sup (A A' B : Subgroup G) (hA : A ≤ B) (hA' : A' ≤ B) :
   refine'
     map_injective_of_ker_le B.subtype (ker_le_comap _ _)
       (le_trans (ker_le_comap B.subtype _) le_sup_left) _
-  · simp only [subgroupOf, map_comap_eq, map_sup, subtype_range]
-    rw [inf_of_le_right (sup_le hA hA'), inf_of_le_right hA', inf_of_le_right hA]
+  simp only [subgroupOf, map_comap_eq, map_sup, subtype_range]
+  rw [inf_of_le_right (sup_le hA hA'), inf_of_le_right hA', inf_of_le_right hA]
 #align subgroup.subgroup_of_sup Subgroup.subgroupOf_sup
 #align add_subgroup.add_subgroup_of_sup AddSubgroup.addSubgroupOf_sup
 
diff --git a/Mathlib/GroupTheory/Subsemigroup/Membership.lean b/Mathlib/GroupTheory/Subsemigroup/Membership.lean
index ef1cfbb1d26a7..1f37b25066c25 100644
--- a/Mathlib/GroupTheory/Subsemigroup/Membership.lean
+++ b/Mathlib/GroupTheory/Subsemigroup/Membership.lean
@@ -48,9 +48,9 @@ theorem mem_iSup_of_directed {S : ι → Subsemigroup M} (hS : Directed (· ≤
   suffices x ∈ closure (⋃ i, (S i : Set M)) → ∃ i, x ∈ S i by
     simpa only [closure_iUnion, closure_eq (S _)] using this
   refine fun hx ↦ closure_induction hx (fun y hy ↦ mem_iUnion.mp hy) ?_
-  · rintro x y ⟨i, hi⟩ ⟨j, hj⟩
-    rcases hS i j with ⟨k, hki, hkj⟩
-    exact ⟨k, (S k).mul_mem (hki hi) (hkj hj)⟩
+  rintro x y ⟨i, hi⟩ ⟨j, hj⟩
+  rcases hS i j with ⟨k, hki, hkj⟩
+  exact ⟨k, (S k).mul_mem (hki hi) (hkj hj)⟩
 #align subsemigroup.mem_supr_of_directed Subsemigroup.mem_iSup_of_directed
 #align add_subsemigroup.mem_supr_of_directed AddSubsemigroup.mem_iSup_of_directed
 
diff --git a/Mathlib/GroupTheory/Subsemigroup/Operations.lean b/Mathlib/GroupTheory/Subsemigroup/Operations.lean
index 3a7e9588e0ffd..7bb61f391c5f3 100644
--- a/Mathlib/GroupTheory/Subsemigroup/Operations.lean
+++ b/Mathlib/GroupTheory/Subsemigroup/Operations.lean
@@ -625,7 +625,7 @@ theorem closure_closure_coe_preimage {s : Set M} :
   eq_top_iff.2 fun x =>
     Subtype.recOn x fun x hx _ => by
       refine' closure_induction' _ (fun g hg => subset_closure hg) (fun g₁ g₂ hg₁ hg₂ => _) hx
-      · exact Subsemigroup.mul_mem _
+      exact Subsemigroup.mul_mem _
 #align subsemigroup.closure_closure_coe_preimage Subsemigroup.closure_closure_coe_preimage
 #align add_subsemigroup.closure_closure_coe_preimage AddSubsemigroup.closure_closure_coe_preimage
 
diff --git a/Mathlib/LinearAlgebra/Basic.lean b/Mathlib/LinearAlgebra/Basic.lean
index bc396713c9c60..6b73ea1f4b888 100644
--- a/Mathlib/LinearAlgebra/Basic.lean
+++ b/Mathlib/LinearAlgebra/Basic.lean
@@ -1170,12 +1170,12 @@ theorem funLeft_surjective_of_injective (f : m → n) (hf : Injective f) :
   classical
     intro g
     refine' ⟨fun x => if h : ∃ y, f y = x then g h.choose else 0, _⟩
-    · ext
-      dsimp only [funLeft_apply]
-      split_ifs with w
-      · congr
-        exact hf w.choose_spec
-      · simp only [not_true, exists_apply_eq_apply] at w
+    ext
+    dsimp only [funLeft_apply]
+    split_ifs with w
+    · congr
+      exact hf w.choose_spec
+    · simp only [not_true, exists_apply_eq_apply] at w
 #align linear_map.fun_left_surjective_of_injective LinearMap.funLeft_surjective_of_injective
 
 theorem funLeft_injective_of_surjective (f : m → n) (hf : Surjective f) :
diff --git a/Mathlib/LinearAlgebra/BilinearForm/Hom.lean b/Mathlib/LinearAlgebra/BilinearForm/Hom.lean
index 2914e65827962..70db56bfc5276 100644
--- a/Mathlib/LinearAlgebra/BilinearForm/Hom.lean
+++ b/Mathlib/LinearAlgebra/BilinearForm/Hom.lean
@@ -60,14 +60,18 @@ def toLinHomAux₁ (A : BilinForm R M) (x : M) : M →ₗ[R] R := A x
 #align bilin_form.to_lin_hom_aux₁ LinearMap.BilinForm.toLinHomAux₁
 
 /-- Auxiliary definition to define `toLinHom`; see below. -/
+@[deprecated]
 def toLinHomAux₂ (A : BilinForm R M) : M →ₗ[R] M →ₗ[R] R := A
 #align bilin_form.to_lin_hom_aux₂ LinearMap.BilinForm.toLinHomAux₂
 
 /-- The linear map obtained from a `BilinForm` by fixing the left co-ordinate and evaluating in
 the right. -/
+@[deprecated]
 def toLinHom : BilinForm R M →ₗ[R] M →ₗ[R] M →ₗ[R] R := LinearMap.id
 #align bilin_form.to_lin_hom LinearMap.BilinForm.toLinHom
 
+set_option linter.deprecated false in
+@[deprecated]
 theorem toLin'_apply (A : BilinForm R M) (x : M) : toLinHom (M := M) A x = A x :=
   rfl
 #align bilin_form.to_lin'_apply LinearMap.BilinForm.toLin'_apply
@@ -76,7 +80,7 @@ variable (B)
 
 theorem sum_left {α} (t : Finset α) (g : α → M) (w : M) :
     B (∑ i in t, g i) w = ∑ i in t, B (g i) w :=
-  (BilinForm.toLinHom (M := M) B).map_sum₂ t g w
+  B.map_sum₂ t g w
 #align bilin_form.sum_left LinearMap.BilinForm.sum_left
 
 variable (w : M)
@@ -94,7 +98,7 @@ variable {B}
 /-- The linear map obtained from a `BilinForm` by fixing the right co-ordinate and evaluating in
 the left. -/
 def toLinHomFlip : BilinForm R M →ₗ[R] M →ₗ[R] M →ₗ[R] R :=
-  toLinHom.comp flipHom.toLinearMap
+  flipHom.toLinearMap
 #align bilin_form.to_lin_hom_flip LinearMap.BilinForm.toLinHomFlip
 
 theorem toLin'Flip_apply (A : BilinForm R M) (x : M) : toLinHomFlip (M := M) A x = fun y => A y x :=
@@ -116,7 +120,9 @@ This is an auxiliary definition for the full linear equivalence `LinearMap.toBil
 def LinearMap.toBilinAux (f : M →ₗ[R] M →ₗ[R] R) : BilinForm R M := f
 #align linear_map.to_bilin_aux LinearMap.toBilinAux
 
+set_option linter.deprecated false in
 /-- Bilinear forms are linearly equivalent to maps with two arguments that are linear in both. -/
+@[deprecated]
 def LinearMap.BilinForm.toLin : BilinForm R M ≃ₗ[R] M →ₗ[R] M →ₗ[R] R :=
   { BilinForm.toLinHom with
     invFun := LinearMap.toBilinAux
@@ -124,35 +130,41 @@ def LinearMap.BilinForm.toLin : BilinForm R M ≃ₗ[R] M →ₗ[R] M →ₗ[R]
     right_inv := fun _ => rfl }
 #align bilin_form.to_lin LinearMap.BilinForm.toLin
 
+set_option linter.deprecated false in
 /-- A map with two arguments that is linear in both is linearly equivalent to bilinear form. -/
+@[deprecated]
 def LinearMap.toBilin : (M →ₗ[R] M →ₗ[R] R) ≃ₗ[R] BilinForm R M :=
   BilinForm.toLin.symm
 #align linear_map.to_bilin LinearMap.toBilin
 
-@[simp]
+@[deprecated]
 theorem LinearMap.toBilinAux_eq (f : M →ₗ[R] M →ₗ[R] R) :
-    LinearMap.toBilinAux f = LinearMap.toBilin f :=
+    LinearMap.toBilinAux f = f :=
   rfl
 #align linear_map.to_bilin_aux_eq LinearMap.toBilinAux_eq
 
-@[simp]
+set_option linter.deprecated false in
+@[deprecated]
 theorem LinearMap.toBilin_symm :
     (LinearMap.toBilin.symm : BilinForm R M ≃ₗ[R] _) = BilinForm.toLin :=
   rfl
 #align linear_map.to_bilin_symm LinearMap.toBilin_symm
 
-@[simp]
+set_option linter.deprecated false in
+@[deprecated]
 theorem BilinForm.toLin_symm :
     (BilinForm.toLin.symm : _ ≃ₗ[R] BilinForm R M) = LinearMap.toBilin :=
   LinearMap.toBilin.symm_symm
 #align bilin_form.to_lin_symm BilinForm.toLin_symm
 
-@[simp]
+set_option linter.deprecated false in
+@[deprecated]
 theorem LinearMap.toBilin_apply (f : M →ₗ[R] M →ₗ[R] R) (x y : M) :
     toBilin f x y = f x y :=
   rfl
 
-@[simp]
+set_option linter.deprecated false in
+@[deprecated]
 theorem BilinForm.toLin_apply (x : M) : BilinForm.toLin B x = B x :=
   rfl
 #align bilin_form.to_lin_apply BilinForm.toLin_apply
diff --git a/Mathlib/LinearAlgebra/BilinearForm/Properties.lean b/Mathlib/LinearAlgebra/BilinearForm/Properties.lean
index adf83912e67b3..d62b73ac8b8e1 100644
--- a/Mathlib/LinearAlgebra/BilinearForm/Properties.lean
+++ b/Mathlib/LinearAlgebra/BilinearForm/Properties.lean
@@ -417,7 +417,7 @@ theorem nondegenerate_iff_ker_eq_bot {B : BilinForm R M} :
 #align bilin_form.nondegenerate_iff_ker_eq_bot LinearMap.BilinForm.nondegenerate_iff_ker_eq_bot
 
 theorem Nondegenerate.ker_eq_bot {B : BilinForm R M} (h : B.Nondegenerate) :
-    LinearMap.ker (BilinForm.toLin B) = ⊥ :=
+    LinearMap.ker B = ⊥ :=
   nondegenerate_iff_ker_eq_bot.mp h
 #align bilin_form.nondegenerate.ker_eq_bot LinearMap.BilinForm.Nondegenerate.ker_eq_bot
 
@@ -507,8 +507,7 @@ lemma dualBasis_dualBasis_flip (B : BilinForm K V) (hB : B.Nondegenerate) {ι}
     B.dualBasis hB (B.flip.dualBasis hB.flip b) = b := by
   ext i
   refine LinearMap.ker_eq_bot.mp hB.ker_eq_bot ((B.flip.dualBasis hB.flip b).ext (fun j ↦ ?_))
-  simp_rw [BilinForm.toLin_apply, apply_dualBasis_left, ← B.flip_apply,
-    apply_dualBasis_left, @eq_comm _ i j]
+  simp_rw [apply_dualBasis_left, ← B.flip_apply, apply_dualBasis_left, @eq_comm _ i j]
 
 @[simp]
 lemma dualBasis_flip_dualBasis (B : BilinForm K V) (hB : B.Nondegenerate) {ι}
@@ -531,7 +530,7 @@ section LinearAdjoints
 is the linear map `B₂.toLin⁻¹ ∘ B₁.toLin`. -/
 noncomputable def symmCompOfNondegenerate (B₁ B₂ : BilinForm K V) (b₂ : B₂.Nondegenerate) :
     V →ₗ[K] V :=
-  (B₂.toDual b₂).symm.toLinearMap.comp (BilinForm.toLin B₁)
+  (B₂.toDual b₂).symm.toLinearMap.comp B₁
 #align bilin_form.symm_comp_of_nondegenerate LinearMap.BilinForm.symmCompOfNondegenerate
 
 theorem comp_symmCompOfNondegenerate_apply (B₁ : BilinForm K V) {B₂ : BilinForm K V}
@@ -540,7 +539,6 @@ theorem comp_symmCompOfNondegenerate_apply (B₁ : BilinForm K V) {B₂ : BilinF
   erw [symmCompOfNondegenerate]
   simp only [coe_comp, LinearEquiv.coe_coe, Function.comp_apply, DFunLike.coe_fn_eq]
   erw [LinearEquiv.apply_symm_apply (B₂.toDual b₂)]
-  rfl
 #align bilin_form.comp_symm_comp_of_nondegenerate_apply LinearMap.BilinForm.comp_symmCompOfNondegenerate_apply
 
 @[simp]
diff --git a/Mathlib/LinearAlgebra/Eigenspace/Zero.lean b/Mathlib/LinearAlgebra/Eigenspace/Zero.lean
index 3843064b61487..1f87f1dcae75b 100644
--- a/Mathlib/LinearAlgebra/Eigenspace/Zero.lean
+++ b/Mathlib/LinearAlgebra/Eigenspace/Zero.lean
@@ -69,10 +69,7 @@ lemma charpoly_nilpotent_tfae [IsNoetherian R M] (φ : Module.End R M) :
     rw [← mem_ker] at hk
     exact Submodule.mem_iSup_of_mem _ hk
   tfae_have 2 ↔ 4
-  · rw [← φ.charpoly_natDegree]
-    refine ⟨?_, φ.charpoly_monic.eq_X_pow_of_natTrailingDegree_eq_natDegree⟩
-    intro h
-    rw [← natTrailingDegree_X_pow (R := R) φ.charpoly.natDegree, ← h]
+  · rw [← φ.charpoly_natDegree, φ.charpoly_monic.eq_X_pow_iff_natTrailingDegree_eq_natDegree]
   tfae_finish
 
 lemma charpoly_eq_X_pow_iff [IsNoetherian R M] (φ : Module.End R M) :
diff --git a/Mathlib/LinearAlgebra/Matrix/BilinearForm.lean b/Mathlib/LinearAlgebra/Matrix/BilinearForm.lean
index 1d6478eb0937d..5d78de28e25b4 100644
--- a/Mathlib/LinearAlgebra/Matrix/BilinearForm.lean
+++ b/Mathlib/LinearAlgebra/Matrix/BilinearForm.lean
@@ -62,7 +62,7 @@ open Matrix
 
 This is an auxiliary definition for the equivalence `Matrix.toBilin'`. -/
 def Matrix.toBilin'Aux [Fintype n] (M : Matrix n n R₂) : BilinForm R₂ (n → R₂) :=
-  LinearMap.toBilin (Matrix.toLinearMap₂'Aux _ _ M)
+  Matrix.toLinearMap₂'Aux _ _ M
 #align matrix.to_bilin'_aux Matrix.toBilin'Aux
 
 theorem Matrix.toBilin'Aux_stdBasis [Fintype n] [DecidableEq n] (M : Matrix n n R₂) (i j : n) :
@@ -75,7 +75,7 @@ theorem Matrix.toBilin'Aux_stdBasis [Fintype n] [DecidableEq n] (M : Matrix n n
 
 This is an auxiliary definition for the equivalence `Matrix.toBilin'`. -/
 def BilinForm.toMatrixAux (b : n → M₂) : BilinForm R₂ M₂ →ₗ[R₂] Matrix n n R₂ :=
-  (LinearMap.toMatrix₂Aux b b) ∘ₗ BilinForm.toLinHom
+  LinearMap.toMatrix₂Aux b b
 #align bilin_form.to_matrix_aux BilinForm.toMatrixAux
 
 @[simp]
@@ -91,11 +91,8 @@ theorem toBilin'Aux_toMatrixAux [DecidableEq n] (B₂ : BilinForm R₂ (n → R
     -- Porting note: had to hint the base ring even though it should be clear from context...
     Matrix.toBilin'Aux (BilinForm.toMatrixAux (R₂ := R₂)
       (fun j => stdBasis R₂ (fun _ => R₂) j 1) B₂) = B₂ := by
-  rw [BilinForm.toMatrixAux, Matrix.toBilin'Aux, coe_comp, Function.comp_apply,
+  rw [BilinForm.toMatrixAux, Matrix.toBilin'Aux,
     toLinearMap₂'Aux_toMatrix₂Aux]
-  ext x y
-  simp only [coe_comp, coe_single, Function.comp_apply, toBilin_apply]
-  rfl
 #align to_bilin'_aux_to_matrix_aux toBilin'Aux_toMatrixAux
 
 section ToMatrix'
@@ -236,7 +233,7 @@ variable [DecidableEq n] (b : Basis n R₂ M₂)
 /-- `BilinForm.toMatrix b` is the equivalence between `R`-bilinear forms on `M` and
 `n`-by-`n` matrices with entries in `R`, if `b` is an `R`-basis for `M`. -/
 noncomputable def BilinForm.toMatrix : BilinForm R₂ M₂ ≃ₗ[R₂] Matrix n n R₂ :=
-  BilinForm.toLin ≪≫ₗ (LinearMap.toMatrix₂ b b)
+  LinearMap.toMatrix₂ b b
 #align bilin_form.to_matrix BilinForm.toMatrix
 
 /-- `BilinForm.toMatrix b` is the equivalence between `R`-bilinear forms on `M` and
@@ -282,7 +279,6 @@ theorem Matrix.toBilin_basisFun : Matrix.toBilin (Pi.basisFun R₂ n) = Matrix.t
 theorem BilinForm.toMatrix_basisFun :
     BilinForm.toMatrix (Pi.basisFun R₂ n) = BilinForm.toMatrix' := by
   rw [BilinForm.toMatrix, BilinForm.toMatrix', LinearMap.toMatrix₂_basisFun]
-  rfl
 #align bilin_form.to_matrix_basis_fun BilinForm.toMatrix_basisFun
 
 @[simp]
@@ -343,11 +339,8 @@ theorem BilinForm.toMatrix_mul (B : BilinForm R₂ M₂) (M : Matrix n n R₂) :
 theorem Matrix.toBilin_comp (M : Matrix n n R₂) (P Q : Matrix n o R₂) :
     (Matrix.toBilin b M).comp (toLin c b P) (toLin c b Q) = Matrix.toBilin c (Pᵀ * M * Q) := by
   ext x y
-  rw [Matrix.toBilin,
-    BilinForm.toMatrix, Matrix.toBilin, BilinForm.toMatrix, LinearEquiv.trans_symm,
-    LinearEquiv.trans_symm, toMatrix₂_symm, BilinForm.toLin_symm, LinearEquiv.trans_apply,
-    toMatrix₂_symm, BilinForm.toLin_symm, LinearEquiv.trans_apply,
-    ← Matrix.toLinearMap₂_compl₁₂ b b c c]
+  rw [Matrix.toBilin, BilinForm.toMatrix, Matrix.toBilin, BilinForm.toMatrix, toMatrix₂_symm,
+    toMatrix₂_symm, ← Matrix.toLinearMap₂_compl₁₂ b b c c]
   simp
 #align matrix.to_bilin_comp Matrix.toBilin_comp
 
diff --git a/Mathlib/LinearAlgebra/TensorProduct/Basic.lean b/Mathlib/LinearAlgebra/TensorProduct/Basic.lean
index e58e2c3612964..7de214f7671d0 100644
--- a/Mathlib/LinearAlgebra/TensorProduct/Basic.lean
+++ b/Mathlib/LinearAlgebra/TensorProduct/Basic.lean
@@ -1032,6 +1032,30 @@ theorem congr_symm_tmul (f : M ≃ₗ[R] P) (g : N ≃ₗ[R] Q) (p : P) (q : Q)
   rfl
 #align tensor_product.congr_symm_tmul TensorProduct.congr_symm_tmul
 
+theorem congr_symm (f : M ≃ₗ[R] P) (g : N ≃ₗ[R] Q) : (congr f g).symm = congr f.symm g.symm := rfl
+
+@[simp] theorem congr_refl_refl : congr (.refl R M) (.refl R N) = .refl R _ :=
+  LinearEquiv.toLinearMap_injective <| ext' fun _ _ ↦ rfl
+
+theorem congr_trans (f : M ≃ₗ[R] P) (g : N ≃ₗ[R] Q) (f' : P ≃ₗ[R] S) (g' : Q ≃ₗ[R] T) :
+    congr (f ≪≫ₗ f') (g ≪≫ₗ g') = congr f g ≪≫ₗ congr f' g' :=
+  LinearEquiv.toLinearMap_injective <| map_comp _ _ _ _
+
+theorem congr_mul (f : M ≃ₗ[R] M) (g : N ≃ₗ[R] N) (f' : M ≃ₗ[R] M) (g' : N ≃ₗ[R] N) :
+    congr (f * f') (g * g') = congr f g * congr f' g' := congr_trans _ _ _ _
+
+@[simp] theorem congr_pow (f : M ≃ₗ[R] M) (g : N ≃ₗ[R] N) (n : ℕ) :
+    congr f g ^ n = congr (f ^ n) (g ^ n) := by
+  induction n with
+  | zero => exact congr_refl_refl.symm
+  | succ n ih => simp_rw [pow_succ, ih, congr_mul]
+
+@[simp] theorem congr_zpow (f : M ≃ₗ[R] M) (g : N ≃ₗ[R] N) (n : ℤ) :
+    congr f g ^ n = congr (f ^ n) (g ^ n) := by
+  induction n with
+  | ofNat n => exact congr_pow _ _ _
+  | negSucc n => simp_rw [zpow_negSucc, congr_pow]; exact congr_symm _ _
+
 variable (R M N P Q)
 
 /-- A tensor product analogue of `mul_left_comm`. -/
@@ -1121,16 +1145,19 @@ theorem tensorTensorTensorAssoc_symm_tmul (m : M) (n : N) (p : P) (q : Q) :
 end TensorProduct
 
 open scoped TensorProduct
+
 namespace LinearMap
 
 variable {N}
 
-/-- `lTensor M f : M ⊗ N →ₗ M ⊗ P` is the natural linear map induced by `f : N →ₗ P`. -/
+/-- `LinearMap.lTensor M f : M ⊗ N →ₗ M ⊗ P` is the natural linear map
+induced by `f : N →ₗ P`. -/
 def lTensor (f : N →ₗ[R] P) : M ⊗[R] N →ₗ[R] M ⊗[R] P :=
   TensorProduct.map id f
 #align linear_map.ltensor LinearMap.lTensor
 
-/-- `rTensor f M : N₁ ⊗ M →ₗ N₂ ⊗ M` is the natural linear map induced by `f : N₁ →ₗ N₂`. -/
+/-- `LinearMap.rTensor M f : N₁ ⊗ M →ₗ N₂ ⊗ M` is the natural linear map
+induced by `f : N₁ →ₗ N₂`. -/
 def rTensor (f : N →ₗ[R] P) : N ⊗[R] M →ₗ[R] P ⊗[R] M :=
   TensorProduct.map f id
 #align linear_map.rtensor LinearMap.rTensor
@@ -1355,6 +1382,114 @@ theorem lTensor_pow (f : N →ₗ[R] N) (n : ℕ) : f.lTensor M ^ n = (f ^ n).lT
 
 end LinearMap
 
+namespace LinearEquiv
+
+variable {N}
+
+/-- `LinearEquiv.lTensor M f : M ⊗ N ≃ₗ M ⊗ P` is the natural linear equivalence
+induced by `f : N ≃ₗ P`. -/
+def lTensor (f : N ≃ₗ[R] P) : M ⊗[R] N ≃ₗ[R] M ⊗[R] P := TensorProduct.congr (refl R M) f
+
+/-- `LinearEquiv.rTensor M f : N₁ ⊗ M ≃ₗ N₂ ⊗ M` is the natural linear equivalence
+induced by `f : N₁ ≃ₗ N₂`. -/
+def rTensor (f : N ≃ₗ[R] P) : N ⊗[R] M ≃ₗ[R] P ⊗[R] M := TensorProduct.congr f (refl R M)
+
+variable (g : P ≃ₗ[R] Q) (f : N ≃ₗ[R] P) (m : M) (n : N) (p : P) (x : M ⊗[R] N) (y : N ⊗[R] M)
+
+@[simp] theorem coe_lTensor : lTensor M f = (f : N →ₗ[R] P).lTensor M := rfl
+
+@[simp] theorem coe_lTensor_symm : (lTensor M f).symm = (f.symm : P →ₗ[R] N).lTensor M := rfl
+
+@[simp] theorem coe_rTensor : rTensor M f = (f : N →ₗ[R] P).rTensor M := rfl
+
+@[simp] theorem coe_rTensor_symm : (rTensor M f).symm = (f.symm : P →ₗ[R] N).rTensor M := rfl
+
+@[simp] theorem lTensor_tmul : f.lTensor M (m ⊗ₜ n) = m ⊗ₜ f n := rfl
+
+@[simp] theorem lTensor_symm_tmul : (f.lTensor M).symm (m ⊗ₜ p) = m ⊗ₜ f.symm p := rfl
+
+@[simp] theorem rTensor_tmul : f.rTensor M (n ⊗ₜ m) = f n ⊗ₜ m := rfl
+
+@[simp] theorem rTensor_symm_tmul : (f.rTensor M).symm (p ⊗ₜ m) = f.symm p ⊗ₜ m := rfl
+
+lemma comm_trans_rTensor_trans_comm_eq (g : N ≃ₗ[R] P) :
+    TensorProduct.comm R Q N ≪≫ₗ rTensor Q g ≪≫ₗ TensorProduct.comm R P Q = lTensor Q g :=
+  toLinearMap_injective <| TensorProduct.ext rfl
+
+lemma comm_trans_lTensor_trans_comm_eq (g : N ≃ₗ[R] P) :
+    TensorProduct.comm R N Q ≪≫ₗ lTensor Q g ≪≫ₗ TensorProduct.comm R Q P = rTensor Q g :=
+  toLinearMap_injective <| TensorProduct.ext rfl
+
+theorem lTensor_trans : (f ≪≫ₗ g).lTensor M = f.lTensor M ≪≫ₗ g.lTensor M :=
+  toLinearMap_injective <| LinearMap.lTensor_comp M _ _
+
+theorem lTensor_trans_apply : (f ≪≫ₗ g).lTensor M x = g.lTensor M (f.lTensor M x) :=
+  LinearMap.lTensor_comp_apply M _ _ x
+
+theorem rTensor_trans : (f ≪≫ₗ g).rTensor M = f.rTensor M ≪≫ₗ g.rTensor M :=
+  toLinearMap_injective <| LinearMap.rTensor_comp M _ _
+
+theorem rTensor_trans_apply : (f ≪≫ₗ g).rTensor M y = g.rTensor M (f.rTensor M y) :=
+  LinearMap.rTensor_comp_apply M _ _ y
+
+theorem lTensor_mul (f g : N ≃ₗ[R] N) : (f * g).lTensor M = f.lTensor M * g.lTensor M :=
+  lTensor_trans M f g
+
+theorem rTensor_mul (f g : N ≃ₗ[R] N) : (f * g).rTensor M = f.rTensor M * g.rTensor M :=
+  rTensor_trans M f g
+
+variable (N)
+
+@[simp] theorem lTensor_refl : (refl R N).lTensor M = refl R _ := TensorProduct.congr_refl_refl
+
+theorem lTensor_refl_apply : (refl R N).lTensor M x = x := by rw [lTensor_refl, refl_apply]
+
+@[simp] theorem rTensor_refl : (refl R N).rTensor M = refl R _ := TensorProduct.congr_refl_refl
+
+theorem rTensor_refl_apply : (refl R N).rTensor M y = y := by rw [rTensor_refl, refl_apply]
+
+variable {N}
+
+@[simp] theorem rTensor_trans_lTensor (f : M ≃ₗ[R] P) (g : N ≃ₗ[R] Q) :
+    f.rTensor N ≪≫ₗ g.lTensor P = TensorProduct.congr f g :=
+  toLinearMap_injective <| LinearMap.lTensor_comp_rTensor M _ _
+
+@[simp] theorem lTensor_trans_rTensor (f : M ≃ₗ[R] P) (g : N ≃ₗ[R] Q) :
+    g.lTensor M ≪≫ₗ f.rTensor Q = TensorProduct.congr f g :=
+  toLinearMap_injective <| LinearMap.rTensor_comp_lTensor M _ _
+
+@[simp] theorem rTensor_trans_congr (f : M ≃ₗ[R] P) (g : N ≃ₗ[R] Q) (f' : S ≃ₗ[R] M) :
+    f'.rTensor _ ≪≫ₗ TensorProduct.congr f g = TensorProduct.congr (f' ≪≫ₗ f) g :=
+  toLinearMap_injective <| LinearMap.map_comp_rTensor M _ _ _
+
+@[simp] theorem lTensor_trans_congr (f : M ≃ₗ[R] P) (g : N ≃ₗ[R] Q) (g' : S ≃ₗ[R] N) :
+    g'.lTensor _ ≪≫ₗ TensorProduct.congr f g = TensorProduct.congr f (g' ≪≫ₗ g) :=
+  toLinearMap_injective <| LinearMap.map_comp_lTensor M _ _ _
+
+@[simp] theorem congr_trans_rTensor (f' : P ≃ₗ[R] S) (f : M ≃ₗ[R] P) (g : N ≃ₗ[R] Q) :
+    TensorProduct.congr f g ≪≫ₗ f'.rTensor _ = TensorProduct.congr (f ≪≫ₗ f') g :=
+  toLinearMap_injective <| LinearMap.rTensor_comp_map M _ _ _
+
+@[simp] theorem congr_trans_lTensor (g' : Q ≃ₗ[R] S) (f : M ≃ₗ[R] P) (g : N ≃ₗ[R] Q) :
+    TensorProduct.congr f g ≪≫ₗ g'.lTensor _ = TensorProduct.congr f (g ≪≫ₗ g') :=
+  toLinearMap_injective <| LinearMap.lTensor_comp_map M _ _ _
+
+variable {M}
+
+@[simp] theorem rTensor_pow (f : M ≃ₗ[R] M) (n : ℕ) : f.rTensor N ^ n = (f ^ n).rTensor N := by
+  simpa only [one_pow] using TensorProduct.congr_pow f (1 : N ≃ₗ[R] N) n
+
+@[simp] theorem rTensor_zpow (f : M ≃ₗ[R] M) (n : ℤ) : f.rTensor N ^ n = (f ^ n).rTensor N := by
+  simpa only [one_zpow] using TensorProduct.congr_zpow f (1 : N ≃ₗ[R] N) n
+
+@[simp] theorem lTensor_pow (f : N ≃ₗ[R] N) (n : ℕ) : f.lTensor M ^ n = (f ^ n).lTensor M := by
+  simpa only [one_pow] using TensorProduct.congr_pow (1 : M ≃ₗ[R] M) f n
+
+@[simp] theorem lTensor_zpow (f : N ≃ₗ[R] N) (n : ℤ) : f.lTensor M ^ n = (f ^ n).lTensor M := by
+  simpa only [one_zpow] using TensorProduct.congr_zpow (1 : M ≃ₗ[R] M) f n
+
+end LinearEquiv
+
 end Semiring
 
 section Ring
diff --git a/Mathlib/MeasureTheory/Constructions/Pi.lean b/Mathlib/MeasureTheory/Constructions/Pi.lean
index 8d37c7cbbe2a9..ebec34f92a691 100644
--- a/Mathlib/MeasureTheory/Constructions/Pi.lean
+++ b/Mathlib/MeasureTheory/Constructions/Pi.lean
@@ -412,6 +412,23 @@ instance {α : ι → Type*} [∀ i, MeasureSpace (α i)] [∀ i, SigmaFinite (v
     SigmaFinite (volume : Measure (∀ i, α i)) :=
   pi.sigmaFinite _
 
+instance pi.instIsFiniteMeasure [∀ i, IsFiniteMeasure (μ i)] :
+    IsFiniteMeasure (Measure.pi μ) :=
+  ⟨Measure.pi_univ μ ▸ ENNReal.prod_lt_top (fun i _ ↦ measure_ne_top (μ i) _)⟩
+
+instance {α : ι → Type*} [∀ i, MeasureSpace (α i)] [∀ i, IsFiniteMeasure (volume : Measure (α i))] :
+    IsFiniteMeasure (volume : Measure (∀ i, α i)) :=
+  pi.instIsFiniteMeasure _
+
+instance pi.instIsProbabilityMeasure [∀ i, IsProbabilityMeasure (μ i)] :
+    IsProbabilityMeasure (Measure.pi μ) :=
+  ⟨by simp only [Measure.pi_univ, measure_univ, Finset.prod_const_one]⟩
+
+instance {α : ι → Type*} [∀ i, MeasureSpace (α i)]
+    [∀ i, IsProbabilityMeasure (volume : Measure (α i))] :
+    IsProbabilityMeasure (volume : Measure (∀ i, α i)) :=
+  pi.instIsProbabilityMeasure _
+
 theorem pi_of_empty {α : Type*} [Fintype α] [IsEmpty α] {β : α → Type*}
     {m : ∀ a, MeasurableSpace (β a)} (μ : ∀ a : α, Measure (β a)) (x : ∀ a, β a := isEmptyElim) :
     Measure.pi μ = dirac x := by
diff --git a/Mathlib/MeasureTheory/Decomposition/Lebesgue.lean b/Mathlib/MeasureTheory/Decomposition/Lebesgue.lean
index c16941179a16f..10f4536cb90d5 100644
--- a/Mathlib/MeasureTheory/Decomposition/Lebesgue.lean
+++ b/Mathlib/MeasureTheory/Decomposition/Lebesgue.lean
@@ -46,19 +46,16 @@ The Lebesgue decomposition provides the Radon-Nikodym theorem readily.
 Lebesgue decomposition theorem
 -/
 
-
-noncomputable section
-
-open scoped Classical MeasureTheory NNReal ENNReal
+open scoped MeasureTheory NNReal ENNReal
 
 open Set
 
-variable {α β : Type*} {m : MeasurableSpace α} {μ ν : MeasureTheory.Measure α}
-
 namespace MeasureTheory
 
 namespace Measure
 
+variable {α β : Type*} {m : MeasurableSpace α} {μ ν : Measure α}
+
 /-- A pair of measures `μ` and `ν` is said to `HaveLebesgueDecomposition` if there exists a
 measure `ξ` and a measurable function `f`, such that `ξ` is mutually singular with respect to
 `ν` and `μ = ξ + ν.withDensity f`. -/
@@ -68,19 +65,21 @@ class HaveLebesgueDecomposition (μ ν : Measure α) : Prop where
 #align measure_theory.measure.have_lebesgue_decomposition MeasureTheory.Measure.HaveLebesgueDecomposition
 #align measure_theory.measure.have_lebesgue_decomposition.lebesgue_decomposition MeasureTheory.Measure.HaveLebesgueDecomposition.lebesgue_decomposition
 
+open Classical in
 /-- If a pair of measures `HaveLebesgueDecomposition`, then `singularPart` chooses the
 measure from `HaveLebesgueDecomposition`, otherwise it returns the zero measure. For sigma-finite
 measures, `μ = μ.singularPart ν + ν.withDensity (μ.rnDeriv ν)`. -/
 @[pp_dot]
-irreducible_def singularPart (μ ν : Measure α) : Measure α :=
+noncomputable irreducible_def singularPart (μ ν : Measure α) : Measure α :=
   if h : HaveLebesgueDecomposition μ ν then (Classical.choose h.lebesgue_decomposition).1 else 0
 #align measure_theory.measure.singular_part MeasureTheory.Measure.singularPart
 
+open Classical in
 /-- If a pair of measures `HaveLebesgueDecomposition`, then `rnDeriv` chooses the
 measurable function from `HaveLebesgueDecomposition`, otherwise it returns the zero function.
 For sigma-finite measures, `μ = μ.singularPart ν + ν.withDensity (μ.rnDeriv ν)`. -/
 @[pp_dot]
-irreducible_def rnDeriv (μ ν : Measure α) : α → ℝ≥0∞ :=
+noncomputable irreducible_def rnDeriv (μ ν : Measure α) : α → ℝ≥0∞ :=
   if h : HaveLebesgueDecomposition μ ν then (Classical.choose h.lebesgue_decomposition).2 else 0
 #align measure_theory.measure.rn_deriv MeasureTheory.Measure.rnDeriv
 
diff --git a/Mathlib/MeasureTheory/MeasurableSpace/Basic.lean b/Mathlib/MeasureTheory/MeasurableSpace/Basic.lean
index 16c147f98c98a..39cf7cf89dd5d 100644
--- a/Mathlib/MeasureTheory/MeasurableSpace/Basic.lean
+++ b/Mathlib/MeasureTheory/MeasurableSpace/Basic.lean
@@ -1844,6 +1844,22 @@ theorem coe_sumPiEquivProdPi (α : δ ⊕ δ' → Type*) [∀ i, MeasurableSpace
 theorem coe_sumPiEquivProdPi_symm (α : δ ⊕ δ' → Type*) [∀ i, MeasurableSpace (α i)] :
     ⇑(MeasurableEquiv.sumPiEquivProdPi α).symm = (Equiv.sumPiEquivProdPi α).symm := by rfl
 
+/-- The measurable equivalence for (dependent) functions on an Option type
+  `(∀ i : Option δ, α i) ≃ᵐ (∀ (i : δ), α i) × α none`. -/
+def piOptionEquivProd {δ : Type*} (α : Option δ → Type*) [∀ i, MeasurableSpace (α i)] :
+    (∀ i, α i) ≃ᵐ (∀ (i : δ), α i) × α none :=
+  let e : Option δ ≃ δ ⊕ PUnit := Equiv.optionEquivSumPUnit δ
+  let em1 : ((i : δ ⊕ PUnit) → α (e.symm i)) ≃ᵐ ((a : Option δ) → α a) :=
+    MeasurableEquiv.piCongrLeft α e.symm
+  let em2 : ((i : δ ⊕ PUnit) → α (e.symm i)) ≃ᵐ ((i : δ) → α (e.symm (Sum.inl i)))
+      × ((i' : PUnit) → α (e.symm (Sum.inr i'))) :=
+    MeasurableEquiv.sumPiEquivProdPi (fun i ↦ α (e.symm i))
+  let em3 : ((i : δ) → α (e.symm (Sum.inl i))) × ((i' : PUnit.{u_3 + 1}) → α (e.symm (Sum.inr i')))
+      ≃ᵐ ((i : δ) → α (some i)) × α none :=
+    MeasurableEquiv.prodCongr (MeasurableEquiv.refl ((i : δ) → α (e.symm (Sum.inl i))))
+      (MeasurableEquiv.piUnique fun i ↦ α (e.symm (Sum.inr i)))
+  em1.symm.trans <| em2.trans em3
+
 /-- The measurable equivalence `(∀ i : s, π i) × (∀ i : t, π i) ≃ᵐ (∀ i : s ∪ t, π i)`
   for disjoint finsets `s` and `t`. `Equiv.piFinsetUnion` as a measurable equivalence. -/
 def piFinsetUnion [DecidableEq δ'] {s t : Finset δ'} (h : Disjoint s t) :
diff --git a/Mathlib/MeasureTheory/Measure/MeasureSpace.lean b/Mathlib/MeasureTheory/Measure/MeasureSpace.lean
index cfcc444cb3bdf..cf3ab615882c9 100644
--- a/Mathlib/MeasureTheory/Measure/MeasureSpace.lean
+++ b/Mathlib/MeasureTheory/Measure/MeasureSpace.lean
@@ -1663,6 +1663,10 @@ lemma add_right (h1 : μ ≪ ν) (ν' : Measure α) : μ ≪ ν + ν' := by
 
 end AbsolutelyContinuous
 
+@[simp]
+lemma absolutelyContinuous_zero_iff : μ ≪ 0 ↔ μ = 0 :=
+  ⟨fun h ↦ measure_univ_eq_zero.mp (h rfl), fun h ↦ h.symm ▸ AbsolutelyContinuous.zero _⟩
+
 alias absolutelyContinuous_refl := AbsolutelyContinuous.refl
 alias absolutelyContinuous_rfl := AbsolutelyContinuous.rfl
 
diff --git a/Mathlib/ModelTheory/Definability.lean b/Mathlib/ModelTheory/Definability.lean
index 1bec13723cfe3..6bdabe5cb215b 100644
--- a/Mathlib/ModelTheory/Definability.lean
+++ b/Mathlib/ModelTheory/Definability.lean
@@ -205,8 +205,8 @@ theorem definable_iff_finitely_definable :
         Set.mem_setOf_eq]
       apply Iff.symm
       convert BoundedFormula.realize_restrictFreeVar _
-      · ext a
-        rcases a with ⟨_ | _, _⟩ <;> simp
+      ext a
+      rcases a with ⟨_ | _, _⟩ <;> simp
   · rintro ⟨A0, hA0, hd⟩
     exact Definable.mono hd hA0
 
diff --git a/Mathlib/ModelTheory/Semantics.lean b/Mathlib/ModelTheory/Semantics.lean
index 21c50cf8a162c..5698a16f5b51e 100644
--- a/Mathlib/ModelTheory/Semantics.lean
+++ b/Mathlib/ModelTheory/Semantics.lean
@@ -452,9 +452,9 @@ theorem realize_subst {φ : L.BoundedFormula α n} {tf : α → L.Term β} {v :
     (fun n t x => by
       rw [Term.realize_subst]
       rcongr a
-      · cases a
-        · simp only [Sum.elim_inl, Function.comp_apply, Term.realize_relabel, Sum.elim_comp_inl]
-        · rfl)
+      cases a
+      · simp only [Sum.elim_inl, Function.comp_apply, Term.realize_relabel, Sum.elim_comp_inl]
+      · rfl)
     (by simp)
 #align first_order.language.bounded_formula.realize_subst FirstOrder.Language.BoundedFormula.realize_subst
 
@@ -924,8 +924,8 @@ theorem _root_.FirstOrder.Language.Formula.realize_iAlls
   · intro x
     rw [Formula.Realize, iff_iff_eq]
     congr
-    · funext i
-      exact i.elim0
+    funext i
+    exact i.elim0
 
 @[simp]
 theorem realize_iAlls [Finite γ] {f : α → β ⊕ γ}
@@ -951,8 +951,8 @@ theorem _root_.FirstOrder.Language.Formula.realize_iExs
   · intro x
     rw [Formula.Realize, iff_iff_eq]
     congr
-    · funext i
-      exact i.elim0
+    funext i
+    exact i.elim0
 
 @[simp]
 theorem realize_iExs [Finite γ] {f : α → β ⊕ γ}
diff --git a/Mathlib/NumberTheory/Padics/PadicVal.lean b/Mathlib/NumberTheory/Padics/PadicVal.lean
index f0160db4dfea2..61df9aaaf3ef6 100644
--- a/Mathlib/NumberTheory/Padics/PadicVal.lean
+++ b/Mathlib/NumberTheory/Padics/PadicVal.lean
@@ -480,8 +480,8 @@ theorem sum_pos_of_pos {n : ℕ} {F : ℕ → ℚ} (hF : ∀ i, i < n → 0 < pa
     · rw [h, zero_add]
       exact hF d (lt_add_one _)
     · refine' lt_of_lt_of_le _ (min_le_padicValRat_add hn0)
-      · refine' lt_min (hd (fun i hi => _) h) (hF d (lt_add_one _))
-        exact hF _ (lt_trans hi (lt_add_one _))
+      refine' lt_min (hd (fun i hi => _) h) (hF d (lt_add_one _))
+      exact hF _ (lt_trans hi (lt_add_one _))
 #align padic_val_rat.sum_pos_of_pos padicValRat.sum_pos_of_pos
 
 /-- If the p-adic valuation of a finite set of positive rationals is greater than a given rational
diff --git a/Mathlib/Order/CompactlyGenerated/Basic.lean b/Mathlib/Order/CompactlyGenerated/Basic.lean
index e6f67385c77e1..d82b297d91714 100644
--- a/Mathlib/Order/CompactlyGenerated/Basic.lean
+++ b/Mathlib/Order/CompactlyGenerated/Basic.lean
@@ -90,10 +90,10 @@ theorem isCompactElement_iff.{u} {α : Type u} [CompleteLattice α] (k : α) :
       have : ∀ x : t, ∃ i, s i = x := fun x => ht x.prop
       choose f hf using this
       refine' ⟨Finset.univ.image f, ht'.trans _⟩
-      · rw [Finset.sup_le_iff]
-        intro b hb
-        rw [← show s (f ⟨b, hb⟩) = id b from hf _]
-        exact Finset.le_sup (Finset.mem_image_of_mem f <| Finset.mem_univ (Subtype.mk b hb))
+      rw [Finset.sup_le_iff]
+      intro b hb
+      rw [← show s (f ⟨b, hb⟩) = id b from hf _]
+      exact Finset.le_sup (Finset.mem_image_of_mem f <| Finset.mem_univ (Subtype.mk b hb))
     · intro H s hs
       obtain ⟨t, ht⟩ :=
         H s Subtype.val
diff --git a/Mathlib/Order/Interval/Finset/Basic.lean b/Mathlib/Order/Interval/Finset/Basic.lean
index 0dfd876771062..ff8324bc4b1e4 100644
--- a/Mathlib/Order/Interval/Finset/Basic.lean
+++ b/Mathlib/Order/Interval/Finset/Basic.lean
@@ -1170,7 +1170,7 @@ lemma strictMono_iff_forall_covBy [Preorder α] [LocallyFiniteOrder α] [Preorde
   refine ⟨fun hf _ _ h ↦ hf h.lt, fun h a b hab ↦ ?_⟩
   have := Relation.TransGen.lift f h (a := a) (b := b)
   rw [← lt_iff_transGen_covBy, transGen_eq_self (@lt_trans β _)] at this
-  · exact this hab
+  exact this hab
 
 /-- A function from a locally finite preorder is antitone if and only if it is antitone when
 restricted to pairs satisfying `a ⩿ b`. -/
diff --git a/Mathlib/RingTheory/OreLocalization/Basic.lean b/Mathlib/RingTheory/OreLocalization/Basic.lean
index 2e960ec07d416..4cd989d5a18ae 100644
--- a/Mathlib/RingTheory/OreLocalization/Basic.lean
+++ b/Mathlib/RingTheory/OreLocalization/Basic.lean
@@ -636,11 +636,11 @@ protected theorem add_assoc (x y z : R[S⁻¹]) : x + y + z = x + (y + z) := by
       ← OreLocalization.expand', Subtype.coe_eq_of_eq_mk ha, ← OreLocalization.expand]
     apply OreLocalization.expand'
   · rcases oreCondition (sd : R) (sa * sc) with ⟨re, _, _⟩
-    · simp_rw [← Submonoid.coe_mul] at hb hc hd
-      rw [← mul_assoc, Subtype.coe_eq_of_eq_mk hc]
-      rw [← OreLocalization.expand, Subtype.coe_eq_of_eq_mk hd, ← mul_assoc, ←
-        OreLocalization.expand, Subtype.coe_eq_of_eq_mk hb]
-      apply OreLocalization.expand
+    simp_rw [← Submonoid.coe_mul] at hb hc hd
+    rw [← mul_assoc, Subtype.coe_eq_of_eq_mk hc]
+    rw [← OreLocalization.expand, Subtype.coe_eq_of_eq_mk hd, ← mul_assoc, ←
+      OreLocalization.expand, Subtype.coe_eq_of_eq_mk hb]
+    apply OreLocalization.expand
 #align ore_localization.add_assoc OreLocalization.add_assoc
 
 private def zero : R[S⁻¹] :=
diff --git a/Mathlib/RingTheory/Trace.lean b/Mathlib/RingTheory/Trace.lean
index 6c356c29308e8..0512a745a218a 100644
--- a/Mathlib/RingTheory/Trace.lean
+++ b/Mathlib/RingTheory/Trace.lean
@@ -190,8 +190,8 @@ variable (R S)
 /-- The `traceForm` maps `x y : S` to the trace of `x * y`.
 It is a symmetric bilinear form and is nondegenerate if the extension is separable. -/
 noncomputable def traceForm : BilinForm R S :=
-  -- Porting note: dot notation `().toBilin` does not work anymore.
-  LinearMap.toBilin (LinearMap.compr₂ (lmul R S).toLinearMap (trace R S))
+-- Porting note: dot notation `().toBilin` does not work anymore.
+  LinearMap.compr₂ (lmul R S).toLinearMap (trace R S)
 #align algebra.trace_form Algebra.traceForm
 
 variable {S}
diff --git a/Mathlib/SetTheory/Ordinal/Principal.lean b/Mathlib/SetTheory/Ordinal/Principal.lean
index e658261a1153f..75fd3ba806f6c 100644
--- a/Mathlib/SetTheory/Ordinal/Principal.lean
+++ b/Mathlib/SetTheory/Ordinal/Principal.lean
@@ -251,11 +251,11 @@ theorem mul_principal_add_is_principal_add (a : Ordinal.{u}) {b : Ordinal.{u}} (
     · rw [← succ_le_iff, succ_zero] at hb₁'
       intro c d hc hd
       rw [lt_mul_of_limit (principal_add_isLimit (lt_of_le_of_ne hb₁' hb₁.symm) hb)] at *
-      · rcases hc with ⟨x, hx, hx'⟩
-        rcases hd with ⟨y, hy, hy'⟩
-        use x + y, hb hx hy
-        rw [mul_add]
-        exact Left.add_lt_add hx' hy'
+      rcases hc with ⟨x, hx, hx'⟩
+      rcases hd with ⟨y, hy, hy'⟩
+      use x + y, hb hx hy
+      rw [mul_add]
+      exact Left.add_lt_add hx' hy'
 #align ordinal.mul_principal_add_is_principal_add Ordinal.mul_principal_add_is_principal_add
 
 /-! #### Multiplicative principal ordinals -/
diff --git a/Mathlib/SetTheory/ZFC/Basic.lean b/Mathlib/SetTheory/ZFC/Basic.lean
index 52db0f4474231..90f72b7a4c856 100644
--- a/Mathlib/SetTheory/ZFC/Basic.lean
+++ b/Mathlib/SetTheory/ZFC/Basic.lean
@@ -1495,9 +1495,9 @@ theorem mem_wf : @WellFounded Class.{u} (· ∈ ·) :=
       refine' fun a => ZFSet.inductionOn a fun x IH => ⟨_, _⟩
       rintro A ⟨z, rfl, hz⟩
       exact IH z hz
-    · refine' fun A => ⟨A, _⟩
-      rintro B ⟨x, rfl, _⟩
-      exact H x⟩
+    refine' fun A => ⟨A, _⟩
+    rintro B ⟨x, rfl, _⟩
+    exact H x⟩
 #align Class.mem_wf Class.mem_wf
 
 instance : WellFoundedRelation Class :=
diff --git a/Mathlib/Topology/Constructions.lean b/Mathlib/Topology/Constructions.lean
index a18ba36a9c1f8..d33c822ebc0c3 100644
--- a/Mathlib/Topology/Constructions.lean
+++ b/Mathlib/Topology/Constructions.lean
@@ -796,8 +796,8 @@ theorem isOpen_prod_iff' {s : Set X} {t : Set Y} :
       show IsOpen s
       · rw [← fst_image_prod s st.2]
         exact isOpenMap_fst _ H
-      show IsOpen t
-      · rw [← snd_image_prod st.1 t]
+      · show IsOpen t
+        rw [← snd_image_prod st.1 t]
         exact isOpenMap_snd _ H
     · intro H
       simp only [st.1.ne_empty, st.2.ne_empty, not_false_iff, or_false_iff] at H
diff --git a/scripts/style-exceptions.txt b/scripts/style-exceptions.txt
index c750a9cd4c4b7..4e09b8f07e761 100644
--- a/scripts/style-exceptions.txt
+++ b/scripts/style-exceptions.txt
@@ -66,6 +66,7 @@ Mathlib/LinearAlgebra/Basis.lean : line 1 : ERR_NUM_LIN : 1800 file contains 164
 Mathlib/LinearAlgebra/Dual.lean : line 1 : ERR_NUM_LIN : 2000 file contains 1847 lines, try to split it up
 Mathlib/LinearAlgebra/LinearIndependent.lean : line 1 : ERR_NUM_LIN : 1700 file contains 1537 lines, try to split it up
 Mathlib/LinearAlgebra/Multilinear/Basic.lean : line 1 : ERR_NUM_LIN : 2000 file contains 1819 lines, try to split it up
+Mathlib/LinearAlgebra/TensorProduct/Basic.lean : line 1 : ERR_NUM_LIN : 1800 file contains 1660 lines, try to split it up
 Mathlib/Logic/Equiv/Basic.lean : line 1 : ERR_NUM_LIN : 2200 file contains 2065 lines, try to split it up
 Mathlib/Mathport/Attributes.lean : line 8 : ERR_MOD : Module docstring missing, or too late
 Mathlib/Mathport/Rename.lean : line 9 : ERR_MOD : Module docstring missing, or too late