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
f : X ⟶ Y
inst_1 : HasPullback f f
H : IsIso (Y := diagonalObj f) (diagonal f)
Z : C
x x_1 : Z ⟶ X
e : x ≫ f = x_1 ≫ f
rw : CategoryStruct.comp (Y := pullback f f) (lift x x_1 e) (fst f f) = x_1
rw₁ : CategoryStruct.comp (Y := pullback f f) (lift x x_1 e) (snd f f) = x_1
rw₂ rw₃ : x_1 = x_1
⊢ x = x_1

Tactic:
rw [← lift_fst _ _ e, (cancel_epi (g := fst f f) (h := snd f f)
    (diagonal f)).mp (by simp), lift_snd]

Premises used: CategoryTheory.Limits.pullback.lift_snd, Iff.mp, CategoryTheory.Limits.pullback.diagonal, CategoryTheory.cancel_epi, CategoryTheory.Limits.pullback.lift_fst
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Diagonal
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X Y : C
f : X ⟶ Y
inst_1 : HasPullback f f
⊢ IsKernelPair (R := pullback f f) f (fst f f) (snd f f)

Tactic:
IsPullback.of_hasPullback f f

Premises used: CategoryTheory.IsPullback.of_hasPullback
-- 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
⊢ (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
⊢ (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
rw : fst (diagonal f) (map (i₁ ≫ snd f i) (i₂ ≫ snd f i) f f (i₁ ≫ fst f i) (i₂ ≫ fst f i) i ⋯ ⋯) ≫ 𝟙 X
| fst (diagonal f) (map (i₁ ≫ snd f i) (i₂ ≫ snd f i) f f (i₁ ≫ fst f i) (i₂ ≫ fst f i) i ⋯ ⋯)

Tactic:
rw [← Category.comp_id (pullback.fst _ _)]

Premises used: CategoryTheory.Category.comp_id, CategoryTheory.Limits.pullback.fst
-- 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
conv_rhs :
  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 ⋯ ⋯) ⟶
      X)
    (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) ≫ i₁ ≫ fst f i)
    (fst (diagonal f) (map (i₁ ≫ snd f i) (i₂ ≫ snd f i) f f (i₁ ≫ fst f i) (i₂ ≫ fst f i) i ⋯ ⋯) ≫ 𝟙 X)
⊢ 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 ⋯ ⋯) ⟶
      X)
    (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) ≫ i₁ ≫ fst f i)
    (fst (diagonal f) (map (i₁ ≫ snd f i) (i₂ ≫ snd f i) f f (i₁ ≫ fst f i) (i₂ ≫ fst f i) i ⋯ ⋯))

Tactic:
conv_rhs => rw [← Category.comp_id (pullback.fst _ _)]

Premises used: CategoryTheory.Category.comp_id, CategoryTheory.Limits.pullback.fst
-- 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
rw :
  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 ⋯ ⋯) ⟶
      X)
    (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) ≫ i₁ ≫ fst f i)
    (fst (diagonal f) (map (i₁ ≫ snd f i) (i₂ ≫ snd f i) f f (i₁ ≫ fst f i) (i₂ ≫ fst f i) i ⋯ ⋯) ≫
      CategoryStruct.comp (Y := diagonalObj f) (diagonal f) (fst f f))
rw₁ :
  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 ⋯ ⋯) ⟶
      X)
    (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) ≫ i₁ ≫ fst f i)
    (snd (diagonal f) (map (i₁ ≫ snd f i) (i₂ ≫ snd f i) f f (i₁ ≫ fst f i) (i₂ ≫ fst f i) i ⋯ ⋯) ≫
      CategoryStruct.comp (Y := diagonalObj f)
        (map (i₁ ≫ snd f i) (i₂ ≫ snd f i) f f (i₁ ≫ fst f i) (i₂ ≫ fst f i) i ⋯ ⋯) (fst f f))
rw₂ rw₃ :
  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 ⋯ ⋯) ⟶
      X)
    (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) ≫ i₁ ≫ fst f 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) ≫ i₁ ≫ fst f 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 ⋯ ⋯) ⟶
      X)
    (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) ≫ i₁ ≫ fst f i)
    (fst (diagonal f) (map (i₁ ≫ snd f i) (i₂ ≫ snd f i) f f (i₁ ≫ fst f i) (i₂ ≫ fst f i) i ⋯ ⋯) ≫ 𝟙 X)

Tactic:
rw [← diagonal_fst f, pullback.condition_assoc, pullback.lift_fst]

Premises used: CategoryTheory.Limits.pullback.diagonal_fst, CategoryTheory.Limits.pullback.condition_assoc, CategoryTheory.Limits.pullback.lift_fst
-- 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
conv_rhs :
  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 ⋯ ⋯) ⟶
      X)
    (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) ≫ i₂ ≫ fst f i)
    (fst (diagonal f) (map (i₁ ≫ snd f i) (i₂ ≫ snd f i) f f (i₁ ≫ fst f i) (i₂ ≫ fst f i) i ⋯ ⋯) ≫ 𝟙 X)
⊢ 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 ⋯ ⋯) ⟶
      X)
    (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) ≫ i₂ ≫ fst f i)
    (fst (diagonal f) (map (i₁ ≫ snd f i) (i₂ ≫ snd f i) f f (i₁ ≫ fst f i) (i₂ ≫ fst f i) i ⋯ ⋯))

Tactic:
conv_rhs => rw [← Category.comp_id (pullback.fst _ _)]

Premises used: CategoryTheory.Category.comp_id, CategoryTheory.Limits.pullback.fst
-- 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
rw :
  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 ⋯ ⋯) ⟶
      X)
    (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) ≫ i₂ ≫ fst f i)
    (fst (diagonal f) (map (i₁ ≫ snd f i) (i₂ ≫ snd f i) f f (i₁ ≫ fst f i) (i₂ ≫ fst f i) i ⋯ ⋯) ≫
      CategoryStruct.comp (Y := diagonalObj f) (diagonal f) (snd f f))
rw₁ :
  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 ⋯ ⋯) ⟶
      X)
    (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) ≫ i₂ ≫ fst f i)
    (snd (diagonal f) (map (i₁ ≫ snd f i) (i₂ ≫ snd f i) f f (i₁ ≫ fst f i) (i₂ ≫ fst f i) i ⋯ ⋯) ≫
      CategoryStruct.comp (Y := diagonalObj f)
        (map (i₁ ≫ snd f i) (i₂ ≫ snd f i) f f (i₁ ≫ fst f i) (i₂ ≫ fst f i) i ⋯ ⋯) (snd f f))
rw₂ rw₃ :
  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 ⋯ ⋯) ⟶
      X)
    (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) ≫ i₂ ≫ fst f 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) ≫ i₂ ≫ fst f 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 ⋯ ⋯) ⟶
      X)
    (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) ≫ i₂ ≫ fst f i)
    (fst (diagonal f) (map (i₁ ≫ snd f i) (i₂ ≫ snd f i) f f (i₁ ≫ fst f i) (i₂ ≫ fst f i) i ⋯ ⋯) ≫ 𝟙 X)

Tactic:
rw [← diagonal_snd f, pullback.condition_assoc, pullback.lift_snd]

Premises used: CategoryTheory.Limits.pullback.diagonal_snd, CategoryTheory.Limits.pullback.lift_snd, 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
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 only [Category.assoc, condition]

Premises used: CategoryTheory.Category.assoc, 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 only [Category.assoc, condition]

Premises used: CategoryTheory.Category.assoc, 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₂
h₀ :
  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 ⋯ ⋯) ⟶
      X)
    (((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)) ≫
        i₁) ≫
      fst f 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)) ≫
        i₂) ≫
      fst f i)
h₁ :
  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 ⋯ ⋯) ⟶
      U)
    (((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)) ≫
        i₁) ≫
      snd f 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)) ≫
        i₂) ≫
      snd f 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 ⋯ ⋯) ⟶
      pullback f 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)) ≫
      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)) ≫
      i₂)

Tactic:
ext
-- 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₂
⊢ 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 ⋯ ⋯) ⟶
      X)
    (((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)) ≫
        i₁) ≫
      fst f 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)) ≫
        i₂) ≫
      fst f i)

Tactic:
simp only [Category.assoc, pullback_diagonal_map_snd_fst_fst,
      pullback_diagonal_map_snd_snd_fst]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Limits.pullback_diagonal_map_snd_fst_fst, CategoryTheory.Limits.pullback_diagonal_map_snd_snd_fst
-- 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₂
⊢ 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 ⋯ ⋯) ⟶
      U)
    (((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)) ≫
        i₁) ≫
      snd f 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)) ≫
        i₂) ≫
      snd f i)

Tactic:
simp only [Category.assoc, condition]

Premises used: CategoryTheory.Category.assoc, 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₂
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 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₂
⊢ 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 only [Category.assoc, diagonal_fst, Category.comp_id, limit.lift_π,
            PullbackCone.mk_pt, PullbackCone.mk_π_app, limit.lift_π_assoc, cospan_left]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Limits.PullbackCone.mk_π_app, CategoryTheory.Limits.cospan_left, CategoryTheory.Limits.pullback.diagonal_fst, CategoryTheory.Category.comp_id, CategoryTheory.Limits.PullbackCone.mk_pt, CategoryTheory.Limits.limit.lift_π_assoc, CategoryTheory.Limits.limit.lift_π
-- 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₂
⊢ 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 only [condition_assoc, Category.assoc, diagonal_snd, Category.comp_id, limit.lift_π,
            PullbackCone.mk_pt, PullbackCone.mk_π_app, limit.lift_π_assoc, cospan_right]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Limits.PullbackCone.mk_π_app, CategoryTheory.Limits.pullback.diagonal_snd, CategoryTheory.Category.comp_id, CategoryTheory.Limits.pullback.condition_assoc, CategoryTheory.Limits.cospan_right, CategoryTheory.Limits.PullbackCone.mk_pt, CategoryTheory.Limits.limit.lift_π_assoc, 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 (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₂)
        (fst 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 ⋯ ⋯) ≫
        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₁)
⊢ 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₂)
        (fst 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 ⋯ ⋯) ≫
        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₁)

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₂)
        (fst 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 ⋯ ⋯) ≫
        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₁)

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_π