diff --git a/Mathlib/CategoryTheory/Bicategory/Functor.lean b/Mathlib/CategoryTheory/Bicategory/Functor.lean
index 743fa8bcf8dac3..697fe96332ca45 100644
--- a/Mathlib/CategoryTheory/Bicategory/Functor.lean
+++ b/Mathlib/CategoryTheory/Bicategory/Functor.lean
@@ -33,8 +33,8 @@ pseudofunctors can be defined by using the composition of oplax functors as foll
 ```lean
 def comp (F : Pseudofunctor B C) (G : Pseudofunctor C D) : Pseudofunctor B D :=
   mkOfOplax ((F : OplaxFunctor B C).comp G)
-  { mapIdIso := λ a => (G.mapFunctor _ _).mapIso (F.mapId a) ≪≫ G.mapId (F.obj a),
-    mapCompIso := λ f g =>
+  { mapIdIso := fun a ↦ (G.mapFunctor _ _).mapIso (F.mapId a) ≪≫ G.mapId (F.obj a),
+    mapCompIso := fun f g ↦
       (G.mapFunctor _ _).mapIso (F.mapComp f g) ≪≫ G.mapComp (F.map f) (F.map g) }
 ```
 although the composition of pseudofunctors in this file is defined by using the default constructor
diff --git a/Mathlib/CategoryTheory/Limits/Shapes/WideEqualizers.lean b/Mathlib/CategoryTheory/Limits/Shapes/WideEqualizers.lean
index 367c12fa7e8388..2676b0a63faa1d 100644
--- a/Mathlib/CategoryTheory/Limits/Shapes/WideEqualizers.lean
+++ b/Mathlib/CategoryTheory/Limits/Shapes/WideEqualizers.lean
@@ -429,7 +429,7 @@ theorem Cotrident.IsColimit.homIso_natural [Nonempty J] {t : Cotrident f} {Z Z'
 
 /-- This is a helper construction that can be useful when verifying that a category has certain wide
     equalizers. Given `F : WalkingParallelFamily ⥤ C`, which is really the same as
-    `parallelFamily (λ j, F.map (line j))`, and a trident on `fun j ↦ F.map (line j)`,
+    `parallelFamily (fun j ↦ F.map (line j))`, and a trident on `fun j ↦ F.map (line j)`,
     we get a cone on `F`.
 
     If you're thinking about using this, have a look at
diff --git a/Mathlib/CategoryTheory/Limits/VanKampen.lean b/Mathlib/CategoryTheory/Limits/VanKampen.lean
index 69b55eed800c38..9a582bfcde3f6d 100644
--- a/Mathlib/CategoryTheory/Limits/VanKampen.lean
+++ b/Mathlib/CategoryTheory/Limits/VanKampen.lean
@@ -339,7 +339,7 @@ theorem IsUniversalColimit.map_reflective
   let c'' : Cocone (F' ⋙ Gr) := by
     refine
     { pt := pullback (Gr.map f) (adj.unit.app _)
-      ι := { app := λ j ↦ pullback.lift (Gr.map <| c'.ι.app j) (Gr.map (α'.app j) ≫ c.ι.app j) ?_
+      ι := { app := fun j ↦ pullback.lift (Gr.map <| c'.ι.app j) (Gr.map (α'.app j) ≫ c.ι.app j) ?_
              naturality := ?_ } }
     · rw [← Gr.map_comp, ← hc'']
       erw [← adj.unit_naturality]
diff --git a/Mathlib/CategoryTheory/Products/Basic.lean b/Mathlib/CategoryTheory/Products/Basic.lean
index 35d61193eceda0..277220907bb3be 100644
--- a/Mathlib/CategoryTheory/Products/Basic.lean
+++ b/Mathlib/CategoryTheory/Products/Basic.lean
@@ -384,11 +384,11 @@ open Opposite
 @[simps]
 def prodOpEquiv : (C × D)ᵒᵖ ≌ Cᵒᵖ × Dᵒᵖ where
   functor :=
-    { obj := λ X => ⟨op X.unop.1, op X.unop.2⟩,
-      map := λ f => ⟨f.unop.1.op, f.unop.2.op⟩ }
+    { obj := fun X ↦ ⟨op X.unop.1, op X.unop.2⟩,
+      map := fun f ↦ ⟨f.unop.1.op, f.unop.2.op⟩ }
   inverse :=
-    { obj := λ ⟨X,Y⟩ => op ⟨X.unop, Y.unop⟩,
-      map := λ ⟨f,g⟩ => op ⟨f.unop, g.unop⟩ }
+    { obj := fun ⟨X,Y⟩ ↦ op ⟨X.unop, Y.unop⟩,
+      map := fun ⟨f,g⟩ ↦ op ⟨f.unop, g.unop⟩ }
   unitIso := Iso.refl _
   counitIso := Iso.refl _
   functor_unitIso_comp := fun ⟨X, Y⟩ => by
diff --git a/Mathlib/CategoryTheory/Sites/CoverLifting.lean b/Mathlib/CategoryTheory/Sites/CoverLifting.lean
index 82d16c597d9e91..5a1640abc955f6 100644
--- a/Mathlib/CategoryTheory/Sites/CoverLifting.lean
+++ b/Mathlib/CategoryTheory/Sites/CoverLifting.lean
@@ -258,7 +258,7 @@ theorem gluedSection_isAmalgamation : x.IsAmalgamation (gluedSection ℱ hS hx)
   -- Porting note: next line was `ext W`
   -- Now `ext` can't see that `ran` is defined as a limit.
   -- See https://github.com/leanprover-community/mathlib4/issues/5229
-  refine limit.hom_ext (λ (W : StructuredArrow (op V) G.op) => ?_)
+  refine limit.hom_ext (fun (W : StructuredArrow (op V) G.op) ↦ ?_)
   simp only [Functor.comp_map, limit.lift_pre, coyoneda_obj_map, ran_obj_map, gluedSection]
   erw [limit.lift_π]
   symm
@@ -275,7 +275,7 @@ theorem gluedSection_is_unique (y) (hy : x.IsAmalgamation y) : y = gluedSection
   -- Porting note: next line was `ext W`
   -- Now `ext` can't see that `ran` is defined as a limit.
   -- See https://github.com/leanprover-community/mathlib4/issues/5229
-  refine limit.hom_ext (λ (W : StructuredArrow (op U) G.op) => ?_)
+  refine limit.hom_ext (fun (W : StructuredArrow (op U) G.op) ↦ ?_)
   erw [limit.lift_π]
   convert helper ℱ hS hx (𝟙 _) y W _
   · simp only [op_id, StructuredArrow.map_id]
diff --git a/Mathlib/Control/Fold.lean b/Mathlib/Control/Fold.lean
index 7dbaae6e16d83e..bcaff464e79bf6 100644
--- a/Mathlib/Control/Fold.lean
+++ b/Mathlib/Control/Fold.lean
@@ -88,10 +88,11 @@ We can view the above as a composition of functions:
 
 We can use traverse and const to construct this composition:
 ```
-calc   const.run (traverse (λ y, const.mk' (flip f y)) [y₀,y₁]) x
-     = const.run ((::) <$> const.mk' (flip f y₀) <*> traverse (λ y, const.mk' (flip f y)) [y₁]) x
+calc   const.run (traverse (fun y ↦ const.mk' (flip f y)) [y₀,y₁]) x
+     = const.run ((::) <$> const.mk' (flip f y₀) <*>
+         traverse (fun y ↦ const.mk' (flip f y)) [y₁]) x
 ...  = const.run ((::) <$> const.mk' (flip f y₀) <*>
-         ( (::) <$> const.mk' (flip f y₁) <*> traverse (λ y, const.mk' (flip f y)) [] )) x
+         ( (::) <$> const.mk' (flip f y₁) <*> traverse (fun y ↦ const.mk' (flip f y)) [] )) x
 ...  = const.run ((::) <$> const.mk' (flip f y₀) <*>
          ( (::) <$> const.mk' (flip f y₁) <*> pure [] )) x
 ...  = const.run ( ((::) <$> const.mk' (flip f y₁) <*> pure []) ∘
diff --git a/Mathlib/Tactic/Linarith/Verification.lean b/Mathlib/Tactic/Linarith/Verification.lean
index 25bc888c26ff9d..d85aebe47273ab 100644
--- a/Mathlib/Tactic/Linarith/Verification.lean
+++ b/Mathlib/Tactic/Linarith/Verification.lean
@@ -109,7 +109,7 @@ def mkLTZeroProof : List (Expr × ℕ) → MetaM Expr
       return t
   | ((h, c)::t) => do
       let (iq, h') ← mkSingleCompZeroOf c h
-      let (_, t) ← t.foldlM (λ pr ce => step pr.1 pr.2 ce.1 ce.2) (iq, h')
+      let (_, t) ← t.foldlM (fun pr ce ↦ step pr.1 pr.2 ce.1 ce.2) (iq, h')
       return t
   where
     /--
diff --git a/Mathlib/Testing/SlimCheck/Testable.lean b/Mathlib/Testing/SlimCheck/Testable.lean
index b21cf14e1e83bb..131283467919f7 100644
--- a/Mathlib/Testing/SlimCheck/Testable.lean
+++ b/Mathlib/Testing/SlimCheck/Testable.lean
@@ -47,9 +47,9 @@ of `Shrinkable MyType` and `SampleableExt MyType`. We can define one as follows:
 
 ```lean
 instance : Shrinkable MyType where
-  shrink := λ ⟨x,y,h⟩ =>
+  shrink := fun ⟨x,y,h⟩ ↦
     let proxy := Shrinkable.shrink (x, y - x)
-    proxy.map (λ ⟨⟨fst, snd⟩, ha⟩ => ⟨⟨fst, fst + snd, sorry⟩, sorry⟩)
+    proxy.map (fun ⟨⟨fst, snd⟩, ha⟩ ↦ ⟨⟨fst, fst + snd, sorry⟩, sorry⟩)
 
 instance : SampleableExt MyType :=
   SampleableExt.mkSelfContained do
diff --git a/Mathlib/Util/Tactic.lean b/Mathlib/Util/Tactic.lean
index 2b3f7f94378719..db75c24d5fe295 100644
--- a/Mathlib/Util/Tactic.lean
+++ b/Mathlib/Util/Tactic.lean
@@ -33,7 +33,7 @@ If `mvarId` does not refer to a declared metavariable, nothing happens.
 -/
 def modifyMetavarDecl [MonadMCtx m] (mvarId : MVarId)
     (f : MetavarDecl → MetavarDecl) : m Unit := do
-  modifyMCtx λ mctx =>
+  modifyMCtx fun mctx ↦
     match mctx.decls.find? mvarId with
     | none => mctx
     | some mdecl => { mctx with decls := mctx.decls.insert mvarId (f mdecl) }
diff --git a/test/apply_fun.lean b/test/apply_fun.lean
index f7a11d93bca0fc..04e0bbdf84af96 100644
--- a/test/apply_fun.lean
+++ b/test/apply_fun.lean
@@ -142,11 +142,9 @@ example (a b : ℕ) (h : a ≠ b) : a + 1 ≠ b + 1 := by
 
 -- TODO
 -- -- monotonicity will be proved by `mono` in the next example
--- example (a b : ℕ) (h : a ≤ b) : a + 1 ≤ b + 1 :=
--- begin
---   apply_fun (λ n, n+1) at h,
+-- example (a b : ℕ) (h : a ≤ b) : a + 1 ≤ b + 1 := by
+--   apply_fun (fun n ↦ n+1) at h
 --   exact h
--- end
 
 example {n : Type} [Fintype n] {X : Type} [Semiring X]
   (f : Matrix n n X → Matrix n n X) (A B : Matrix n n X) (h : A * B = 0) : f (A * B) = f 0 := by