From ea58bd52ae0f43482af5c9a0129f1a8ca43fa887 Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Thu, 11 Jul 2024 08:13:55 +0000 Subject: [PATCH] chore: robustify proof in CategoryTheory.GlueData (#14634) (With https://github.com/leanprover/lean4/pull/4595, `aesop` goes astray here, and this proof is better anyway.) --- Mathlib/CategoryTheory/GlueData.lean | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/Mathlib/CategoryTheory/GlueData.lean b/Mathlib/CategoryTheory/GlueData.lean index e20de5b5171d42..d471dcdbc63b2d 100644 --- a/Mathlib/CategoryTheory/GlueData.lean +++ b/Mathlib/CategoryTheory/GlueData.lean @@ -381,8 +381,7 @@ def vPullbackConeIsLimitOfMap (i j : D.J) [ReflectsLimit (cospan (D.ι i) (D.ι apply hc.ofIsoLimit refine Cones.ext (Iso.refl _) ?_ rintro (_ | _ | _) - on_goal 1 => change _ = _ ≫ (_ ≫ _) ≫ _ - all_goals change _ = 𝟙 _ ≫ _ ≫ _; aesop_cat + all_goals simp [e]; rfl set_option linter.uppercaseLean3 false in #align category_theory.glue_data.V_pullback_cone_is_limit_of_map CategoryTheory.GlueData.vPullbackConeIsLimitOfMap