chore: Replace (· op ·) a by (a op ·) (#8843)

I used the regex `\(\(· (.) ·\) (.)\)`, replacing with `($2 $1 ·)`.

Counterexamples/HomogeneousPrimeNotPrime.lean

@@ -65,7 +65,7 @@ def submoduleZ : Submodule R (R × R) where
   carrier := {zz | zz.1 = zz.2}
   zero_mem' := rfl
   add_mem' := @fun _ _ ha hb => congr_arg₂ (· + ·) ha hb
-  smul_mem' a _ hb := congr_arg ((· * ·) a) hb
+  smul_mem' a _ hb := congr_arg (a * ·) hb
 #align counterexample.counterexample_not_prime_but_homogeneous_prime.submodule_z Counterexample.CounterexampleNotPrimeButHomogeneousPrime.submoduleZ
 
 /-- The grade 1 part of `R²` is `{(0, b) | b ∈ R}`. -/

Mathlib/Algebra/AddTorsor.lean

@@ -379,15 +379,13 @@ theorem coe_vaddConst_symm (p : P) : ⇑(vaddConst p).symm = fun p' => p' -ᵥ p
 
 /-- `p' ↦ p -ᵥ p'` as an equivalence. -/
 def constVSub (p : P) : P ≃ G where
-  toFun := (· -ᵥ ·) p
-  invFun v := -v +ᵥ p
+  toFun := (p -ᵥ ·)
+  invFun := (-· +ᵥ p)
   left_inv p' := by simp
   right_inv v := by simp [vsub_vadd_eq_vsub_sub]
 #align equiv.const_vsub Equiv.constVSub
 
-@[simp]
-theorem coe_constVSub (p : P) : ⇑(constVSub p) = (· -ᵥ ·) p :=
-  rfl
+@[simp] lemma coe_constVSub (p : P) : ⇑(constVSub p) = (p -ᵥ ·) := rfl
 #align equiv.coe_const_vsub Equiv.coe_constVSub
 
 @[simp]
@@ -399,15 +397,13 @@ variable (P)
 
 /-- The permutation given by `p ↦ v +ᵥ p`. -/
 def constVAdd (v : G) : Equiv.Perm P where
-  toFun := (· +ᵥ ·) v
-  invFun := (· +ᵥ ·) (-v)
+  toFun := (v +ᵥ ·)
+  invFun := (-v +ᵥ ·)
   left_inv p := by simp [vadd_vadd]
   right_inv p := by simp [vadd_vadd]
 #align equiv.const_vadd Equiv.constVAdd
 
-@[simp]
-theorem coe_constVAdd (v : G) : ⇑(constVAdd P v) = (· +ᵥ ·) v :=
-  rfl
+@[simp] lemma coe_constVAdd (v : G) : ⇑(constVAdd P v) = (v +ᵥ ·) := rfl
 #align equiv.coe_const_vadd Equiv.coe_constVAdd
 
 variable (G)

Mathlib/Algebra/Algebra/Spectrum.lean

@@ -290,9 +290,7 @@ theorem subset_starSubalgebra [StarRing R] [StarRing A] [StarModule R A] {S : St
 
 theorem singleton_add_eq (a : A) (r : R) : {r} + σ a = σ (↑ₐ r + a) :=
   ext fun x => by
-    rw [singleton_add, image_add_left, mem_preimage]
-    simp only
-    rw [add_comm, add_mem_iff, map_neg, neg_neg]
+    rw [singleton_add, image_add_left, mem_preimage, add_comm, add_mem_iff, map_neg, neg_neg]
 #align spectrum.singleton_add_eq spectrum.singleton_add_eq
 
 theorem add_singleton_eq (a : A) (r : R) : σ a + {r} = σ (a + ↑ₐ r) :=

Mathlib/Algebra/Algebra/Tower.lean

@@ -73,7 +73,7 @@ def lsmul : A →ₐ[R] Module.End B M where
 #align algebra.lsmul Algebra.lsmulₓ
 
 @[simp]
-theorem lsmul_coe (a : A) : (lsmul R B M a : M → M) = (· • ·) a := rfl
+theorem lsmul_coe (a : A) : (lsmul R B M a : M → M) = (a • ·) := rfl
 #align algebra.lsmul_coe Algebra.lsmul_coe
 
 end Algebra

Mathlib/Algebra/BigOperators/Order.lean

@@ -323,7 +323,7 @@ variable [DecidableEq α] {s : Finset α} {B : Finset (Finset α)} {n : ℕ}
 
 /-- If every element belongs to at most `n` Finsets, then the sum of their sizes is at most `n`
 times how many they are. -/
-theorem sum_card_inter_le (h : ∀ a ∈ s, (B.filter <| (· ∈ ·) a).card ≤ n) :
+theorem sum_card_inter_le (h : ∀ a ∈ s, (B.filter (a ∈ ·)).card ≤ n) :
     (∑ t in B, (s ∩ t).card) ≤ s.card * n := by
   refine' le_trans _ (s.sum_le_card_nsmul _ _ h)
   simp_rw [← filter_mem_eq_inter, card_eq_sum_ones, sum_filter]
@@ -332,7 +332,7 @@ theorem sum_card_inter_le (h : ∀ a ∈ s, (B.filter <| (· ∈ ·) a).card ≤
 
 /-- If every element belongs to at most `n` Finsets, then the sum of their sizes is at most `n`
 times how many they are. -/
-theorem sum_card_le [Fintype α] (h : ∀ a, (B.filter <| (· ∈ ·) a).card ≤ n) :
+theorem sum_card_le [Fintype α] (h : ∀ a, (B.filter (a ∈ ·)).card ≤ n) :
     ∑ s in B, s.card ≤ Fintype.card α * n :=
   calc
     ∑ s in B, s.card = ∑ s in B, (univ ∩ s).card := by simp_rw [univ_inter]
@@ -341,7 +341,7 @@ theorem sum_card_le [Fintype α] (h : ∀ a, (B.filter <| (· ∈ ·) a).card 
 
 /-- If every element belongs to at least `n` Finsets, then the sum of their sizes is at least `n`
 times how many they are. -/
-theorem le_sum_card_inter (h : ∀ a ∈ s, n ≤ (B.filter <| (· ∈ ·) a).card) :
+theorem le_sum_card_inter (h : ∀ a ∈ s, n ≤ (B.filter (a ∈ ·)).card) :
     s.card * n ≤ ∑ t in B, (s ∩ t).card := by
   apply (s.card_nsmul_le_sum _ _ h).trans
   simp_rw [← filter_mem_eq_inter, card_eq_sum_ones, sum_filter]
@@ -350,7 +350,7 @@ theorem le_sum_card_inter (h : ∀ a ∈ s, n ≤ (B.filter <| (· ∈ ·) a).ca
 
 /-- If every element belongs to at least `n` Finsets, then the sum of their sizes is at least `n`
 times how many they are. -/
-theorem le_sum_card [Fintype α] (h : ∀ a, n ≤ (B.filter <| (· ∈ ·) a).card) :
+theorem le_sum_card [Fintype α] (h : ∀ a, n ≤ (B.filter (a ∈ ·)).card) :
     Fintype.card α * n ≤ ∑ s in B, s.card :=
   calc
     Fintype.card α * n ≤ ∑ s in B, (univ ∩ s).card := le_sum_card_inter fun a _ ↦ h a
@@ -359,14 +359,14 @@ theorem le_sum_card [Fintype α] (h : ∀ a, n ≤ (B.filter <| (· ∈ ·) a).c
 
 /-- If every element belongs to exactly `n` Finsets, then the sum of their sizes is `n` times how
 many they are. -/
-theorem sum_card_inter (h : ∀ a ∈ s, (B.filter <| (· ∈ ·) a).card = n) :
+theorem sum_card_inter (h : ∀ a ∈ s, (B.filter (a ∈ ·)).card = n) :
     (∑ t in B, (s ∩ t).card) = s.card * n :=
   (sum_card_inter_le fun a ha ↦ (h a ha).le).antisymm (le_sum_card_inter fun a ha ↦ (h a ha).ge)
 #align finset.sum_card_inter Finset.sum_card_inter
 
 /-- If every element belongs to exactly `n` Finsets, then the sum of their sizes is `n` times how
 many they are. -/
-theorem sum_card [Fintype α] (h : ∀ a, (B.filter <| (· ∈ ·) a).card = n) :
+theorem sum_card [Fintype α] (h : ∀ a, (B.filter (a ∈ ·)).card = n) :
     ∑ s in B, s.card = Fintype.card α * n := by
   simp_rw [Fintype.card, ← sum_card_inter fun a _ ↦ h a, univ_inter]
 #align finset.sum_card Finset.sum_card

Mathlib/Algebra/ContinuedFractions/Computation/Translations.lean

@@ -345,7 +345,7 @@ theorem convergents'_succ :
     rw [convergents'_of_int, fract_intCast, inv_zero, ← cast_zero, convergents'_of_int, cast_zero,
       div_zero, add_zero, floor_intCast]
   · rw [convergents', of_h_eq_floor, add_right_inj, convergents'Aux_succ_some (of_s_head h)]
-    exact congr_arg ((· / ·) 1) (by rw [convergents', of_h_eq_floor, add_right_inj, of_s_tail])
+    exact congr_arg (1 / ·) (by rw [convergents', of_h_eq_floor, add_right_inj, of_s_tail])
 #align generalized_continued_fraction.convergents'_succ GeneralizedContinuedFraction.convergents'_succ
 
 end Values

Mathlib/Algebra/GCDMonoid/Multiset.lean

@@ -182,7 +182,7 @@ theorem gcd_eq_zero_iff (s : Multiset α) : s.gcd = 0 ↔ ∀ x : α, x ∈ s 
     simp [h a (mem_cons_self a s), sgcd fun x hx ↦ h x (mem_cons_of_mem hx)]
 #align multiset.gcd_eq_zero_iff Multiset.gcd_eq_zero_iff
 
-theorem gcd_map_mul (a : α) (s : Multiset α) : (s.map ((· * ·) a)).gcd = normalize a * s.gcd := by
+theorem gcd_map_mul (a : α) (s : Multiset α) : (s.map (a * ·)).gcd = normalize a * s.gcd := by
   refine' s.induction_on _ fun b s ih ↦ _
   · simp_rw [map_zero, gcd_zero, mul_zero]
   · simp_rw [map_cons, gcd_cons, ← gcd_mul_left]
@@ -224,7 +224,7 @@ theorem gcd_ndinsert (a : α) (s : Multiset α) : (ndinsert a s).gcd = GCDMonoid
 end
 
 theorem extract_gcd' (s t : Multiset α) (hs : ∃ x, x ∈ s ∧ x ≠ (0 : α))
-    (ht : s = t.map ((· * ·) s.gcd)) : t.gcd = 1 :=
+    (ht : s = t.map (s.gcd * ·)) : t.gcd = 1 :=
   ((@mul_right_eq_self₀ _ _ s.gcd _).1 <| by
         conv_lhs => rw [← normalize_gcd, ← gcd_map_mul, ← ht]).resolve_right <| by
     contrapose! hs
@@ -238,23 +238,20 @@ using the originals. -/
 `have := _, refine ⟨s.pmap @f (λ _, id), this, extract_gcd' s _ h this⟩,`
 so I rearranged the proof slightly. -/
 theorem extract_gcd (s : Multiset α) (hs : s ≠ 0) :
-    ∃ t : Multiset α, s = t.map ((· * ·) s.gcd) ∧ t.gcd = 1 := by
+    ∃ t : Multiset α, s = t.map (s.gcd * ·) ∧ t.gcd = 1 := by
   classical
     by_cases h : ∀ x ∈ s, x = (0 : α)
     · use replicate (card s) 1
-      simp only
       rw [map_replicate, eq_replicate, mul_one, s.gcd_eq_zero_iff.2 h, ← nsmul_singleton,
     ← gcd_dedup, dedup_nsmul (card_pos.2 hs).ne', dedup_singleton, gcd_singleton]
       exact ⟨⟨rfl, h⟩, normalize_one⟩
     · choose f hf using @gcd_dvd _ _ _ s
       push_neg at h
-      refine' ⟨s.pmap @f fun _ ↦ id, _, extract_gcd' s _ h _⟩ <;>
+      refine ⟨s.pmap @f fun _ ↦ id, ?_, extract_gcd' s _ h ?_⟩ <;>
       · rw [map_pmap]
         conv_lhs => rw [← s.map_id, ← s.pmap_eq_map _ _ fun _ ↦ id]
         congr with (x hx)
-        simp only
-        rw [id]
-        rw [← hf hx]
+        rw [id, ← hf hx]
 #align multiset.extract_gcd Multiset.extract_gcd
 
 end gcd

Mathlib/Algebra/Group/Basic.lean

@@ -75,7 +75,7 @@ theorem eq_one_iff_eq_one_of_mul_eq_one {a b : M} (h : a * b = 1) : a = 1 ↔ b
 #align eq_zero_iff_eq_zero_of_add_eq_zero eq_zero_iff_eq_zero_of_add_eq_zero
 
 @[to_additive]
-theorem one_mul_eq_id : (· * ·) (1 : M) = id :=
+theorem one_mul_eq_id : ((1 : M) * ·) = id :=
   funext one_mul
 #align one_mul_eq_id one_mul_eq_id
 #align zero_add_eq_id zero_add_eq_id
@@ -600,7 +600,7 @@ theorem div_eq_inv_self : a / b = b⁻¹ ↔ a = 1 := by rw [div_eq_mul_inv, mul
 #align sub_eq_neg_self sub_eq_neg_self
 
 @[to_additive]
-theorem mul_left_surjective (a : G) : Function.Surjective ((· * ·) a) :=
+theorem mul_left_surjective (a : G) : Surjective (a * ·) :=
   fun x ↦ ⟨a⁻¹ * x, mul_inv_cancel_left a x⟩
 #align mul_left_surjective mul_left_surjective
 #align add_left_surjective add_left_surjective

Mathlib/Algebra/Group/Defs.lean

@@ -222,7 +222,7 @@ theorem mul_left_cancel_iff : a * b = a * c ↔ b = c :=
 #align add_left_cancel_iff add_left_cancel_iff
 
 @[to_additive]
-theorem mul_right_injective (a : G) : Function.Injective ((· * ·) a) := fun _ _ ↦ mul_left_cancel
+theorem mul_right_injective (a : G) : Injective (a * ·) := fun _ _ ↦ mul_left_cancel
 #align mul_right_injective mul_right_injective
 #align add_right_injective add_right_injective
 
@@ -989,7 +989,7 @@ theorem zpow_ofNat (a : G) : ∀ n : ℕ, a ^ (n : ℤ) = a ^ n
   | 0 => (zpow_zero _).trans (pow_zero _).symm
   | n + 1 => calc
     a ^ (↑(n + 1) : ℤ) = a * a ^ (n : ℤ) := DivInvMonoid.zpow_succ' _ _
-    _ = a * a ^ n := congr_arg ((· * ·) a) (zpow_ofNat a n)
+    _ = a * a ^ n := congr_arg (a * ·) (zpow_ofNat a n)
     _ = a ^ (n + 1) := (pow_succ _ _).symm
 #align zpow_coe_nat zpow_ofNat
 #align zpow_of_nat zpow_ofNat

Mathlib/Algebra/Group/Units.lean

@@ -785,7 +785,7 @@ protected theorem mul_right_cancel (h : IsUnit b) : a * b = c * b → a = c :=
 #align is_add_unit.add_right_cancel IsAddUnit.add_right_cancel
 
 @[to_additive]
-protected theorem mul_right_injective (h : IsUnit a) : Injective ((· * ·) a) :=
+protected theorem mul_right_injective (h : IsUnit a) : Injective (a * ·) :=
   fun _ _ => h.mul_left_cancel
 #align is_unit.mul_right_injective IsUnit.mul_right_injective
 #align is_add_unit.add_right_injective IsAddUnit.add_right_injective

Mathlib/Algebra/Group/Units/Equiv.lean

@@ -120,7 +120,7 @@ protected def mulLeft (a : G) : Perm G :=
 #align equiv.add_left Equiv.addLeft
 
 @[to_additive (attr := simp)]
-theorem coe_mulLeft (a : G) : ⇑(Equiv.mulLeft a) = (· * ·) a :=
+theorem coe_mulLeft (a : G) : ⇑(Equiv.mulLeft a) = (a * ·) :=
   rfl
 #align equiv.coe_mul_left Equiv.coe_mulLeft
 #align equiv.coe_add_left Equiv.coe_addLeft

Mathlib/Algebra/GroupPower/CovariantClass.lean

@@ -99,7 +99,7 @@ theorem pow_lt_pow' [CovariantClass M M (· * ·) (· < ·)] {a : M} {n m : ℕ}
 
 @[to_additive nsmul_strictMono_right]
 theorem pow_strictMono_left [CovariantClass M M (· * ·) (· < ·)] {a : M} (ha : 1 < a) :
-    StrictMono ((· ^ ·) a : ℕ → M) := fun _ _ => pow_lt_pow' ha
+    StrictMono ((a ^ ·) : ℕ → M) := fun _ _ => pow_lt_pow' ha
 #align pow_strict_mono_left pow_strictMono_left
 #align nsmul_strict_mono_right nsmul_strictMono_right
 

Mathlib/Algebra/GroupPower/Lemmas.lean

@@ -791,8 +791,8 @@ alias le_self_pow_two := le_self_sq
 #align int.le_self_pow_two Int.le_self_pow_two
 
 theorem pow_right_injective {x : ℤ} (h : 1 < x.natAbs) :
-    Function.Injective ((· ^ ·) x : ℕ → ℤ) := by
-  suffices Function.Injective (natAbs ∘ ((· ^ ·) x : ℕ → ℤ)) by
+    Function.Injective ((x ^ ·) : ℕ → ℤ) := by
+  suffices Function.Injective (natAbs ∘ (x ^ · : ℕ → ℤ)) by
     exact Function.Injective.of_comp this
   convert Nat.pow_right_injective h using 2
   rw [Function.comp_apply, natAbs_pow]

Mathlib/Algebra/GroupWithZero/Basic.lean

@@ -65,7 +65,7 @@ theorem mul_eq_zero_of_ne_zero_imp_eq_zero {a b : M₀} (h : a ≠ 0 → b = 0)
 #align mul_eq_zero_of_ne_zero_imp_eq_zero mul_eq_zero_of_ne_zero_imp_eq_zero
 
 /-- To match `one_mul_eq_id`. -/
-theorem zero_mul_eq_const : (· * ·) (0 : M₀) = Function.const _ 0 :=
+theorem zero_mul_eq_const : ((0 : M₀) * ·) = Function.const _ 0 :=
   funext zero_mul
 #align zero_mul_eq_const zero_mul_eq_const
 

Mathlib/Algebra/GroupWithZero/Defs.lean

@@ -49,7 +49,7 @@ theorem mul_left_cancel₀ (ha : a ≠ 0) (h : a * b = a * c) : b = c :=
   IsLeftCancelMulZero.mul_left_cancel_of_ne_zero ha h
 #align mul_left_cancel₀ mul_left_cancel₀
 
-theorem mul_right_injective₀ (ha : a ≠ 0) : Function.Injective ((· * ·) a) :=
+theorem mul_right_injective₀ (ha : a ≠ 0) : Function.Injective (a * ·) :=
   fun _ _ => mul_left_cancel₀ ha
 #align mul_right_injective₀ mul_right_injective₀
 

Mathlib/Algebra/GroupWithZero/Units/Equiv.lean

@@ -30,7 +30,7 @@ protected def mulLeft₀ (a : G) (ha : a ≠ 0) : Perm G :=
 #align equiv.mul_left₀_symm_apply Equiv.mulLeft₀_symm_apply
 #align equiv.mul_left₀_apply Equiv.mulLeft₀_apply
 
-theorem _root_.mulLeft_bijective₀ (a : G) (ha : a ≠ 0) : Function.Bijective ((· * ·) a : G → G) :=
+theorem _root_.mulLeft_bijective₀ (a : G) (ha : a ≠ 0) : Function.Bijective (a * · : G → G) :=
   (Equiv.mulLeft₀ a ha).bijective
 #align mul_left_bijective₀ mulLeft_bijective₀
 

Mathlib/Algebra/Lie/Free.lean

@@ -123,7 +123,7 @@ instance : Inhabited (FreeLieAlgebra R X) := by rw [FreeLieAlgebra]; infer_insta
 namespace FreeLieAlgebra
 
 instance {S : Type*} [Monoid S] [DistribMulAction S R] [IsScalarTower S R R] :
-    SMul S (FreeLieAlgebra R X) where smul t := Quot.map ((· • ·) t) (Rel.smulOfTower t)
+    SMul S (FreeLieAlgebra R X) where smul t := Quot.map (t • ·) (Rel.smulOfTower t)
 
 instance {S : Type*} [Monoid S] [DistribMulAction S R] [DistribMulAction Sᵐᵒᵖ R]
     [IsScalarTower S R R] [IsCentralScalar S R] : IsCentralScalar S (FreeLieAlgebra R X) where

Mathlib/Algebra/Module/Basic.lean

@@ -623,7 +623,7 @@ section SMulInjective
 variable (M)
 
 theorem smul_right_injective [NoZeroSMulDivisors R M] {c : R} (hc : c ≠ 0) :
-    Function.Injective ((· • ·) c : M → M) :=
+    Function.Injective (c • · : M → M) :=
   (injective_iff_map_eq_zero (smulAddHom R M c)).2 fun _ ha => (smul_eq_zero.mp ha).resolve_left hc
 #align smul_right_injective smul_right_injective
 

Mathlib/Algebra/Module/Injective.lean

@@ -219,7 +219,7 @@ instance ExtensionOf.inhabited : Inhabited (ExtensionOf i f) where
             dsimp
             rw [← Fact.out (p := Function.Injective i) eq1, map_add]
           map_smul' := fun r x => by
-            have eq1 : r • _ = (r • x).1 := congr_arg ((· • ·) r) x.2.choose_spec
+            have eq1 : r • _ = (r • x).1 := congr_arg (r • ·) x.2.choose_spec
             rw [← LinearMap.map_smul, ← (r • x).2.choose_spec] at eq1
             dsimp
             rw [← Fact.out (p := Function.Injective i) eq1, LinearMap.map_smul] }

Mathlib/Algebra/Module/LocalizedModule.lean

@@ -61,8 +61,8 @@ theorem r.isEquiv : IsEquiv _ (r S M) :=
     trans := fun ⟨m1, s1⟩ ⟨m2, s2⟩ ⟨m3, s3⟩ ⟨u1, hu1⟩ ⟨u2, hu2⟩ => by
       use u1 * u2 * s2
       -- Put everything in the same shape, sorting the terms using `simp`
-      have hu1' := congr_arg ((· • ·) (u2 * s3)) hu1.symm
-      have hu2' := congr_arg ((· • ·) (u1 * s1)) hu2.symm
+      have hu1' := congr_arg ((u2 * s3) • ·) hu1.symm
+      have hu2' := congr_arg ((u1 * s1) • ·) hu2.symm
       simp only [← mul_smul, smul_assoc, mul_assoc, mul_comm, mul_left_comm] at hu1' hu2' ⊢
       rw [hu2', hu1']
     symm := fun ⟨m1, s1⟩ ⟨m2, s2⟩ ⟨u, hu⟩ => ⟨u, hu.symm⟩ }
@@ -154,8 +154,8 @@ instance : Add (LocalizedModule S M) where
           mk_eq.mpr
             ⟨u1 * u2, by
               -- Put everything in the same shape, sorting the terms using `simp`
-              have hu1' := congr_arg ((· • ·) (u2 * s2 * s2')) hu1
-              have hu2' := congr_arg ((· • ·) (u1 * s1 * s1')) hu2
+              have hu1' := congr_arg ((u2 * s2 * s2') • ·) hu1
+              have hu2' := congr_arg ((u1 * s1 * s1') • ·) hu2
               simp only [smul_add, ← mul_smul, smul_assoc, mul_assoc, mul_comm,
                 mul_left_comm] at hu1' hu2' ⊢
               rw [hu1', hu2']⟩
@@ -320,7 +320,7 @@ instance : SMul (Localization S) (LocalizedModule S M) where
           (by
             rintro ⟨m1, t1⟩ ⟨m2, t2⟩ ⟨u, h⟩
             refine' mk_eq.mpr ⟨u, _⟩
-            have h' := congr_arg ((· • ·) (s • r)) h
+            have h' := congr_arg ((s • r) • ·) h
             simp only [← mul_smul, smul_eq_mul, mul_comm, mul_left_comm, Submonoid.smul_def,
               Submonoid.coe_mul] at h' ⊢
             rw [h'])))

Mathlib/Algebra/Module/MinimalAxioms.lean

@@ -36,6 +36,6 @@ def Module.ofMinimalAxioms {R : Type u} {M : Type v} [Semiring R] [AddCommGroup
     mul_smul := mul_smul,
     one_smul := one_smul,
     zero_smul := fun x =>
-      (AddMonoidHom.mk' (fun r : R => r • x) fun r s => add_smul r s x).map_zero
-    smul_zero := fun r => (AddMonoidHom.mk' ((· • ·) r) (smul_add r)).map_zero }
+      (AddMonoidHom.mk' (· • x) fun r s => add_smul r s x).map_zero
+    smul_zero := fun r => (AddMonoidHom.mk' (r • ·) (smul_add r)).map_zero }
 #align module.of_core Module.ofMinimalAxioms

Mathlib/Algebra/MonoidAlgebra/Division.lean

@@ -52,7 +52,7 @@ noncomputable def divOf (x : k[G]) (g : G) : k[G] :=
   -- the support, and discarding the elements of the support from which `g` can't be subtracted.
   -- If `G` is an additive group, such as `ℤ` when used for `LaurentPolynomial`,
   -- then no discarding occurs.
-  @Finsupp.comapDomain.addMonoidHom _ _ _ _ ((· + ·) g) (add_right_injective g) x
+  @Finsupp.comapDomain.addMonoidHom _ _ _ _ (g + ·) (add_right_injective g) x
 #align add_monoid_algebra.div_of AddMonoidAlgebra.divOf
 
 local infixl:70 " /ᵒᶠ " => divOf
@@ -65,7 +65,7 @@ theorem divOf_apply (g : G) (x : k[G]) (g' : G) : (x /ᵒᶠ g) g' = x (g + g')
 @[simp]
 theorem support_divOf (g : G) (x : k[G]) :
     (x /ᵒᶠ g).support =
-      x.support.preimage ((· + ·) g) (Function.Injective.injOn (add_right_injective g) _) :=
+      x.support.preimage (g + ·) (Function.Injective.injOn (add_right_injective g) _) :=
   rfl
 #align add_monoid_algebra.support_div_of AddMonoidAlgebra.support_divOf
 

Mathlib/Algebra/MonoidAlgebra/Support.lean

@@ -21,7 +21,7 @@ open Finset Finsupp
 variable {k : Type u₁} {G : Type u₂} [Semiring k]
 
 theorem support_single_mul_subset [DecidableEq G] [Mul G] (f : MonoidAlgebra k G) (r : k) (a : G) :
-    (single a r * f : MonoidAlgebra k G).support ⊆ Finset.image ((· * ·) a) f.support := by
+    (single a r * f : MonoidAlgebra k G).support ⊆ Finset.image (a * ·) f.support := by
   intro x hx
   contrapose hx
   have : ∀ y, a * y = x → f y = 0 := by
@@ -54,7 +54,7 @@ theorem support_mul_single_subset [DecidableEq G] [Mul G] (f : MonoidAlgebra k G
 
 theorem support_single_mul_eq_image [DecidableEq G] [Mul G] (f : MonoidAlgebra k G) {r : k}
     (hr : ∀ y, r * y = 0 ↔ y = 0) {x : G} (lx : IsLeftRegular x) :
-    (single x r * f : MonoidAlgebra k G).support = Finset.image ((· * ·) x) f.support := by
+    (single x r * f : MonoidAlgebra k G).support = Finset.image (x * ·) f.support := by
   refine' subset_antisymm (support_single_mul_subset f _ _) fun y hy => _
   obtain ⟨y, yf, rfl⟩ : ∃ a : G, a ∈ f.support ∧ x * a = y := by
     simpa only [Finset.mem_image, exists_prop] using hy