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
U V₁ V₂ : C
f : X ⟶ Y
i : U ⟶ Y
i₁ : V₁ ⟶ pullback f i
i₂ : V₂ ⟶ pullback f i
inst_2 : HasPullback i₁ i₂
delta :
  Eq (α :=
    pullback (Y := pullback (i₁ ≫ snd f i) (i₂ ≫ snd f i)) (Z := diagonalObj f) (diagonal f)
        (map (i₁ ≫ snd f i) (i₂ ≫ snd f i) f f (i₁ ≫ fst f i) (i₂ ≫ fst f i) i ⋯ ⋯) ⟶
      V₂)
    (CategoryStruct.comp (Y := pullback i₁ i₂)
        (Iso.hom { hom := hom f i i₁ i₂, inv := inv f i i₁ i₂, hom_inv_id := ⋯, inv_hom_id := ⋯ } :
          pullback (Y := pullback (i₁ ≫ snd f i) (i₂ ≫ snd f i)) (Z := diagonalObj f) (diagonal f)
              (map (i₁ ≫ snd f i) (i₂ ≫ snd f i) f f (i₁ ≫ fst f i) (i₂ ≫ fst f i) i ⋯ ⋯) ⟶
            pullback i₁ i₂)
        (snd i₁ i₂ : pullback i₁ i₂ ⟶ V₂) :
      pullback (Y := pullback (i₁ ≫ snd f i) (i₂ ≫ snd f i)) (Z := diagonalObj f) (diagonal f)
          (map (i₁ ≫ snd f i) (i₂ ≫ snd f i) f f (i₁ ≫ fst f i) (i₂ ≫ fst f i) i ⋯ ⋯) ⟶
        V₂)
    (snd (diagonal f) (map (i₁ ≫ snd f i) (i₂ ≫ snd f i) f f (i₁ ≫ fst f i) (i₂ ≫ fst f i) i ⋯ ⋯) ≫
        snd (i₁ ≫ snd f i) (i₂ ≫ snd f i) :
      pullback (Y := pullback (i₁ ≫ snd f i) (i₂ ≫ snd f i)) (Z := diagonalObj f) (diagonal f)
          (map (i₁ ≫ snd f i) (i₂ ≫ snd f i) f f (i₁ ≫ fst f i) (i₂ ≫ fst f i) i ⋯ ⋯) ⟶
        V₂)
⊢ Eq (α :=
    pullback (Y := pullback (i₁ ≫ snd f i) (i₂ ≫ snd f i)) (Z := diagonalObj f) (diagonal f)
        (map (i₁ ≫ snd f i) (i₂ ≫ snd f i) f f (i₁ ≫ fst f i) (i₂ ≫ fst f i) i ⋯ ⋯) ⟶
      V₂)
    (CategoryStruct.comp (Y := pullback i₁ i₂)
        (Iso.hom (pullbackDiagonalMapIso f i i₁ i₂) :
          pullback (Y := pullback (i₁ ≫ snd f i) (i₂ ≫ snd f i)) (Z := diagonalObj f) (diagonal f)
              (map (i₁ ≫ snd f i) (i₂ ≫ snd f i) f f (i₁ ≫ fst f i) (i₂ ≫ fst f i) i ⋯ ⋯) ⟶
            pullback i₁ i₂)
        (snd i₁ i₂ : pullback i₁ i₂ ⟶ V₂) :
      pullback (Y := pullback (i₁ ≫ snd f i) (i₂ ≫ snd f i)) (Z := diagonalObj f) (diagonal f)
          (map (i₁ ≫ snd f i) (i₂ ≫ snd f i) f f (i₁ ≫ fst f i) (i₂ ≫ fst f i) i ⋯ ⋯) ⟶
        V₂)
    (snd (diagonal f) (map (i₁ ≫ snd f i) (i₂ ≫ snd f i) f f (i₁ ≫ fst f i) (i₂ ≫ fst f i) i ⋯ ⋯) ≫
        snd (i₁ ≫ snd f i) (i₂ ≫ snd f i) :
      pullback (Y := pullback (i₁ ≫ snd f i) (i₂ ≫ snd f i)) (Z := diagonalObj f) (diagonal f)
          (map (i₁ ≫ snd f i) (i₂ ≫ snd f i) f f (i₁ ≫ fst f i) (i₂ ≫ fst f i) i ⋯ ⋯) ⟶
        V₂)

Tactic:
delta pullbackDiagonalMapIso

Premises used: CategoryTheory.Limits.pullbackDiagonalMapIso
-- 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
U V₁ V₂ : C
f : X ⟶ Y
i : U ⟶ Y
i₁ : V₁ ⟶ pullback f i
i₂ : V₂ ⟶ pullback f i
inst_2 : HasPullback i₁ i₂
⊢ Eq (α :=
    pullback (Y := pullback (i₁ ≫ snd f i) (i₂ ≫ snd f i)) (Z := diagonalObj f) (diagonal f)
        (map (i₁ ≫ snd f i) (i₂ ≫ snd f i) f f (i₁ ≫ fst f i) (i₂ ≫ fst f i) i ⋯ ⋯) ⟶
      V₂)
    (CategoryStruct.comp (Y := pullback i₁ i₂)
        (Iso.hom { hom := hom f i i₁ i₂, inv := inv f i i₁ i₂, hom_inv_id := ⋯, inv_hom_id := ⋯ } :
          pullback (Y := pullback (i₁ ≫ snd f i) (i₂ ≫ snd f i)) (Z := diagonalObj f) (diagonal f)
              (map (i₁ ≫ snd f i) (i₂ ≫ snd f i) f f (i₁ ≫ fst f i) (i₂ ≫ fst f i) i ⋯ ⋯) ⟶
            pullback i₁ i₂)
        (snd i₁ i₂ : pullback i₁ i₂ ⟶ V₂) :
      pullback (Y := pullback (i₁ ≫ snd f i) (i₂ ≫ snd f i)) (Z := diagonalObj f) (diagonal f)
          (map (i₁ ≫ snd f i) (i₂ ≫ snd f i) f f (i₁ ≫ fst f i) (i₂ ≫ fst f i) i ⋯ ⋯) ⟶
        V₂)
    (snd (diagonal f) (map (i₁ ≫ snd f i) (i₂ ≫ snd f i) f f (i₁ ≫ fst f i) (i₂ ≫ fst f i) i ⋯ ⋯) ≫
        snd (i₁ ≫ snd f i) (i₂ ≫ snd f i) :
      pullback (Y := pullback (i₁ ≫ snd f i) (i₂ ≫ snd f i)) (Z := diagonalObj f) (diagonal f)
          (map (i₁ ≫ snd f i) (i₂ ≫ snd f i) f f (i₁ ≫ fst f i) (i₂ ≫ fst f i) i ⋯ ⋯) ⟶
        V₂)

Tactic:
simp only [limit.lift_π, PullbackCone.mk_pt, PullbackCone.mk_π_app]

Premises used: CategoryTheory.Limits.PullbackCone.mk_π_app, CategoryTheory.Limits.PullbackCone.mk_pt, CategoryTheory.Limits.limit.lift_π
-- 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
U V₁ V₂ : C
f : X ⟶ Y
i : U ⟶ Y
i₁ : V₁ ⟶ pullback f i
i₂ : V₂ ⟶ pullback f i
inst_2 : HasPullback i₁ i₂
delta :
  Eq (α := pullback i₁ i₂ ⟶ X)
    (CategoryStruct.comp (Y :=
        pullback (Y := pullback (i₁ ≫ snd f i) (i₂ ≫ snd f i)) (Z := diagonalObj f) (diagonal f)
          (map (i₁ ≫ snd f i) (i₂ ≫ snd f i) f f (i₁ ≫ fst f i) (i₂ ≫ fst f i) i ⋯ ⋯))
        (Iso.inv { hom := hom f i i₁ i₂, inv := inv f i i₁ i₂, hom_inv_id := ⋯, inv_hom_id := ⋯ } :
          pullback i₁ i₂ ⟶
            pullback (Y := pullback (i₁ ≫ snd f i) (i₂ ≫ snd f i)) (Z := diagonalObj f) (diagonal f)
              (map (i₁ ≫ snd f i) (i₂ ≫ snd f i) f f (i₁ ≫ fst f i) (i₂ ≫ fst f i) i ⋯ ⋯))
        (fst (diagonal f) (map (i₁ ≫ snd f i) (i₂ ≫ snd f i) f f (i₁ ≫ fst f i) (i₂ ≫ fst f i) i ⋯ ⋯) :
          pullback (Y := pullback (i₁ ≫ snd f i) (i₂ ≫ snd f i)) (Z := diagonalObj f) (diagonal f)
              (map (i₁ ≫ snd f i) (i₂ ≫ snd f i) f f (i₁ ≫ fst f i) (i₂ ≫ fst f i) i ⋯ ⋯) ⟶
            X) :
      pullback i₁ i₂ ⟶ X)
    (fst i₁ i₂ ≫ i₁ ≫ fst f i : pullback i₁ i₂ ⟶ X)
⊢ Eq (α := pullback i₁ i₂ ⟶ X)
    (CategoryStruct.comp (Y :=
        pullback (Y := pullback (i₁ ≫ snd f i) (i₂ ≫ snd f i)) (Z := diagonalObj f) (diagonal f)
          (map (i₁ ≫ snd f i) (i₂ ≫ snd f i) f f (i₁ ≫ fst f i) (i₂ ≫ fst f i) i ⋯ ⋯))
        (Iso.inv (pullbackDiagonalMapIso f i i₁ i₂) :
          pullback i₁ i₂ ⟶
            pullback (Y := pullback (i₁ ≫ snd f i) (i₂ ≫ snd f i)) (Z := diagonalObj f) (diagonal f)
              (map (i₁ ≫ snd f i) (i₂ ≫ snd f i) f f (i₁ ≫ fst f i) (i₂ ≫ fst f i) i ⋯ ⋯))
        (fst (diagonal f) (map (i₁ ≫ snd f i) (i₂ ≫ snd f i) f f (i₁ ≫ fst f i) (i₂ ≫ fst f i) i ⋯ ⋯) :
          pullback (Y := pullback (i₁ ≫ snd f i) (i₂ ≫ snd f i)) (Z := diagonalObj f) (diagonal f)
              (map (i₁ ≫ snd f i) (i₂ ≫ snd f i) f f (i₁ ≫ fst f i) (i₂ ≫ fst f i) i ⋯ ⋯) ⟶
            X) :
      pullback i₁ i₂ ⟶ X)
    (fst i₁ i₂ ≫ i₁ ≫ fst f i : pullback i₁ i₂ ⟶ X)

Tactic:
delta pullbackDiagonalMapIso

Premises used: CategoryTheory.Limits.pullbackDiagonalMapIso
-- 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
U V₁ V₂ : C
f : X ⟶ Y
i : U ⟶ Y
i₁ : V₁ ⟶ pullback f i
i₂ : V₂ ⟶ pullback f i
inst_2 : HasPullback i₁ i₂
⊢ Eq (α := pullback i₁ i₂ ⟶ X)
    (CategoryStruct.comp (Y :=
        pullback (Y := pullback (i₁ ≫ snd f i) (i₂ ≫ snd f i)) (Z := diagonalObj f) (diagonal f)
          (map (i₁ ≫ snd f i) (i₂ ≫ snd f i) f f (i₁ ≫ fst f i) (i₂ ≫ fst f i) i ⋯ ⋯))
        (Iso.inv { hom := hom f i i₁ i₂, inv := inv f i i₁ i₂, hom_inv_id := ⋯, inv_hom_id := ⋯ } :
          pullback i₁ i₂ ⟶
            pullback (Y := pullback (i₁ ≫ snd f i) (i₂ ≫ snd f i)) (Z := diagonalObj f) (diagonal f)
              (map (i₁ ≫ snd f i) (i₂ ≫ snd f i) f f (i₁ ≫ fst f i) (i₂ ≫ fst f i) i ⋯ ⋯))
        (fst (diagonal f) (map (i₁ ≫ snd f i) (i₂ ≫ snd f i) f f (i₁ ≫ fst f i) (i₂ ≫ fst f i) i ⋯ ⋯) :
          pullback (Y := pullback (i₁ ≫ snd f i) (i₂ ≫ snd f i)) (Z := diagonalObj f) (diagonal f)
              (map (i₁ ≫ snd f i) (i₂ ≫ snd f i) f f (i₁ ≫ fst f i) (i₂ ≫ fst f i) i ⋯ ⋯) ⟶
            X) :
      pullback i₁ i₂ ⟶ X)
    (fst i₁ i₂ ≫ i₁ ≫ fst f i : pullback i₁ i₂ ⟶ X)

Tactic:
simp only [limit.lift_π, PullbackCone.mk_pt, PullbackCone.mk_π_app]

Premises used: CategoryTheory.Limits.PullbackCone.mk_π_app, CategoryTheory.Limits.PullbackCone.mk_pt, CategoryTheory.Limits.limit.lift_π
-- 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
U V₁ V₂ : C
f : X ⟶ Y
i : U ⟶ Y
i₁ : V₁ ⟶ pullback f i
i₂ : V₂ ⟶ pullback f i
inst_2 : HasPullback i₁ i₂
delta :
  Eq (α := pullback i₁ i₂ ⟶ V₁)
    (CategoryStruct.comp (Y :=
        pullback (Y := pullback (i₁ ≫ snd f i) (i₂ ≫ snd f i)) (Z := diagonalObj f) (diagonal f)
          (map (i₁ ≫ snd f i) (i₂ ≫ snd f i) f f (i₁ ≫ fst f i) (i₂ ≫ fst f i) i ⋯ ⋯))
        (Iso.inv { hom := hom f i i₁ i₂, inv := inv f i i₁ i₂, hom_inv_id := ⋯, inv_hom_id := ⋯ } :
          pullback i₁ i₂ ⟶
            pullback (Y := pullback (i₁ ≫ snd f i) (i₂ ≫ snd f i)) (Z := diagonalObj f) (diagonal f)
              (map (i₁ ≫ snd f i) (i₂ ≫ snd f i) f f (i₁ ≫ fst f i) (i₂ ≫ fst f i) i ⋯ ⋯))
        (snd (diagonal f) (map (i₁ ≫ snd f i) (i₂ ≫ snd f i) f f (i₁ ≫ fst f i) (i₂ ≫ fst f i) i ⋯ ⋯) ≫
            fst (i₁ ≫ snd f i) (i₂ ≫ snd f i) :
          pullback (Y := pullback (i₁ ≫ snd f i) (i₂ ≫ snd f i)) (Z := diagonalObj f) (diagonal f)
              (map (i₁ ≫ snd f i) (i₂ ≫ snd f i) f f (i₁ ≫ fst f i) (i₂ ≫ fst f i) i ⋯ ⋯) ⟶
            V₁) :
      pullback i₁ i₂ ⟶ V₁)
    (fst i₁ i₂ : pullback i₁ i₂ ⟶ V₁)
⊢ Eq (α := pullback i₁ i₂ ⟶ V₁)
    (CategoryStruct.comp (Y :=
        pullback (Y := pullback (i₁ ≫ snd f i) (i₂ ≫ snd f i)) (Z := diagonalObj f) (diagonal f)
          (map (i₁ ≫ snd f i) (i₂ ≫ snd f i) f f (i₁ ≫ fst f i) (i₂ ≫ fst f i) i ⋯ ⋯))
        (Iso.inv (pullbackDiagonalMapIso f i i₁ i₂) :
          pullback i₁ i₂ ⟶
            pullback (Y := pullback (i₁ ≫ snd f i) (i₂ ≫ snd f i)) (Z := diagonalObj f) (diagonal f)
              (map (i₁ ≫ snd f i) (i₂ ≫ snd f i) f f (i₁ ≫ fst f i) (i₂ ≫ fst f i) i ⋯ ⋯))
        (snd (diagonal f) (map (i₁ ≫ snd f i) (i₂ ≫ snd f i) f f (i₁ ≫ fst f i) (i₂ ≫ fst f i) i ⋯ ⋯) ≫
            fst (i₁ ≫ snd f i) (i₂ ≫ snd f i) :
          pullback (Y := pullback (i₁ ≫ snd f i) (i₂ ≫ snd f i)) (Z := diagonalObj f) (diagonal f)
              (map (i₁ ≫ snd f i) (i₂ ≫ snd f i) f f (i₁ ≫ fst f i) (i₂ ≫ fst f i) i ⋯ ⋯) ⟶
            V₁) :
      pullback i₁ i₂ ⟶ V₁)
    (fst i₁ i₂ : pullback i₁ i₂ ⟶ V₁)

Tactic:
delta pullbackDiagonalMapIso

Premises used: CategoryTheory.Limits.pullbackDiagonalMapIso
-- 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
U V₁ V₂ : C
f : X ⟶ Y
i : U ⟶ Y
i₁ : V₁ ⟶ pullback f i
i₂ : V₂ ⟶ pullback f i
inst_2 : HasPullback i₁ i₂
⊢ Eq (α := pullback i₁ i₂ ⟶ V₁)
    (CategoryStruct.comp (Y :=
        pullback (Y := pullback (i₁ ≫ snd f i) (i₂ ≫ snd f i)) (Z := diagonalObj f) (diagonal f)
          (map (i₁ ≫ snd f i) (i₂ ≫ snd f i) f f (i₁ ≫ fst f i) (i₂ ≫ fst f i) i ⋯ ⋯))
        (Iso.inv { hom := hom f i i₁ i₂, inv := inv f i i₁ i₂, hom_inv_id := ⋯, inv_hom_id := ⋯ } :
          pullback i₁ i₂ ⟶
            pullback (Y := pullback (i₁ ≫ snd f i) (i₂ ≫ snd f i)) (Z := diagonalObj f) (diagonal f)
              (map (i₁ ≫ snd f i) (i₂ ≫ snd f i) f f (i₁ ≫ fst f i) (i₂ ≫ fst f i) i ⋯ ⋯))
        (snd (diagonal f) (map (i₁ ≫ snd f i) (i₂ ≫ snd f i) f f (i₁ ≫ fst f i) (i₂ ≫ fst f i) i ⋯ ⋯) ≫
            fst (i₁ ≫ snd f i) (i₂ ≫ snd f i) :
          pullback (Y := pullback (i₁ ≫ snd f i) (i₂ ≫ snd f i)) (Z := diagonalObj f) (diagonal f)
              (map (i₁ ≫ snd f i) (i₂ ≫ snd f i) f f (i₁ ≫ fst f i) (i₂ ≫ fst f i) i ⋯ ⋯) ⟶
            V₁) :
      pullback i₁ i₂ ⟶ V₁)
    (fst i₁ i₂ : pullback i₁ i₂ ⟶ V₁)

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
U V₁ V₂ : C
f : X ⟶ Y
i : U ⟶ Y
i₁ : V₁ ⟶ pullback f i
i₂ : V₂ ⟶ pullback f i
inst_2 : HasPullback i₁ i₂
delta :
  Eq (α := pullback i₁ i₂ ⟶ V₂)
    (CategoryStruct.comp (Y :=
        pullback (Y := pullback (i₁ ≫ snd f i) (i₂ ≫ snd f i)) (Z := diagonalObj f) (diagonal f)
          (map (i₁ ≫ snd f i) (i₂ ≫ snd f i) f f (i₁ ≫ fst f i) (i₂ ≫ fst f i) i ⋯ ⋯))
        (Iso.inv { hom := hom f i i₁ i₂, inv := inv f i i₁ i₂, hom_inv_id := ⋯, inv_hom_id := ⋯ } :
          pullback i₁ i₂ ⟶
            pullback (Y := pullback (i₁ ≫ snd f i) (i₂ ≫ snd f i)) (Z := diagonalObj f) (diagonal f)
              (map (i₁ ≫ snd f i) (i₂ ≫ snd f i) f f (i₁ ≫ fst f i) (i₂ ≫ fst f i) i ⋯ ⋯))
        (snd (diagonal f) (map (i₁ ≫ snd f i) (i₂ ≫ snd f i) f f (i₁ ≫ fst f i) (i₂ ≫ fst f i) i ⋯ ⋯) ≫
            snd (i₁ ≫ snd f i) (i₂ ≫ snd f i) :
          pullback (Y := pullback (i₁ ≫ snd f i) (i₂ ≫ snd f i)) (Z := diagonalObj f) (diagonal f)
              (map (i₁ ≫ snd f i) (i₂ ≫ snd f i) f f (i₁ ≫ fst f i) (i₂ ≫ fst f i) i ⋯ ⋯) ⟶
            V₂) :
      pullback i₁ i₂ ⟶ V₂)
    (snd i₁ i₂ : pullback i₁ i₂ ⟶ V₂)
⊢ Eq (α := pullback i₁ i₂ ⟶ V₂)
    (CategoryStruct.comp (Y :=
        pullback (Y := pullback (i₁ ≫ snd f i) (i₂ ≫ snd f i)) (Z := diagonalObj f) (diagonal f)
          (map (i₁ ≫ snd f i) (i₂ ≫ snd f i) f f (i₁ ≫ fst f i) (i₂ ≫ fst f i) i ⋯ ⋯))
        (Iso.inv (pullbackDiagonalMapIso f i i₁ i₂) :
          pullback i₁ i₂ ⟶
            pullback (Y := pullback (i₁ ≫ snd f i) (i₂ ≫ snd f i)) (Z := diagonalObj f) (diagonal f)
              (map (i₁ ≫ snd f i) (i₂ ≫ snd f i) f f (i₁ ≫ fst f i) (i₂ ≫ fst f i) i ⋯ ⋯))
        (snd (diagonal f) (map (i₁ ≫ snd f i) (i₂ ≫ snd f i) f f (i₁ ≫ fst f i) (i₂ ≫ fst f i) i ⋯ ⋯) ≫
            snd (i₁ ≫ snd f i) (i₂ ≫ snd f i) :
          pullback (Y := pullback (i₁ ≫ snd f i) (i₂ ≫ snd f i)) (Z := diagonalObj f) (diagonal f)
              (map (i₁ ≫ snd f i) (i₂ ≫ snd f i) f f (i₁ ≫ fst f i) (i₂ ≫ fst f i) i ⋯ ⋯) ⟶
            V₂) :
      pullback i₁ i₂ ⟶ V₂)
    (snd i₁ i₂ : pullback i₁ i₂ ⟶ V₂)

Tactic:
delta pullbackDiagonalMapIso

Premises used: CategoryTheory.Limits.pullbackDiagonalMapIso
-- 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
U V₁ V₂ : C
f : X ⟶ Y
i : U ⟶ Y
i₁ : V₁ ⟶ pullback f i
i₂ : V₂ ⟶ pullback f i
inst_2 : HasPullback i₁ i₂
⊢ Eq (α := pullback i₁ i₂ ⟶ V₂)
    (CategoryStruct.comp (Y :=
        pullback (Y := pullback (i₁ ≫ snd f i) (i₂ ≫ snd f i)) (Z := diagonalObj f) (diagonal f)
          (map (i₁ ≫ snd f i) (i₂ ≫ snd f i) f f (i₁ ≫ fst f i) (i₂ ≫ fst f i) i ⋯ ⋯))
        (Iso.inv { hom := hom f i i₁ i₂, inv := inv f i i₁ i₂, hom_inv_id := ⋯, inv_hom_id := ⋯ } :
          pullback i₁ i₂ ⟶
            pullback (Y := pullback (i₁ ≫ snd f i) (i₂ ≫ snd f i)) (Z := diagonalObj f) (diagonal f)
              (map (i₁ ≫ snd f i) (i₂ ≫ snd f i) f f (i₁ ≫ fst f i) (i₂ ≫ fst f i) i ⋯ ⋯))
        (snd (diagonal f) (map (i₁ ≫ snd f i) (i₂ ≫ snd f i) f f (i₁ ≫ fst f i) (i₂ ≫ fst f i) i ⋯ ⋯) ≫
            snd (i₁ ≫ snd f i) (i₂ ≫ snd f i) :
          pullback (Y := pullback (i₁ ≫ snd f i) (i₂ ≫ snd f i)) (Z := diagonalObj f) (diagonal f)
              (map (i₁ ≫ snd f i) (i₂ ≫ snd f i) f f (i₁ ≫ fst f i) (i₂ ≫ fst f i) i ⋯ ⋯) ⟶
            V₂) :
      pullback i₁ i₂ ⟶ V₂)
    (snd i₁ i₂ : pullback i₁ i₂ ⟶ V₂)

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
U V₁ V₂ : C
f : X ⟶ Y
i : U ⟶ Y
i₁ : V₁ ⟶ pullback f i
i₂ : V₂ ⟶ pullback f i
inst_2 : HasPullback i₁ i₂
⊢ (i₁ ≫ snd f i) ≫ i = (i₁ ≫ fst f i) ≫ f

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 Z : C
inst_1 : HasPullbacks.{v_1, u_1} C
U V₁ V₂ : C
f : X ⟶ Y
i : U ⟶ Y
i₁ : V₁ ⟶ pullback f i
i₂ : V₂ ⟶ pullback f i
inst_2 : HasPullback i₁ i₂
⊢ (i₂ ≫ snd f i) ≫ i = (i₂ ≫ fst f i) ≫ f

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
U V₁ V₂ : C
f : X ⟶ Y
i : U ⟶ Y
i₁ : V₁ ⟶ pullback f i
i₂ : V₂ ⟶ pullback f i
inst_2 : HasPullback i₁ i₂
h₀ :
  Eq (α := pullback i₁ i₂ ⟶ X)
    (CategoryStruct.comp (Y := pullback f f) ((fst i₁ i₂ ≫ i₁ ≫ fst f i) ≫ diagonal f) (fst f f))
    (CategoryStruct.comp (Y := pullback f f)
      (CategoryStruct.comp (Y := pullback (i₁ ≫ snd f i) (i₂ ≫ snd f i))
        (map i₁ i₂ (i₁ ≫ snd f i) (i₂ ≫ snd f i) (𝟙 V₁) (𝟙 V₂) (snd f i) ⋯ ⋯)
        (map (i₁ ≫ snd f i) (i₂ ≫ snd f i) f f (i₁ ≫ fst f i) (i₂ ≫ fst f i) i ⋯ ⋯))
      (fst f f))
h₁ :
  Eq (α := pullback i₁ i₂ ⟶ X)
    (CategoryStruct.comp (Y := pullback f f) ((fst i₁ i₂ ≫ i₁ ≫ fst f i) ≫ diagonal f) (snd f f))
    (CategoryStruct.comp (Y := pullback f f)
      (CategoryStruct.comp (Y := pullback (i₁ ≫ snd f i) (i₂ ≫ snd f i))
        (map i₁ i₂ (i₁ ≫ snd f i) (i₂ ≫ snd f i) (𝟙 V₁) (𝟙 V₂) (snd f i) ⋯ ⋯)
        (map (i₁ ≫ snd f i) (i₂ ≫ snd f i) f f (i₁ ≫ fst f i) (i₂ ≫ fst f i) i ⋯ ⋯))
      (snd f f))
⊢ Eq (α := pullback i₁ i₂ ⟶ diagonalObj f) ((fst i₁ i₂ ≫ i₁ ≫ fst f i) ≫ diagonal f)
    (CategoryStruct.comp (Y := pullback (i₁ ≫ snd f i) (i₂ ≫ snd f i))
      (map i₁ i₂ (i₁ ≫ snd f i) (i₂ ≫ snd f i) (𝟙 V₁) (𝟙 V₂) (snd f i) ⋯ ⋯)
      (map (i₁ ≫ snd f i) (i₂ ≫ snd f i) f f (i₁ ≫ fst f i) (i₂ ≫ fst f i) 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
U V₁ V₂ : C
f : X ⟶ Y
i : U ⟶ Y
i₁ : V₁ ⟶ pullback f i
i₂ : V₂ ⟶ pullback f i
inst_2 : HasPullback i₁ i₂
⊢ Eq (α := pullback i₁ i₂ ⟶ X)
    (CategoryStruct.comp (Y := pullback f f) ((fst i₁ i₂ ≫ i₁ ≫ fst f i) ≫ diagonal f) (fst f f))
    (CategoryStruct.comp (Y := pullback f f)
      (CategoryStruct.comp (Y := pullback (i₁ ≫ snd f i) (i₂ ≫ snd f i))
        (map i₁ i₂ (i₁ ≫ snd f i) (i₂ ≫ snd f i) (𝟙 V₁) (𝟙 V₂) (snd f i) ⋯ ⋯)
        (map (i₁ ≫ snd f i) (i₂ ≫ snd f i) f f (i₁ ≫ fst f i) (i₂ ≫ fst f i) i ⋯ ⋯))
      (fst f f))

Tactic:
simp [condition_assoc]

Premises used: CategoryTheory.Limits.pullback.condition_assoc
-- 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
U V₁ V₂ : C
f : X ⟶ Y
i : U ⟶ Y
i₁ : V₁ ⟶ pullback f i
i₂ : V₂ ⟶ pullback f i
inst_2 : HasPullback i₁ i₂
⊢ Eq (α := pullback i₁ i₂ ⟶ X)
    (CategoryStruct.comp (Y := pullback f f) ((fst i₁ i₂ ≫ i₁ ≫ fst f i) ≫ diagonal f) (snd f f))
    (CategoryStruct.comp (Y := pullback f f)
      (CategoryStruct.comp (Y := pullback (i₁ ≫ snd f i) (i₂ ≫ snd f i))
        (map i₁ i₂ (i₁ ≫ snd f i) (i₂ ≫ snd f i) (𝟙 V₁) (𝟙 V₂) (snd f i) ⋯ ⋯)
        (map (i₁ ≫ snd f i) (i₂ ≫ snd f i) f f (i₁ ≫ fst f i) (i₂ ≫ fst f i) i ⋯ ⋯))
      (snd f f))

Tactic:
simp [condition_assoc]

Premises used: CategoryTheory.Limits.pullback.condition_assoc
-- 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 : 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) ⋯ ⋯)
refine_1 :
  pullback (Y := pullback (f ≫ i) (g ≫ i)) (Z := diagonalObj i) (diagonal i) (map (f ≫ i) (g ≫ i) i i f g (𝟙 S) ⋯ ⋯) ≅
    pullback (Y :=
      pullback (CategoryStruct.comp (Y := pullback i (𝟙 S)) (f ≫ inv (fst i (𝟙 S))) (snd i (𝟙 S)))
        (CategoryStruct.comp (Y := pullback i (𝟙 S)) (g ≫ inv (fst i (𝟙 S))) (snd i (𝟙 S))))
      (Z := diagonalObj i) (diagonal i)
      (map (CategoryStruct.comp (Y := pullback i (𝟙 S)) (f ≫ inv (fst i (𝟙 S))) (snd i (𝟙 S)))
        (CategoryStruct.comp (Y := pullback i (𝟙 S)) (g ≫ inv (fst i (𝟙 S))) (snd i (𝟙 S))) i i
        (CategoryStruct.comp (Y := pullback i (𝟙 S)) (f ≫ inv (fst i (𝟙 S))) (fst i (𝟙 S)))
        (CategoryStruct.comp (Y := pullback i (𝟙 S)) (g ≫ inv (fst i (𝟙 S))) (fst i (𝟙 S))) (𝟙 S) ⋯ ⋯)
refine_2 : pullback (Z := pullback i (𝟙 S)) (f ≫ inv (fst i (𝟙 S))) (g ≫ inv (fst i (𝟙 S))) ≅ pullback f g
⊢ pullback (Y := pullback (f ≫ i) (g ≫ i)) (Z := diagonalObj i) (diagonal i) (map (f ≫ i) (g ≫ i) i i f g (𝟙 S) ⋯ ⋯) ≅
    pullback f g

Tactic:
refine ?_ ≪≫
    pullbackDiagonalMapIso i (𝟙 _) (f ≫ inv (pullback.fst _ _)) (g ≫ inv (pullback.fst _ _)) ≪≫ ?_

Premises used: CategoryTheory.Limits.pullbackDiagonalMapIso, CategoryTheory.CategoryStruct.id, CategoryTheory.Limits.pullback.fst, CategoryTheory.CategoryStruct.comp, CategoryTheory.inv
-- 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 : 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) ⋯ ⋯)
refine_1 : f ≫ i = CategoryStruct.comp (Y := pullback i (𝟙 S)) (f ≫ inv (fst i (𝟙 S))) (snd i (𝟙 S) ≫ 𝟙 S)
refine_1₁ : f ≫ i = CategoryStruct.comp (Y := pullback i (𝟙 S)) (f ≫ inv (fst i (𝟙 S))) (fst i (𝟙 S) ≫ i)
refine_1₂ : f ≫ i = f ≫ CategoryStruct.comp (Y := pullback i (𝟙 S)) (inv (fst i (𝟙 S))) (fst i (𝟙 S) ≫ i)
refine_1₃ refine_1₄ : f ≫ i = f ≫ i
⊢ f ≫ i = CategoryStruct.comp (Y := pullback i (𝟙 S)) (f ≫ inv (fst i (𝟙 S))) (snd i (𝟙 S))

Tactic:
rw [← Category.comp_id (pullback.snd ..), ← condition, Category.assoc, IsIso.inv_hom_id_assoc]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Limits.pullback.snd, CategoryTheory.Category.comp_id, CategoryTheory.Limits.pullback.condition, CategoryTheory.IsIso.inv_hom_id_assoc
-- 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 : 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) ⋯ ⋯)
refine_1 : g ≫ i = CategoryStruct.comp (Y := pullback i (𝟙 S)) (g ≫ inv (fst i (𝟙 S))) (snd i (𝟙 S) ≫ 𝟙 S)
refine_1₁ : g ≫ i = CategoryStruct.comp (Y := pullback i (𝟙 S)) (g ≫ inv (fst i (𝟙 S))) (fst i (𝟙 S) ≫ i)
refine_1₂ : g ≫ i = g ≫ CategoryStruct.comp (Y := pullback i (𝟙 S)) (inv (fst i (𝟙 S))) (fst i (𝟙 S) ≫ i)
refine_1₃ refine_1₄ : g ≫ i = g ≫ i
⊢ g ≫ i = CategoryStruct.comp (Y := pullback i (𝟙 S)) (g ≫ inv (fst i (𝟙 S))) (snd i (𝟙 S))

Tactic:
rw [← Category.comp_id (pullback.snd ..), ← condition, Category.assoc, IsIso.inv_hom_id_assoc]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Limits.pullback.snd, CategoryTheory.Category.comp_id, CategoryTheory.Limits.pullback.condition, CategoryTheory.IsIso.inv_hom_id_assoc
-- 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 : 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) ⋯ ⋯)
refine_1 : Eq (α := T ⟶ diagonalObj i) (diagonal i) (𝟙 T ≫ diagonal i)
refine_1₁ refine_1₂ : Eq (α := T ⟶ diagonalObj i) (diagonal i) (diagonal i)
⊢ diagonal i ≫ 𝟙 (diagonalObj i) = 𝟙 T ≫ diagonal i

Tactic:
rw [Category.comp_id, Category.id_comp]

Premises used: CategoryTheory.Category.comp_id, CategoryTheory.Category.id_comp