chore: use · instead of . (#6085)

Mathlib/Algebra/Category/GroupCat/Colimits.lean

@@ -268,7 +268,7 @@ def descMorphism (s : Cocone F) : colimit.{v} F ⟶ s.pt where
   toFun := descFun F s
   map_zero' := rfl
   -- Porting note : in `mathlib3`, nothing needs to be done after `induction`
-  map_add' x y := Quot.induction_on₂ x y fun _ _ => by dsimp [(. + .)]; rw [←quot_add F]; rfl
+  map_add' x y := Quot.induction_on₂ x y fun _ _ => by dsimp [(· + ·)]; rw [←quot_add F]; rfl
 #align AddCommGroup.colimits.desc_morphism AddCommGroupCat.Colimits.descMorphism
 
 /-- Evidence that the proposed colimit is the colimit. -/

Mathlib/Algebra/Category/Ring/Colimits.lean

@@ -169,11 +169,11 @@ instance ColimitType.AddGroup : AddGroup (ColimitType F) where
   zero_add x := Quot.inductionOn x fun _ => Quot.sound (Relation.zero_add _)
   add_zero x := Quot.inductionOn x fun _ => Quot.sound (Relation.add_zero _)
   add_left_neg := Quot.ind fun x => by
-    simp only [(. + .)]
+    simp only [(· + ·)]
     exact Quot.sound (Relation.add_left_neg x)
   add_assoc x y z := by
     refine Quot.induction_on₃ x y z (fun a b c => ?_)
-    simp only [(. + .)]
+    simp only [(· + ·)]
     apply Quot.sound
     apply Relation.add_assoc
 
@@ -188,18 +188,18 @@ instance : CommRing (ColimitType.{v} F) :=
     add_comm := fun x y => Quot.induction_on₂ x y fun x y => Quot.sound <| Relation.add_comm _ _
     mul_comm := fun x y => Quot.induction_on₂ x y fun x y => Quot.sound <| Relation.mul_comm _ _
     add_assoc := fun x y z => Quot.induction_on₃ x y z fun x y z => by
-      simp only [(. + .), Add.add]
+      simp only [(· + ·), Add.add]
       exact Quot.sound (Relation.add_assoc _ _ _)
     mul_assoc := fun x y z => Quot.induction_on₃ x y z fun x y z => by
-      simp only [(. * .)]
+      simp only [(· * ·)]
       exact Quot.sound (Relation.mul_assoc _ _ _)
     mul_zero := fun x => Quot.inductionOn x fun x => Quot.sound <| Relation.mul_zero _
     zero_mul := fun x => Quot.inductionOn x fun x => Quot.sound <| Relation.zero_mul _
     left_distrib := fun x y z => Quot.induction_on₃ x y z fun x y z => by
-      simp only [(. + .), (. * .), Add.add]
+      simp only [(· + ·), (· * ·), Add.add]
       exact Quot.sound (Relation.left_distrib _ _ _)
     right_distrib := fun x y z => Quot.induction_on₃ x y z fun x y z => by
-      simp only [(. + .), (. * .), Add.add]
+      simp only [(· + ·), (· * ·), Add.add]
       exact Quot.sound (Relation.right_distrib _ _ _) }
 
 @[simp]
@@ -332,7 +332,7 @@ def descMorphism (s : Cocone F) : colimit F ⟶ s.pt where
   map_zero' := rfl
   map_add' x y := by
     refine Quot.induction_on₂ x y fun a b => ?_
-    dsimp [descFun, (. + .)]
+    dsimp [descFun, (· + ·)]
     rw [←quot_add]
     rfl
   map_mul' x y := by exact Quot.induction_on₂ x y fun a b => rfl

Mathlib/Algebra/Category/Ring/Constructions.lean

@@ -160,7 +160,7 @@ instance commRingCat_hasStrictTerminalObjects : HasStrictTerminalObjects CommRin
   have e : (0 : X) = 1 := by
     rw [← f.map_one, ← f.map_zero]
     congr
-  replace e : 0 * x = 1 * x := congr_arg (. * x) e
+  replace e : 0 * x = 1 * x := congr_arg (· * x) e
   rw [one_mul, MulZeroClass.zero_mul, ← f.map_zero] at e
   exact e
 set_option linter.uppercaseLean3 false in

Mathlib/Algebra/Free.lean

@@ -272,10 +272,10 @@ instance : LawfulTraversable FreeMagma.{u} :=
         rw [traverse_mul, ih1, ih2, mul_map_seq]
     comp_traverse := fun f g x ↦
       FreeMagma.recOnPure x
-        (fun x ↦ by simp only [(. ∘ .), traverse_pure, traverse_pure', functor_norm])
+        (fun x ↦ by simp only [(· ∘ ·), traverse_pure, traverse_pure', functor_norm])
         (fun x y ih1 ih2 ↦ by
           rw [traverse_mul, ih1, ih2, traverse_mul];
-          simp [Functor.Comp.map_mk, Functor.map_map, (. ∘ .), Comp.seq_mk, seq_map_assoc,
+          simp [Functor.Comp.map_mk, Functor.map_map, (· ∘ ·), Comp.seq_mk, seq_map_assoc,
             map_seq, traverse_mul])
     naturality := fun η α β f x ↦
       FreeMagma.recOnPure x
@@ -687,7 +687,7 @@ instance : LawfulTraversable FreeSemigroup.{u} :=
       FreeSemigroup.recOnMul x (fun x ↦ rfl) fun x y ih1 ih2 ↦ by
         rw [traverse_mul, ih1, ih2, mul_map_seq]
     comp_traverse := fun f g x ↦
-      recOnPure x (fun x ↦ by simp only [traverse_pure, functor_norm, (. ∘ .)])
+      recOnPure x (fun x ↦ by simp only [traverse_pure, functor_norm, (· ∘ ·)])
         fun x y ih1 ih2 ↦ by (rw [traverse_mul, ih1, ih2,
           traverse_mul, Functor.Comp.map_mk]; simp only [Function.comp, functor_norm, traverse_mul])
     naturality := fun η α β f x ↦

Mathlib/Algebra/Order/Group/MinMax.lean

@@ -15,7 +15,7 @@ import Mathlib.Algebra.Order.Monoid.MinMax
 
 section
 
-variable {α : Type _} [Group α] [LinearOrder α] [CovariantClass α α (. * .) (. ≤ .)]
+variable {α : Type _} [Group α] [LinearOrder α] [CovariantClass α α (· * ·) (· ≤ ·)]
 
 @[to_additive (attr := simp)]
 theorem max_one_div_max_inv_one_eq_self (a : α) : max a 1 / max a⁻¹ 1 = a := by

Mathlib/AlgebraicGeometry/OpenImmersion/Basic.lean

@@ -220,7 +220,7 @@ theorem inv_invApp (U : Opens X) :
           -- See https://github.com/leanprover-community/mathlib4/issues/5026
           -- I think this is because `Set.preimage_image_eq _ H.base_open.inj` can't see through a
           -- structure
-          apply congr_arg (op .); ext
+          apply congr_arg (op ·); ext
           dsimp [openFunctor, IsOpenMap.functor]
           rw [Set.preimage_image_eq _ H.base_open.inj])) := by
   rw [← cancel_epi (H.invApp U), IsIso.hom_inv_id]
@@ -236,7 +236,7 @@ theorem invApp_app (U : Opens X) :
         -- See https://github.com/leanprover-community/mathlib4/issues/5026
         -- I think this is because `Set.preimage_image_eq _ H.base_open.inj` can't see through a
         -- structure
-        apply congr_arg (op .); ext
+        apply congr_arg (op ·); ext
         dsimp [openFunctor, IsOpenMap.functor]
         rw [Set.preimage_image_eq _ H.base_open.inj])) :=
   by rw [invApp, Category.assoc, IsIso.inv_hom_id, Category.comp_id]

Mathlib/AlgebraicGeometry/OpenImmersion/Scheme.lean

@@ -255,7 +255,7 @@ theorem affineBasisCover_map_range (X : Scheme) (x : X)
       (X.affineCover.map x).1.base '' (PrimeSpectrum.basicOpen r).1 := by
   erw [coe_comp, Set.range_comp]
   -- Porting note : `congr` fails to see the goal is comparing image of the same function
-  refine congr_arg (_ '' .) ?_
+  refine congr_arg (_ '' ·) ?_
   exact (PrimeSpectrum.localization_away_comap_range (Localization.Away r) r : _)
 #align algebraic_geometry.Scheme.affine_basis_cover_map_range AlgebraicGeometry.Scheme.affineBasisCover_map_range
 
@@ -1102,7 +1102,7 @@ def morphismRestrictRestrict {X Y : Scheme} (f : X ⟶ Y) (U : Opens Y) (V : Ope
   ext1
   dsimp
   rw [coe_comp, Set.range_comp]
-  apply congr_arg (U.inclusion '' .)
+  apply congr_arg (U.inclusion '' ·)
   exact Subtype.range_val
 #align algebraic_geometry.morphism_restrict_restrict AlgebraicGeometry.morphismRestrictRestrict
 

Mathlib/AlgebraicGeometry/PresheafedSpace/Gluing.lean

@@ -192,15 +192,15 @@ theorem snd_invApp_t_app' (i j k : D.J) (U : Opens (pullback (D.f i j) (D.f i k)
     congr
     have := (𝖣.t_fac k i j).symm
     rw [←IsIso.inv_comp_eq] at this
-    replace this := (congr_arg ((PresheafedSpace.Hom.base .)) this).symm
-    replace this := congr_arg (ContinuousMap.toFun .) this
+    replace this := (congr_arg ((PresheafedSpace.Hom.base ·)) this).symm
+    replace this := congr_arg (ContinuousMap.toFun ·) this
     dsimp at this
     rw [coe_comp, coe_comp] at this
     rw [this, Set.image_comp, Set.image_comp, Set.preimage_image_eq]
     swap
     · refine Function.HasLeftInverse.injective ⟨(D.t i k).base, fun x => ?_⟩
       rw [←comp_apply, ←comp_base, D.t_inv, id_base, id_apply]
-    refine congr_arg (_ '' .) ?_
+    refine congr_arg (_ '' ·) ?_
     refine congr_fun ?_ _
     refine Set.image_eq_preimage_of_inverse ?_ ?_
     · intro x
@@ -258,7 +258,7 @@ theorem ι_image_preimage_eq (i j : D.J) (U : Opens (D.U i).carrier) :
   · refine' Eq.trans (D.toTopGlueData.preimage_image_eq_image' _ _ _) _
     dsimp
     rw [coe_comp, Set.image_comp]
-    refine congr_arg (_ '' .) ?_
+    refine congr_arg (_ '' ·) ?_
     rw [Set.eq_preimage_iff_image_eq, ← Set.image_comp]
     swap
     · apply CategoryTheory.ConcreteCategory.bijective_of_isIso
@@ -315,7 +315,7 @@ theorem opensImagePreimageMap_app_assoc (i j k : D.J) (U : Opens (D.U i).carrier
         (π₂⁻¹ j, i, k) (unop _) ≫
           (D.V (j, k)).presheaf.map
             (eqToHom (opensImagePreimageMap_app' D i j k U).choose) ≫ f' := by
-  simpa only [Category.assoc] using congr_arg (. ≫ f') (opensImagePreimageMap_app D i j k U)
+  simpa only [Category.assoc] using congr_arg (· ≫ f') (opensImagePreimageMap_app D i j k U)
 #align algebraic_geometry.PresheafedSpace.glue_data.opens_image_preimage_map_app_assoc AlgebraicGeometry.PresheafedSpace.GlueData.opensImagePreimageMap_app_assoc
 
 /-- (Implementation) Given an open subset of one of the spaces `U ⊆ Uᵢ`, the sheaf component of
@@ -345,9 +345,9 @@ def ιInvAppπApp {i : D.J} (U : Opens (D.U i).carrier) (j) :
     rw [Set.preimage_preimage]
     change (D.f j k ≫ 𝖣.ι j).base ⁻¹' _ = _
     -- Porting note : used to be `congr 3`
-    refine congr_arg (. ⁻¹' _) ?_
-    convert congr_arg (ContinuousMap.toFun (α := D.V ⟨j, k⟩) (β := D.glued) .) ?_
-    refine congr_arg (PresheafedSpace.Hom.base (C := C) .) ?_
+    refine congr_arg (· ⁻¹' _) ?_
+    convert congr_arg (ContinuousMap.toFun (α := D.V ⟨j, k⟩) (β := D.glued) ·) ?_
+    refine congr_arg (PresheafedSpace.Hom.base (C := C) ·) ?_
     exact colimit.w 𝖣.diagram.multispan (WalkingMultispan.Hom.fst (j, k))
   · exact D.opensImagePreimageMap i j U
 #align algebraic_geometry.PresheafedSpace.glue_data.ι_inv_app_π_app AlgebraicGeometry.PresheafedSpace.GlueData.ιInvAppπApp
@@ -406,7 +406,7 @@ def ιInvApp {i : D.J} (U : Opens (D.U i).carrier) :
               IsOpenImmersion.inv_naturality_assoc, IsOpenImmersion.app_invApp_assoc]
             repeat' erw [← (D.V (j, k)).presheaf.map_comp]
             -- Porting note : was just `congr`
-            exact congr_arg ((D.V (j, k)).presheaf.map .) rfl } }
+            exact congr_arg ((D.V (j, k)).presheaf.map ·) rfl } }
 #align algebraic_geometry.PresheafedSpace.glue_data.ι_inv_app AlgebraicGeometry.PresheafedSpace.GlueData.ιInvApp
 
 /-- `ιInvApp` is the left inverse of `D.ι i` on `U`. -/

Mathlib/AlgebraicGeometry/PrimeSpectrum/Basic.lean

@@ -655,7 +655,7 @@ theorem localization_comap_inducing [Algebra R S] (M : Submonoid R) [IsLocalizat
     refine ⟨_, ⟨algebraMap R S ⁻¹' Ideal.span s, rfl⟩, ?_⟩
     rw [preimage_comap_zeroLocus, ← zeroLocus_span, ← zeroLocus_span s]
     congr 2
-    exact congr_arg (zeroLocus .) <| Submodule.carrier_inj.mpr
+    exact congr_arg (zeroLocus ·) <| Submodule.carrier_inj.mpr
       (IsLocalization.map_comap M S (Ideal.span s))
   · rintro ⟨_, ⟨t, rfl⟩, rfl⟩
     rw [preimage_comap_zeroLocus]

Mathlib/Combinatorics/SetFamily/LYM.lean

@@ -63,7 +63,7 @@ variable [DecidableEq α] [Fintype α]
 (the finsets of card `r`) than `∂𝒜` takes up of `α^(r - 1)`. -/
 theorem card_mul_le_card_shadow_mul (h𝒜 : (𝒜 : Set (Finset α)).Sized r) :
     𝒜.card * r ≤ (∂ 𝒜).card * (Fintype.card α - r + 1) := by
-  let i : DecidableRel ((. ⊆ .) : Finset α → Finset α → Prop) := fun _ _ => Classical.dec _
+  let i : DecidableRel ((· ⊆ ·) : Finset α → Finset α → Prop) := fun _ _ => Classical.dec _
   refine' card_mul_le_card_mul' (· ⊆ ·) (fun s hs => _) (fun s hs => _)
   · rw [← h𝒜 hs, ← card_image_of_injOn s.erase_injOn]
     refine' card_le_of_subset _

Mathlib/Data/ByteArray.lean

@@ -12,7 +12,7 @@ def Up (ub a i : ℕ) := i < a ∧ i < ub
 lemma Up.next {ub i} (h : i < ub) : Up ub (i+1) i := ⟨Nat.lt_succ_self _, h⟩
 
 lemma Up.WF (ub) : WellFounded (Up ub) :=
-  Subrelation.wf (h₂ := (measure (ub - .)).wf) fun ⟨ia, iu⟩ ↦ Nat.sub_lt_sub_left iu ia
+  Subrelation.wf (h₂ := (measure (ub - ·)).wf) fun ⟨ia, iu⟩ ↦ Nat.sub_lt_sub_left iu ia
 
 /-- A well-ordered relation for "upwards" induction on the natural numbers up to some bound `ub`. -/
 def upRel (ub : ℕ) : WellFoundedRelation Nat := ⟨Up ub, Up.WF ub⟩

Mathlib/Data/Fin/Basic.lean

@@ -1169,7 +1169,7 @@ theorem castLT_castAdd (m : ℕ) (i : Fin n) : castLT (castAdd m i) (castAdd_lt
 
 /-- For rewriting in the reverse direction, see `Fin.castIso_castAdd_left`. -/
 theorem castAdd_castIso {n n' : ℕ} (m : ℕ) (i : Fin n') (h : n' = n) :
-    castAdd m (Fin.castIso h i) = Fin.castIso (congr_arg (. + m) h) (castAdd m i) :=
+    castAdd m (Fin.castIso h i) = Fin.castIso (congr_arg (· + m) h) (castAdd m i) :=
   ext rfl
 #align fin.cast_add_cast Fin.castAdd_castIso
 
@@ -1389,7 +1389,7 @@ theorem castIso_addNat_zero {n n' : ℕ} (i : Fin n) (h : n + 0 = n') :
 
 /-- For rewriting in the reverse direction, see `Fin.castIso_addNat_left`. -/
 theorem addNat_castIso {n n' m : ℕ} (i : Fin n') (h : n' = n) :
-    addNat (castIso h i) m = castIso (congr_arg (. + m) h) (addNat i m) :=
+    addNat (castIso h i) m = castIso (congr_arg (· + m) h) (addNat i m) :=
   ext rfl
 #align fin.add_nat_cast Fin.addNat_castIso
 

Mathlib/Data/List/BigOperators/Basic.lean

@@ -99,7 +99,7 @@ theorem prod_hom_rel (l : List ι) {r : M → N → Prop} {f : ι → M} {g : ι
 theorem prod_hom (l : List M) {F : Type _} [MonoidHomClass F M N] (f : F) :
     (l.map f).prod = f l.prod := by
   simp only [prod, foldl_map, ← map_one f]
-  exact l.foldl_hom f (. * .) (. * f .) 1 (fun x y => (map_mul f x y).symm)
+  exact l.foldl_hom f (· * ·) (· * f ·) 1 (fun x y => (map_mul f x y).symm)
 #align list.prod_hom List.prod_hom
 #align list.sum_hom List.sum_hom
 

Mathlib/Data/List/Forall2.lean

@@ -245,7 +245,7 @@ theorem rel_map : ((R ⇒ P) ⇒ Forall₂ R ⇒ Forall₂ P) map map
   | _, _, h, _ :: _, _ :: _, Forall₂.cons h₁ h₂ => Forall₂.cons (h h₁) (rel_map (@h) h₂)
 #align list.rel_map List.rel_map
 
-theorem rel_append : (Forall₂ R ⇒ Forall₂ R ⇒ Forall₂ R) (. ++ .) (. ++ .)
+theorem rel_append : (Forall₂ R ⇒ Forall₂ R ⇒ Forall₂ R) (· ++ ·) (· ++ ·)
   | [], [], _, _, _, hl => hl
   | _, _, Forall₂.cons h₁ h₂, _, _, hl => Forall₂.cons h₁ (rel_append h₂ hl)
 #align list.rel_append List.rel_append

Mathlib/Data/List/Nodup.lean

@@ -448,7 +448,7 @@ theorem Nodup.pairwise_coe [IsSymm α r] (hl : l.Nodup)
 
 --Porting note: new theorem
 theorem Nodup.take_eq_filter_mem [DecidableEq α] :
-    ∀ {l : List α} {n : ℕ} (_ : l.Nodup), l.take n = l.filter (. ∈ l.take n)
+    ∀ {l : List α} {n : ℕ} (_ : l.Nodup), l.take n = l.filter (· ∈ l.take n)
   | [], n, _ => by simp
   | b::l, 0, _ => by simp
   | b::l, n+1, hl => by

Mathlib/Data/List/Perm.lean

@@ -1155,7 +1155,7 @@ theorem Perm.erasep (f : α → Prop) [DecidablePred f] {l₁ l₂ : List α}
 theorem Perm.take_inter {α : Type _} [DecidableEq α] {xs ys : List α} (n : ℕ) (h : xs ~ ys)
     (h' : ys.Nodup) : xs.take n ~ ys.inter (xs.take n) := by
   simp only [List.inter]
-  exact Perm.trans (show xs.take n ~ xs.filter (. ∈ xs.take n) by
+  exact Perm.trans (show xs.take n ~ xs.filter (· ∈ xs.take n) by
       conv_lhs => rw [Nodup.take_eq_filter_mem ((Perm.nodup_iff h).2 h')])
     (Perm.filter _ h)
 #align list.perm.take_inter List.Perm.take_inter

Mathlib/Data/List/Permutation.lean

@@ -141,12 +141,12 @@ theorem permutations'Aux_eq_permutationsAux2 (t : α) (ts : List α) :
 #align list.permutations'_aux_eq_permutations_aux2 List.permutations'Aux_eq_permutationsAux2
 
 theorem mem_permutationsAux2 {t : α} {ts : List α} {ys : List α} {l l' : List α} :
-    l' ∈ (permutationsAux2 t ts [] ys (l ++ .)).2 ↔
+    l' ∈ (permutationsAux2 t ts [] ys (l ++ ·)).2 ↔
       ∃ l₁ l₂, l₂ ≠ [] ∧ ys = l₁ ++ l₂ ∧ l' = l ++ l₁ ++ t :: l₂ ++ ts := by
   induction' ys with y ys ih generalizing l
   · simp (config := { contextual := true })
   rw [permutationsAux2_snd_cons,
-    show (fun x : List α => l ++ y :: x) = (l ++ [y] ++ .) by funext _; simp, mem_cons, ih]
+    show (fun x : List α => l ++ y :: x) = (l ++ [y] ++ ·) by funext _; simp, mem_cons, ih]
   constructor
   · rintro (rfl | ⟨l₁, l₂, l0, rfl, rfl⟩)
     · exact ⟨[], y :: ys, by simp⟩
@@ -161,7 +161,7 @@ theorem mem_permutationsAux2 {t : α} {ts : List α} {ys : List α} {l l' : List
 theorem mem_permutationsAux2' {t : α} {ts : List α} {ys : List α} {l : List α} :
     l ∈ (permutationsAux2 t ts [] ys id).2 ↔
       ∃ l₁ l₂, l₂ ≠ [] ∧ ys = l₁ ++ l₂ ∧ l = l₁ ++ t :: l₂ ++ ts :=
-  by rw [show @id (List α) = ([] ++ .) by funext _; rfl]; apply mem_permutationsAux2
+  by rw [show @id (List α) = ([] ++ ·) by funext _; rfl]; apply mem_permutationsAux2
 #align list.mem_permutations_aux2' List.mem_permutationsAux2'
 
 theorem length_permutationsAux2 (t : α) (ts : List α) (ys : List α) (f : List α → β) :

Mathlib/Data/List/Sublists.lean

@@ -154,7 +154,7 @@ theorem sublists_eq_sublistsAux (l : List α) :
 #noalign list.sublists_aux_cons_append
 
 theorem sublists_append (l₁ l₂ : List α) :
-    sublists (l₁ ++ l₂) = (sublists l₂) >>= (fun x => (sublists l₁).map (. ++ x)) := by
+    sublists (l₁ ++ l₂) = (sublists l₂) >>= (fun x => (sublists l₁).map (· ++ x)) := by
   simp only [sublists_eq_sublistsAux, foldr_append, sublistsAux_eq_bind]
   induction l₁
   · case nil => simp
@@ -389,7 +389,7 @@ alias nodup_sublists' ↔ nodup.of_sublists' nodup.sublists'
 --attribute [protected] nodup.sublists nodup.sublists'
 
 theorem nodup_sublistsLen (n : ℕ) {l : List α} (h : Nodup l) : (sublistsLen n l).Nodup := by
-  have : Pairwise (. ≠ .) l.sublists' := Pairwise.imp
+  have : Pairwise (· ≠ ·) l.sublists' := Pairwise.imp
     (fun h => Lex.to_ne (by convert h using 3; simp [swap, eq_comm])) h.sublists'
   exact this.sublist (sublistsLen_sublist_sublists' _ _)
 #align list.nodup_sublists_len List.nodup_sublistsLen

Mathlib/Data/Multiset/Range.lean

@@ -59,19 +59,19 @@ theorem self_mem_range_succ (n : ℕ) : n ∈ range (n + 1) :=
   List.self_mem_range_succ n
 #align multiset.self_mem_range_succ Multiset.self_mem_range_succ
 
-theorem range_add (a b : ℕ) : range (a + b) = range a + (range b).map (a + .) :=
+theorem range_add (a b : ℕ) : range (a + b) = range a + (range b).map (a + ·) :=
   congr_arg ((↑) : List ℕ → Multiset ℕ) (List.range_add _ _)
 #align multiset.range_add Multiset.range_add
 
 theorem range_disjoint_map_add (a : ℕ) (m : Multiset ℕ) :
-    (range a).Disjoint (m.map (a + .)) := by
+    (range a).Disjoint (m.map (a + ·)) := by
   intro x hxa hxb
   rw [range, mem_coe, List.mem_range] at hxa
   obtain ⟨c, _, rfl⟩ := mem_map.1 hxb
   exact (self_le_add_right _ _).not_lt hxa
 #align multiset.range_disjoint_map_add Multiset.range_disjoint_map_add
 
-theorem range_add_eq_union (a b : ℕ) : range (a + b) = range a ∪ (range b).map (a + .) := by
+theorem range_add_eq_union (a b : ℕ) : range (a + b) = range a ∪ (range b).map (a + ·) := by
   rw [range_add, add_eq_union_iff_disjoint]
   apply range_disjoint_map_add
 #align multiset.range_add_eq_union Multiset.range_add_eq_union