From d6c51e7377efc36e4d824d220010a8a7eee493b7 Mon Sep 17 00:00:00 2001 From: emilyriehl Date: Mon, 6 Jan 2025 18:00:48 -0500 Subject: [PATCH] golfing --- .../AlgebraicTopology/SimplicialSet/CoherentIso.lean | 12 +----------- 1 file changed, 1 insertion(+), 11 deletions(-) diff --git a/InfinityCosmos/ForMathlib/AlgebraicTopology/SimplicialSet/CoherentIso.lean b/InfinityCosmos/ForMathlib/AlgebraicTopology/SimplicialSet/CoherentIso.lean index d19d8a7..63d95ab 100644 --- a/InfinityCosmos/ForMathlib/AlgebraicTopology/SimplicialSet/CoherentIso.lean +++ b/InfinityCosmos/ForMathlib/AlgebraicTopology/SimplicialSet/CoherentIso.lean @@ -53,17 +53,7 @@ def fromIso {X Y : C} (e : X ≅ Y) : WalkingIso ⥤ C where | zero, one, _ => e.hom | one, zero, _ => e.inv | one, one, _ => 𝟙 _ - map_comp := by - intro X Y Z f g - match X, Y, Z with - | zero, zero, zero => simp - | zero, zero, one => simp - | zero, one, zero => simp - | zero, one, one => simp - | one, zero, zero => simp - | one, zero, one => simp - | one, one, zero => simp - | one, one, one => simp + map_comp := by rintro (_ | _) (_ | _) (_ | _) _ _ <;> simp def equiv : (WalkingIso ⥤ C) ≃ Σ (X : C) (Y : C), (X ≅ Y) where toFun F := ⟨F.obj zero, F.obj one, toIso F⟩