awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Diagonal (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X Y : C
inst_1 : HasPullbacks.{v_1, u_1} C
S T : C
f : X ⟶ T
g : Y ⟶ T
i : T ⟶ S
inst_2 : HasPullback i i
inst_3 : HasPullback f g
inst_4 : HasPullback (f ≫ i) (g ≫ i)
inst_5 :
  HasPullback (Y := pullback (f ≫ i) (g ≫ i)) (Z := diagonalObj i) (diagonal i) (map (f ≫ i) (g ≫ i) i i f g (𝟙 S) ⋯ ⋯)
⊢ CommSq (W := pullback f g) (Y := pullback (f ≫ i) (g ≫ i)) (Z := diagonalObj i) (fst f g ≫ f)
    (map f g (f ≫ i) (g ≫ i) (𝟙 X) (𝟙 Y) i ⋯ ⋯) (diagonal i) (map (f ≫ i) (g ≫ i) i i f g (𝟙 S) ⋯ ⋯)
have w : autoParam
  (Eq (α := pullback f g ⟶ diagonalObj i) ((fst f g ≫ f) ≫ diagonal i)
    (CategoryStruct.comp (Y := pullback (f ≫ i) (g ≫ i)) (map f g (f ≫ i) (g ≫ i) (𝟙 X) (𝟙 Y) i sorry sorry)
      (map (f ≫ i) (g ≫ i) i i f g (𝟙 S) sorry sorry)))
  CommSq.w._autoParam
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Diagonal (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X Y : C
inst_1 : HasPullbacks.{v_1, u_1} C
S T : C
f : X ⟶ T
g : Y ⟶ T
i : T ⟶ S
inst_2 : HasPullback i i
inst_3 : HasPullback f g
inst_4 : HasPullback (f ≫ i) (g ≫ i)
inst_5 :
  HasPullback (Y := pullback (f ≫ i) (g ≫ i)) (Z := diagonalObj i) (diagonal i) (map (f ≫ i) (g ≫ i) i i f g (𝟙 S) ⋯ ⋯)
⊢ autoParam
    (Eq (α := pullback f g ⟶ diagonalObj i) ((fst f g ≫ f) ≫ diagonal i)
      (CategoryStruct.comp (Y := pullback (f ≫ i) (g ≫ i)) (map f g (f ≫ i) (g ≫ i) (𝟙 X) (𝟙 Y) i ⋯ ⋯)
        (map (f ≫ i) (g ≫ i) i i f g (𝟙 S) ⋯ ⋯)))
    CommSq.w._autoParam
have w : Eq (α := pullback f g ⟶ T) (CategoryStruct.comp (Y := pullback i i) ((fst f g ≫ f) ≫ diagonal i) (fst i i))
  (CategoryStruct.comp (Y := pullback i i)
    (CategoryStruct.comp (Y := pullback (f ≫ i) (g ≫ i)) (map f g (f ≫ i) (g ≫ i) (𝟙 X) (𝟙 Y) i sorry sorry)
      (map (f ≫ i) (g ≫ i) i i f g (𝟙 S) sorry sorry))
    (fst i i))
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Diagonal (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X Y : C
inst_1 : HasPullbacks.{v_1, u_1} C
S T : C
f : X ⟶ T
g : Y ⟶ T
i : T ⟶ S
inst_2 : HasPullback i i
inst_3 : HasPullback f g
inst_4 : HasPullback (f ≫ i) (g ≫ i)
inst_5 :
  HasPullback (Y := pullback (f ≫ i) (g ≫ i)) (Z := diagonalObj i) (diagonal i) (map (f ≫ i) (g ≫ i) i i f g (𝟙 S) ⋯ ⋯)
w :
  Eq (α := pullback f g ⟶ T) (CategoryStruct.comp (Y := pullback i i) ((fst f g ≫ f) ≫ diagonal i) (fst i i))
    (CategoryStruct.comp (Y := pullback i i)
      (CategoryStruct.comp (Y := pullback (f ≫ i) (g ≫ i)) (map f g (f ≫ i) (g ≫ i) (𝟙 X) (𝟙 Y) i ⋯ ⋯)
        (map (f ≫ i) (g ≫ i) i i f g (𝟙 S) ⋯ ⋯))
      (fst i i))
⊢ autoParam
    (Eq (α := pullback f g ⟶ diagonalObj i) ((fst f g ≫ f) ≫ diagonal i)
      (CategoryStruct.comp (Y := pullback (f ≫ i) (g ≫ i)) (map f g (f ≫ i) (g ≫ i) (𝟙 X) (𝟙 Y) i ⋯ ⋯)
        (map (f ≫ i) (g ≫ i) i i f g (𝟙 S) ⋯ ⋯)))
    CommSq.w._autoParam
have w₁ : Eq (α := pullback f g ⟶ T) (CategoryStruct.comp (Y := pullback i i) ((fst f g ≫ f) ≫ diagonal i) (snd i i))
  (CategoryStruct.comp (Y := pullback i i)
    (CategoryStruct.comp (Y := pullback (f ≫ i) (g ≫ i)) (map f g (f ≫ i) (g ≫ i) (𝟙 X) (𝟙 Y) i sorry sorry)
      (map (f ≫ i) (g ≫ i) i i f g (𝟙 S) sorry sorry))
    (snd i i))
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Diagonal (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasPullbacks.{v_1, u_1} C
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
⊢ Eq (α := diagonalObj (X := pullback f g) (fst f g) ⟶ Y)
    (CategoryStruct.comp (Y := pullback (X := diagonalObj g) (snd g g ≫ g) f)
        (Iso.hom (diagonalObjPullbackFstIso f g) :
          diagonalObj (X := pullback f g) (fst f g) ⟶ pullback (X := diagonalObj g) (snd g g ≫ g) f)
        (fst (snd g g ≫ g) f ≫ fst g g : pullback (X := diagonalObj g) (snd g g ≫ g) f ⟶ Y) :
      diagonalObj (X := pullback f g) (fst f g) ⟶ Y)
    (fst (fst f g) (fst f g) ≫ snd f g : pullback (X := pullback f g) (Y := pullback f g) (fst f g) (fst f g) ⟶ Y)
have delta : Eq (α := diagonalObj (X := pullback f g) (fst f g) ⟶ Y)
  (CategoryStruct.comp (Y := pullback (X := diagonalObj g) (snd g g ≫ g) f)
      (Iso.hom
          (pullbackRightPullbackFstIso f g (fst f g) ≪≫
            Iso.trans (Y := pullback (X := pullback f g) (snd f g ≫ g) g)
              (congrHom sorry sorry :
                pullback (X := pullback f g) (fst f g ≫ f) g ≅ pullback (X := pullback f g) (snd f g ≫ g) g)
              (Iso.trans (Y := pullback (Y := pullback g g) f (fst g g ≫ g))
                  (pullbackAssoc f g g g :
                    pullback (X := pullback f g) (snd f g ≫ g) g ≅ pullback (Y := pullback g g) f (fst g g ≫ g))
                  (pullbackSymmetry f (fst g g ≫ g) ≪≫ congrHom sorry sorry :
                    pullback (Y := pullback g g) f (fst g g ≫ g) ≅ pullback (X := diagonalObj g) (snd g g ≫ g) f) :
                pullback (X := pullback f g) (snd f g ≫ g) g ≅ pullback (X := diagonalObj g) (snd g g ≫ g) f)) :
        diagonalObj (X := pullback f g) (fst f g) ⟶ pullback (X := diagonalObj g) (snd g g ≫ g) f)
      (fst (snd g g ≫ g) f ≫ fst g g : pullback (X := diagonalObj g) (snd g g ≫ g) f ⟶ Y) :
    diagonalObj (X := pullback f g) (fst f g) ⟶ Y)
  (fst (fst f g) (fst f g) ≫ snd f g : pullback (X := pullback f g) (Y := pullback f g) (fst f g) (fst f g) ⟶ Y)
Tactic: delta diagonalObjPullbackFstIso
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Diagonal (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasPullbacks.{v_1, u_1} C
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
⊢ Eq (α := diagonalObj (X := pullback f g) (fst f g) ⟶ Y)
    (CategoryStruct.comp (Y := pullback (X := diagonalObj g) (snd g g ≫ g) f)
        (Iso.hom (diagonalObjPullbackFstIso f g) :
          diagonalObj (X := pullback f g) (fst f g) ⟶ pullback (X := diagonalObj g) (snd g g ≫ g) f)
        (fst (snd g g ≫ g) f ≫ snd g g : pullback (X := diagonalObj g) (snd g g ≫ g) f ⟶ Y) :
      diagonalObj (X := pullback f g) (fst f g) ⟶ Y)
    (snd (fst f g) (fst f g) ≫ snd f g : pullback (X := pullback f g) (Y := pullback f g) (fst f g) (fst f g) ⟶ Y)
have delta : Eq (α := diagonalObj (X := pullback f g) (fst f g) ⟶ Y)
  (CategoryStruct.comp (Y := pullback (X := diagonalObj g) (snd g g ≫ g) f)
      (Iso.hom
          (pullbackRightPullbackFstIso f g (fst f g) ≪≫
            Iso.trans (Y := pullback (X := pullback f g) (snd f g ≫ g) g)
              (congrHom sorry sorry :
                pullback (X := pullback f g) (fst f g ≫ f) g ≅ pullback (X := pullback f g) (snd f g ≫ g) g)
              (Iso.trans (Y := pullback (Y := pullback g g) f (fst g g ≫ g))
                  (pullbackAssoc f g g g :
                    pullback (X := pullback f g) (snd f g ≫ g) g ≅ pullback (Y := pullback g g) f (fst g g ≫ g))
                  (pullbackSymmetry f (fst g g ≫ g) ≪≫ congrHom sorry sorry :
                    pullback (Y := pullback g g) f (fst g g ≫ g) ≅ pullback (X := diagonalObj g) (snd g g ≫ g) f) :
                pullback (X := pullback f g) (snd f g ≫ g) g ≅ pullback (X := diagonalObj g) (snd g g ≫ g) f)) :
        diagonalObj (X := pullback f g) (fst f g) ⟶ pullback (X := diagonalObj g) (snd g g ≫ g) f)
      (fst (snd g g ≫ g) f ≫ snd g g : pullback (X := diagonalObj g) (snd g g ≫ g) f ⟶ Y) :
    diagonalObj (X := pullback f g) (fst f g) ⟶ Y)
  (snd (fst f g) (fst f g) ≫ snd f g : pullback (X := pullback f g) (Y := pullback f g) (fst f g) (fst f g) ⟶ Y)
Tactic: delta diagonalObjPullbackFstIso
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Diagonal (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasPullbacks.{v_1, u_1} C
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
⊢ Eq (α := diagonalObj (X := pullback f g) (fst f g) ⟶ X)
    (CategoryStruct.comp (Y := pullback (X := diagonalObj g) (snd g g ≫ g) f)
        (Iso.hom (diagonalObjPullbackFstIso f g) :
          diagonalObj (X := pullback f g) (fst f g) ⟶ pullback (X := diagonalObj g) (snd g g ≫ g) f)
        (snd (snd g g ≫ g) f : pullback (X := diagonalObj g) (snd g g ≫ g) f ⟶ X) :
      diagonalObj (X := pullback f g) (fst f g) ⟶ X)
    (fst (fst f g) (fst f g) ≫ fst f g : pullback (X := pullback f g) (Y := pullback f g) (fst f g) (fst f g) ⟶ X)
have delta : Eq (α := diagonalObj (X := pullback f g) (fst f g) ⟶ X)
  (CategoryStruct.comp (Y := pullback (X := diagonalObj g) (snd g g ≫ g) f)
      (Iso.hom
          (pullbackRightPullbackFstIso f g (fst f g) ≪≫
            Iso.trans (Y := pullback (X := pullback f g) (snd f g ≫ g) g)
              (congrHom sorry sorry :
                pullback (X := pullback f g) (fst f g ≫ f) g ≅ pullback (X := pullback f g) (snd f g ≫ g) g)
              (Iso.trans (Y := pullback (Y := pullback g g) f (fst g g ≫ g))
                  (pullbackAssoc f g g g :
                    pullback (X := pullback f g) (snd f g ≫ g) g ≅ pullback (Y := pullback g g) f (fst g g ≫ g))
                  (pullbackSymmetry f (fst g g ≫ g) ≪≫ congrHom sorry sorry :
                    pullback (Y := pullback g g) f (fst g g ≫ g) ≅ pullback (X := diagonalObj g) (snd g g ≫ g) f) :
                pullback (X := pullback f g) (snd f g ≫ g) g ≅ pullback (X := diagonalObj g) (snd g g ≫ g) f)) :
        diagonalObj (X := pullback f g) (fst f g) ⟶ pullback (X := diagonalObj g) (snd g g ≫ g) f)
      (snd (snd g g ≫ g) f : pullback (X := diagonalObj g) (snd g g ≫ g) f ⟶ X) :
    diagonalObj (X := pullback f g) (fst f g) ⟶ X)
  (fst (fst f g) (fst f g) ≫ fst f g : pullback (X := pullback f g) (Y := pullback f g) (fst f g) (fst f g) ⟶ X)
Tactic: delta diagonalObjPullbackFstIso
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Diagonal (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasPullbacks.{v_1, u_1} C
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
⊢ Eq (α := pullback (X := diagonalObj g) (snd g g ≫ g) f ⟶ X)
    (CategoryStruct.comp (Y := diagonalObj (X := pullback f g) (fst f g))
        (Iso.inv (diagonalObjPullbackFstIso f g) :
          pullback (X := diagonalObj g) (snd g g ≫ g) f ⟶ diagonalObj (X := pullback f g) (fst f g))
        (fst (fst f g) (fst f g) ≫ fst f g : diagonalObj (X := pullback f g) (fst f g) ⟶ X) :
      pullback (X := diagonalObj g) (snd g g ≫ g) f ⟶ X)
    (snd (snd g g ≫ g) f : pullback (X := diagonalObj g) (snd g g ≫ g) f ⟶ X)
have delta : Eq (α := pullback (X := diagonalObj g) (snd g g ≫ g) f ⟶ X)
  (CategoryStruct.comp (Y := diagonalObj (X := pullback f g) (fst f g))
      (Iso.inv
          (pullbackRightPullbackFstIso f g (fst f g) ≪≫
            Iso.trans (Y := pullback (X := pullback f g) (snd f g ≫ g) g)
              (congrHom sorry sorry :
                pullback (X := pullback f g) (fst f g ≫ f) g ≅ pullback (X := pullback f g) (snd f g ≫ g) g)
              (Iso.trans (Y := pullback (Y := pullback g g) f (fst g g ≫ g))
                  (pullbackAssoc f g g g :
                    pullback (X := pullback f g) (snd f g ≫ g) g ≅ pullback (Y := pullback g g) f (fst g g ≫ g))
                  (pullbackSymmetry f (fst g g ≫ g) ≪≫ congrHom sorry sorry :
                    pullback (Y := pullback g g) f (fst g g ≫ g) ≅ pullback (X := diagonalObj g) (snd g g ≫ g) f) :
                pullback (X := pullback f g) (snd f g ≫ g) g ≅ pullback (X := diagonalObj g) (snd g g ≫ g) f)) :
        pullback (X := diagonalObj g) (snd g g ≫ g) f ⟶ diagonalObj (X := pullback f g) (fst f g))
      (fst (fst f g) (fst f g) ≫ fst f g : diagonalObj (X := pullback f g) (fst f g) ⟶ X) :
    pullback (X := diagonalObj g) (snd g g ≫ g) f ⟶ X)
  (snd (snd g g ≫ g) f : pullback (X := diagonalObj g) (snd g g ≫ g) f ⟶ X)
Tactic: delta diagonalObjPullbackFstIso
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Diagonal (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasPullbacks.{v_1, u_1} C
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
⊢ Eq (α := pullback (X := diagonalObj g) (snd g g ≫ g) f ⟶ Y)
    (CategoryStruct.comp (Y := diagonalObj (X := pullback f g) (fst f g))
        (Iso.inv (diagonalObjPullbackFstIso f g) :
          pullback (X := diagonalObj g) (snd g g ≫ g) f ⟶ diagonalObj (X := pullback f g) (fst f g))
        (fst (fst f g) (fst f g) ≫ snd f g : diagonalObj (X := pullback f g) (fst f g) ⟶ Y) :
      pullback (X := diagonalObj g) (snd g g ≫ g) f ⟶ Y)
    (fst (snd g g ≫ g) f ≫ fst g g : pullback (X := pullback g g) (snd g g ≫ g) f ⟶ Y)
have delta : Eq (α := pullback (X := diagonalObj g) (snd g g ≫ g) f ⟶ Y)
  (CategoryStruct.comp (Y := diagonalObj (X := pullback f g) (fst f g))
      (Iso.inv
          (pullbackRightPullbackFstIso f g (fst f g) ≪≫
            Iso.trans (Y := pullback (X := pullback f g) (snd f g ≫ g) g)
              (congrHom sorry sorry :
                pullback (X := pullback f g) (fst f g ≫ f) g ≅ pullback (X := pullback f g) (snd f g ≫ g) g)
              (Iso.trans (Y := pullback (Y := pullback g g) f (fst g g ≫ g))
                  (pullbackAssoc f g g g :
                    pullback (X := pullback f g) (snd f g ≫ g) g ≅ pullback (Y := pullback g g) f (fst g g ≫ g))
                  (pullbackSymmetry f (fst g g ≫ g) ≪≫ congrHom sorry sorry :
                    pullback (Y := pullback g g) f (fst g g ≫ g) ≅ pullback (X := diagonalObj g) (snd g g ≫ g) f) :
                pullback (X := pullback f g) (snd f g ≫ g) g ≅ pullback (X := diagonalObj g) (snd g g ≫ g) f)) :
        pullback (X := diagonalObj g) (snd g g ≫ g) f ⟶ diagonalObj (X := pullback f g) (fst f g))
      (fst (fst f g) (fst f g) ≫ snd f g : diagonalObj (X := pullback f g) (fst f g) ⟶ Y) :
    pullback (X := diagonalObj g) (snd g g ≫ g) f ⟶ Y)
  (fst (snd g g ≫ g) f ≫ fst g g : pullback (X := pullback g g) (snd g g ≫ g) f ⟶ Y)
Tactic: delta diagonalObjPullbackFstIso
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Diagonal (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasPullbacks.{v_1, u_1} C
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
⊢ Eq (α := pullback (X := diagonalObj g) (snd g g ≫ g) f ⟶ X)
    (CategoryStruct.comp (Y := diagonalObj (X := pullback f g) (fst f g))
        (Iso.inv (diagonalObjPullbackFstIso f g) :
          pullback (X := diagonalObj g) (snd g g ≫ g) f ⟶ diagonalObj (X := pullback f g) (fst f g))
        (snd (fst f g) (fst f g) ≫ fst f g : diagonalObj (X := pullback f g) (fst f g) ⟶ X) :
      pullback (X := diagonalObj g) (snd g g ≫ g) f ⟶ X)
    (snd (snd g g ≫ g) f : pullback (X := diagonalObj g) (snd g g ≫ g) f ⟶ X)
have delta : Eq (α := pullback (X := diagonalObj g) (snd g g ≫ g) f ⟶ X)
  (CategoryStruct.comp (Y := diagonalObj (X := pullback f g) (fst f g))
      (Iso.inv
          (pullbackRightPullbackFstIso f g (fst f g) ≪≫
            Iso.trans (Y := pullback (X := pullback f g) (snd f g ≫ g) g)
              (congrHom sorry sorry :
                pullback (X := pullback f g) (fst f g ≫ f) g ≅ pullback (X := pullback f g) (snd f g ≫ g) g)
              (Iso.trans (Y := pullback (Y := pullback g g) f (fst g g ≫ g))
                  (pullbackAssoc f g g g :
                    pullback (X := pullback f g) (snd f g ≫ g) g ≅ pullback (Y := pullback g g) f (fst g g ≫ g))
                  (pullbackSymmetry f (fst g g ≫ g) ≪≫ congrHom sorry sorry :
                    pullback (Y := pullback g g) f (fst g g ≫ g) ≅ pullback (X := diagonalObj g) (snd g g ≫ g) f) :
                pullback (X := pullback f g) (snd f g ≫ g) g ≅ pullback (X := diagonalObj g) (snd g g ≫ g) f)) :
        pullback (X := diagonalObj g) (snd g g ≫ g) f ⟶ diagonalObj (X := pullback f g) (fst f g))
      (snd (fst f g) (fst f g) ≫ fst f g : diagonalObj (X := pullback f g) (fst f g) ⟶ X) :
    pullback (X := diagonalObj g) (snd g g ≫ g) f ⟶ X)
  (snd (snd g g ≫ g) f : pullback (X := diagonalObj g) (snd g g ≫ g) f ⟶ X)
Tactic: delta diagonalObjPullbackFstIso
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Diagonal (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasPullbacks.{v_1, u_1} C
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
⊢ Eq (α := pullback (X := diagonalObj g) (snd g g ≫ g) f ⟶ Y)
    (CategoryStruct.comp (Y := diagonalObj (X := pullback f g) (fst f g))
        (Iso.inv (diagonalObjPullbackFstIso f g) :
          pullback (X := diagonalObj g) (snd g g ≫ g) f ⟶ diagonalObj (X := pullback f g) (fst f g))
        (snd (fst f g) (fst f g) ≫ snd f g : diagonalObj (X := pullback f g) (fst f g) ⟶ Y) :
      pullback (X := diagonalObj g) (snd g g ≫ g) f ⟶ Y)
    (fst (snd g g ≫ g) f ≫ snd g g : pullback (X := pullback g g) (snd g g ≫ g) f ⟶ Y)
have delta : Eq (α := pullback (X := diagonalObj g) (snd g g ≫ g) f ⟶ Y)
  (CategoryStruct.comp (Y := diagonalObj (X := pullback f g) (fst f g))
      (Iso.inv
          (pullbackRightPullbackFstIso f g (fst f g) ≪≫
            Iso.trans (Y := pullback (X := pullback f g) (snd f g ≫ g) g)
              (congrHom sorry sorry :
                pullback (X := pullback f g) (fst f g ≫ f) g ≅ pullback (X := pullback f g) (snd f g ≫ g) g)
              (Iso.trans (Y := pullback (Y := pullback g g) f (fst g g ≫ g))
                  (pullbackAssoc f g g g :
                    pullback (X := pullback f g) (snd f g ≫ g) g ≅ pullback (Y := pullback g g) f (fst g g ≫ g))
                  (pullbackSymmetry f (fst g g ≫ g) ≪≫ congrHom sorry sorry :
                    pullback (Y := pullback g g) f (fst g g ≫ g) ≅ pullback (X := diagonalObj g) (snd g g ≫ g) f) :
                pullback (X := pullback f g) (snd f g ≫ g) g ≅ pullback (X := diagonalObj g) (snd g g ≫ g) f)) :
        pullback (X := diagonalObj g) (snd g g ≫ g) f ⟶ diagonalObj (X := pullback f g) (fst f g))
      (snd (fst f g) (fst f g) ≫ snd f g : diagonalObj (X := pullback f g) (fst f g) ⟶ Y) :
    pullback (X := diagonalObj g) (snd g g ≫ g) f ⟶ Y)
  (fst (snd g g ≫ g) f ≫ snd g g : pullback (X := pullback g g) (snd g g ≫ g) f ⟶ Y)
Tactic: delta diagonalObjPullbackFstIso
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Diagonal (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasPullbacks.{v_1, u_1} C
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
⊢ Eq (α := pullback f g ⟶ diagonalObj (X := pullback f g) (fst f g)) (diagonal (fst f g))
    (Iso.hom (pullbackSymmetry f (Over.mk g).hom) ≫
      CategoryStruct.comp (Y := ((Over.pullback f).obj (Over.mk (Y := pullback g g) (snd g g ≫ g))).left)
        (Over.Hom.left ((Over.pullback f).map (Over.homMk (diagonal g) ⋯))) (Iso.inv (diagonalObjPullbackFstIso f g)))
have h₀ : Eq (α := pullback f g ⟶ X)
  (CategoryStruct.comp (Y := pullback (X := pullback f g) (Y := pullback f g) (fst f g) (fst f g)) (diagonal (fst f g))
      (fst (fst f g) (fst f g)) ≫
    fst f g)
  (CategoryStruct.comp (Y := pullback f g)
    (CategoryStruct.comp (Y := pullback (X := pullback f g) (Y := pullback f g) (fst f g) (fst f g))
      (Iso.hom (pullbackSymmetry f (Over.mk g).hom) ≫
        CategoryStruct.comp (Y := ((Over.pullback f).obj (Over.mk (Y := pullback g g) (snd g g ≫ g))).left)
          (Over.Hom.left ((Over.pullback f).map (Over.homMk (diagonal g) sorry))) (Iso.inv (diagonalObjPullbackFstIso f g)))
      (fst (fst f g) (fst f g)))
    (fst f g))
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Diagonal (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasPullbacks.{v_1, u_1} C
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
h₀ :
  Eq (α := pullback f g ⟶ X)
    (CategoryStruct.comp (Y := pullback (X := pullback f g) (Y := pullback f g) (fst f g) (fst f g))
        (diagonal (fst f g)) (fst (fst f g) (fst f g)) ≫
      fst f g)
    (CategoryStruct.comp (Y := pullback f g)
      (CategoryStruct.comp (Y := pullback (X := pullback f g) (Y := pullback f g) (fst f g) (fst f g))
        (Iso.hom (pullbackSymmetry f (Over.mk g).hom) ≫
          CategoryStruct.comp (Y := ((Over.pullback f).obj (Over.mk (Y := pullback g g) (snd g g ≫ g))).left)
            (Over.Hom.left ((Over.pullback f).map (Over.homMk (diagonal g) ⋯)))
            (Iso.inv (diagonalObjPullbackFstIso f g)))
        (fst (fst f g) (fst f g)))
      (fst f g))
⊢ Eq (α := pullback f g ⟶ diagonalObj (X := pullback f g) (fst f g)) (diagonal (fst f g))
    (Iso.hom (pullbackSymmetry f (Over.mk g).hom) ≫
      CategoryStruct.comp (Y := ((Over.pullback f).obj (Over.mk (Y := pullback g g) (snd g g ≫ g))).left)
        (Over.Hom.left ((Over.pullback f).map (Over.homMk (diagonal g) ⋯))) (Iso.inv (diagonalObjPullbackFstIso f g)))
have h₁ : Eq (α := pullback f g ⟶ Y)
  (CategoryStruct.comp (Y := pullback (X := pullback f g) (Y := pullback f g) (fst f g) (fst f g)) (diagonal (fst f g))
      (fst (fst f g) (fst f g)) ≫
    snd f g)
  (CategoryStruct.comp (Y := pullback f g)
    (CategoryStruct.comp (Y := pullback (X := pullback f g) (Y := pullback f g) (fst f g) (fst f g))
      (Iso.hom (pullbackSymmetry f (Over.mk g).hom) ≫
        CategoryStruct.comp (Y := ((Over.pullback f).obj (Over.mk (Y := pullback g g) (snd g g ≫ g))).left)
          (Over.Hom.left ((Over.pullback f).map (Over.homMk (diagonal g) sorry))) (Iso.inv (diagonalObjPullbackFstIso f g)))
      (fst (fst f g) (fst f g)))
    (snd f g))
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Diagonal (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasPullbacks.{v_1, u_1} C
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
h₀ :
  Eq (α := pullback f g ⟶ X)
    (CategoryStruct.comp (Y := pullback (X := pullback f g) (Y := pullback f g) (fst f g) (fst f g))
        (diagonal (fst f g)) (fst (fst f g) (fst f g)) ≫
      fst f g)
    (CategoryStruct.comp (Y := pullback f g)
      (CategoryStruct.comp (Y := pullback (X := pullback f g) (Y := pullback f g) (fst f g) (fst f g))
        (Iso.hom (pullbackSymmetry f (Over.mk g).hom) ≫
          CategoryStruct.comp (Y := ((Over.pullback f).obj (Over.mk (Y := pullback g g) (snd g g ≫ g))).left)
            (Over.Hom.left ((Over.pullback f).map (Over.homMk (diagonal g) ⋯)))
            (Iso.inv (diagonalObjPullbackFstIso f g)))
        (fst (fst f g) (fst f g)))
      (fst f g))
h₁ :
  Eq (α := pullback f g ⟶ Y)
    (CategoryStruct.comp (Y := pullback (X := pullback f g) (Y := pullback f g) (fst f g) (fst f g))
        (diagonal (fst f g)) (fst (fst f g) (fst f g)) ≫
      snd f g)
    (CategoryStruct.comp (Y := pullback f g)
      (CategoryStruct.comp (Y := pullback (X := pullback f g) (Y := pullback f g) (fst f g) (fst f g))
        (Iso.hom (pullbackSymmetry f (Over.mk g).hom) ≫
          CategoryStruct.comp (Y := ((Over.pullback f).obj (Over.mk (Y := pullback g g) (snd g g ≫ g))).left)
            (Over.Hom.left ((Over.pullback f).map (Over.homMk (diagonal g) ⋯)))
            (Iso.inv (diagonalObjPullbackFstIso f g)))
        (fst (fst f g) (fst f g)))
      (snd f g))
⊢ Eq (α := pullback f g ⟶ diagonalObj (X := pullback f g) (fst f g)) (diagonal (fst f g))
    (Iso.hom (pullbackSymmetry f (Over.mk g).hom) ≫
      CategoryStruct.comp (Y := ((Over.pullback f).obj (Over.mk (Y := pullback g g) (snd g g ≫ g))).left)
        (Over.Hom.left ((Over.pullback f).map (Over.homMk (diagonal g) ⋯))) (Iso.inv (diagonalObjPullbackFstIso f g)))
have h₂ : Eq (α := pullback f g ⟶ X)
  (CategoryStruct.comp (Y := pullback (X := pullback f g) (Y := pullback f g) (fst f g) (fst f g)) (diagonal (fst f g))
      (snd (fst f g) (fst f g)) ≫
    fst f g)
  (CategoryStruct.comp (Y := pullback f g)
    (CategoryStruct.comp (Y := pullback (X := pullback f g) (Y := pullback f g) (fst f g) (fst f g))
      (Iso.hom (pullbackSymmetry f (Over.mk g).hom) ≫
        CategoryStruct.comp (Y := ((Over.pullback f).obj (Over.mk (Y := pullback g g) (snd g g ≫ g))).left)
          (Over.Hom.left ((Over.pullback f).map (Over.homMk (diagonal g) sorry))) (Iso.inv (diagonalObjPullbackFstIso f g)))
      (snd (fst f g) (fst f g)))
    (fst f g))
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Diagonal (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X Y : C
inst_1 : HasPullbacks.{v_1, u_1} C
S : C
g : Y ⟶ X
f : X ⟶ S
i : pullback (g ≫ f) f ≅ pullback (g ≫ f) (𝟙 X ≫ f) := congrHom ⋯ ⋯
⊢ map (g ≫ f) (𝟙 X ≫ f) f f g (𝟙 X) (𝟙 S) ⋯ ⋯ ≫ 𝟙 (diagonalObj f) = i.inv ≫ map (g ≫ f) f f f g (𝟙 X) (𝟙 S) ⋯ ⋯
have h₀ : (map (g ≫ f) (𝟙 X ≫ f) f f g (𝟙 X) (𝟙 S) sorry sorry ≫ 𝟙 (diagonalObj f)) ≫ fst f f =
  CategoryStruct.comp (Y := pullback f f) (i.inv ≫ map (g ≫ f) f f f g (𝟙 X) (𝟙 S) sorry sorry) (fst f f)
Tactic: ext