chore: robustify proof in CategoryTheory.GlueData (#14634)

(With leanprover/lean4#4595, `aesop` goes astray here, and this proof is better anyway.)
leanprover-community · Jul 11, 2024 · ea58bd5 · ea58bd5
1 parent b7d36b6
commit ea58bd5
Showing 1 changed file with 1 addition and 2 deletions.
diff --git 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