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
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) ⋯ ⋯)
⊢ Eq (α := pullback f g ⟶ T)
    (CategoryStruct.comp (Y :=
      pullback (Y := pullback (f ≫ i) (g ≫ i)) (Z := diagonalObj i) (diagonal i)
        (map (f ≫ i) (g ≫ i) i i f g (𝟙 S) ⋯ ⋯))
      (Iso.hom (Iso.symm (pullbackDiagonalMapIdIso f g i))) (fst (diagonal i) (map (f ≫ i) (g ≫ i) i i f g (𝟙 S) ⋯ ⋯)))
    (fst 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 : 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 ⟶ X)
    (CategoryStruct.comp (Y := pullback (f ≫ i) (g ≫ i))
      (CategoryStruct.comp (Y :=
        pullback (Y := pullback (f ≫ i) (g ≫ i)) (Z := diagonalObj i) (diagonal i)
          (map (f ≫ i) (g ≫ i) i i f g (𝟙 S) ⋯ ⋯))
        (Iso.hom (Iso.symm (pullbackDiagonalMapIdIso f g i)))
        (snd (diagonal i) (map (f ≫ i) (g ≫ i) i i f g (𝟙 S) ⋯ ⋯)))
      (fst (f ≫ i) (g ≫ i)))
    (CategoryStruct.comp (Y := pullback (f ≫ i) (g ≫ i)) (map f g (f ≫ i) (g ≫ i) (𝟙 X) (𝟙 Y) i ⋯ ⋯)
      (fst (f ≫ i) (g ≫ i)))
w₃ :
  Eq (α := pullback f g ⟶ Y)
    (CategoryStruct.comp (Y := pullback (f ≫ i) (g ≫ i))
      (CategoryStruct.comp (Y :=
        pullback (Y := pullback (f ≫ i) (g ≫ i)) (Z := diagonalObj i) (diagonal i)
          (map (f ≫ i) (g ≫ i) i i f g (𝟙 S) ⋯ ⋯))
        (Iso.hom (Iso.symm (pullbackDiagonalMapIdIso f g i)))
        (snd (diagonal i) (map (f ≫ i) (g ≫ i) i i f g (𝟙 S) ⋯ ⋯)))
      (snd (f ≫ i) (g ≫ i)))
    (CategoryStruct.comp (Y := pullback (f ≫ i) (g ≫ i)) (map f g (f ≫ i) (g ≫ i) (𝟙 X) (𝟙 Y) i ⋯ ⋯)
      (snd (f ≫ i) (g ≫ i)))
⊢ Eq (α := pullback f g ⟶ pullback (f ≫ i) (g ≫ i))
    (CategoryStruct.comp (Y :=
      pullback (Y := pullback (f ≫ i) (g ≫ i)) (Z := diagonalObj i) (diagonal i)
        (map (f ≫ i) (g ≫ i) i i f g (𝟙 S) ⋯ ⋯))
      (Iso.hom (Iso.symm (pullbackDiagonalMapIdIso f g i))) (snd (diagonal i) (map (f ≫ i) (g ≫ i) i i f g (𝟙 S) ⋯ ⋯)))
    (map f g (f ≫ i) (g ≫ i) (𝟙 X) (𝟙 Y) i ⋯ ⋯)

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 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) ⋯ ⋯)
⊢ Eq (α := pullback f g ⟶ X)
    (CategoryStruct.comp (Y := pullback (f ≫ i) (g ≫ i))
      (CategoryStruct.comp (Y :=
        pullback (Y := pullback (f ≫ i) (g ≫ i)) (Z := diagonalObj i) (diagonal i)
          (map (f ≫ i) (g ≫ i) i i f g (𝟙 S) ⋯ ⋯))
        (Iso.hom (Iso.symm (pullbackDiagonalMapIdIso f g i)))
        (snd (diagonal i) (map (f ≫ i) (g ≫ i) i i f g (𝟙 S) ⋯ ⋯)))
      (fst (f ≫ i) (g ≫ i)))
    (CategoryStruct.comp (Y := pullback (f ≫ i) (g ≫ i)) (map f g (f ≫ i) (g ≫ i) (𝟙 X) (𝟙 Y) i ⋯ ⋯)
      (fst (f ≫ i) (g ≫ i)))

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 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) ⋯ ⋯)
⊢ Eq (α := pullback f g ⟶ Y)
    (CategoryStruct.comp (Y := pullback (f ≫ i) (g ≫ i))
      (CategoryStruct.comp (Y :=
        pullback (Y := pullback (f ≫ i) (g ≫ i)) (Z := diagonalObj i) (diagonal i)
          (map (f ≫ i) (g ≫ i) i i f g (𝟙 S) ⋯ ⋯))
        (Iso.hom (Iso.symm (pullbackDiagonalMapIdIso f g i)))
        (snd (diagonal i) (map (f ≫ i) (g ≫ i) i i f g (𝟙 S) ⋯ ⋯)))
      (snd (f ≫ i) (g ≫ i)))
    (CategoryStruct.comp (Y := pullback (f ≫ i) (g ≫ i)) (map f g (f ≫ i) (g ≫ i) (𝟙 X) (𝟙 Y) i ⋯ ⋯)
      (snd (f ≫ i) (g ≫ i)))

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 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 :
  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
⊢ 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) ⋯ ⋯)

Tactic:
constructor
-- 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 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))
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 ⋯ ⋯)
        (map (f ≫ i) (g ≫ i) i i f g (𝟙 S) ⋯ ⋯))
      (snd 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

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 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) ⋯ ⋯)
⊢ 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))

Tactic:
simp [condition]

Premises used: CategoryTheory.Limits.pullback.condition
-- 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 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) ⋯ ⋯)
⊢ 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 ⋯ ⋯)
        (map (f ≫ i) (g ≫ i) i i f g (𝟙 S) ⋯ ⋯))
      (snd i i))

Tactic:
simp [condition]

Premises used: CategoryTheory.Limits.pullback.condition
-- 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 (α := 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 ⋯ ⋯ :
                  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)) :
          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)
⊢ 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)

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 (α := 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 ⋯ ⋯ :
                  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)) :
          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:
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 (α := 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 ⋯ ⋯ :
                  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)) :
          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)
⊢ 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)

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 (α := 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 ⋯ ⋯ :
                  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)) :
          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:
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 (α := 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 ⋯ ⋯ :
                  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)) :
          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)
⊢ 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)

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 (α := 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 ⋯ ⋯ :
                  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)) :
          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:
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))
        (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)
⊢ 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)

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))
        (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:
simp