Update Mathlib/AlgebraicTopology/SimplicialSet/NerveAdjunction.lean

Co-authored-by: Joël Riou <[email protected]>
leanprover-community · Feb 25, 2025 · 5556a3a · 5556a3a
1 parent d90e5fe
commit 5556a3a
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/Mathlib/AlgebraicTopology/SimplicialSet/NerveAdjunction.lean b/Mathlib/AlgebraicTopology/SimplicialSet/NerveAdjunction.lean
@@ -251,7 +251,7 @@ theorem toNerve₂.mk_naturality : toNerve₂.mk.naturalityProperty F = ⊤ :=
 recovered from the underlying ReflPrefunctor. -/
 @[simps!]
 def toNerve₂.mk : X ⟶ nerveFunctor₂.obj (Cat.of C) where
-  app := fun n => toNerve₂.mk.app F n.unop
+  app n := toNerve₂.mk.app F n.unop
   naturality _ _ f := MorphismProperty.of_eq_top (toNerve₂.mk_naturality F hyp) f.unop
 
 end