awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.GlueData (goal)
Goal:
D : GlueData (Type v)
x : D.glued
⊢ ∃ (i : D.J) (y : D.U i),
    (ConcreteCategory.hom (FC := TypeCat.Fun) (D.ι i) :
          (a : (fun (X : Type v) ↦ X) (D.U i)) → (fun (X : Type v) ↦ X) D.glued)
        y =
      x
have delta : ∃ (i : D.J) (y : D.U i),
  (ConcreteCategory.hom (FC := TypeCat.Fun) (Multicoequalizer.π D.diagram i) :
        (a : (fun (X : Type v) ↦ X) (D.U i)) → (fun (X : Type v) ↦ X) D.glued)
      y =
    x
Tactic: delta CategoryTheory.GlueData.ι
-- Lean 4 proof step from Mathlib.CategoryTheory.GlueData (goal)
Goal:
D : GlueData (Type v)
x : D.glued
⊢ ∃ (i : D.J) (y : D.U i),
    (ConcreteCategory.hom (FC := TypeCat.Fun) (Multicoequalizer.π D.diagram i) :
          (a : (fun (X : Type v) ↦ X) (D.U i)) → (fun (X : Type v) ↦ X) D.glued)
        y =
      x
have simp_rw : ∃ (i : D.J) (y : D.U i),
  (ConcreteCategory.hom (FC := TypeCat.Fun)
          (CategoryStruct.comp (Y := ∐ D.diagram.right) (Sigma.ι D.diagram.right i)
            (Multicoequalizer.sigmaπ D.diagram)) :
        (a : D.U i) → D.glued)
      y =
    x
Tactic: simp_rw [← Multicoequalizer.ι_sigmaπ D.diagram]
-- Lean 4 proof step from Mathlib.CategoryTheory.GlueData (goal)
Goal:
D : GlueData (Type v)
x : D.glued
⊢ ∃ (i : D.J) (y : D.U i),
    (ConcreteCategory.hom (FC := TypeCat.Fun)
            (CategoryStruct.comp (Y := ∐ D.diagram.right) (Sigma.ι D.diagram.right i)
              (Multicoequalizer.sigmaπ D.diagram)) :
          (a : D.U i) → D.glued)
        y =
      x
have rcases : ∀ (x' : D.sigmaOpens),
  ∃ (i : D.J) (y : D.U i),
    Eq (α := D.glued)
      ((ConcreteCategory.hom (FC := TypeCat.Fun)
              (CategoryStruct.comp (Y := ∐ D.diagram.right) (Sigma.ι D.diagram.right i)
                (Multicoequalizer.sigmaπ D.diagram)) :
            (a : D.U i) → D.glued)
          y :
        D.glued)
      (((ConcreteCategory.hom (FC := TypeCat.Fun) D.π : TypeCat.Fun D.sigmaOpens D.glued) :
            (a : (fun (X : Type v) ↦ X) D.sigmaOpens) → (fun (X : Type v) ↦ X) D.glued)
          x' :
        (fun (X : Type v) ↦ X) D.glued)
Tactic: rcases D.types_π_surjective x with ⟨x', rfl⟩
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.CategoryTheory.GlueData (goal)
Goal:
D : GlueData (Type v)
x' : D.sigmaOpens
⊢ ∃ (i : D.J) (y : D.U i),
    Eq (α := D.glued)
      ((ConcreteCategory.hom (FC := TypeCat.Fun)
              (CategoryStruct.comp (Y := ∐ D.diagram.right) (Sigma.ι D.diagram.right i)
                (Multicoequalizer.sigmaπ D.diagram)) :
            (a : D.U i) → D.glued)
          y :
        D.glued)
      (((ConcreteCategory.hom (FC := TypeCat.Fun) D.π : TypeCat.Fun D.sigmaOpens D.glued) :
            (a : (fun (X : Type v) ↦ X) D.sigmaOpens) → (fun (X : Type v) ↦ X) D.glued)
          x' :
        (fun (X : Type v) ↦ X) D.glued)
have rw : ∃ (i : D.J) (y : D.U i),
  Eq (α := D.glued)
    ((ConcreteCategory.hom (FC := TypeCat.Fun)
            (CategoryStruct.comp (Y := ∐ D.diagram.right) (Sigma.ι D.diagram.right i)
              (Multicoequalizer.sigmaπ D.diagram)) :
          (a : D.U i) → D.glued)
        y :
      D.glued)
    (((ConcreteCategory.hom (FC := TypeCat.Fun) D.π : TypeCat.Fun D.sigmaOpens D.glued) :
          (a : (fun (X : Type v) ↦ X) D.sigmaOpens) → (fun (X : Type v) ↦ X) D.glued)
        ((ConcreteCategory.hom (FC := TypeCat.Fun)
                (Iso.inv (colimit.isoColimitCocone (Types.coproductColimitCocone D.U))) :
              (a : (Types.coproductColimitCocone D.U).cocone.pt) → colimit (Discrete.functor D.U))
            ((ConcreteCategory.hom (FC := TypeCat.Fun)
                    (Iso.hom (colimit.isoColimitCocone (Types.coproductColimitCocone D.U))) :
                  (a : colimit (Discrete.functor D.U)) → (Types.coproductColimitCocone D.U).cocone.pt)
                x' :
              (Types.coproductColimitCocone D.U).cocone.pt) :
          colimit (Discrete.functor D.U)) :
      (fun (X : Type v) ↦ X) D.glued)
Tactic: rw [← dsimp% ConcreteCategory.congr_hom
    (colimit.isoColimitCocone (Types.coproductColimitCocone _)).hom_inv_id x']
-- Lean 4 proof step from Mathlib.CategoryTheory.GlueData (goal)
Goal:
D : GlueData (Type v)
x' : D.sigmaOpens
⊢ ∃ (i : D.J) (y : D.U i),
    Eq (α := D.glued)
      ((ConcreteCategory.hom (FC := TypeCat.Fun)
              (CategoryStruct.comp (Y := ∐ D.diagram.right) (Sigma.ι D.diagram.right i)
                (Multicoequalizer.sigmaπ D.diagram)) :
            (a : D.U i) → D.glued)
          y :
        D.glued)
      (((ConcreteCategory.hom (FC := TypeCat.Fun) D.π : TypeCat.Fun D.sigmaOpens D.glued) :
            (a : (fun (X : Type v) ↦ X) D.sigmaOpens) → (fun (X : Type v) ↦ X) D.glued)
          ((ConcreteCategory.hom (FC := TypeCat.Fun)
                  (Iso.inv (colimit.isoColimitCocone (Types.coproductColimitCocone D.U))) :
                (a : (Types.coproductColimitCocone D.U).cocone.pt) → colimit (Discrete.functor D.U))
              ((ConcreteCategory.hom (FC := TypeCat.Fun)
                      (Iso.hom (colimit.isoColimitCocone (Types.coproductColimitCocone D.U))) :
                    (a : colimit (Discrete.functor D.U)) → (Types.coproductColimitCocone D.U).cocone.pt)
                  x' :
                (Types.coproductColimitCocone D.U).cocone.pt) :
            colimit (Discrete.functor D.U)) :
        (fun (X : Type v) ↦ X) D.glued)
have rcases : ∀ (i : D.J) (y : D.U i),
  ∃ (i_1 : D.J) (y_1 : D.U i_1),
    Eq (α := D.glued)
      ((ConcreteCategory.hom (FC := TypeCat.Fun)
              (CategoryStruct.comp (Y := ∐ D.diagram.right) (Sigma.ι D.diagram.right i_1)
                (Multicoequalizer.sigmaπ D.diagram)) :
            (a : D.U i_1) → D.glued)
          y_1 :
        D.glued)
      (((ConcreteCategory.hom (FC := TypeCat.Fun) D.π : TypeCat.Fun D.sigmaOpens D.glued) :
            (a : (fun (X : Type v) ↦ X) D.sigmaOpens) → (fun (X : Type v) ↦ X) D.glued)
          ((ConcreteCategory.hom (FC := TypeCat.Fun)
                  (Iso.inv (colimit.isoColimitCocone (Types.coproductColimitCocone D.U))) :
                (a : (Types.coproductColimitCocone D.U).cocone.pt) → colimit (Discrete.functor D.U))
              (Sigma.mk (β := fun (j : D.J) ↦ D.U j) i y) :
            colimit (Discrete.functor D.U)) :
        (fun (X : Type v) ↦ X) D.glued)
Tactic: rcases (colimit.isoColimitCocone (Types.coproductColimitCocone _)).hom x' with ⟨i, y⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.GlueData (goal)
Goal:
D : GlueData (Type v)
x' : D.sigmaOpens
i : D.J
y : D.U i
⊢ ∃ (i_1 : D.J) (y_1 : D.U i_1),
    Eq (α := D.glued)
      ((ConcreteCategory.hom (FC := TypeCat.Fun)
              (CategoryStruct.comp (Y := ∐ D.diagram.right) (Sigma.ι D.diagram.right i_1)
                (Multicoequalizer.sigmaπ D.diagram)) :
            (a : D.U i_1) → D.glued)
          y_1 :
        D.glued)
      (((ConcreteCategory.hom (FC := TypeCat.Fun) D.π : TypeCat.Fun D.sigmaOpens D.glued) :
            (a : (fun (X : Type v) ↦ X) D.sigmaOpens) → (fun (X : Type v) ↦ X) D.glued)
          ((ConcreteCategory.hom (FC := TypeCat.Fun)
                  (Iso.inv (colimit.isoColimitCocone (Types.coproductColimitCocone D.U))) :
                (a : (Types.coproductColimitCocone D.U).cocone.pt) → colimit (Discrete.functor D.U))
              (Sigma.mk (β := fun (j : D.J) ↦ D.U j) i y) :
            colimit (Discrete.functor D.U)) :
        (fun (X : Type v) ↦ X) D.glued)
have refine : Eq (α := D.glued)
  ((ConcreteCategory.hom (FC := TypeCat.Fun)
          (CategoryStruct.comp (Y := ∐ D.diagram.right) (Sigma.ι D.diagram.right i)
            (Multicoequalizer.sigmaπ D.diagram)) :
        (a : D.U i) → D.glued)
      y :
    D.glued)
  (((ConcreteCategory.hom (FC := TypeCat.Fun) D.π : TypeCat.Fun D.sigmaOpens D.glued) :
        (a : (fun (X : Type v) ↦ X) D.sigmaOpens) → (fun (X : Type v) ↦ X) D.glued)
      ((ConcreteCategory.hom (FC := TypeCat.Fun)
              (Iso.inv (colimit.isoColimitCocone (Types.coproductColimitCocone D.U))) :
            (a : (Types.coproductColimitCocone D.U).cocone.pt) → colimit (Discrete.functor D.U))
          (Sigma.mk (β := fun (j : D.J) ↦ D.U j) i y) :
        colimit (Discrete.functor D.U)) :
    (fun (X : Type v) ↦ X) D.glued)
Tactic: refine ⟨i, y, ?_⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.GlueData (goal)
Goal:
D : GlueData (Type v)
x' : D.sigmaOpens
i : D.J
y : D.U i
⊢ Eq (α := D.glued)
    ((ConcreteCategory.hom (FC := TypeCat.Fun)
            (CategoryStruct.comp (Y := ∐ D.diagram.right) (Sigma.ι D.diagram.right i)
              (Multicoequalizer.sigmaπ D.diagram)) :
          (a : D.U i) → D.glued)
        y :
      D.glued)
    (((ConcreteCategory.hom (FC := TypeCat.Fun) D.π : TypeCat.Fun D.sigmaOpens D.glued) :
          (a : (fun (X : Type v) ↦ X) D.sigmaOpens) → (fun (X : Type v) ↦ X) D.glued)
        ((ConcreteCategory.hom (FC := TypeCat.Fun)
                (Iso.inv (colimit.isoColimitCocone (Types.coproductColimitCocone D.U))) :
              (a : (Types.coproductColimitCocone D.U).cocone.pt) → colimit (Discrete.functor D.U))
            (Sigma.mk (β := fun (j : D.J) ↦ D.U j) i y) :
          colimit (Discrete.functor D.U)) :
      (fun (X : Type v) ↦ X) D.glued)
have simp : Eq (α := D.glued)
  ((ConcreteCategory.hom (FC := TypeCat.Fun)
          (CategoryStruct.comp (Y := ∐ D.U) (Sigma.ι D.U i) (Multicoequalizer.sigmaπ D.diagram)) :
        (a : D.U i) → D.glued)
      y :
    D.glued)
  (((ConcreteCategory.hom (FC := TypeCat.Fun) D.π : TypeCat.Fun D.sigmaOpens D.glued) : (a : D.sigmaOpens) → D.glued)
      ((ConcreteCategory.hom (FC := TypeCat.Fun)
              (Iso.inv (colimit.isoColimitCocone (Types.coproductColimitCocone D.U))) :
            (a : (Types.coproductColimitCocone D.U).cocone.pt) → colimit (Discrete.functor D.U))
          (Sigma.mk (β := fun (j : D.J) ↦ D.U j) i y) :
        colimit (Discrete.functor D.U)) :
    D.glued)
Tactic: simp
-- Lean 4 proof step from Mathlib.CategoryTheory.GlueData (goal)
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 (α := (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))
have 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)
Tactic: rw [Iso.comp_inv_eq, ι_gluedIso_hom]
-- Lean 4 proof step from Mathlib.CategoryTheory.GlueData (goal)
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)
⊢ 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))
have rw₁ : Eq (α := (D.mapGlueData F).U i ⟶ (D.mapGlueData F).glued) ((D.mapGlueData F).ι i) ((D.mapGlueData F).ι i)
Tactic: rw [Iso.comp_inv_eq, ι_gluedIso_hom]
-- Lean 4 proof step from Mathlib.CategoryTheory.GlueData (goal)
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)
⊢ IsLimit (F := cospan (Z := D.glued) (D.ι i) (D.ι j)) (D.vPullbackCone i j)
have t : IsLimit (F := cospan (Z := D.glued) (D.ι i) (D.ι j) ⋙ F) (F.mapCone (D.vPullbackCone i j))
Tactic: apply isLimitOfReflects F
-- Lean 4 proof step from Mathlib.CategoryTheory.GlueData (goal)
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)
⊢ IsLimit (F := cospan (Z := D.glued) (D.ι i) (D.ι j) ⋙ F) (F.mapCone (D.vPullbackCone i j))
have 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)) sorry)
Tactic: apply (isLimitMapConePullbackConeEquiv _ _).symm _
-- Lean 4 proof step from Mathlib.CategoryTheory.GlueData (goal)
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
⊢ (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
have none : (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: cases x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.CategoryTheory.GlueData (goal)
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
⊢ (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
have some : (val : WalkingPair) →
  (cospan (Z := F.obj D.glued) (F.map (D.ι i)) (F.map (D.ι j))).obj (some val) ≅
    (cospan (Z := (D.mapGlueData F).glued) ((D.mapGlueData F).ι i) ((D.mapGlueData F).ι j)).obj (some val)
Tactic: cases x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.CategoryTheory.GlueData (goal)
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))) ⋯)
        ⋯)
    ⋯
⊢ 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)) ⋯)
have 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)) sorry))
Tactic: apply IsLimit.postcomposeHomEquiv e _ _
-- Lean 4 proof step from Mathlib.CategoryTheory.GlueData (goal)
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))) ⋯)
        ⋯)
    ⋯
⊢ IsLimit ((Cone.postcompose e.hom).obj (PullbackCone.mk (F.map (D.f i j)) (F.map (D.t i j ≫ D.f j i)) ⋯))
have 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)) sorry)
Tactic: apply hc.ofIsoLimit
-- Lean 4 proof step from Mathlib.CategoryTheory.GlueData (goal)
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))) ⋯)
        ⋯)
    ⋯
⊢ (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)) ⋯)
have refine : ∀ (j_1 : WalkingCospan),
  NatTrans.app (Cone.π ((D.mapGlueData F).vPullbackCone i j)) j_1 =
    Iso.hom
        (Iso.refl
          (Cone.pt (F := cospan (Z := (D.mapGlueData F).glued) ((D.mapGlueData F).ι i) ((D.mapGlueData F).ι j))
            ((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)) sorry)).π.app j_1
Tactic: refine Cone.ext (Iso.refl _) ?_