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 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 (α := pullback (f ≫ i) (g ≫ i) ⟶ T) ((map (f ≫ i) (g ≫ i) i i f g (𝟙 S) ⋯ ⋯ ≫ 𝟙 (diagonalObj i)) ≫ fst i i)
    (CategoryStruct.comp (Y := pullback i i)
      (CategoryStruct.comp (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))))
        (Iso.hom (congrHom ⋯ ⋯))
        (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) ⋯ ⋯))
      (fst i i))
refine_1₁ :
  Eq (α := pullback (f ≫ i) (g ≫ i) ⟶ T) ((map (f ≫ i) (g ≫ i) i i f g (𝟙 S) ⋯ ⋯ ≫ 𝟙 (diagonalObj i)) ≫ snd i i)
    (CategoryStruct.comp (Y := pullback i i)
      (CategoryStruct.comp (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))))
        (Iso.hom (congrHom ⋯ ⋯))
        (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) ⋯ ⋯))
      (snd i i))
⊢ Eq (α := pullback (f ≫ i) (g ≫ i) ⟶ diagonalObj i) (map (f ≫ i) (g ≫ i) i i f g (𝟙 S) ⋯ ⋯ ≫ 𝟙 (diagonalObj i))
    (CategoryStruct.comp (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))))
      (Iso.hom (congrHom ⋯ ⋯))
      (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) ⋯ ⋯))

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
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 ≫ i) (g ≫ i) ⟶ T) ((map (f ≫ i) (g ≫ i) i i f g (𝟙 S) ⋯ ⋯ ≫ 𝟙 (diagonalObj i)) ≫ fst i i)
    (CategoryStruct.comp (Y := pullback i i)
      (CategoryStruct.comp (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))))
        (Iso.hom (congrHom ⋯ ⋯))
        (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) ⋯ ⋯))
      (fst i i))

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 : 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 ≫ i) (g ≫ i) ⟶ T) ((map (f ≫ i) (g ≫ i) i i f g (𝟙 S) ⋯ ⋯ ≫ 𝟙 (diagonalObj i)) ≫ snd i i)
    (CategoryStruct.comp (Y := pullback i i)
      (CategoryStruct.comp (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))))
        (Iso.hom (congrHom ⋯ ⋯))
        (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) ⋯ ⋯))
      (snd i i))

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 : 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) ⋯ ⋯)
⊢ IsIso (X :=
    pullback (Y := pullback (f ≫ i) (g ≫ i)) (Z := diagonalObj i) (diagonal i) (map (f ≫ i) (g ≫ i) i i f g (𝟙 S) ⋯ ⋯))
    (Y :=
    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) ⋯ ⋯))
    (map (diagonal i) (map (f ≫ i) (g ≫ i) i i f g (𝟙 S) ⋯ ⋯) (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) ⋯ ⋯)
      (𝟙 T) (Iso.hom (congrHom ⋯ ⋯)) (𝟙 (diagonalObj i)) ⋯ ⋯)

Tactic:
infer_instance
-- 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_2 : CategoryStruct.comp (Y := pullback i (𝟙 S)) (f ≫ inv (fst i (𝟙 S))) (fst i (𝟙 S)) = 𝟙 X ≫ f
refine_2₁ : CategoryStruct.comp (Y := pullback i (𝟙 S)) (g ≫ inv (fst i (𝟙 S))) (fst i (𝟙 S)) = 𝟙 Y ≫ g
refine_2₂ :
  IsIso (X := pullback (Z := pullback i (𝟙 S)) (f ≫ inv (fst i (𝟙 S))) (g ≫ inv (fst i (𝟙 S)))) (Y := pullback f g)
    (map (f ≫ inv (fst i (𝟙 S))) (g ≫ inv (fst i (𝟙 S))) f g (𝟙 X) (𝟙 Y) (fst i (𝟙 S)) ⋯ ⋯)
⊢ pullback (Z := pullback i (𝟙 S)) (f ≫ inv (fst i (𝟙 S))) (g ≫ inv (fst i (𝟙 S))) ≅ pullback f g

Tactic:
refine @asIso _ _ _ _ (pullback.map _ _ _ _ (𝟙 _) (𝟙 _) (pullback.fst _ _) ?_ ?_) ?_

Premises used: CategoryTheory.CategoryStruct.id, CategoryTheory.Limits.pullback.map, CategoryTheory.Limits.pullback.fst, CategoryTheory.asIso
-- 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_2 : f ≫ CategoryStruct.comp (Y := pullback i (𝟙 S)) (inv (fst i (𝟙 S))) (fst i (𝟙 S)) = 𝟙 X ≫ f
refine_2₁ : f ≫ 𝟙 T = 𝟙 X ≫ f
refine_2₂ : f = 𝟙 X ≫ f
refine_2₃ refine_2₄ : f = f
⊢ CategoryStruct.comp (Y := pullback i (𝟙 S)) (f ≫ inv (fst i (𝟙 S))) (fst i (𝟙 S)) = 𝟙 X ≫ f

Tactic:
rw [Category.assoc, IsIso.inv_hom_id, Category.comp_id, Category.id_comp]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.IsIso.inv_hom_id, CategoryTheory.Category.comp_id, CategoryTheory.Category.id_comp
-- 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_2 : g ≫ CategoryStruct.comp (Y := pullback i (𝟙 S)) (inv (fst i (𝟙 S))) (fst i (𝟙 S)) = 𝟙 Y ≫ g
refine_2₁ : g ≫ 𝟙 T = 𝟙 Y ≫ g
refine_2₂ : g = 𝟙 Y ≫ g
refine_2₃ refine_2₄ : g = g
⊢ CategoryStruct.comp (Y := pullback i (𝟙 S)) (g ≫ inv (fst i (𝟙 S))) (fst i (𝟙 S)) = 𝟙 Y ≫ g

Tactic:
rw [Category.assoc, IsIso.inv_hom_id, Category.comp_id, Category.id_comp]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.IsIso.inv_hom_id, CategoryTheory.Category.comp_id, CategoryTheory.Category.id_comp
-- 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) ⋯ ⋯)
⊢ IsIso (X := pullback (Z := pullback i (𝟙 S)) (f ≫ inv (fst i (𝟙 S))) (g ≫ inv (fst i (𝟙 S)))) (Y := pullback f g)
    (map (f ≫ inv (fst i (𝟙 S))) (g ≫ inv (fst i (𝟙 S))) f g (𝟙 X) (𝟙 Y) (fst i (𝟙 S)) ⋯ ⋯)

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

Tactic:
rw [Iso.inv_comp_eq, ← Category.comp_id (pullback.fst _ _), ← diagonal_fst i,
    pullback.condition_assoc]

Premises used: CategoryTheory.Iso.inv_comp_eq, CategoryTheory.Limits.pullback.diagonal_fst, CategoryTheory.Category.comp_id, CategoryTheory.Limits.pullback.condition_assoc, 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
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 (Y := pullback (f ≫ i) (g ≫ i)) (Z := diagonalObj i) (diagonal i) (map (f ≫ i) (g ≫ i) i i f g (𝟙 S) ⋯ ⋯) ⟶
      T)
    (snd (diagonal i) (map (f ≫ i) (g ≫ i) i i f g (𝟙 S) ⋯ ⋯) ≫
      CategoryStruct.comp (Y := diagonalObj i) (map (f ≫ i) (g ≫ i) i i f g (𝟙 S) ⋯ ⋯) (fst i i))
    (CategoryStruct.comp (Y := pullback f g) (Iso.hom (pullbackDiagonalMapIdIso f g i)) (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) ⋯ ⋯)
rw :
  Eq (α :=
    pullback (Y := pullback (f ≫ i) (g ≫ i)) (Z := diagonalObj i) (diagonal i) (map (f ≫ i) (g ≫ i) i i f g (𝟙 S) ⋯ ⋯) ⟶
      X)
    (snd (diagonal i) (map (f ≫ i) (g ≫ i) i i f g (𝟙 S) ⋯ ⋯) ≫ fst (f ≫ i) (g ≫ i))
    (CategoryStruct.comp (Y := pullback f g) (Iso.hom (pullbackDiagonalMapIdIso f g i)) (fst f g))
⊢ Eq (α := pullback f g ⟶ X)
    (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.inv (pullbackDiagonalMapIdIso f g i))
      (snd (diagonal i) (map (f ≫ i) (g ≫ i) i i f g (𝟙 S) ⋯ ⋯) ≫ fst (f ≫ i) (g ≫ i)))
    (fst f g)

Tactic:
rw [Iso.inv_comp_eq]

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

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

Tactic:
rw [Iso.inv_comp_eq]

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

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

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
f : X ⟶ Y
g : Y ⟶ Z
⊢ CategoryStruct.comp (Y := pullback g g) (f ≫ diagonal g) (fst g g) =
    CategoryStruct.comp (Y := pullback g g)
      (CategoryStruct.comp (Y := diagonalObj (f ≫ g)) (diagonal (f ≫ g)) (map (f ≫ g) (f ≫ g) g g f f (𝟙 Z) ⋯ ⋯))
      (fst g 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
f : X ⟶ Y
g : Y ⟶ Z
⊢ CategoryStruct.comp (Y := pullback g g) (f ≫ diagonal g) (snd g g) =
    CategoryStruct.comp (Y := pullback g g)
      (CategoryStruct.comp (Y := diagonalObj (f ≫ g)) (diagonal (f ≫ g)) (map (f ≫ g) (f ≫ g) g g f f (𝟙 Z) ⋯ ⋯))
      (snd g g)

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 ⟶ 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)
w₂ :
  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 ⋯ ⋯)
apply :
  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) ⋯ ⋯)
⊢ IsPullback (P := 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:
apply IsPullback.of_iso_pullback _ (pullbackDiagonalMapIdIso f g i).symm

Premises used: CategoryTheory.Iso.symm, CategoryTheory.IsPullback.of_iso_pullback, CategoryTheory.Limits.pullbackDiagonalMapIdIso