-- Module: Mathlib.CategoryTheory.GlueData
Goal:
C : Type u₁
inst : Category.{v, u₁} C
C' : Type u₂
inst_1 : Category.{v, u₂} C'
D : GlueData.{v, u₁} C
F : Functor.{v, v, u₁, u₂} C C'
inst_2 : HasMulticoequalizer D.diagram
inst_3 : PreservesColimit D.diagram.multispan F
inst_4 : ∀ (i j k : D.J), PreservesLimit (cospan (D.f i j) (D.f i k)) F
i j : D.J
inst_5 : ReflectsLimit (cospan (Z := D.glued) (D.ι i) (D.ι j)) F
hc :
  IsLimit (F := cospan (Z := (D.mapGlueData F).glued) ((D.mapGlueData F).ι i) ((D.mapGlueData F).ι j))
    ((D.mapGlueData F).vPullbackCone i j)
⊢ (cospan (Z := F.obj D.glued) (F.map (D.ι i)) (F.map (D.ι j))).map (WidePullbackShape.Hom.term WalkingPair.left) ≫
      Iso.hom
        ((fun (x : WalkingCospan) ↦
            (Option.casesOn (motive := fun (t : Option WalkingPair) ↦
                (h : x = t) →
                  (cospan (Z := F.obj D.glued) (F.map (D.ι i)) (F.map (D.ι j))).obj x ≅
                    (cospan (Z := (D.mapGlueData F).glued) ((D.mapGlueData F).ι i) ((D.mapGlueData F).ι j)).obj x)
                x
                (fun (h : x = none) ↦
                  Eq.ndrec (motive := fun (x : WalkingCospan) ↦
                    (cospan (Z := F.obj D.glued) (F.map (D.ι i)) (F.map (D.ι j))).obj x ≅
                      (cospan (Z := (D.mapGlueData F).glued) ((D.mapGlueData F).ι i) ((D.mapGlueData F).ι j)).obj x)
                    (D.gluedIso F) ⋯)
                (fun (val : WalkingPair) (h : x = some val) ↦
                  Eq.ndrec (motive := fun (x : WalkingCospan) ↦
                    (cospan (Z := F.obj D.glued) (F.map (D.ι i)) (F.map (D.ι j))).obj x ≅
                      (cospan (Z := (D.mapGlueData F).glued) ((D.mapGlueData F).ι i) ((D.mapGlueData F).ι j)).obj x)
                    (Iso.refl ((cospan (Z := F.obj D.glued) (F.map (D.ι i)) (F.map (D.ι j))).obj (some val))) ⋯)
                ⋯ :
              (cospan (Z := F.obj D.glued) (F.map (D.ι i)) (F.map (D.ι j))).obj x ≅
                (cospan (Z := (D.mapGlueData F).glued) ((D.mapGlueData F).ι i) ((D.mapGlueData F).ι j)).obj x))
          none) =
    Iso.hom
        ((fun (x : WalkingCospan) ↦
            (Option.casesOn (motive := fun (t : Option WalkingPair) ↦
                (h : x = t) →
                  (cospan (Z := F.obj D.glued) (F.map (D.ι i)) (F.map (D.ι j))).obj x ≅
                    (cospan (Z := (D.mapGlueData F).glued) ((D.mapGlueData F).ι i) ((D.mapGlueData F).ι j)).obj x)
                x
                (fun (h : x = none) ↦
                  Eq.ndrec (motive := fun (x : WalkingCospan) ↦
                    (cospan (Z := F.obj D.glued) (F.map (D.ι i)) (F.map (D.ι j))).obj x ≅
                      (cospan (Z := (D.mapGlueData F).glued) ((D.mapGlueData F).ι i) ((D.mapGlueData F).ι j)).obj x)
                    (D.gluedIso F) ⋯)
                (fun (val : WalkingPair) (h : x = some val) ↦
                  Eq.ndrec (motive := fun (x : WalkingCospan) ↦
                    (cospan (Z := F.obj D.glued) (F.map (D.ι i)) (F.map (D.ι j))).obj x ≅
                      (cospan (Z := (D.mapGlueData F).glued) ((D.mapGlueData F).ι i) ((D.mapGlueData F).ι j)).obj x)
                    (Iso.refl ((cospan (Z := F.obj D.glued) (F.map (D.ι i)) (F.map (D.ι j))).obj (some val))) ⋯)
                ⋯ :
              (cospan (Z := F.obj D.glued) (F.map (D.ι i)) (F.map (D.ι j))).obj x ≅
                (cospan (Z := (D.mapGlueData F).glued) ((D.mapGlueData F).ι i) ((D.mapGlueData F).ι j)).obj x))
          (some WalkingPair.left)) ≫
      (cospan (Z := (D.mapGlueData F).glued) ((D.mapGlueData F).ι i) ((D.mapGlueData F).ι j)).map
        (WidePullbackShape.Hom.term WalkingPair.left)

Tactic:
simp