awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 : ∀ (i j k : D.J), PreservesLimit (cospan (D.f i j) (D.f i k)) F
i j k : D.J
⊢ CategoryStruct.comp (Y := pullback (F.map (D.f j k)) (F.map (D.f j i)))
      (Iso.inv (PreservesPullback.iso F (D.f i j) (D.f i k)) ≫
        F.map (D.t' i j k) ≫ Iso.hom (PreservesPullback.iso F (D.f j k) (D.f j i)))
      (CategoryStruct.comp (Y := pullback (F.map (D.f k i)) (F.map (D.f k j)))
        (Iso.inv (PreservesPullback.iso F (D.f j k) (D.f j i)) ≫
          F.map (D.t' j k i) ≫ Iso.hom (PreservesPullback.iso F (D.f k i) (D.f k j)))
        (Iso.inv (PreservesPullback.iso F (D.f k i) (D.f k j)) ≫
          F.map (D.t' k i j) ≫ Iso.hom (PreservesPullback.iso F (D.f i j) (D.f i k)))) =
    𝟙 (pullback (F.map (D.f i j)) (F.map (D.f i k)))

Tactic:
simp only [Category.assoc, Iso.hom_inv_id_assoc, ← Functor.map_comp_assoc, D.cocycle,
      Iso.inv_hom_id, CategoryTheory.Functor.map_id, Category.id_comp]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Iso.inv_hom_id, CategoryTheory.Functor.map_comp_assoc, CategoryTheory.Functor.map_id, CategoryTheory.Iso.hom_inv_id_assoc, CategoryTheory.GlueData.cocycle, CategoryTheory.Category.id_comp
-- 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 : ∀ (i j k : D.J), PreservesLimit (cospan (D.f i j) (D.f i k)) F
fst snd : D.J
⊢ Eq (α :=
    (D.diagram.multispan ⋙ F).obj (WalkingMultispan.left (fst, snd)) ⟶
      (D.mapGlueData F).diagram.multispan.obj (WalkingMultispan.left (fst, snd)))
    ((D.diagram.multispan ⋙ F).map (WalkingMultispan.Hom.id (WalkingMultispan.left (fst, snd))) ≫
      Iso.hom
        ((fun (x : WalkingMultispan (MultispanShape.prod D.J)) ↦
            (match (motive :=
                (x : WalkingMultispan (MultispanShape.prod D.J)) →
                  (D.diagram.multispan ⋙ F).obj x ≅ (D.mapGlueData F).diagram.multispan.obj x)
                x with
              | WalkingMultispan.left a => Iso.refl ((D.diagram.multispan ⋙ F).obj (WalkingMultispan.left a))
              | WalkingMultispan.right a => Iso.refl ((D.diagram.multispan ⋙ F).obj (WalkingMultispan.right a)) :
              (D.diagram.multispan ⋙ F).obj x ≅ (D.mapGlueData F).diagram.multispan.obj x))
          (WalkingMultispan.left (fst, snd))))
    (Iso.hom
        ((fun (x : WalkingMultispan (MultispanShape.prod D.J)) ↦
            (match (motive :=
                (x : WalkingMultispan (MultispanShape.prod D.J)) →
                  (D.diagram.multispan ⋙ F).obj x ≅ (D.mapGlueData F).diagram.multispan.obj x)
                x with
              | WalkingMultispan.left a => Iso.refl ((D.diagram.multispan ⋙ F).obj (WalkingMultispan.left a))
              | WalkingMultispan.right a => Iso.refl ((D.diagram.multispan ⋙ F).obj (WalkingMultispan.right a)) :
              (D.diagram.multispan ⋙ F).obj x ≅ (D.mapGlueData F).diagram.multispan.obj x))
          (WalkingMultispan.left (fst, snd))) ≫
      (D.mapGlueData F).diagram.multispan.map (WalkingMultispan.Hom.id (WalkingMultispan.left (fst, snd))))

Tactic:
simp
-- 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 : ∀ (i j k : D.J), PreservesLimit (cospan (D.f i j) (D.f i k)) F
fst snd : D.J
⊢ Eq (α :=
    (D.diagram.multispan ⋙ F).obj (WalkingMultispan.left (fst, snd)) ⟶
      (D.mapGlueData F).diagram.multispan.obj (WalkingMultispan.right ((MultispanShape.prod D.J).fst (fst, snd))))
    ((D.diagram.multispan ⋙ F).map (WalkingMultispan.Hom.fst (fst, snd)) ≫
      Iso.hom
        ((fun (x : WalkingMultispan (MultispanShape.prod D.J)) ↦
            (match (motive :=
                (x : WalkingMultispan (MultispanShape.prod D.J)) →
                  (D.diagram.multispan ⋙ F).obj x ≅ (D.mapGlueData F).diagram.multispan.obj x)
                x with
              | WalkingMultispan.left a => Iso.refl ((D.diagram.multispan ⋙ F).obj (WalkingMultispan.left a))
              | WalkingMultispan.right a => Iso.refl ((D.diagram.multispan ⋙ F).obj (WalkingMultispan.right a)) :
              (D.diagram.multispan ⋙ F).obj x ≅ (D.mapGlueData F).diagram.multispan.obj x))
          (WalkingMultispan.right ((MultispanShape.prod D.J).fst (fst, snd)))))
    (Iso.hom
        ((fun (x : WalkingMultispan (MultispanShape.prod D.J)) ↦
            (match (motive :=
                (x : WalkingMultispan (MultispanShape.prod D.J)) →
                  (D.diagram.multispan ⋙ F).obj x ≅ (D.mapGlueData F).diagram.multispan.obj x)
                x with
              | WalkingMultispan.left a => Iso.refl ((D.diagram.multispan ⋙ F).obj (WalkingMultispan.left a))
              | WalkingMultispan.right a => Iso.refl ((D.diagram.multispan ⋙ F).obj (WalkingMultispan.right a)) :
              (D.diagram.multispan ⋙ F).obj x ≅ (D.mapGlueData F).diagram.multispan.obj x))
          (WalkingMultispan.left (fst, snd))) ≫
      (D.mapGlueData F).diagram.multispan.map (WalkingMultispan.Hom.fst (fst, snd)))

Tactic:
simp
-- 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 : ∀ (i j k : D.J), PreservesLimit (cospan (D.f i j) (D.f i k)) F
fst snd : D.J
⊢ Eq (α :=
    (D.diagram.multispan ⋙ F).obj (WalkingMultispan.left (fst, snd)) ⟶
      (D.mapGlueData F).diagram.multispan.obj (WalkingMultispan.right ((MultispanShape.prod D.J).snd (fst, snd))))
    ((D.diagram.multispan ⋙ F).map (WalkingMultispan.Hom.snd (fst, snd)) ≫
      Iso.hom
        ((fun (x : WalkingMultispan (MultispanShape.prod D.J)) ↦
            (match (motive :=
                (x : WalkingMultispan (MultispanShape.prod D.J)) →
                  (D.diagram.multispan ⋙ F).obj x ≅ (D.mapGlueData F).diagram.multispan.obj x)
                x with
              | WalkingMultispan.left a => Iso.refl ((D.diagram.multispan ⋙ F).obj (WalkingMultispan.left a))
              | WalkingMultispan.right a => Iso.refl ((D.diagram.multispan ⋙ F).obj (WalkingMultispan.right a)) :
              (D.diagram.multispan ⋙ F).obj x ≅ (D.mapGlueData F).diagram.multispan.obj x))
          (WalkingMultispan.right ((MultispanShape.prod D.J).snd (fst, snd)))))
    (Iso.hom
        ((fun (x : WalkingMultispan (MultispanShape.prod D.J)) ↦
            (match (motive :=
                (x : WalkingMultispan (MultispanShape.prod D.J)) →
                  (D.diagram.multispan ⋙ F).obj x ≅ (D.mapGlueData F).diagram.multispan.obj x)
                x with
              | WalkingMultispan.left a => Iso.refl ((D.diagram.multispan ⋙ F).obj (WalkingMultispan.left a))
              | WalkingMultispan.right a => Iso.refl ((D.diagram.multispan ⋙ F).obj (WalkingMultispan.right a)) :
              (D.diagram.multispan ⋙ F).obj x ≅ (D.mapGlueData F).diagram.multispan.obj x))
          (WalkingMultispan.left (fst, snd))) ≫
      (D.mapGlueData F).diagram.multispan.map (WalkingMultispan.Hom.snd (fst, snd)))

Tactic:
simp
-- 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 : ∀ (i j k : D.J), PreservesLimit (cospan (D.f i j) (D.f i k)) F
a : (MultispanShape.prod D.J).R
⊢ (D.diagram.multispan ⋙ F).map (WalkingMultispan.Hom.id (WalkingMultispan.right a)) ≫
      Iso.hom
        ((fun (x : WalkingMultispan (MultispanShape.prod D.J)) ↦
            (match (motive :=
                (x : WalkingMultispan (MultispanShape.prod D.J)) →
                  (D.diagram.multispan ⋙ F).obj x ≅ (D.mapGlueData F).diagram.multispan.obj x)
                x with
              | WalkingMultispan.left a => Iso.refl ((D.diagram.multispan ⋙ F).obj (WalkingMultispan.left a))
              | WalkingMultispan.right a => Iso.refl ((D.diagram.multispan ⋙ F).obj (WalkingMultispan.right a)) :
              (D.diagram.multispan ⋙ F).obj x ≅ (D.mapGlueData F).diagram.multispan.obj x))
          (WalkingMultispan.right a)) =
    Iso.hom
        ((fun (x : WalkingMultispan (MultispanShape.prod D.J)) ↦
            (match (motive :=
                (x : WalkingMultispan (MultispanShape.prod D.J)) →
                  (D.diagram.multispan ⋙ F).obj x ≅ (D.mapGlueData F).diagram.multispan.obj x)
                x with
              | WalkingMultispan.left a => Iso.refl ((D.diagram.multispan ⋙ F).obj (WalkingMultispan.left a))
              | WalkingMultispan.right a => Iso.refl ((D.diagram.multispan ⋙ F).obj (WalkingMultispan.right a)) :
              (D.diagram.multispan ⋙ F).obj x ≅ (D.mapGlueData F).diagram.multispan.obj x))
          (WalkingMultispan.right a)) ≫
      (D.mapGlueData F).diagram.multispan.map (WalkingMultispan.Hom.id (WalkingMultispan.right a))

Tactic:
simp
-- 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 : ∀ (i j k : D.J), PreservesLimit (cospan (D.f i j) (D.f i k)) F
i : D.J × D.J
⊢ Eq (α :=
    (D.diagram.multispan ⋙ F).obj (WalkingMultispan.left i) ≅
      (D.mapGlueData F).diagram.multispan.obj (WalkingMultispan.left i))
    (Iso.app (D.diagramIso F) (WalkingMultispan.left i))
    (Iso.refl ((D.diagram.multispan ⋙ F).obj (WalkingMultispan.left i)))

Tactic:
rfl

Premises used: CategoryTheory.Iso.refl, CategoryTheory.Iso.app, rfl
-- 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 : ∀ (i j k : D.J), PreservesLimit (cospan (D.f i j) (D.f i k)) F
i : D.J
⊢ Eq (α :=
    (D.diagram.multispan ⋙ F).obj (WalkingMultispan.right i) ≅
      (D.mapGlueData F).diagram.multispan.obj (WalkingMultispan.right i))
    (Iso.app (D.diagramIso F) (WalkingMultispan.right i))
    (Iso.refl ((D.diagram.multispan ⋙ F).obj (WalkingMultispan.right i)))

Tactic:
rfl

Premises used: CategoryTheory.Iso.refl, CategoryTheory.Iso.app, rfl
-- 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 : ∀ (i j k : D.J), PreservesLimit (cospan (D.f i j) (D.f i k)) F
i : D.J × D.J
⊢ Eq (α :=
    (D.diagram.multispan ⋙ F).obj (WalkingMultispan.left i) ⟶
      (D.mapGlueData F).diagram.multispan.obj (WalkingMultispan.left i))
    (NatTrans.app (Iso.hom (D.diagramIso F)) (WalkingMultispan.left i))
    (𝟙 ((D.diagram.multispan ⋙ F).obj (WalkingMultispan.left i)))

Tactic:
rfl

Premises used: rfl
-- 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 : ∀ (i j k : D.J), PreservesLimit (cospan (D.f i j) (D.f i k)) F
i : D.J
⊢ Eq (α :=
    (D.diagram.multispan ⋙ F).obj (WalkingMultispan.right i) ⟶
      (D.mapGlueData F).diagram.multispan.obj (WalkingMultispan.right i))
    (NatTrans.app (Iso.hom (D.diagramIso F)) (WalkingMultispan.right i))
    (𝟙 ((D.diagram.multispan ⋙ F).obj (WalkingMultispan.right i)))

Tactic:
rfl

Premises used: rfl
-- 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 : ∀ (i j k : D.J), PreservesLimit (cospan (D.f i j) (D.f i k)) F
i : D.J × D.J
⊢ NatTrans.app (Iso.inv (D.diagramIso F)) (WalkingMultispan.left i) =
    𝟙 ((D.mapGlueData F).diagram.multispan.obj (WalkingMultispan.left i))

Tactic:
rfl

Premises used: rfl
-- 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 : ∀ (i j k : D.J), PreservesLimit (cospan (D.f i j) (D.f i k)) F
i : D.J
⊢ NatTrans.app (Iso.inv (D.diagramIso F)) (WalkingMultispan.right i) =
    𝟙 ((D.mapGlueData F).diagram.multispan.obj (WalkingMultispan.right i))

Tactic:
rfl

Premises used: rfl
-- 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
⊢ HasColimit (D.diagram.multispan ⋙ F)

Tactic:
⟨⟨⟨_, isColimitOfPreserves _ (colimit.isColimit _)⟩⟩⟩

Premises used: CategoryTheory.Limits.colimit.isColimit, Nonempty.intro, CategoryTheory.Limits.HasColimit.mk', CategoryTheory.Limits.ColimitCocone.mk, CategoryTheory.Limits.isColimitOfPreserves
-- 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
⊢ HasMulticoequalizer (D.mapGlueData F).diagram

Tactic:
hasColimit_of_iso (D.diagramIso F).symm

Premises used: CategoryTheory.GlueData.diagramIso, CategoryTheory.Limits.hasColimit_of_iso, CategoryTheory.Iso.symm
-- 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 : D.J
⊢ Eq (α := F.obj (D.U i) ⟶ (D.mapGlueData F).glued)
    (CategoryStruct.comp (Y := F.obj D.glued) (F.map (D.ι i)) (Iso.hom (D.gluedIso F)) :
      F.obj (D.U i) ⟶ (D.mapGlueData F).glued)
    ((D.mapGlueData F).ι i : (D.mapGlueData F).U i ⟶ (D.mapGlueData F).glued)

Tactic:
simp [gluedIso, GlueData.ι]

Premises used: CategoryTheory.GlueData.ι, CategoryTheory.GlueData.gluedIso
-- 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 : D.J
rw :
  Eq (α := (D.mapGlueData F).U i ⟶ (D.mapGlueData F).glued)
    ((D.mapGlueData F).ι i : (D.mapGlueData F).U i ⟶ (D.mapGlueData F).glued)
    (CategoryStruct.comp (Y := F.obj D.glued) (F.map (D.ι i)) (Iso.hom (D.gluedIso F)) :
      (D.mapGlueData F).U i ⟶ (D.mapGlueData F).glued)
rw₁ rw₂ : Eq (α := (D.mapGlueData F).U i ⟶ (D.mapGlueData F).glued) ((D.mapGlueData F).ι i) ((D.mapGlueData F).ι i)
⊢ Eq (α := (D.mapGlueData F).U i ⟶ F.obj D.glued)
    (CategoryStruct.comp (Y := (D.mapGlueData F).glued)
      ((D.mapGlueData F).ι i : (D.mapGlueData F).U i ⟶ (D.mapGlueData F).glued)
      (Iso.inv (D.gluedIso F) : (D.mapGlueData F).glued ⟶ F.obj D.glued))
    (F.map (D.ι i))

Tactic:
rw [Iso.comp_inv_eq, ι_gluedIso_hom]

Premises used: CategoryTheory.Iso.comp_inv_eq, CategoryTheory.GlueData.ι_gluedIso_hom
-- 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)
t : IsLimit (F := cospan (Z := D.glued) (D.ι i) (D.ι j) ⋙ F) (F.mapCone (D.vPullbackCone i j))
⊢ IsLimit (F := cospan (Z := D.glued) (D.ι i) (D.ι j)) (D.vPullbackCone i j)

Tactic:
apply isLimitOfReflects F

Premises used: CategoryTheory.Limits.isLimitOfReflects
-- 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)
apply :
  IsLimit (F := cospan (Z := F.obj D.glued) (F.map (D.ι i)) (F.map (D.ι j)))
    (PullbackCone.mk (F.map (D.f i j)) (F.map (D.t i j ≫ D.f j i)) ⋯)
⊢ IsLimit (F := cospan (Z := D.glued) (D.ι i) (D.ι j) ⋙ F) (F.mapCone (D.vPullbackCone i j))

Tactic:
apply (isLimitMapConePullbackConeEquiv _ _).symm _

Premises used: CategoryTheory.Limits.isLimitMapConePullbackConeEquiv, Equiv.symm, DFunLike.coe
-- 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)
x : WalkingCospan
none :
  (cospan (Z := F.obj D.glued) (F.map (D.ι i)) (F.map (D.ι j))).obj Option.none ≅
    (cospan (Z := (D.mapGlueData F).glued) ((D.mapGlueData F).ι i) ((D.mapGlueData F).ι j)).obj Option.none
some :
  (val : WalkingPair) →
    (cospan (Z := F.obj D.glued) (F.map (D.ι i)) (F.map (D.ι j))).obj (Option.some val) ≅
      (cospan (Z := (D.mapGlueData F).glued) ((D.mapGlueData F).ι i) ((D.mapGlueData F).ι j)).obj (Option.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

Tactic:
cases x
-- 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))).obj none ≅
    (cospan (Z := (D.mapGlueData F).glued) ((D.mapGlueData F).ι i) ((D.mapGlueData F).ι j)).obj none

Tactic:
exacts [D.gluedIso F, Iso.refl _]

Premises used: CategoryTheory.Iso.refl, CategoryTheory.GlueData.gluedIso
-- 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)
e : cospan (Z := F.obj D.glued) (F.map (D.ι i)) (F.map (D.ι j)) ≅
  cospan (Z := (D.mapGlueData F).glued) ((D.mapGlueData F).ι i) ((D.mapGlueData F).ι j) :=
  NatIso.ofComponents
    (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))) ⋯)
        ⋯)
    ⋯
apply : IsLimit ((Cone.postcompose e.hom).obj (PullbackCone.mk (F.map (D.f i j)) (F.map (D.t i j ≫ D.f j i)) ⋯))
⊢ IsLimit (F := cospan (Z := F.obj D.glued) (F.map (D.ι i)) (F.map (D.ι j)))
    (PullbackCone.mk (F.map (D.f i j)) (F.map (D.t i j ≫ D.f j i)) ⋯)

Tactic:
apply IsLimit.postcomposeHomEquiv e _ _

Premises used: CategoryTheory.Limits.IsLimit.postcomposeHomEquiv, DFunLike.coe
-- 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)
e : cospan (Z := F.obj D.glued) (F.map (D.ι i)) (F.map (D.ι j)) ≅
  cospan (Z := (D.mapGlueData F).glued) ((D.mapGlueData F).ι i) ((D.mapGlueData F).ι j) :=
  NatIso.ofComponents
    (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))) ⋯)
        ⋯)
    ⋯
apply :
  (D.mapGlueData F).vPullbackCone i j ≅
    (Cone.postcompose e.hom).obj (PullbackCone.mk (F.map (D.f i j)) (F.map (D.t i j ≫ D.f j i)) ⋯)
⊢ IsLimit ((Cone.postcompose e.hom).obj (PullbackCone.mk (F.map (D.f i j)) (F.map (D.t i j ≫ D.f j i)) ⋯))

Tactic:
apply hc.ofIsoLimit

Premises used: CategoryTheory.Limits.IsLimit.ofIsoLimit