[Merged by Bors] - chore: remove remaining cdots that were not ·

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
 

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]

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) → τ) :

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

Mathlib/Geometry/RingedSpace/PresheafedSpace/HasColimits.lean

@@ -394,7 +394,7 @@ def colimitPresheafObjIsoComponentwiseLimit (F : J ⥤ PresheafedSpace.{_, _, v}
     refine' (F.obj (unop X)).presheaf.mapIso (eqToIso _)
     simp only [Functor.op_obj, unop_op, op_inj_iff, Opens.map_coe, SetLike.ext'_iff,
       Set.preimage_preimage]
-    refine congr_arg (Set.preimage . U.1) (funext fun x => ?_)
+    refine congr_arg (Set.preimage · U.1) (funext fun x => ?_)
     erw [← TopCat.comp_app]
     congr
     exact ι_preservesColimitsIso_inv (forget C) F (unop X)

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 :=

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])

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])

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]

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}

Mathlib/Order/CompletePartialOrder.lean

@@ -39,31 +39,31 @@ 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
 
 /-- 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

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,15 +489,15 @@ 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
 
 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
 

Mathlib/RingTheory/Ideal/Over.lean

@@ -396,7 +396,7 @@ theorem exists_ideal_over_prime_of_isIntegral_of_isPrime
   refine' _root_.trans _ (_root_.trans (congr_arg (comap (Ideal.Quotient.mk
     (comap (algebraMap R S) I))) hQ') _)
   · rw [comap_comap]
-    exact congr_arg (comap . Q') (RingHom.ext fun r => rfl)
+    exact congr_arg (comap · Q') (RingHom.ext fun r => rfl)
   · refine' _root_.trans (comap_map_of_surjective _ Quotient.mk_surjective _) (sup_eq_left.2 _)
     simpa [← RingHom.ker_eq_comap_bot] using hIP