diff --git a/Mathlib/Algebra/GroupPower/Order.lean b/Mathlib/Algebra/GroupPower/Order.lean
index 64ceddae0f399..5a41cc99d3ee5 100644
--- a/Mathlib/Algebra/GroupPower/Order.lean
+++ b/Mathlib/Algebra/GroupPower/Order.lean
@@ -532,7 +532,7 @@ namespace Nat
 variable {n : ℕ} {f : α → ℕ}
 
 /-- See also `pow_left_strictMonoOn`. -/
-protected lemma pow_left_strictMono (hn : n ≠ 0) : StrictMono (. ^ n : ℕ → ℕ) :=
+protected lemma pow_left_strictMono (hn : n ≠ 0) : StrictMono (· ^ n : ℕ → ℕ) :=
   fun _ _ h ↦ Nat.pow_lt_pow_left h hn
 #align nat.pow_left_strict_mono Nat.pow_left_strictMono
 
diff --git a/Mathlib/Algebra/Polynomial/Basic.lean b/Mathlib/Algebra/Polynomial/Basic.lean
index 05a2446d2cf27..c6c33bae55741 100644
--- a/Mathlib/Algebra/Polynomial/Basic.lean
+++ b/Mathlib/Algebra/Polynomial/Basic.lean
@@ -299,7 +299,7 @@ instance semiring : Semiring R[X] :=
     toMul := Polynomial.mul'
     toZero := Polynomial.zero
     toOne := Polynomial.one
-    nsmul := (. • .)
+    nsmul := (· • ·)
     npow := fun n x => (x ^ n) }
 #align polynomial.semiring Polynomial.semiring
 
@@ -1190,7 +1190,7 @@ instance ring : Ring R[X] :=
     toIntCast := Polynomial.intCast
     toNeg := Polynomial.neg'
     toSub := Polynomial.sub
-    zsmul := ((. • .) : ℤ → R[X] → R[X]) }
+    zsmul := ((· • ·) : ℤ → R[X] → R[X]) }
 #align polynomial.ring Polynomial.ring
 
 @[simp]
diff --git a/Mathlib/Data/Fin/Tuple/Curry.lean b/Mathlib/Data/Fin/Tuple/Curry.lean
index e58ab105fd22d..1b752e325ecb5 100644
--- a/Mathlib/Data/Fin/Tuple/Curry.lean
+++ b/Mathlib/Data/Fin/Tuple/Curry.lean
@@ -73,7 +73,7 @@ variable {n : ℕ} {p : Fin n → Type u} {τ : Type u}
 theorem curry_uncurry (f : Function.FromTypes p τ) : curry (uncurry f) = f := by
   induction n with
   | zero => rfl
-  | succ n ih => exact funext (ih $ f .)
+  | succ n ih => exact funext (ih $ f ·)
 
 @[simp]
 theorem uncurry_curry (f : ((i : Fin n) → p i) → τ) :
diff --git a/Mathlib/Data/Pi/Lex.lean b/Mathlib/Data/Pi/Lex.lean
index f2b05078e2c7e..6f7239630b3d8 100644
--- a/Mathlib/Data/Pi/Lex.lean
+++ b/Mathlib/Data/Pi/Lex.lean
@@ -119,7 +119,7 @@ open Function
 
 theorem toLex_monotone : Monotone (@toLex (∀ i, β i)) := fun a b h =>
   or_iff_not_imp_left.2 fun hne =>
-    let ⟨i, hi, hl⟩ := IsWellFounded.wf.has_min (r := (· < · )) { i | a i ≠ b i }
+    let ⟨i, hi, hl⟩ := IsWellFounded.wf.has_min (r := (· < ·)) { i | a i ≠ b i }
       (Function.ne_iff.1 hne)
     ⟨i, fun j hj => by
       contrapose! hl
@@ -127,7 +127,7 @@ theorem toLex_monotone : Monotone (@toLex (∀ i, β i)) := fun a b h =>
 #align pi.to_lex_monotone Pi.toLex_monotone
 
 theorem toLex_strictMono : StrictMono (@toLex (∀ i, β i)) := fun a b h =>
-  let ⟨i, hi, hl⟩ := IsWellFounded.wf.has_min (r := (· < · )) { i | a i ≠ b i }
+  let ⟨i, hi, hl⟩ := IsWellFounded.wf.has_min (r := (· < ·)) { i | a i ≠ b i }
     (Function.ne_iff.1 h.ne)
   ⟨i, fun j hj => by
     contrapose! hl
diff --git a/Mathlib/Data/Set/Subset.lean b/Mathlib/Data/Set/Subset.lean
index 8f67365a303f0..f6aca09eb48ec 100644
--- a/Mathlib/Data/Set/Subset.lean
+++ b/Mathlib/Data/Set/Subset.lean
@@ -74,7 +74,7 @@ lemma preimage_val_sInter : A ↓∩ (⋂₀ S) = ⋂₀ { (A ↓∩ B) | B ∈
   erw [sInter_image]
   simp_rw [sInter_eq_biInter, preimage_iInter]
 
-lemma preimage_val_sInter_eq_sInter : A ↓∩ (⋂₀ S) = ⋂₀ ((A ↓∩ .) '' S) := by
+lemma preimage_val_sInter_eq_sInter : A ↓∩ (⋂₀ S) = ⋂₀ ((A ↓∩ ·) '' S) := by
   simp only [preimage_sInter, sInter_image]
 
 lemma eq_of_preimage_val_eq_of_subset (hB : B ⊆ A) (hC : C ⊆ A) (h : A ↓∩ B = A ↓∩ C) : B = C := by
diff --git a/Mathlib/GroupTheory/Exponent.lean b/Mathlib/GroupTheory/Exponent.lean
index f2f0578d553d5..0b7472fe9bc4a 100644
--- a/Mathlib/GroupTheory/Exponent.lean
+++ b/Mathlib/GroupTheory/Exponent.lean
@@ -93,7 +93,7 @@ open MulOpposite in
 theorem _root_.MulOpposite.exponent : exponent (MulOpposite G) = exponent G := by
   simp only [Monoid.exponent, ExponentExists]
   congr!
-  all_goals exact ⟨(op_injective <| · <| op ·), (unop_injective <| . <| unop .)⟩
+  all_goals exact ⟨(op_injective <| · <| op ·), (unop_injective <| · <| unop ·)⟩
 
 @[to_additive]
 theorem ExponentExists.isOfFinOrder (h : ExponentExists G) {g : G} : IsOfFinOrder g :=
diff --git a/Mathlib/GroupTheory/HNNExtension.lean b/Mathlib/GroupTheory/HNNExtension.lean
index a6c5fd4777f71..c4af9564ddb23 100644
--- a/Mathlib/GroupTheory/HNNExtension.lean
+++ b/Mathlib/GroupTheory/HNNExtension.lean
@@ -591,7 +591,7 @@ open NormalWord
 theorem of_injective : Function.Injective (of : G → HNNExtension G A B φ) := by
   rcases TransversalPair.nonempty G A B with ⟨d⟩
   refine Function.Injective.of_comp
-    (f := ((. • .) : HNNExtension G A B φ → NormalWord d → NormalWord d)) ?_
+    (f := ((· • ·) : HNNExtension G A B φ → NormalWord d → NormalWord d)) ?_
   intros _ _ h
   exact eq_of_smul_eq_smul (fun w : NormalWord d =>
     by simp_all [Function.funext_iff, of_smul_eq_smul])
diff --git a/Mathlib/GroupTheory/PushoutI.lean b/Mathlib/GroupTheory/PushoutI.lean
index 48e938f32da86..3019f3918016f 100644
--- a/Mathlib/GroupTheory/PushoutI.lean
+++ b/Mathlib/GroupTheory/PushoutI.lean
@@ -596,7 +596,7 @@ theorem of_injective (hφ : ∀ i, Function.Injective (φ i)) (i : ι) :
   let _ := Classical.decEq ι
   let _ := fun i => Classical.decEq (G i)
   refine Function.Injective.of_comp
-    (f := ((. • .) : PushoutI φ → NormalWord d → NormalWord d)) ?_
+    (f := ((· • ·) : PushoutI φ → NormalWord d → NormalWord d)) ?_
   intros _ _ h
   exact eq_of_smul_eq_smul (fun w : NormalWord d =>
     by simp_all [Function.funext_iff, of_smul_eq_smul])
@@ -607,7 +607,7 @@ theorem base_injective (hφ : ∀ i, Function.Injective (φ i)) :
   let _ := Classical.decEq ι
   let _ := fun i => Classical.decEq (G i)
   refine Function.Injective.of_comp
-    (f := ((. • .) : PushoutI φ → NormalWord d → NormalWord d)) ?_
+    (f := ((· • ·) : PushoutI φ → NormalWord d → NormalWord d)) ?_
   intros _ _ h
   exact eq_of_smul_eq_smul (fun w : NormalWord d =>
     by simp_all [Function.funext_iff, base_smul_eq_smul])
diff --git a/Mathlib/ModelTheory/Definability.lean b/Mathlib/ModelTheory/Definability.lean
index 38a310e9e21bc..1bec13723cfe3 100644
--- a/Mathlib/ModelTheory/Definability.lean
+++ b/Mathlib/ModelTheory/Definability.lean
@@ -60,7 +60,7 @@ theorem Definable.map_expansion {L' : FirstOrder.Language} [L'.Structure M] (h :
 theorem definable_iff_exists_formula_sum :
     A.Definable L s ↔ ∃ φ : L.Formula (A ⊕ α), s = {v | φ.Realize (Sum.elim (↑) v)} := by
   rw [Definable, Equiv.exists_congr_left (BoundedFormula.constantsVarsEquiv)]
-  refine exists_congr (fun φ => iff_iff_eq.2 (congr_arg (s = .) ?_))
+  refine exists_congr (fun φ => iff_iff_eq.2 (congr_arg (s = ·) ?_))
   ext
   simp only [Formula.Realize, BoundedFormula.constantsVarsEquiv, constantsOn, mk₂_Relations,
     BoundedFormula.mapTermRelEquiv_symm_apply, mem_setOf_eq]
diff --git a/Mathlib/ModelTheory/Syntax.lean b/Mathlib/ModelTheory/Syntax.lean
index 07ebed4538a4d..1e5964ee9e17d 100644
--- a/Mathlib/ModelTheory/Syntax.lean
+++ b/Mathlib/ModelTheory/Syntax.lean
@@ -667,11 +667,11 @@ def toFormula : ∀ {n : ℕ}, L.BoundedFormula α n → L.Formula (Sum α (Fin
 
 /-- take the disjunction of a finite set of formulas -/
 noncomputable def iSup (s : Finset β) (f : β → L.BoundedFormula α n) : L.BoundedFormula α n :=
-  (s.toList.map f).foldr (. ⊔ .) ⊥
+  (s.toList.map f).foldr (· ⊔ ·) ⊥
 
 /-- take the conjunction of a finite set of formulas -/
 noncomputable def iInf (s : Finset β) (f : β → L.BoundedFormula α n) : L.BoundedFormula α n :=
-  (s.toList.map f).foldr (. ⊓ .) ⊤
+  (s.toList.map f).foldr (· ⊓ ·) ⊤
 
 
 variable {l : ℕ} {φ ψ : L.BoundedFormula α l} {θ : L.BoundedFormula α l.succ}
diff --git a/Mathlib/Order/CompletePartialOrder.lean b/Mathlib/Order/CompletePartialOrder.lean
index 75339b3c8abad..6eb960bb57485 100644
--- a/Mathlib/Order/CompletePartialOrder.lean
+++ b/Mathlib/Order/CompletePartialOrder.lean
@@ -39,23 +39,23 @@ Complete partial orders are partial orders where every directed set has a least
 -/
 class CompletePartialOrder (α : Type*) extends PartialOrder α, SupSet α where
   /-- For each directed set `d`, `sSup d` is the least upper bound of `d`. -/
-  lubOfDirected : ∀ d, DirectedOn (. ≤ .) d → IsLUB d (sSup d)
+  lubOfDirected : ∀ d, DirectedOn (· ≤ ·) d → IsLUB d (sSup d)
 
 variable [CompletePartialOrder α] [Preorder β] {f : ι → α} {d : Set α} {a : α}
 
-protected lemma DirectedOn.isLUB_sSup : DirectedOn (. ≤ .) d → IsLUB d (sSup d) :=
+protected lemma DirectedOn.isLUB_sSup : DirectedOn (· ≤ ·) d → IsLUB d (sSup d) :=
 CompletePartialOrder.lubOfDirected _
 
-protected lemma DirectedOn.le_sSup (hd : DirectedOn (. ≤ .) d) (ha : a ∈ d) : a ≤ sSup d :=
+protected lemma DirectedOn.le_sSup (hd : DirectedOn (· ≤ ·) d) (ha : a ∈ d) : a ≤ sSup d :=
 hd.isLUB_sSup.1 ha
 
-protected lemma DirectedOn.sSup_le (hd : DirectedOn (. ≤ .) d) (ha : ∀ b ∈ d, b ≤ a) : sSup d ≤ a :=
+protected lemma DirectedOn.sSup_le (hd : DirectedOn (· ≤ ·) d) (ha : ∀ b ∈ d, b ≤ a) : sSup d ≤ a :=
 hd.isLUB_sSup.2 ha
 
-protected lemma Directed.le_iSup (hf : Directed (. ≤ .) f) (i : ι) : f i ≤ ⨆ j, f j :=
+protected lemma Directed.le_iSup (hf : Directed (· ≤ ·) f) (i : ι) : f i ≤ ⨆ j, f j :=
 hf.directedOn_range.le_sSup <| Set.mem_range_self _
 
-protected lemma Directed.iSup_le (hf : Directed (. ≤ .) f) (ha : ∀ i, f i ≤ a) :  ⨆ i, f i ≤ a :=
+protected lemma Directed.iSup_le (hf : Directed (· ≤ ·) f) (ha : ∀ i, f i ≤ a) :  ⨆ i, f i ≤ a :=
 hf.directedOn_range.sSup_le <| Set.forall_mem_range.2 ha
 
 --TODO: We could mimic more `sSup`/`iSup` lemmas
@@ -63,7 +63,7 @@ hf.directedOn_range.sSup_le <| Set.forall_mem_range.2 ha
 /-- Scott-continuity takes on a simpler form in complete partial orders. -/
 lemma CompletePartialOrder.scottContinuous {f : α → β} :
     ScottContinuous f ↔
-    ∀ ⦃d : Set α⦄, d.Nonempty → DirectedOn (. ≤ .) d → IsLUB (f '' d) (f (sSup d)) := by
+    ∀ ⦃d : Set α⦄, d.Nonempty → DirectedOn (· ≤ ·) d → IsLUB (f '' d) (f (sSup d)) := by
   refine' ⟨fun h d hd₁ hd₂ ↦ h hd₁ hd₂ hd₂.isLUB_sSup, fun h d hne hd a hda ↦ ?_⟩
   rw [hda.unique hd.isLUB_sSup]
   exact h hne hd
diff --git a/Mathlib/Order/RelSeries.lean b/Mathlib/Order/RelSeries.lean
index a9e3d2b09fa8e..894debf053298 100644
--- a/Mathlib/Order/RelSeries.lean
+++ b/Mathlib/Order/RelSeries.lean
@@ -256,7 +256,7 @@ For two types `α, β` and relation on them `r, s`, if `f : α → β` preserves
 def map (p : RelSeries r) (f : r →r s) : RelSeries s where
   length := p.length
   toFun := f.1.comp p
-  step := (f.2 <| p.step .)
+  step := (f.2 <| p.step ·)
 
 @[simp] lemma map_apply (p : RelSeries r) (f : r →r s) (i : Fin (p.length + 1)) :
     p.map f i = f (p i) := rfl
@@ -479,7 +479,7 @@ end RelSeries
 
 /-- A type is finite dimensional if its `LTSeries` has bounded length. -/
 abbrev FiniteDimensionalOrder (γ : Type*) [Preorder γ] :=
-  Rel.FiniteDimensional ((. < .) : γ → γ → Prop)
+  Rel.FiniteDimensional ((· < ·) : γ → γ → Prop)
 
 instance FiniteDimensionalOrder.ofUnique (γ : Type*) [Preorder γ] [Unique γ] :
     FiniteDimensionalOrder γ where
@@ -489,7 +489,7 @@ instance FiniteDimensionalOrder.ofUnique (γ : Type*) [Preorder γ] [Unique γ]
 
 /-- A type is infinite dimensional if it has `LTSeries` of at least arbitrary length -/
 abbrev InfiniteDimensionalOrder (γ : Type*) [Preorder γ] :=
-  Rel.InfiniteDimensional ((. < .) : γ → γ → Prop)
+  Rel.InfiniteDimensional ((· < ·) : γ → γ → Prop)
 
 section LTSeries
 
@@ -497,7 +497,7 @@ variable (α) [Preorder α] [Preorder β]
 /--
 If `α` is a preorder, a LTSeries is a relation series of the less than relation.
 -/
-abbrev LTSeries := RelSeries ((. < .) : Rel α α)
+abbrev LTSeries := RelSeries ((· < ·) : Rel α α)
 
 namespace LTSeries
 
diff --git a/Mathlib/SetTheory/Ordinal/Arithmetic.lean b/Mathlib/SetTheory/Ordinal/Arithmetic.lean
index 498cb3bb26225..27a56bc660431 100644
--- a/Mathlib/SetTheory/Ordinal/Arithmetic.lean
+++ b/Mathlib/SetTheory/Ordinal/Arithmetic.lean
@@ -2009,8 +2009,8 @@ def blsub₂ (o₁ o₂ : Ordinal) (op : {a : Ordinal} → (a < o₁) → {b : O
 theorem lt_blsub₂ {o₁ o₂ : Ordinal}
     (op : {a : Ordinal} → (a < o₁) → {b : Ordinal} → (b < o₂) → Ordinal) {a b : Ordinal}
     (ha : a < o₁) (hb : b < o₂) : op ha hb < blsub₂ o₁ o₂ op := by
-  convert lt_lsub _ (Prod.mk (enum (· < · ) a (by rwa [type_lt]))
-    (enum (· < · ) b (by rwa [type_lt])))
+  convert lt_lsub _ (Prod.mk (enum (· < ·) a (by rwa [type_lt]))
+    (enum (· < ·) b (by rwa [type_lt])))
   simp only [typein_enum]
 #align ordinal.lt_blsub₂ Ordinal.lt_blsub₂