diff --git a/Mathlib/CategoryTheory/GlueData.lean b/Mathlib/CategoryTheory/GlueData.lean
index e20de5b5171d4..d471dcdbc63b2 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