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 : 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))
⊢ 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 ⋯ ⋯))
have 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) sorry sorry)
      (map (i₁ ≫ snd f i) (i₂ ≫ snd f i) f f (i₁ ≫ fst f i) (i₂ ≫ fst f i) i sorry sorry))
    (snd f f))
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
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 (Y := pullback (f ≫ i) (g ≫ i)) (Z := diagonalObj i) (diagonal i) (map (f ≫ i) (g ≫ i) i i f g (𝟙 S) ⋯ ⋯) ≅
    pullback f g
have refine_1 : pullback (Y := pullback (f ≫ i) (g ≫ i)) (Z := diagonalObj i) (diagonal i) (map (f ≫ i) (g ≫ i) i i f g (𝟙 S) sorry sorry) ≅
  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) sorry sorry)
Tactic: refine ?_ ≪≫
    pullbackDiagonalMapIso i (𝟙 _) (f ≫ inv (pullback.fst _ _)) (g ≫ inv (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_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) ⋯ ⋯)
⊢ 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
have refine_2 : pullback (Z := pullback i (𝟙 S)) (f ≫ inv (fst i (𝟙 S))) (g ≫ inv (fst i (𝟙 S))) ≅ pullback f g
Tactic: refine ?_ ≪≫
    pullbackDiagonalMapIso i (𝟙 _) (f ≫ inv (pullback.fst _ _)) (g ≫ inv (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) ⋯ ⋯)
⊢ 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) ⋯ ⋯)
have refine_1 : f ≫ i = CategoryStruct.comp (Y := pullback i (𝟙 S)) (f ≫ inv (fst i (𝟙 S))) (snd i (𝟙 S))
Tactic: refine @asIso _ _ _ _ (pullback.map _ _ _ _ (𝟙 T) ((pullback.congrHom ?_ ?_).hom) (𝟙 _) ?_ ?_)
      ?_
-- 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_1 : f ≫ i = CategoryStruct.comp (Y := pullback i (𝟙 S)) (f ≫ inv (fst i (𝟙 S))) (snd i (𝟙 S))
⊢ 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) ⋯ ⋯)
have refine_1₁ : g ≫ i = CategoryStruct.comp (Y := pullback i (𝟙 S)) (g ≫ inv (fst i (𝟙 S))) (snd i (𝟙 S))
Tactic: refine @asIso _ _ _ _ (pullback.map _ _ _ _ (𝟙 T) ((pullback.congrHom ?_ ?_).hom) (𝟙 _) ?_ ?_)
      ?_
-- 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_1 : f ≫ i = CategoryStruct.comp (Y := pullback i (𝟙 S)) (f ≫ inv (fst i (𝟙 S))) (snd i (𝟙 S))
refine_1₁ : g ≫ i = CategoryStruct.comp (Y := pullback i (𝟙 S)) (g ≫ inv (fst i (𝟙 S))) (snd i (𝟙 S))
⊢ 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) ⋯ ⋯)
have refine_1₂ : diagonal i ≫ 𝟙 (diagonalObj i) = 𝟙 T ≫ diagonal i
Tactic: refine @asIso _ _ _ _ (pullback.map _ _ _ _ (𝟙 T) ((pullback.congrHom ?_ ?_).hom) (𝟙 _) ?_ ?_)
      ?_
-- 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_1 : f ≫ i = CategoryStruct.comp (Y := pullback i (𝟙 S)) (f ≫ inv (fst i (𝟙 S))) (snd i (𝟙 S))
refine_1₁ : g ≫ i = CategoryStruct.comp (Y := pullback i (𝟙 S)) (g ≫ inv (fst i (𝟙 S))) (snd i (𝟙 S))
refine_1₂ : diagonal i ≫ 𝟙 (diagonalObj i) = 𝟙 T ≫ diagonal i
⊢ 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) ⋯ ⋯)
have refine_1₃ : Eq (α := pullback (f ≫ i) (g ≫ i) ⟶ diagonalObj i) (map (f ≫ i) (g ≫ i) i i f g (𝟙 S) sorry sorry ≫ 𝟙 (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 sorry sorry))
    (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) sorry sorry))
Tactic: refine @asIso _ _ _ _ (pullback.map _ _ _ _ (𝟙 T) ((pullback.congrHom ?_ ?_).hom) (𝟙 _) ?_ ?_)
      ?_
-- 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) ⋯ ⋯)
⊢ f ≫ i = CategoryStruct.comp (Y := pullback i (𝟙 S)) (f ≫ inv (fst i (𝟙 S))) (snd i (𝟙 S))
have refine_1 : f ≫ i = CategoryStruct.comp (Y := pullback i (𝟙 S)) (f ≫ inv (fst i (𝟙 S))) (snd i (𝟙 S) ≫ 𝟙 S)
Tactic: rw [← Category.comp_id (pullback.snd ..), ← condition, Category.assoc, IsIso.inv_hom_id_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 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)
⊢ f ≫ i = CategoryStruct.comp (Y := pullback i (𝟙 S)) (f ≫ inv (fst i (𝟙 S))) (snd i (𝟙 S))
have refine_1₁ : f ≫ i = CategoryStruct.comp (Y := pullback i (𝟙 S)) (f ≫ inv (fst i (𝟙 S))) (fst i (𝟙 S) ≫ i)
Tactic: rw [← Category.comp_id (pullback.snd ..), ← condition, Category.assoc, IsIso.inv_hom_id_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 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)
⊢ f ≫ i = CategoryStruct.comp (Y := pullback i (𝟙 S)) (f ≫ inv (fst i (𝟙 S))) (snd i (𝟙 S))
have refine_1₂ : f ≫ i = f ≫ CategoryStruct.comp (Y := pullback i (𝟙 S)) (inv (fst i (𝟙 S))) (fst i (𝟙 S) ≫ i)
Tactic: rw [← Category.comp_id (pullback.snd ..), ← condition, Category.assoc, IsIso.inv_hom_id_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 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)
⊢ f ≫ i = CategoryStruct.comp (Y := pullback i (𝟙 S)) (f ≫ inv (fst i (𝟙 S))) (snd i (𝟙 S))
have refine_1₃ : f ≫ i = f ≫ i
Tactic: rw [← Category.comp_id (pullback.snd ..), ← condition, Category.assoc, IsIso.inv_hom_id_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 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) ⋯ ⋯)
⊢ g ≫ i = CategoryStruct.comp (Y := pullback i (𝟙 S)) (g ≫ inv (fst i (𝟙 S))) (snd i (𝟙 S))
have refine_1 : g ≫ i = CategoryStruct.comp (Y := pullback i (𝟙 S)) (g ≫ inv (fst i (𝟙 S))) (snd i (𝟙 S) ≫ 𝟙 S)
Tactic: rw [← Category.comp_id (pullback.snd ..), ← condition, Category.assoc, IsIso.inv_hom_id_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 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)
⊢ g ≫ i = CategoryStruct.comp (Y := pullback i (𝟙 S)) (g ≫ inv (fst i (𝟙 S))) (snd i (𝟙 S))
have refine_1₁ : g ≫ i = CategoryStruct.comp (Y := pullback i (𝟙 S)) (g ≫ inv (fst i (𝟙 S))) (fst i (𝟙 S) ≫ i)
Tactic: rw [← Category.comp_id (pullback.snd ..), ← condition, Category.assoc, IsIso.inv_hom_id_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 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)
⊢ g ≫ i = CategoryStruct.comp (Y := pullback i (𝟙 S)) (g ≫ inv (fst i (𝟙 S))) (snd i (𝟙 S))
have refine_1₂ : g ≫ i = g ≫ CategoryStruct.comp (Y := pullback i (𝟙 S)) (inv (fst i (𝟙 S))) (fst i (𝟙 S) ≫ i)
Tactic: rw [← Category.comp_id (pullback.snd ..), ← condition, Category.assoc, IsIso.inv_hom_id_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 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)
⊢ g ≫ i = CategoryStruct.comp (Y := pullback i (𝟙 S)) (g ≫ inv (fst i (𝟙 S))) (snd i (𝟙 S))
have refine_1₃ : g ≫ i = g ≫ i
Tactic: rw [← Category.comp_id (pullback.snd ..), ← condition, Category.assoc, IsIso.inv_hom_id_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 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) ⋯ ⋯)
⊢ diagonal i ≫ 𝟙 (diagonalObj i) = 𝟙 T ≫ diagonal i
have refine_1 : Eq (α := T ⟶ diagonalObj i) (diagonal i) (𝟙 T ≫ diagonal i)
Tactic: rw [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_1 : Eq (α := T ⟶ diagonalObj i) (diagonal i) (𝟙 T ≫ diagonal i)
⊢ diagonal i ≫ 𝟙 (diagonalObj i) = 𝟙 T ≫ diagonal i
have refine_1₁ : Eq (α := T ⟶ diagonalObj i) (diagonal i) (diagonal i)
Tactic: rw [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) ⋯ ⋯)
⊢ 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) ⋯ ⋯))
have refine_1 : Eq (α := pullback (f ≫ i) (g ≫ i) ⟶ T) ((map (f ≫ i) (g ≫ i) i i f g (𝟙 S) sorry sorry ≫ 𝟙 (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 sorry sorry))
      (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) sorry sorry))
    (fst i 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 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))
⊢ 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) ⋯ ⋯))
have refine_1₁ : Eq (α := pullback (f ≫ i) (g ≫ i) ⟶ T) ((map (f ≫ i) (g ≫ i) i i f g (𝟙 S) sorry sorry ≫ 𝟙 (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 sorry sorry))
      (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) sorry sorry))
    (snd i i))
Tactic: ext