awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Diagonal
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
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 ⋯ ⋯ :
                  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 ⋯ ⋯ :
                      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)
⊢ 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)

Tactic:
delta diagonalObjPullbackFstIso

Premises used: CategoryTheory.Limits.diagonalObjPullbackFstIso
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Diagonal
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
            (pullbackRightPullbackFstIso f g (fst f g) ≪≫
              Iso.trans (Y := pullback (X := pullback f g) (snd f g ≫ g) g)
                (congrHom ⋯ ⋯ :
                  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 ⋯ ⋯ :
                      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:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Diagonal
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
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 ⋯ ⋯ :
                  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 ⋯ ⋯ :
                      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)
⊢ 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)

Tactic:
delta diagonalObjPullbackFstIso

Premises used: CategoryTheory.Limits.diagonalObjPullbackFstIso
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Diagonal
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
            (pullbackRightPullbackFstIso f g (fst f g) ≪≫
              Iso.trans (Y := pullback (X := pullback f g) (snd f g ≫ g) g)
                (congrHom ⋯ ⋯ :
                  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 ⋯ ⋯ :
                      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:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Diagonal
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
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 ⋯ ⋯ :
                  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 ⋯ ⋯ :
                      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)
⊢ 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)

Tactic:
delta diagonalObjPullbackFstIso

Premises used: CategoryTheory.Limits.diagonalObjPullbackFstIso
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Diagonal
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
            (pullbackRightPullbackFstIso f g (fst f g) ≪≫
              Iso.trans (Y := pullback (X := pullback f g) (snd f g ≫ g) g)
                (congrHom ⋯ ⋯ :
                  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 ⋯ ⋯ :
                      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:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Diagonal
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 ⟶ 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))

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Diagonal
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 ⟶ 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))

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Diagonal
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 ⟶ 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) ⋯)))
            (Iso.inv (diagonalObjPullbackFstIso f g)))
        (snd (fst f g) (fst f g)))
      (fst f g))

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Diagonal
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 ⟶ Y)
    (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)) ≫
      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)))
        (snd (fst f g) (fst f g)))
      (snd f g))

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Diagonal
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X Y Z : C
inst_1 : HasPullbacks.{v_1, u_1} C
S T : C
f_1 : X ⟶ T
g_1 : Y ⟶ T
i : T ⟶ S
inst_2 : HasPullback i i
inst_3 : HasPullback f_1 g_1
inst_4 : HasPullback (f_1 ≫ i) (g_1 ≫ i)
inst_5 :
  HasPullback (Y := pullback (f_1 ≫ i) (g_1 ≫ i)) (Z := diagonalObj i) (diagonal i)
    (map (f_1 ≫ i) (g_1 ≫ i) i i f_1 g_1 (𝟙 S) ⋯ ⋯)
g : Y ⟶ X
f : X ⟶ S
⊢ 𝟙 Y ≫ g ≫ f = g ≫ f

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Diagonal
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X Y Z : C
inst_1 : HasPullbacks.{v_1, u_1} C
S T : C
f_1 : X ⟶ T
g_1 : Y ⟶ T
i : T ⟶ S
inst_2 : HasPullback i i
inst_3 : HasPullback f_1 g_1
inst_4 : HasPullback (f_1 ≫ i) (g_1 ≫ i)
inst_5 :
  HasPullback (Y := pullback (f_1 ≫ i) (g_1 ≫ i)) (Z := diagonalObj i) (diagonal i)
    (map (f_1 ≫ i) (g_1 ≫ i) i i f_1 g_1 (𝟙 S) ⋯ ⋯)
g : Y ⟶ X
f : X ⟶ S
⊢ (g ≫ f) ≫ 𝟙 S = g ≫ f

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Diagonal
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X Y Z : C
inst_1 : HasPullbacks.{v_1, u_1} C
S T : C
f_1 : X ⟶ T
g_1 : Y ⟶ T
i : T ⟶ S
inst_2 : HasPullback i i
inst_3 : HasPullback f_1 g_1
inst_4 : HasPullback (f_1 ≫ i) (g_1 ≫ i)
inst_5 :
  HasPullback (Y := pullback (f_1 ≫ i) (g_1 ≫ i)) (Z := diagonalObj i) (diagonal i)
    (map (f_1 ≫ i) (g_1 ≫ i) i i f_1 g_1 (𝟙 S) ⋯ ⋯)
g : Y ⟶ X
f : X ⟶ S
⊢ f ≫ 𝟙 S = 𝟙 X ≫ f

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Diagonal
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
⊢ f = 𝟙 X ≫ f

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Diagonal
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 ⋯ ⋯
⊢ (g ≫ f) ≫ 𝟙 S = g ≫ f

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Diagonal
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 ⋯ ⋯
⊢ f ≫ 𝟙 S = 𝟙 X ≫ f

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Diagonal
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 ⋯ ⋯
⊢ (𝟙 X ≫ f) ≫ 𝟙 S = 𝟙 X ≫ f

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Diagonal
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 ⋯ ⋯
⊢ diagonal f ≫ 𝟙 (diagonalObj f) = 𝟙 X ≫ diagonal f

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Diagonal
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 ⋯ ⋯
h₀ :
  (map (g ≫ f) (𝟙 X ≫ f) f f g (𝟙 X) (𝟙 S) ⋯ ⋯ ≫ 𝟙 (diagonalObj f)) ≫ fst f f =
    CategoryStruct.comp (Y := pullback f f) (i.inv ≫ map (g ≫ f) f f f g (𝟙 X) (𝟙 S) ⋯ ⋯) (fst f f)
h₁ :
  (map (g ≫ f) (𝟙 X ≫ f) f f g (𝟙 X) (𝟙 S) ⋯ ⋯ ≫ 𝟙 (diagonalObj f)) ≫ snd f f =
    CategoryStruct.comp (Y := pullback f f) (i.inv ≫ map (g ≫ f) f f f g (𝟙 X) (𝟙 S) ⋯ ⋯) (snd f f)
⊢ map (g ≫ f) (𝟙 X ≫ f) f f g (𝟙 X) (𝟙 S) ⋯ ⋯ ≫ 𝟙 (diagonalObj f) = i.inv ≫ map (g ≫ f) f f f g (𝟙 X) (𝟙 S) ⋯ ⋯

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Diagonal
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)) ≫ fst f f =
    CategoryStruct.comp (Y := pullback f f) (i.inv ≫ map (g ≫ f) f f f g (𝟙 X) (𝟙 S) ⋯ ⋯) (fst f f)

Tactic:
simp [i]
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Diagonal
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)) ≫ snd f f =
    CategoryStruct.comp (Y := pullback f f) (i.inv ≫ map (g ≫ f) f f f g (𝟙 X) (𝟙 S) ⋯ ⋯) (snd f f)

Tactic:
simp [i]
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Diagonal
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 ⋯ ⋯
e : pullback (Y := pullback (g ≫ f) f) (Z := diagonalObj f) (diagonal f) (map (g ≫ f) f f f g (𝟙 X) (𝟙 S) ⋯ ⋯) ≅
  pullback (Y := pullback (g ≫ f) (𝟙 X ≫ f)) (Z := diagonalObj f) (diagonal f)
    (map (g ≫ f) (𝟙 X ≫ f) f f g (𝟙 X) (𝟙 S) ⋯ ⋯) :=
  Iso.symm
    (asIso
      (map (diagonal f) (map (g ≫ f) (𝟙 X ≫ f) f f g (𝟙 X) (𝟙 S) ⋯ ⋯) (diagonal f) (map (g ≫ f) f f f g (𝟙 X) (𝟙 S) ⋯ ⋯)
        (𝟙 X) i.inv (𝟙 (diagonalObj f)) ⋯ ⋯))
w₁ :
  (e ≪≫ Iso.trans (Y := pullback g (𝟙 X)) (pullbackDiagonalMapIdIso g (𝟙 X) f) (asIso (fst g (𝟙 X)))).symm.hom ≫
      fst (diagonal f) (map (g ≫ f) f f f g (𝟙 X) (𝟙 S) ⋯ ⋯) =
    g
w₂ :
  (e ≪≫ Iso.trans (Y := pullback g (𝟙 X)) (pullbackDiagonalMapIdIso g (𝟙 X) f) (asIso (fst g (𝟙 X)))).symm.hom ≫
      snd (diagonal f) (map (g ≫ f) f f f g (𝟙 X) (𝟙 S) ⋯ ⋯) =
    lift (𝟙 Y) g ⋯
apply :
  CommSq (Y := pullback (g ≫ f) f) (Z := diagonalObj f) g (lift (𝟙 Y) g ⋯) (diagonal f)
    (map (g ≫ f) f f f g (𝟙 X) (𝟙 S) ⋯ ⋯)
⊢ IsPullback (Y := pullback (g ≫ f) f) (Z := diagonalObj f) g (lift (𝟙 Y) g ⋯) (diagonal f)
    (map (g ≫ f) f f f g (𝟙 X) (𝟙 S) ⋯ ⋯)

Tactic:
apply IsPullback.of_iso_pullback _
      (e ≪≫ pullbackDiagonalMapIdIso (T := X) (S := S) g (𝟙 X) f ≪≫ asIso (pullback.fst _ _)).symm

Premises used: CategoryTheory.CategoryStruct.id, CategoryTheory.Iso.trans, CategoryTheory.Limits.pullback.fst, CategoryTheory.Iso.symm, CategoryTheory.IsPullback.of_iso_pullback, CategoryTheory.Limits.pullbackDiagonalMapIdIso, CategoryTheory.asIso
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Diagonal
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 ⋯ ⋯
e : pullback (Y := pullback (g ≫ f) f) (Z := diagonalObj f) (diagonal f) (map (g ≫ f) f f f g (𝟙 X) (𝟙 S) ⋯ ⋯) ≅
  pullback (Y := pullback (g ≫ f) (𝟙 X ≫ f)) (Z := diagonalObj f) (diagonal f)
    (map (g ≫ f) (𝟙 X ≫ f) f f g (𝟙 X) (𝟙 S) ⋯ ⋯) :=
  Iso.symm
    (asIso
      (map (diagonal f) (map (g ≫ f) (𝟙 X ≫ f) f f g (𝟙 X) (𝟙 S) ⋯ ⋯) (diagonal f) (map (g ≫ f) f f f g (𝟙 X) (𝟙 S) ⋯ ⋯)
        (𝟙 X) i.inv (𝟙 (diagonalObj f)) ⋯ ⋯))
⊢ (e ≪≫ Iso.trans (Y := pullback g (𝟙 X)) (pullbackDiagonalMapIdIso g (𝟙 X) f) (asIso (fst g (𝟙 X)))).symm.hom ≫
      fst (diagonal f) (map (g ≫ f) f f f g (𝟙 X) (𝟙 S) ⋯ ⋯) =
    g

Tactic:
simp [e]
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Diagonal
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 ⋯ ⋯
e : pullback (Y := pullback (g ≫ f) f) (Z := diagonalObj f) (diagonal f) (map (g ≫ f) f f f g (𝟙 X) (𝟙 S) ⋯ ⋯) ≅
  pullback (Y := pullback (g ≫ f) (𝟙 X ≫ f)) (Z := diagonalObj f) (diagonal f)
    (map (g ≫ f) (𝟙 X ≫ f) f f g (𝟙 X) (𝟙 S) ⋯ ⋯) :=
  Iso.symm
    (asIso
      (map (diagonal f) (map (g ≫ f) (𝟙 X ≫ f) f f g (𝟙 X) (𝟙 S) ⋯ ⋯) (diagonal f) (map (g ≫ f) f f f g (𝟙 X) (𝟙 S) ⋯ ⋯)
        (𝟙 X) i.inv (𝟙 (diagonalObj f)) ⋯ ⋯))
w₂ :
  ((e ≪≫ Iso.trans (Y := pullback g (𝟙 X)) (pullbackDiagonalMapIdIso g (𝟙 X) f) (asIso (fst g (𝟙 X)))).symm.hom ≫
        snd (diagonal f) (map (g ≫ f) f f f g (𝟙 X) (𝟙 S) ⋯ ⋯)) ≫
      fst (g ≫ f) f =
    CategoryStruct.comp (Y := pullback (g ≫ f) f) (lift (𝟙 Y) g ⋯) (fst (g ≫ f) f)
w₃ :
  ((e ≪≫ Iso.trans (Y := pullback g (𝟙 X)) (pullbackDiagonalMapIdIso g (𝟙 X) f) (asIso (fst g (𝟙 X)))).symm.hom ≫
        snd (diagonal f) (map (g ≫ f) f f f g (𝟙 X) (𝟙 S) ⋯ ⋯)) ≫
      snd (g ≫ f) f =
    CategoryStruct.comp (Y := pullback (g ≫ f) f) (lift (𝟙 Y) g ⋯) (snd (g ≫ f) f)
⊢ (e ≪≫ Iso.trans (Y := pullback g (𝟙 X)) (pullbackDiagonalMapIdIso g (𝟙 X) f) (asIso (fst g (𝟙 X)))).symm.hom ≫
      snd (diagonal f) (map (g ≫ f) f f f g (𝟙 X) (𝟙 S) ⋯ ⋯) =
    lift (𝟙 Y) g ⋯

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Diagonal
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 ⋯ ⋯
e : pullback (Y := pullback (g ≫ f) f) (Z := diagonalObj f) (diagonal f) (map (g ≫ f) f f f g (𝟙 X) (𝟙 S) ⋯ ⋯) ≅
  pullback (Y := pullback (g ≫ f) (𝟙 X ≫ f)) (Z := diagonalObj f) (diagonal f)
    (map (g ≫ f) (𝟙 X ≫ f) f f g (𝟙 X) (𝟙 S) ⋯ ⋯) :=
  Iso.symm
    (asIso
      (map (diagonal f) (map (g ≫ f) (𝟙 X ≫ f) f f g (𝟙 X) (𝟙 S) ⋯ ⋯) (diagonal f) (map (g ≫ f) f f f g (𝟙 X) (𝟙 S) ⋯ ⋯)
        (𝟙 X) i.inv (𝟙 (diagonalObj f)) ⋯ ⋯))
⊢ ((e ≪≫ Iso.trans (Y := pullback g (𝟙 X)) (pullbackDiagonalMapIdIso g (𝟙 X) f) (asIso (fst g (𝟙 X)))).symm.hom ≫
        snd (diagonal f) (map (g ≫ f) f f f g (𝟙 X) (𝟙 S) ⋯ ⋯)) ≫
      fst (g ≫ f) f =
    CategoryStruct.comp (Y := pullback (g ≫ f) f) (lift (𝟙 Y) g ⋯) (fst (g ≫ f) f)

Tactic:
simp [e, i]