chore(*): drop $/<| before fun (#9361)

Subset of #9319

Mathlib/Algebra/Algebra/NonUnitalSubalgebra.lean

@@ -570,16 +570,16 @@ lemma adjoin_induction' {s : Set A} {p : adjoin R s → Prop} (a : adjoin R s)
     (Hs : ∀ x (h : x ∈ s), p ⟨x, subset_adjoin R h⟩)
     (Hadd : ∀ x y, p x → p y → p (x + y)) (H0 : p 0)
     (Hmul : ∀ x y, p x → p y → p (x * y)) (Hsmul : ∀ (r : R) x, p x → p (r • x)) : p a :=
-  Subtype.recOn a <| fun b hb => by
+  Subtype.recOn a fun b hb => by
     refine Exists.elim ?_ (fun (hb : b ∈ adjoin R s) (hc : p ⟨b, hb⟩) => hc)
     apply adjoin_induction hb
     · exact fun x hx => ⟨subset_adjoin R hx, Hs x hx⟩
-    · exact fun x y hx hy => Exists.elim hx <| fun hx' hx => Exists.elim hy <| fun hy' hy =>
+    · exact fun x y hx hy => Exists.elim hx fun hx' hx => Exists.elim hy fun hy' hy =>
         ⟨add_mem hx' hy', Hadd _ _ hx hy⟩
     · exact ⟨_, H0⟩
-    · exact fun x y hx hy => Exists.elim hx <| fun hx' hx => Exists.elim hy <| fun hy' hy =>
+    · exact fun x y hx hy => Exists.elim hx fun hx' hx => Exists.elim hy fun hy' hy =>
         ⟨mul_mem hx' hy', Hmul _ _ hx hy⟩
-    · exact fun r x hx => Exists.elim hx <| fun hx' hx =>
+    · exact fun r x hx => Exists.elim hx fun hx' hx =>
         ⟨SMulMemClass.smul_mem r hx', Hsmul r _ hx⟩
 
 protected theorem gc : GaloisConnection (adjoin R : Set A → NonUnitalSubalgebra R A) (↑) :=

Mathlib/Algebra/Algebra/Subalgebra/Basic.lean

@@ -338,7 +338,7 @@ def toSubmodule : Subalgebra R A ↪o Submodule R A where
           carrier := S
           smul_mem' := fun c {x} hx ↦
             (Algebra.smul_def c x).symm ▸ mul_mem (S.range_le ⟨c, rfl⟩) hx }
-      inj' := fun _ _ h ↦ ext <| fun x ↦ SetLike.ext_iff.mp h x }
+      inj' := fun _ _ h ↦ ext fun x ↦ SetLike.ext_iff.mp h x }
   map_rel_iff' := SetLike.coe_subset_coe.symm.trans SetLike.coe_subset_coe
 #align subalgebra.to_submodule Subalgebra.toSubmodule
 

Mathlib/Algebra/Associated.lean

@@ -849,13 +849,13 @@ theorem mk_mul_mk {x y : α} : Associates.mk x * Associates.mk y = Associates.mk
 instance instCommMonoid : CommMonoid (Associates α) where
   one := 1
   mul := (· * ·)
-  mul_one a' := Quotient.inductionOn a' <| fun a => show ⟦a * 1⟧ = ⟦a⟧ by simp
-  one_mul a' := Quotient.inductionOn a' <| fun a => show ⟦1 * a⟧ = ⟦a⟧ by simp
+  mul_one a' := Quotient.inductionOn a' fun a => show ⟦a * 1⟧ = ⟦a⟧ by simp
+  one_mul a' := Quotient.inductionOn a' fun a => show ⟦1 * a⟧ = ⟦a⟧ by simp
   mul_assoc a' b' c' :=
-    Quotient.inductionOn₃ a' b' c' <| fun a b c =>
+    Quotient.inductionOn₃ a' b' c' fun a b c =>
       show ⟦a * b * c⟧ = ⟦a * (b * c)⟧ by rw [mul_assoc]
   mul_comm a' b' :=
-    Quotient.inductionOn₂ a' b' <| fun a b => show ⟦a * b⟧ = ⟦b * a⟧ by rw [mul_comm]
+    Quotient.inductionOn₂ a' b' fun a b => show ⟦a * b⟧ = ⟦b * a⟧ by rw [mul_comm]
 
 instance instPreorder : Preorder (Associates α) where
   le := Dvd.dvd
@@ -890,7 +890,7 @@ theorem dvd_eq_le : ((· ∣ ·) : Associates α → Associates α → Prop) = (
 
 theorem mul_eq_one_iff {x y : Associates α} : x * y = 1 ↔ x = 1 ∧ y = 1 :=
   Iff.intro
-    (Quotient.inductionOn₂ x y <| fun a b h =>
+    (Quotient.inductionOn₂ x y fun a b h =>
       have : a * b ~ᵤ 1 := Quotient.exact h
       ⟨Quotient.sound <| associated_one_of_associated_mul_one this,
         Quotient.sound <| associated_one_of_associated_mul_one <| by rwa [mul_comm] at this⟩)

Mathlib/Algebra/BigOperators/Associated.lean

@@ -134,7 +134,7 @@ theorem finset_prod_mk {p : Finset β} {f : β → α} :
     (∏ i in p, Associates.mk (f i)) = Associates.mk (∏ i in p, f i) := by
   -- Porting note: added
   have : (fun i => Associates.mk (f i)) = Associates.mk ∘ f :=
-    funext <| fun x => Function.comp_apply
+    funext fun x => Function.comp_apply
   rw [Finset.prod_eq_multiset_prod, this, ← Multiset.map_map, prod_mk,
     ← Finset.prod_eq_multiset_prod]
 #align associates.finset_prod_mk Associates.finset_prod_mk

Mathlib/Algebra/BigOperators/Basic.lean

@@ -666,7 +666,7 @@ lemma prod_fiberwise_of_maps_to' {g : ι → κ} (h : ∀ i ∈ s, g i ∈ t) (f
     ∏ j in t, ∏ _i in s.filter fun i ↦ g i = j, f j = ∏ i in s, f (g i) := by
   calc
     _ = ∏ y in t, ∏ x in s.filter fun x ↦ g x = y, f (g x) :=
-        prod_congr rfl $ fun y _ ↦ prod_congr rfl fun x hx ↦ by rw [(mem_filter.1 hx).2]
+        prod_congr rfl fun y _ ↦ prod_congr rfl fun x hx ↦ by rw [(mem_filter.1 hx).2]
     _ = _ := prod_fiberwise_of_maps_to h _
 
 variable [Fintype κ]

Mathlib/Algebra/Category/GroupCat/Colimits.lean

@@ -111,13 +111,13 @@ def ColimitType : Type max u v w :=
 instance : AddCommGroup (ColimitType.{w} F) where
   zero := Quotient.mk _ zero
   neg := Quotient.map neg Relation.neg_1
-  add := Quotient.map₂ add <| fun x x' rx y y' ry =>
+  add := Quotient.map₂ add fun x x' rx y y' ry =>
     Setoid.trans (Relation.add_1 _ _ y rx) (Relation.add_2 x' _ _ ry)
-  zero_add := Quotient.ind <| fun _ => Quotient.sound <| Relation.zero_add _
-  add_zero := Quotient.ind <| fun _ => Quotient.sound <| Relation.add_zero _
-  add_left_neg := Quotient.ind <| fun _ => Quotient.sound <| Relation.add_left_neg _
-  add_comm := Quotient.ind₂ <| fun _ _ => Quotient.sound <| Relation.add_comm _ _
-  add_assoc := Quotient.ind <| fun _ => Quotient.ind₂ <| fun _ _ =>
+  zero_add := Quotient.ind fun _ => Quotient.sound <| Relation.zero_add _
+  add_zero := Quotient.ind fun _ => Quotient.sound <| Relation.add_zero _
+  add_left_neg := Quotient.ind fun _ => Quotient.sound <| Relation.add_left_neg _
+  add_comm := Quotient.ind₂ fun _ _ => Quotient.sound <| Relation.add_comm _ _
+  add_assoc := Quotient.ind fun _ => Quotient.ind₂ fun _ _ =>
     Quotient.sound <| Relation.add_assoc _ _ _
 
 instance ColimitTypeInhabited : Inhabited (ColimitType.{w} F) := ⟨0⟩
@@ -227,7 +227,7 @@ def descMorphism (s : Cocone F) : colimit.{w} F ⟶ s.pt where
 /-- Evidence that the proposed colimit is the colimit. -/
 def colimitCoconeIsColimit : IsColimit (colimitCocone.{w} F) where
   desc s := descMorphism F s
-  uniq s m w := FunLike.ext _ _ <| fun x => Quot.inductionOn x fun x => by
+  uniq s m w := FunLike.ext _ _ fun x => Quot.inductionOn x fun x => by
     change (m : ColimitType F →+ s.pt) _ = (descMorphism F s : ColimitType F →+ s.pt) _
     induction x using Prequotient.recOn with
     | of j x => exact FunLike.congr_fun (w j) x

Mathlib/Algebra/Category/GroupCat/Kernels.lean

@@ -26,7 +26,7 @@ def kernelCone : KernelFork f :=
 /-- The kernel of a group homomorphism is a kernel in the categorical sense. -/
 def kernelIsLimit : IsLimit <| kernelCone f :=
   Fork.IsLimit.mk _
-    (fun s => (by exact Fork.ι s : _ →+ G).codRestrict _ <| fun c => f.mem_ker.mpr <|
+    (fun s => (by exact Fork.ι s : _ →+ G).codRestrict _ fun c => f.mem_ker.mpr <|
       by exact FunLike.congr_fun s.condition c)
     (fun _ => by rfl)
     (fun _ _ h => ext fun x => Subtype.ext_iff_val.mpr <| by exact FunLike.congr_fun h x)

Mathlib/Algebra/Category/ModuleCat/ChangeOfRings.lean

@@ -129,7 +129,7 @@ instance (priority := 100) sMulCommClass_mk {R : Type u₁} {S : Type u₂} [Rin
     haveI : SMul R M := (RestrictScalars.obj' f (ModuleCat.mk M)).isModule.toSMul
     SMulCommClass R S M :=
   @SMulCommClass.mk R S M (_) _
-   <| fun r s m => (by simp [← mul_smul, mul_comm] : f r • s • m = s • f r • m)
+   fun r s m => (by simp [← mul_smul, mul_comm] : f r • s • m = s • f r • m)
 #align category_theory.Module.smul_comm_class_mk ModuleCat.sMulCommClass_mk
 
 /-- Semilinear maps `M →ₛₗ[f] N` identify to

Mathlib/Algebra/Category/MonCat/Colimits.lean

@@ -132,11 +132,11 @@ instance : Inhabited (ColimitType F) := by
 
 instance monoidColimitType : Monoid (ColimitType F) where
   one := Quotient.mk _ one
-  mul := Quotient.map₂ mul <| fun x x' rx y y' ry =>
+  mul := Quotient.map₂ mul fun x x' rx y y' ry =>
     Setoid.trans (Relation.mul_1 _ _ y rx) (Relation.mul_2 x' _ _ ry)
-  one_mul := Quotient.ind <| fun _ => Quotient.sound <| Relation.one_mul _
-  mul_one := Quotient.ind <| fun _ => Quotient.sound <| Relation.mul_one _
-  mul_assoc := Quotient.ind <| fun _ => Quotient.ind₂ <| fun _ _ =>
+  one_mul := Quotient.ind fun _ => Quotient.sound <| Relation.one_mul _
+  mul_one := Quotient.ind fun _ => Quotient.sound <| Relation.mul_one _
+  mul_assoc := Quotient.ind fun _ => Quotient.ind₂ fun _ _ =>
     Quotient.sound <| Relation.mul_assoc _ _ _
 set_option linter.uppercaseLean3 false in
 #align Mon.colimits.monoid_colimit_type MonCat.Colimits.monoidColimitType

Mathlib/Algebra/Category/Ring/Colimits.lean

@@ -144,12 +144,12 @@ def ColimitType : Type v :=
 instance ColimitType.AddGroup : AddGroup (ColimitType F) where
   zero := Quotient.mk _ zero
   neg := Quotient.map neg Relation.neg_1
-  add := Quotient.map₂ add <| fun x x' rx y y' ry =>
+  add := Quotient.map₂ add fun x x' rx y y' ry =>
     Setoid.trans (Relation.add_1 _ _ y rx) (Relation.add_2 x' _ _ ry)
-  zero_add := Quotient.ind <| fun _ => Quotient.sound <| Relation.zero_add _
-  add_zero := Quotient.ind <| fun _ => Quotient.sound <| Relation.add_zero _
-  add_left_neg := Quotient.ind <| fun _ => Quotient.sound <| Relation.add_left_neg _
-  add_assoc := Quotient.ind <| fun _ => Quotient.ind₂ <| fun _ _ =>
+  zero_add := Quotient.ind fun _ => Quotient.sound <| Relation.zero_add _
+  add_zero := Quotient.ind fun _ => Quotient.sound <| Relation.add_zero _
+  add_left_neg := Quotient.ind fun _ => Quotient.sound <| Relation.add_left_neg _
+  add_assoc := Quotient.ind fun _ => Quotient.ind₂ fun _ _ =>
     Quotient.sound <| Relation.add_assoc _ _ _
 
 -- Porting note : failed to derive `Inhabited` instance

Mathlib/Algebra/GCDMonoid/Finset.lean

@@ -274,7 +274,7 @@ theorem extract_gcd (f : β → α) (hs : s.Nonempty) :
     · choose g' hg using @gcd_dvd _ _ _ _ s f
       push_neg at h
       refine' ⟨fun b ↦ if hb : b ∈ s then g' hb else 0, fun b hb ↦ _,
-          extract_gcd' f _ h <| fun b hb ↦ _⟩
+          extract_gcd' f _ h fun b hb ↦ _⟩
       simp only [hb, hg, dite_true]
       rw [dif_pos hb, hg hb]
 #align finset.extract_gcd Finset.extract_gcd

Mathlib/Algebra/GCDMonoid/Multiset.lean

@@ -79,7 +79,7 @@ this lower priority to avoid linter complaints about simp-normal form -/
 `(Multiset.induction_on s)`, when it should be `Multiset.induction_on s <|`. -/
 @[simp 1100]
 theorem normalize_lcm (s : Multiset α) : normalize s.lcm = s.lcm :=
-  Multiset.induction_on s (by simp) <| fun a s _ ↦ by simp
+  Multiset.induction_on s (by simp) fun a s _ ↦ by simp
 #align multiset.normalize_lcm Multiset.normalize_lcm
 
 @[simp]
@@ -93,7 +93,7 @@ variable [DecidableEq α]
 
 @[simp]
 theorem lcm_dedup (s : Multiset α) : (dedup s).lcm = s.lcm :=
-  Multiset.induction_on s (by simp) <| fun a s IH ↦ by
+  Multiset.induction_on s (by simp) fun a s IH ↦ by
     by_cases h : a ∈ s <;> simp [IH, h]
     unfold lcm
     rw [← cons_erase h, fold_cons_left, ← lcm_assoc, lcm_same]
@@ -167,7 +167,7 @@ theorem gcd_mono {s₁ s₂ : Multiset α} (h : s₁ ⊆ s₂) : s₂.gcd ∣ s
 this lower priority to avoid linter complaints about simp-normal form -/
 @[simp 1100]
 theorem normalize_gcd (s : Multiset α) : normalize s.gcd = s.gcd :=
-  Multiset.induction_on s (by simp) <| fun a s _ ↦ by simp
+  Multiset.induction_on s (by simp) fun a s _ ↦ by simp
 #align multiset.normalize_gcd Multiset.normalize_gcd
 
 theorem gcd_eq_zero_iff (s : Multiset α) : s.gcd = 0 ↔ ∀ x : α, x ∈ s → x = 0 := by
@@ -196,7 +196,7 @@ variable [DecidableEq α]
 
 @[simp]
 theorem gcd_dedup (s : Multiset α) : (dedup s).gcd = s.gcd :=
-  Multiset.induction_on s (by simp) <| fun a s IH ↦ by
+  Multiset.induction_on s (by simp) fun a s IH ↦ by
     by_cases h : a ∈ s <;> simp [IH, h]
     unfold gcd
     rw [← cons_erase h, fold_cons_left, ← gcd_assoc, gcd_same]

Mathlib/Algebra/GradedMonoid.lean

@@ -616,7 +616,7 @@ theorem list_prod_map_mem_graded {ι'} (l : List ι') (i : ι' → ι) (r : ι'
     rw [List.map_cons, List.map_cons, List.prod_cons, List.sum_cons]
     exact
       mul_mem_graded (h _ <| List.mem_cons_self _ _)
-        (list_prod_map_mem_graded tail _ _ <| fun j hj => h _ <| List.mem_cons_of_mem _ hj)
+        (list_prod_map_mem_graded tail _ _ fun j hj => h _ <| List.mem_cons_of_mem _ hj)
 #align set_like.list_prod_map_mem_graded SetLike.list_prod_map_mem_graded
 
 theorem list_prod_ofFn_mem_graded {n} (i : Fin n → ι) (r : Fin n → R) (h : ∀ j, r j ∈ A (i j)) :

Mathlib/Algebra/Group/Equiv/Basic.lean

@@ -195,7 +195,7 @@ instance [Mul α] [Mul β] [MulEquivClass F α β] : CoeTC F (α ≃* β) :=
 @[to_additive]
 theorem MulEquivClass.toMulEquiv_injective [Mul α] [Mul β] [MulEquivClass F α β] :
     Function.Injective ((↑) : F → α ≃* β) :=
-  fun _ _ e ↦ FunLike.ext _ _ <| fun a ↦ congr_arg (fun e : α ≃* β ↦ e.toFun a) e
+  fun _ _ e ↦ FunLike.ext _ _ fun a ↦ congr_arg (fun e : α ≃* β ↦ e.toFun a) e
 
 namespace MulEquiv
 

Mathlib/Algebra/Group/Pi.lean

@@ -171,11 +171,11 @@ instance commGroup [∀ i, CommGroup <| f i] : CommGroup (∀ i : I, f i) :=
 
 @[to_additive]
 instance [∀ i, Mul <| f i] [∀ i, IsLeftCancelMul <| f i] : IsLeftCancelMul (∀ i : I, f i) where
-  mul_left_cancel  _ _ _ h := funext <| fun _ => mul_left_cancel (congr_fun h _)
+  mul_left_cancel  _ _ _ h := funext fun _ => mul_left_cancel (congr_fun h _)
 
 @[to_additive]
 instance [∀ i, Mul <| f i] [∀ i, IsRightCancelMul <| f i] : IsRightCancelMul (∀ i : I, f i) where
-  mul_right_cancel  _ _ _ h := funext <| fun _ => mul_right_cancel (congr_fun h _)
+  mul_right_cancel  _ _ _ h := funext fun _ => mul_right_cancel (congr_fun h _)
 
 @[to_additive]
 instance [∀ i, Mul <| f i] [∀ i, IsCancelMul <| f i] : IsCancelMul (∀ i : I, f i) where

Mathlib/Algebra/GroupWithZero/Basic.lean

@@ -159,7 +159,7 @@ variable [CancelMonoidWithZero M₀] {a b c : M₀}
 
 -- see Note [lower instance priority]
 instance (priority := 10) CancelMonoidWithZero.to_noZeroDivisors : NoZeroDivisors M₀ :=
-  ⟨fun ab0 => or_iff_not_imp_left.mpr <| fun ha => mul_left_cancel₀ ha <|
+  ⟨fun ab0 => or_iff_not_imp_left.mpr fun ha => mul_left_cancel₀ ha <|
     ab0.trans (mul_zero _).symm⟩
 #align cancel_monoid_with_zero.to_no_zero_divisors CancelMonoidWithZero.to_noZeroDivisors
 

Mathlib/Algebra/GroupWithZero/InjSurj.lean

@@ -234,7 +234,7 @@ protected def Function.Surjective.groupWithZero [Zero G₀'] [Mul G₀'] [One G
   { hf.monoidWithZero f zero one mul npow, hf.divInvMonoid f one mul inv div npow zpow with
     inv_zero := by erw [← zero, ← inv, inv_zero],
     mul_inv_cancel := hf.forall.2 fun x hx => by
-        erw [← inv, ← mul, mul_inv_cancel (mt (congr_arg f) <| fun h ↦ hx (h.trans zero)), one]
+        erw [← inv, ← mul, mul_inv_cancel (mt (congr_arg f) fun h ↦ hx (h.trans zero)), one]
     exists_pair_ne := ⟨0, 1, h01⟩ }
 #align function.surjective.group_with_zero Function.Surjective.groupWithZero
 

Mathlib/Algebra/Module/Submodule/Pointwise.lean

@@ -508,7 +508,7 @@ protected def pointwiseSetMulAction [SMulCommClass R R M] :
       fun h => ⟨m, h, (one_smul _ _).symm⟩⟩
   mul_smul s t x := le_antisymm
     (set_smul_le _ _ _ <| by rintro _ _ ⟨_, _, _, _, rfl⟩ _; rw [mul_smul]; aesop)
-    (set_smul_le _ _ _ <| fun r m hr hm ↦ by
+    (set_smul_le _ _ _ fun r m hr hm ↦ by
       have : SMulCommClass R R x := ⟨fun r s m => Subtype.ext <| smul_comm _ _ _⟩
       obtain ⟨c, hc1, rfl⟩ := mem_set_smul _ _ _ |>.mp hm
       simp only [Finsupp.sum, AddSubmonoid.coe_finset_sum, coe_toAddSubmonoid, SetLike.val_smul,

Mathlib/Algebra/MonoidAlgebra/Basic.lean

@@ -979,7 +979,7 @@ def domCongr (e : G ≃* H) : MonoidAlgebra A G ≃ₐ[k] MonoidAlgebra A H :=
         congr_arg₂ _ (equivMapDomain_eq_mapDomain _ _).symm (equivMapDomain_eq_mapDomain _ _).symm)
 
 theorem domCongr_toAlgHom (e : G ≃* H) : (domCongr k A e).toAlgHom = mapDomainAlgHom k A e :=
-  AlgHom.ext <| fun _ => equivMapDomain_eq_mapDomain _ _
+  AlgHom.ext fun _ => equivMapDomain_eq_mapDomain _ _
 
 @[simp] theorem domCongr_apply (e : G ≃* H) (f : MonoidAlgebra A G) (h : H) :
     domCongr k A e f h = f (e.symm h) :=
@@ -2119,7 +2119,7 @@ def domCongr (e : G ≃+ H) : A[G] ≃ₐ[k] A[H] :=
         congr_arg₂ _ (equivMapDomain_eq_mapDomain _ _).symm (equivMapDomain_eq_mapDomain _ _).symm)
 
 theorem domCongr_toAlgHom (e : G ≃+ H) : (domCongr k A e).toAlgHom = mapDomainAlgHom k A e :=
-  AlgHom.ext <| fun _ => equivMapDomain_eq_mapDomain _ _
+  AlgHom.ext fun _ => equivMapDomain_eq_mapDomain _ _
 
 @[simp] theorem domCongr_apply (e : G ≃+ H) (f : MonoidAlgebra A G) (h : H) :
     domCongr k A e f h = f (e.symm h) :=

Mathlib/Algebra/Order/Module/OrderedSMul.lean

@@ -65,7 +65,7 @@ instance OrderedSMul.toPosSMulStrictMono : PosSMulStrictMono R M where
   elim _a ha _b₁ _b₂ hb := OrderedSMul.smul_lt_smul_of_pos hb ha
 
 instance OrderedSMul.toPosSMulReflectLT : PosSMulReflectLT R M :=
-  PosSMulReflectLT.of_pos $ fun _a ha _b₁ _b₂ h ↦ OrderedSMul.lt_of_smul_lt_smul_of_pos h ha
+  PosSMulReflectLT.of_pos fun _a ha _b₁ _b₂ h ↦ OrderedSMul.lt_of_smul_lt_smul_of_pos h ha
 
 instance OrderDual.instOrderedSMul [OrderedSemiring R] [OrderedAddCommMonoid M] [SMulWithZero R M]
     [OrderedSMul R M] : OrderedSMul R Mᵒᵈ where

Mathlib/Algebra/Order/Monovary.lean

@@ -143,19 +143,19 @@ variable [OrderedCommGroup α] [LinearOrderedCommGroup β] {s : Set ι} {f f₁
 
 @[to_additive] lemma Monovary.mul_right (h₁ : Monovary f g₁) (h₂ : Monovary f g₂) :
     Monovary f (g₁ * g₂) :=
-  fun _i _j hij ↦ (lt_or_lt_of_mul_lt_mul hij).elim (fun h ↦ h₁ h) $ fun h ↦ h₂ h
+  fun _i _j hij ↦ (lt_or_lt_of_mul_lt_mul hij).elim (fun h ↦ h₁ h) fun h ↦ h₂ h
 
 @[to_additive] lemma Antivary.mul_right (h₁ : Antivary f g₁) (h₂ : Antivary f g₂) :
     Antivary f (g₁ * g₂) :=
-  fun _i _j hij ↦ (lt_or_lt_of_mul_lt_mul hij).elim (fun h ↦ h₁ h) $ fun h ↦ h₂ h
+  fun _i _j hij ↦ (lt_or_lt_of_mul_lt_mul hij).elim (fun h ↦ h₁ h) fun h ↦ h₂ h
 
 @[to_additive] lemma Monovary.div_right (h₁ : Monovary f g₁) (h₂ : Antivary f g₂) :
     Monovary f (g₁ / g₂) :=
-  fun _i _j hij ↦ (lt_or_lt_of_div_lt_div hij).elim (fun h ↦ h₁ h) $ fun h ↦ h₂ h
+  fun _i _j hij ↦ (lt_or_lt_of_div_lt_div hij).elim (fun h ↦ h₁ h) fun h ↦ h₂ h
 
 @[to_additive] lemma Antivary.div_right (h₁ : Antivary f g₁) (h₂ : Monovary f g₂) :
     Antivary f (g₁ / g₂) :=
-  fun _i _j hij ↦ (lt_or_lt_of_div_lt_div hij).elim (fun h ↦ h₁ h) $ fun h ↦ h₂ h
+  fun _i _j hij ↦ (lt_or_lt_of_div_lt_div hij).elim (fun h ↦ h₁ h) fun h ↦ h₂ h
 
 @[to_additive] lemma Monovary.pow_right (hfg : Monovary f g) (n : ℕ) : Monovary f (g ^ n) :=
   fun _i _j hij ↦ hfg $ lt_of_pow_lt_pow_left' _ hij
@@ -345,7 +345,7 @@ monovary_toDual_right.symm.trans $ by rw [monovary_iff_forall_smul_nonneg]; rfl
 lemma monovaryOn_iff_smul_rearrangement :
     MonovaryOn f g s ↔
       ∀ ⦃i⦄, i ∈ s → ∀ ⦃j⦄, j ∈ s → f i • g j + f j • g i ≤ f i • g i + f j • g j :=
-  monovaryOn_iff_forall_smul_nonneg.trans $ forall₄_congr $ fun i _ j _ ↦ by
+  monovaryOn_iff_forall_smul_nonneg.trans $ forall₄_congr fun i _ j _ ↦ by
     simp [smul_sub, sub_smul, ← add_sub_right_comm, le_sub_iff_add_le, add_comm (f i • g i),
       add_comm (f i • g j)]
 

Mathlib/Algebra/Order/Ring/WithTop.lean

@@ -75,7 +75,7 @@ theorem mul_lt_top [LT α] {a b : WithTop α} (ha : a ≠ ⊤) (hb : b ≠ ⊤)
 #align with_top.mul_lt_top WithTop.mul_lt_top
 
 instance noZeroDivisors [NoZeroDivisors α] : NoZeroDivisors (WithTop α) := by
-  refine ⟨fun h₁ => Decidable.by_contradiction <| fun h₂ => ?_⟩
+  refine ⟨fun h₁ => Decidable.by_contradiction fun h₂ => ?_⟩
   rw [mul_def, if_neg h₂] at h₁
   rcases Option.mem_map₂_iff.1 h₁ with ⟨a, b, (rfl : _ = _), (rfl : _ = _), hab⟩
   exact h₂ ((eq_zero_or_eq_zero_of_mul_eq_zero hab).imp (congr_arg some) (congr_arg some))

Mathlib/Algebra/Ring/CentroidHom.lean

@@ -278,13 +278,13 @@ instance instSMul : SMul M (CentroidHom α) where
 #noalign centroid_hom.has_nsmul
 
 instance [SMul M N] [IsScalarTower M N α] : IsScalarTower M N (CentroidHom α) where
-  smul_assoc _ _ _ := ext <| fun _ => smul_assoc _ _ _
+  smul_assoc _ _ _ := ext fun _ => smul_assoc _ _ _
 
 instance [SMulCommClass M N α] : SMulCommClass M N (CentroidHom α) where
-  smul_comm _ _ _ := ext <| fun _ => smul_comm _ _ _
+  smul_comm _ _ _ := ext fun _ => smul_comm _ _ _
 
 instance [DistribMulAction Mᵐᵒᵖ α] [IsCentralScalar M α] : IsCentralScalar M (CentroidHom α) where
-  op_smul_eq_smul _ _ := ext <| fun _ => op_smul_eq_smul _ _
+  op_smul_eq_smul _ _ := ext fun _ => op_smul_eq_smul _ _
 
 instance isScalarTowerRight : IsScalarTower M (CentroidHom α) (CentroidHom α) where
   smul_assoc _ _ _ := rfl