awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Diagonal (goal)
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) ⋯ ⋯)
⊢ pullback (Z := pullback i (𝟙 S)) (f ≫ inv (fst i (𝟙 S))) (g ≫ inv (fst i (𝟙 S))) ≅ pullback f g
have refine_2 : CategoryStruct.comp (Y := pullback i (𝟙 S)) (f ≫ inv (fst i (𝟙 S))) (fst i (𝟙 S)) = 𝟙 X ≫ f
Tactic: refine @asIso _ _ _ _ (pullback.map _ _ _ _ (𝟙 _) (𝟙 _) (pullback.fst _ _) ?_ ?_) ?_
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Diagonal (goal)
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
⊢ pullback (Z := pullback i (𝟙 S)) (f ≫ inv (fst i (𝟙 S))) (g ≫ inv (fst i (𝟙 S))) ≅ pullback f g
have refine_2₁ : CategoryStruct.comp (Y := pullback i (𝟙 S)) (g ≫ inv (fst i (𝟙 S))) (fst i (𝟙 S)) = 𝟙 Y ≫ g
Tactic: refine @asIso _ _ _ _ (pullback.map _ _ _ _ (𝟙 _) (𝟙 _) (pullback.fst _ _) ?_ ?_) ?_
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Diagonal (goal)
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
⊢ pullback (Z := pullback i (𝟙 S)) (f ≫ inv (fst i (𝟙 S))) (g ≫ inv (fst i (𝟙 S))) ≅ pullback f g
have 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)) sorry sorry)
Tactic: refine @asIso _ _ _ _ (pullback.map _ _ _ _ (𝟙 _) (𝟙 _) (pullback.fst _ _) ?_ ?_) ?_
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Diagonal (goal)
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) ⋯ ⋯)
⊢ CategoryStruct.comp (Y := pullback i (𝟙 S)) (f ≫ inv (fst i (𝟙 S))) (fst i (𝟙 S)) = 𝟙 X ≫ f
have refine_2 : f ≫ CategoryStruct.comp (Y := pullback i (𝟙 S)) (inv (fst i (𝟙 S))) (fst i (𝟙 S)) = 𝟙 X ≫ f
Tactic: rw [Category.assoc, IsIso.inv_hom_id, Category.comp_id, Category.id_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Diagonal (goal)
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
⊢ CategoryStruct.comp (Y := pullback i (𝟙 S)) (f ≫ inv (fst i (𝟙 S))) (fst i (𝟙 S)) = 𝟙 X ≫ f
have refine_2₁ : f ≫ 𝟙 T = 𝟙 X ≫ f
Tactic: rw [Category.assoc, IsIso.inv_hom_id, Category.comp_id, Category.id_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Diagonal (goal)
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
⊢ CategoryStruct.comp (Y := pullback i (𝟙 S)) (f ≫ inv (fst i (𝟙 S))) (fst i (𝟙 S)) = 𝟙 X ≫ f
have refine_2₂ : f = 𝟙 X ≫ f
Tactic: rw [Category.assoc, IsIso.inv_hom_id, Category.comp_id, Category.id_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Diagonal (goal)
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
⊢ CategoryStruct.comp (Y := pullback i (𝟙 S)) (f ≫ inv (fst i (𝟙 S))) (fst i (𝟙 S)) = 𝟙 X ≫ f
have refine_2₃ : f = f
Tactic: rw [Category.assoc, IsIso.inv_hom_id, Category.comp_id, Category.id_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Diagonal (goal)
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) ⋯ ⋯)
⊢ CategoryStruct.comp (Y := pullback i (𝟙 S)) (g ≫ inv (fst i (𝟙 S))) (fst i (𝟙 S)) = 𝟙 Y ≫ g
have refine_2 : g ≫ CategoryStruct.comp (Y := pullback i (𝟙 S)) (inv (fst i (𝟙 S))) (fst i (𝟙 S)) = 𝟙 Y ≫ g
Tactic: rw [Category.assoc, IsIso.inv_hom_id, Category.comp_id, Category.id_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Diagonal (goal)
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
⊢ CategoryStruct.comp (Y := pullback i (𝟙 S)) (g ≫ inv (fst i (𝟙 S))) (fst i (𝟙 S)) = 𝟙 Y ≫ g
have refine_2₁ : g ≫ 𝟙 T = 𝟙 Y ≫ g
Tactic: rw [Category.assoc, IsIso.inv_hom_id, Category.comp_id, Category.id_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Diagonal (goal)
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
⊢ CategoryStruct.comp (Y := pullback i (𝟙 S)) (g ≫ inv (fst i (𝟙 S))) (fst i (𝟙 S)) = 𝟙 Y ≫ g
have refine_2₂ : g = 𝟙 Y ≫ g
Tactic: rw [Category.assoc, IsIso.inv_hom_id, Category.comp_id, Category.id_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Diagonal (goal)
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
⊢ CategoryStruct.comp (Y := pullback i (𝟙 S)) (g ≫ inv (fst i (𝟙 S))) (fst i (𝟙 S)) = 𝟙 Y ≫ g
have refine_2₃ : g = g
Tactic: rw [Category.assoc, IsIso.inv_hom_id, Category.comp_id, Category.id_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Diagonal (goal)
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.inv (pullbackDiagonalMapIdIso f g i)) (fst (diagonal i) (map (f ≫ i) (g ≫ i) i i f g (𝟙 S) ⋯ ⋯)))
    (fst f g ≫ f)
have rw : Eq (α :=
  pullback (Y := pullback (f ≫ i) (g ≫ i)) (Z := diagonalObj i) (diagonal i) (map (f ≫ i) (g ≫ i) i i f g (𝟙 S) sorry sorry) ⟶
    T)
  (snd (diagonal i) (map (f ≫ i) (g ≫ i) i i f g (𝟙 S) sorry sorry) ≫
    CategoryStruct.comp (Y := diagonalObj i) (map (f ≫ i) (g ≫ i) i i f g (𝟙 S) sorry sorry) (fst i i))
  (CategoryStruct.comp (Y := pullback f g) (Iso.hom (pullbackDiagonalMapIdIso f g i)) (fst f g ≫ f))
Tactic: rw [Iso.inv_comp_eq, ← Category.comp_id (pullback.fst _ _), ← diagonal_fst i,
    pullback.condition_assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Diagonal (goal)
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 (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)
have rw : Eq (α :=
  pullback (Y := pullback (f ≫ i) (g ≫ i)) (Z := diagonalObj i) (diagonal i) (map (f ≫ i) (g ≫ i) i i f g (𝟙 S) sorry sorry) ⟶
    X)
  (snd (diagonal i) (map (f ≫ i) (g ≫ i) i i f g (𝟙 S) sorry sorry) ≫ fst (f ≫ i) (g ≫ i))
  (CategoryStruct.comp (Y := pullback f g) (Iso.hom (pullbackDiagonalMapIdIso f g i)) (fst f g))
Tactic: rw [Iso.inv_comp_eq]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Diagonal (goal)
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 (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)
have rw : Eq (α :=
  pullback (Y := pullback (f ≫ i) (g ≫ i)) (Z := diagonalObj i) (diagonal i) (map (f ≫ i) (g ≫ i) i i f g (𝟙 S) sorry sorry) ⟶
    Y)
  (snd (diagonal i) (map (f ≫ i) (g ≫ i) i i f g (𝟙 S) sorry sorry) ≫ snd (f ≫ i) (g ≫ i))
  (CategoryStruct.comp (Y := pullback f g) (Iso.hom (pullbackDiagonalMapIdIso f g i)) (snd f g))
Tactic: rw [Iso.inv_comp_eq]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Diagonal (goal)
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
⊢ 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) ⋯ ⋯))))
have 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) sorry sorry))
        (Iso.inv (pullbackDiagonalMapIdIso f f g)) (snd (diagonal g) (map (f ≫ g) (f ≫ g) g g f f (𝟙 Z) sorry sorry))))
    (fst (f ≫ g) (f ≫ g))
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Diagonal (goal)
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))
⊢ 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) ⋯ ⋯))))
have 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) sorry sorry))
        (Iso.inv (pullbackDiagonalMapIdIso f f g)) (snd (diagonal g) (map (f ≫ g) (f ≫ g) g g f f (𝟙 Z) sorry sorry))))
    (snd (f ≫ g) (f ≫ g))
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Diagonal (goal)
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
⊢ 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) ⋯ ⋯))
have 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) sorry sorry))
    (fst g g)
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Diagonal (goal)
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)
⊢ 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) ⋯ ⋯))
have 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) sorry sorry))
    (snd g g)
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Diagonal (goal)
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) ⋯ ⋯)
⊢ 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) ⋯ ⋯)
have 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) sorry sorry))
    (Iso.hom (Iso.symm (pullbackDiagonalMapIdIso f g i))) (fst (diagonal i) (map (f ≫ i) (g ≫ i) i i f g (𝟙 S) sorry sorry)))
  (fst f g ≫ f)
Tactic: apply IsPullback.of_iso_pullback _ (pullbackDiagonalMapIdIso f g i).symm
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Diagonal (goal)
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)
⊢ 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) ⋯ ⋯)
have 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) sorry sorry))
    (Iso.hom (Iso.symm (pullbackDiagonalMapIdIso f g i))) (snd (diagonal i) (map (f ≫ i) (g ≫ i) i i f g (𝟙 S) sorry sorry)))
  (map f g (f ≫ i) (g ≫ i) (𝟙 X) (𝟙 Y) i sorry sorry)
Tactic: apply IsPullback.of_iso_pullback _ (pullbackDiagonalMapIdIso f g i).symm
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Diagonal (goal)
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 ⋯ ⋯)
⊢ 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) ⋯ ⋯)
have 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 sorry sorry) (diagonal i) (map (f ≫ i) (g ≫ i) i i f g (𝟙 S) sorry sorry)
Tactic: apply IsPullback.of_iso_pullback _ (pullbackDiagonalMapIdIso f g i).symm
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Diagonal (goal)
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 ⟶ 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 ⋯ ⋯)
have 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) sorry sorry))
      (Iso.hom (Iso.symm (pullbackDiagonalMapIdIso f g i))) (snd (diagonal i) (map (f ≫ i) (g ≫ i) i i f g (𝟙 S) sorry sorry)))
    (fst (f ≫ i) (g ≫ i)))
  (CategoryStruct.comp (Y := pullback (f ≫ i) (g ≫ i)) (map f g (f ≫ i) (g ≫ i) (𝟙 X) (𝟙 Y) i sorry sorry)
    (fst (f ≫ i) (g ≫ i)))
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Diagonal (goal)
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)))
⊢ 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 ⋯ ⋯)
have 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) sorry sorry))
      (Iso.hom (Iso.symm (pullbackDiagonalMapIdIso f g i))) (snd (diagonal i) (map (f ≫ i) (g ≫ i) i i f g (𝟙 S) sorry sorry)))
    (snd (f ≫ i) (g ≫ i)))
  (CategoryStruct.comp (Y := pullback (f ≫ i) (g ≫ i)) (map f g (f ≫ i) (g ≫ i) (𝟙 X) (𝟙 Y) i sorry sorry)
    (snd (f ≫ i) (g ≫ i)))
Tactic: ext