awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.HasPullback (goal)
Goal:
C : Type u
inst : Category.{v, u} C
W_1 X_1 Y_1 Z_1 W X Y Z S T : C
f₁ : S ⟶ W
f₂ : S ⟶ X
inst_1 : HasPushout f₁ f₂
g₁ : T ⟶ Y
g₂ : T ⟶ Z
inst_2 : HasPushout g₁ g₂
i₁ : W ⟶ Y
i₂ : X ⟶ Z
i₃ : S ⟶ T
eq₁ : f₁ ≫ i₁ = i₃ ≫ g₁
eq₂ : f₂ ≫ i₂ = i₃ ≫ g₂
inst_3 : IsIso i₁
inst_4 : IsIso i₂
inst_5 : IsIso i₃
⊢ g₂ ≫ inv i₂ = inv i₃ ≫ f₂
have refine_2 : g₂ = (inv i₃ ≫ f₂) ≫ i₂
Tactic: rw [IsIso.comp_inv_eq, Category.assoc, eq₂, IsIso.inv_hom_id_assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.HasPullback (goal)
Goal:
C : Type u
inst : Category.{v, u} C
W_1 X_1 Y_1 Z_1 W X Y Z S T : C
f₁ : S ⟶ W
f₂ : S ⟶ X
inst_1 : HasPushout f₁ f₂
g₁ : T ⟶ Y
g₂ : T ⟶ Z
inst_2 : HasPushout g₁ g₂
i₁ : W ⟶ Y
i₂ : X ⟶ Z
i₃ : S ⟶ T
eq₁ : f₁ ≫ i₁ = i₃ ≫ g₁
eq₂ : f₂ ≫ i₂ = i₃ ≫ g₂
inst_3 : IsIso i₁
inst_4 : IsIso i₂
inst_5 : IsIso i₃
refine_2 : g₂ = (inv i₃ ≫ f₂) ≫ i₂
⊢ g₂ ≫ inv i₂ = inv i₃ ≫ f₂
have refine_2₁ : g₂ = inv i₃ ≫ f₂ ≫ i₂
Tactic: rw [IsIso.comp_inv_eq, Category.assoc, eq₂, IsIso.inv_hom_id_assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.HasPullback (goal)
Goal:
C : Type u
inst : Category.{v, u} C
W_1 X_1 Y_1 Z_1 W X Y Z S T : C
f₁ : S ⟶ W
f₂ : S ⟶ X
inst_1 : HasPushout f₁ f₂
g₁ : T ⟶ Y
g₂ : T ⟶ Z
inst_2 : HasPushout g₁ g₂
i₁ : W ⟶ Y
i₂ : X ⟶ Z
i₃ : S ⟶ T
eq₁ : f₁ ≫ i₁ = i₃ ≫ g₁
eq₂ : f₂ ≫ i₂ = i₃ ≫ g₂
inst_3 : IsIso i₁
inst_4 : IsIso i₂
inst_5 : IsIso i₃
refine_2 : g₂ = (inv i₃ ≫ f₂) ≫ i₂
refine_2₁ : g₂ = inv i₃ ≫ f₂ ≫ i₂
⊢ g₂ ≫ inv i₂ = inv i₃ ≫ f₂
have refine_2₂ : g₂ = inv i₃ ≫ i₃ ≫ g₂
Tactic: rw [IsIso.comp_inv_eq, Category.assoc, eq₂, IsIso.inv_hom_id_assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.HasPullback (goal)
Goal:
C : Type u
inst : Category.{v, u} C
W_1 X_1 Y_1 Z_1 W X Y Z S T : C
f₁ : S ⟶ W
f₂ : S ⟶ X
inst_1 : HasPushout f₁ f₂
g₁ : T ⟶ Y
g₂ : T ⟶ Z
inst_2 : HasPushout g₁ g₂
i₁ : W ⟶ Y
i₂ : X ⟶ Z
i₃ : S ⟶ T
eq₁ : f₁ ≫ i₁ = i₃ ≫ g₁
eq₂ : f₂ ≫ i₂ = i₃ ≫ g₂
inst_3 : IsIso i₁
inst_4 : IsIso i₂
inst_5 : IsIso i₃
refine_2 : g₂ = (inv i₃ ≫ f₂) ≫ i₂
refine_2₁ : g₂ = inv i₃ ≫ f₂ ≫ i₂
refine_2₂ : g₂ = inv i₃ ≫ i₃ ≫ g₂
⊢ g₂ ≫ inv i₂ = inv i₃ ≫ f₂
have refine_2₃ : g₂ = g₂
Tactic: rw [IsIso.comp_inv_eq, Category.assoc, eq₂, IsIso.inv_hom_id_assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.HasPullback (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z : C
f₁ f₂ : X ⟶ Y
g₁ g₂ : X ⟶ Z
h₁ : f₁ = f₂
h₂ : g₁ = g₂
inst_1 : HasPushout f₁ g₁
inst_2 : HasPushout f₂ g₂
⊢ Eq (α := pushout f₂ g₂ ⟶ pushout f₁ g₁) (Iso.inv (congrHom h₁ h₂)) (map f₂ g₂ f₁ g₁ (𝟙 Y) (𝟙 Z) (𝟙 X) ⋯ ⋯)
have h₀ : Eq (α := Y ⟶ pushout f₁ g₁) (CategoryStruct.comp (Y := pushout f₂ g₂) (inl f₂ g₂) (Iso.inv (congrHom h₁ h₂)))
  (CategoryStruct.comp (Y := pushout f₂ g₂) (inl f₂ g₂) (map f₂ g₂ f₁ g₁ (𝟙 Y) (𝟙 Z) (𝟙 X) sorry sorry))
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.HasPullback (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z : C
f₁ f₂ : X ⟶ Y
g₁ g₂ : X ⟶ Z
h₁ : f₁ = f₂
h₂ : g₁ = g₂
inst_1 : HasPushout f₁ g₁
inst_2 : HasPushout f₂ g₂
h₀ :
  Eq (α := Y ⟶ pushout f₁ g₁) (CategoryStruct.comp (Y := pushout f₂ g₂) (inl f₂ g₂) (Iso.inv (congrHom h₁ h₂)))
    (CategoryStruct.comp (Y := pushout f₂ g₂) (inl f₂ g₂) (map f₂ g₂ f₁ g₁ (𝟙 Y) (𝟙 Z) (𝟙 X) ⋯ ⋯))
⊢ Eq (α := pushout f₂ g₂ ⟶ pushout f₁ g₁) (Iso.inv (congrHom h₁ h₂)) (map f₂ g₂ f₁ g₁ (𝟙 Y) (𝟙 Z) (𝟙 X) ⋯ ⋯)
have h₃ : Eq (α := Z ⟶ pushout f₁ g₁) (CategoryStruct.comp (Y := pushout f₂ g₂) (inr f₂ g₂) (Iso.inv (congrHom h₁ h₂)))
  (CategoryStruct.comp (Y := pushout f₂ g₂) (inr f₂ g₂) (map f₂ g₂ f₁ g₁ (𝟙 Y) (𝟙 Z) (𝟙 X) sorry sorry))
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.HasPullback (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z : C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
G : Functor.{v, v₂, u, u₂} C D
f : X ⟶ Z
g : Y ⟶ Z
inst_2 : HasPullback f g
inst_3 : HasPullback (G.map f) (G.map g)
W : C
h : W ⟶ X
k : W ⟶ Y
w : h ≫ f = k ≫ g
⊢ Eq (α := G.obj W ⟶ pullback (G.map f) (G.map g))
    (CategoryStruct.comp (Y := G.obj (pullback f g)) (G.map (pullback.lift h k w)) (pullbackComparison G f g))
    (pullback.lift (G.map h) (G.map k) ⋯)
have h₀ : CategoryStruct.comp (Y := pullback (G.map f) (G.map g))
    (CategoryStruct.comp (Y := G.obj (pullback f g)) (G.map (pullback.lift h k w)) (pullbackComparison G f g))
    (pullback.fst (G.map f) (G.map g)) =
  CategoryStruct.comp (Y := pullback (G.map f) (G.map g)) (pullback.lift (G.map h) (G.map k) sorry)
    (pullback.fst (G.map f) (G.map g))
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.HasPullback (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z : C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
G : Functor.{v, v₂, u, u₂} C D
f : X ⟶ Z
g : Y ⟶ Z
inst_2 : HasPullback f g
inst_3 : HasPullback (G.map f) (G.map g)
W : C
h : W ⟶ X
k : W ⟶ Y
w : h ≫ f = k ≫ g
h₀ :
  CategoryStruct.comp (Y := pullback (G.map f) (G.map g))
      (CategoryStruct.comp (Y := G.obj (pullback f g)) (G.map (pullback.lift h k w)) (pullbackComparison G f g))
      (pullback.fst (G.map f) (G.map g)) =
    CategoryStruct.comp (Y := pullback (G.map f) (G.map g)) (pullback.lift (G.map h) (G.map k) ⋯)
      (pullback.fst (G.map f) (G.map g))
⊢ Eq (α := G.obj W ⟶ pullback (G.map f) (G.map g))
    (CategoryStruct.comp (Y := G.obj (pullback f g)) (G.map (pullback.lift h k w)) (pullbackComparison G f g))
    (pullback.lift (G.map h) (G.map k) ⋯)
have h₁ : CategoryStruct.comp (Y := pullback (G.map f) (G.map g))
    (CategoryStruct.comp (Y := G.obj (pullback f g)) (G.map (pullback.lift h k w)) (pullbackComparison G f g))
    (pullback.snd (G.map f) (G.map g)) =
  CategoryStruct.comp (Y := pullback (G.map f) (G.map g)) (pullback.lift (G.map h) (G.map k) sorry)
    (pullback.snd (G.map f) (G.map g))
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.HasPullback (goal)
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
E : Type u_1
inst_2 : Category.{v_1, u_1} E
F : Functor.{v, v₂, u, u₂} C D
G : Functor.{v₂, v_1, u₂, u_1} D E
X Y S : C
f : X ⟶ S
g : Y ⟶ S
inst_3 : HasPullback f g
inst_4 : HasPullback (F.map f) (F.map g)
inst_5 : HasPullback (G.map (F.map f)) (G.map (F.map g))
inst_6 : HasPullback ((F ⋙ G).map f) ((F ⋙ G).map g)
⊢ Eq (α := (F ⋙ G).obj (pullback f g) ⟶ pullback ((F ⋙ G).map f) ((F ⋙ G).map g)) (pullbackComparison (F ⋙ G) f g)
    (CategoryStruct.comp (Y := G.obj (pullback (F.map f) (F.map g))) (G.map (pullbackComparison F f g))
      (pullbackComparison G (F.map f) (F.map g)))
have h₀ : Eq (α := (F ⋙ G).obj (pullback f g) ⟶ (F ⋙ G).obj X)
  (CategoryStruct.comp (Y := pullback ((F ⋙ G).map f) ((F ⋙ G).map g)) (pullbackComparison (F ⋙ G) f g)
    (pullback.fst ((F ⋙ G).map f) ((F ⋙ G).map g)))
  (CategoryStruct.comp (Y := pullback ((F ⋙ G).map f) ((F ⋙ G).map g))
    (CategoryStruct.comp (Y := G.obj (pullback (F.map f) (F.map g))) (G.map (pullbackComparison F f g))
      (pullbackComparison G (F.map f) (F.map g)))
    (pullback.fst ((F ⋙ G).map f) ((F ⋙ G).map g)))
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.HasPullback (goal)
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
E : Type u_1
inst_2 : Category.{v_1, u_1} E
F : Functor.{v, v₂, u, u₂} C D
G : Functor.{v₂, v_1, u₂, u_1} D E
X Y S : C
f : X ⟶ S
g : Y ⟶ S
inst_3 : HasPullback f g
inst_4 : HasPullback (F.map f) (F.map g)
inst_5 : HasPullback (G.map (F.map f)) (G.map (F.map g))
inst_6 : HasPullback ((F ⋙ G).map f) ((F ⋙ G).map g)
h₀ :
  Eq (α := (F ⋙ G).obj (pullback f g) ⟶ (F ⋙ G).obj X)
    (CategoryStruct.comp (Y := pullback ((F ⋙ G).map f) ((F ⋙ G).map g)) (pullbackComparison (F ⋙ G) f g)
      (pullback.fst ((F ⋙ G).map f) ((F ⋙ G).map g)))
    (CategoryStruct.comp (Y := pullback ((F ⋙ G).map f) ((F ⋙ G).map g))
      (CategoryStruct.comp (Y := G.obj (pullback (F.map f) (F.map g))) (G.map (pullbackComparison F f g))
        (pullbackComparison G (F.map f) (F.map g)))
      (pullback.fst ((F ⋙ G).map f) ((F ⋙ G).map g)))
⊢ Eq (α := (F ⋙ G).obj (pullback f g) ⟶ pullback ((F ⋙ G).map f) ((F ⋙ G).map g)) (pullbackComparison (F ⋙ G) f g)
    (CategoryStruct.comp (Y := G.obj (pullback (F.map f) (F.map g))) (G.map (pullbackComparison F f g))
      (pullbackComparison G (F.map f) (F.map g)))
have h₁ : Eq (α := (F ⋙ G).obj (pullback f g) ⟶ (F ⋙ G).obj Y)
  (CategoryStruct.comp (Y := pullback ((F ⋙ G).map f) ((F ⋙ G).map g)) (pullbackComparison (F ⋙ G) f g)
    (pullback.snd ((F ⋙ G).map f) ((F ⋙ G).map g)))
  (CategoryStruct.comp (Y := pullback ((F ⋙ G).map f) ((F ⋙ G).map g))
    (CategoryStruct.comp (Y := G.obj (pullback (F.map f) (F.map g))) (G.map (pullbackComparison F f g))
      (pullbackComparison G (F.map f) (F.map g)))
    (pullback.snd ((F ⋙ G).map f) ((F ⋙ G).map g)))
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.HasPullback (goal)
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
E : Type u_1
inst_2 : Category.{v_1, u_1} E
F : Functor.{v, v₂, u, u₂} C D
G : Functor.{v₂, v_1, u₂, u_1} D E
X Y S : C
f : X ⟶ S
g : Y ⟶ S
inst_3 : HasPullback f g
inst_4 : HasPullback (F.map f) (F.map g)
inst_5 : HasPullback (G.map (F.map f)) (G.map (F.map g))
inst_6 : HasPullback ((F ⋙ G).map f) ((F ⋙ G).map g)
⊢ Eq (α := (F ⋙ G).obj (pullback f g) ⟶ (F ⋙ G).obj X)
    (CategoryStruct.comp (Y := pullback ((F ⋙ G).map f) ((F ⋙ G).map g)) (pullbackComparison (F ⋙ G) f g)
      (pullback.fst ((F ⋙ G).map f) ((F ⋙ G).map g)))
    (CategoryStruct.comp (Y := pullback ((F ⋙ G).map f) ((F ⋙ G).map g))
      (CategoryStruct.comp (Y := G.obj (pullback (F.map f) (F.map g))) (G.map (pullbackComparison F f g))
        (pullbackComparison G (F.map f) (F.map g)))
      (pullback.fst ((F ⋙ G).map f) ((F ⋙ G).map g)))
have h₀ : Eq (α := (F ⋙ G).obj (pullback f g) ⟶ (F ⋙ G).obj X) ((F ⋙ G).map (pullback.fst f g))
  (CategoryStruct.comp (Y := pullback ((F ⋙ G).map f) ((F ⋙ G).map g))
    (CategoryStruct.comp (Y := G.obj (pullback (F.map f) (F.map g))) (G.map (pullbackComparison F f g))
      (pullbackComparison G (F.map f) (F.map g)))
    (pullback.fst ((F ⋙ G).map f) ((F ⋙ G).map g)))
Tactic: rw [pullbackComparison_comp_fst]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.HasPullback (goal)
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
E : Type u_1
inst_2 : Category.{v_1, u_1} E
F : Functor.{v, v₂, u, u₂} C D
G : Functor.{v₂, v_1, u₂, u_1} D E
X Y S : C
f : X ⟶ S
g : Y ⟶ S
inst_3 : HasPullback f g
inst_4 : HasPullback (F.map f) (F.map g)
inst_5 : HasPullback (G.map (F.map f)) (G.map (F.map g))
inst_6 : HasPullback ((F ⋙ G).map f) ((F ⋙ G).map g)
⊢ Eq (α := (F ⋙ G).obj (pullback f g) ⟶ (F ⋙ G).obj Y)
    (CategoryStruct.comp (Y := pullback ((F ⋙ G).map f) ((F ⋙ G).map g)) (pullbackComparison (F ⋙ G) f g)
      (pullback.snd ((F ⋙ G).map f) ((F ⋙ G).map g)))
    (CategoryStruct.comp (Y := pullback ((F ⋙ G).map f) ((F ⋙ G).map g))
      (CategoryStruct.comp (Y := G.obj (pullback (F.map f) (F.map g))) (G.map (pullbackComparison F f g))
        (pullbackComparison G (F.map f) (F.map g)))
      (pullback.snd ((F ⋙ G).map f) ((F ⋙ G).map g)))
have h₁ : Eq (α := (F ⋙ G).obj (pullback f g) ⟶ (F ⋙ G).obj Y) ((F ⋙ G).map (pullback.snd f g))
  (CategoryStruct.comp (Y := pullback ((F ⋙ G).map f) ((F ⋙ G).map g))
    (CategoryStruct.comp (Y := G.obj (pullback (F.map f) (F.map g))) (G.map (pullbackComparison F f g))
      (pullbackComparison G (F.map f) (F.map g)))
    (pullback.snd ((F ⋙ G).map f) ((F ⋙ G).map g)))
Tactic: rw [pullbackComparison_comp_snd]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.HasPullback (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z : C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
G : Functor.{v, v₂, u, u₂} C D
f : X ⟶ Y
g : X ⟶ Z
inst_2 : HasPushout f g
inst_3 : HasPushout (G.map f) (G.map g)
W : C
h : Y ⟶ W
k : Z ⟶ W
w : f ≫ h = g ≫ k
⊢ Eq (α := pushout (G.map f) (G.map g) ⟶ G.obj W)
    (CategoryStruct.comp (Y := G.obj (pushout f g)) (pushoutComparison G f g) (G.map (pushout.desc h k w)))
    (pushout.desc (G.map h) (G.map k) ⋯)
have h₀ : CategoryStruct.comp (Y := pushout (G.map f) (G.map g)) (pushout.inl (G.map f) (G.map g))
    (CategoryStruct.comp (Y := G.obj (pushout f g)) (pushoutComparison G f g) (G.map (pushout.desc h k w))) =
  CategoryStruct.comp (Y := pushout (G.map f) (G.map g)) (pushout.inl (G.map f) (G.map g))
    (pushout.desc (G.map h) (G.map k) sorry)
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.HasPullback (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X Y Z : C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
G : Functor.{v, v₂, u, u₂} C D
f : X ⟶ Y
g : X ⟶ Z
inst_2 : HasPushout f g
inst_3 : HasPushout (G.map f) (G.map g)
W : C
h : Y ⟶ W
k : Z ⟶ W
w : f ≫ h = g ≫ k
h₀ :
  CategoryStruct.comp (Y := pushout (G.map f) (G.map g)) (pushout.inl (G.map f) (G.map g))
      (CategoryStruct.comp (Y := G.obj (pushout f g)) (pushoutComparison G f g) (G.map (pushout.desc h k w))) =
    CategoryStruct.comp (Y := pushout (G.map f) (G.map g)) (pushout.inl (G.map f) (G.map g))
      (pushout.desc (G.map h) (G.map k) ⋯)
⊢ Eq (α := pushout (G.map f) (G.map g) ⟶ G.obj W)
    (CategoryStruct.comp (Y := G.obj (pushout f g)) (pushoutComparison G f g) (G.map (pushout.desc h k w)))
    (pushout.desc (G.map h) (G.map k) ⋯)
have h₁ : CategoryStruct.comp (Y := pushout (G.map f) (G.map g)) (pushout.inr (G.map f) (G.map g))
    (CategoryStruct.comp (Y := G.obj (pushout f g)) (pushoutComparison G f g) (G.map (pushout.desc h k w))) =
  CategoryStruct.comp (Y := pushout (G.map f) (G.map g)) (pushout.inr (G.map f) (G.map g))
    (pushout.desc (G.map h) (G.map k) sorry)
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.HasPullback (goal)
Goal:
C : Type u
inst : Category.{v, u} C
W X_1 Y_1 Z_1 X Y : C
f : X ⟶ Y
Z : C
inst_1 : HasBinaryProduct.{v, u} Y Z
inst_2 : HasBinaryProduct.{v, u} X Z
inst_3 : HasPullback (Y := prod.{v, u} Y Z) f prod.fst
⊢ CategoryStruct.comp (Y := prod.{v, u} X Z) (prod.lift (pullback.fst f prod.fst) (pullback.snd f prod.fst ≫ prod.snd))
      (pullback.lift prod.fst (prod.map f (𝟙 Z)) ⋯) =
    𝟙 (pullback (Y := prod.{v, u} Y Z) f prod.fst)
have h₀ : CategoryStruct.comp (Y := pullback (Y := prod.{v, u} Y Z) f prod.fst)
    (CategoryStruct.comp (Y := prod.{v, u} X Z)
      (prod.lift (pullback.fst f prod.fst) (pullback.snd f prod.fst ≫ prod.snd))
      (pullback.lift prod.fst (prod.map f (𝟙 Z)) sorry))
    (pullback.fst f prod.fst) =
  𝟙 (pullback (Y := prod.{v, u} Y Z) f prod.fst) ≫ pullback.fst f prod.fst
Tactic: apply pullback.hom_ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.HasPullback (goal)
Goal:
C : Type u
inst : Category.{v, u} C
W X_1 Y_1 Z_1 X Y : C
f : X ⟶ Y
Z : C
inst_1 : HasBinaryProduct.{v, u} Y Z
inst_2 : HasBinaryProduct.{v, u} X Z
inst_3 : HasPullback (Y := prod.{v, u} Y Z) f prod.fst
h₀ :
  CategoryStruct.comp (Y := pullback (Y := prod.{v, u} Y Z) f prod.fst)
      (CategoryStruct.comp (Y := prod.{v, u} X Z)
        (prod.lift (pullback.fst f prod.fst) (pullback.snd f prod.fst ≫ prod.snd))
        (pullback.lift prod.fst (prod.map f (𝟙 Z)) ⋯))
      (pullback.fst f prod.fst) =
    𝟙 (pullback (Y := prod.{v, u} Y Z) f prod.fst) ≫ pullback.fst f prod.fst
⊢ CategoryStruct.comp (Y := prod.{v, u} X Z) (prod.lift (pullback.fst f prod.fst) (pullback.snd f prod.fst ≫ prod.snd))
      (pullback.lift prod.fst (prod.map f (𝟙 Z)) ⋯) =
    𝟙 (pullback (Y := prod.{v, u} Y Z) f prod.fst)
have h₁ : CategoryStruct.comp (Y := pullback (Y := prod.{v, u} Y Z) f prod.fst)
    (CategoryStruct.comp (Y := prod.{v, u} X Z)
      (prod.lift (pullback.fst f prod.fst) (pullback.snd f prod.fst ≫ prod.snd))
      (pullback.lift prod.fst (prod.map f (𝟙 Z)) sorry))
    (pullback.snd f prod.fst) =
  𝟙 (pullback (Y := prod.{v, u} Y Z) f prod.fst) ≫ pullback.snd f prod.fst
Tactic: apply pullback.hom_ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.HasPullback (goal)
Goal:
C : Type u
inst : Category.{v, u} C
W X_1 Y_1 Z_1 X Y : C
f : X ⟶ Y
Z : C
inst_1 : HasBinaryProduct.{v, u} Y Z
inst_2 : HasBinaryProduct.{v, u} X Z
inst_3 : HasPullback (Y := prod.{v, u} Y Z) f prod.fst
⊢ CategoryStruct.comp (Y := pullback (Y := prod.{v, u} Y Z) f prod.fst)
      (CategoryStruct.comp (Y := prod.{v, u} X Z)
        (prod.lift (pullback.fst f prod.fst) (pullback.snd f prod.fst ≫ prod.snd))
        (pullback.lift prod.fst (prod.map f (𝟙 Z)) ⋯))
      (pullback.snd f prod.fst) =
    𝟙 (pullback (Y := prod.{v, u} Y Z) f prod.fst) ≫ pullback.snd f prod.fst
have h₁ : CategoryStruct.comp (Y := prod.{v, u} Y Z)
    (CategoryStruct.comp (Y := pullback (Y := prod.{v, u} Y Z) f prod.fst)
      (CategoryStruct.comp (Y := prod.{v, u} X Z)
        (prod.lift (pullback.fst f prod.fst) (pullback.snd f prod.fst ≫ prod.snd))
        (pullback.lift prod.fst (prod.map f (𝟙 Z)) sorry))
      (pullback.snd f prod.fst))
    prod.fst =
  (𝟙 (pullback (Y := prod.{v, u} Y Z) f prod.fst) ≫ pullback.snd f prod.fst) ≫ prod.fst
Tactic: apply prod.hom_ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.HasPullback (goal)
Goal:
C : Type u
inst : Category.{v, u} C
W X_1 Y_1 Z_1 X Y : C
f : X ⟶ Y
Z : C
inst_1 : HasBinaryProduct.{v, u} Y Z
inst_2 : HasBinaryProduct.{v, u} X Z
inst_3 : HasPullback (Y := prod.{v, u} Y Z) f prod.fst
h₁ :
  CategoryStruct.comp (Y := prod.{v, u} Y Z)
      (CategoryStruct.comp (Y := pullback (Y := prod.{v, u} Y Z) f prod.fst)
        (CategoryStruct.comp (Y := prod.{v, u} X Z)
          (prod.lift (pullback.fst f prod.fst) (pullback.snd f prod.fst ≫ prod.snd))
          (pullback.lift prod.fst (prod.map f (𝟙 Z)) ⋯))
        (pullback.snd f prod.fst))
      prod.fst =
    (𝟙 (pullback (Y := prod.{v, u} Y Z) f prod.fst) ≫ pullback.snd f prod.fst) ≫ prod.fst
⊢ CategoryStruct.comp (Y := pullback (Y := prod.{v, u} Y Z) f prod.fst)
      (CategoryStruct.comp (Y := prod.{v, u} X Z)
        (prod.lift (pullback.fst f prod.fst) (pullback.snd f prod.fst ≫ prod.snd))
        (pullback.lift prod.fst (prod.map f (𝟙 Z)) ⋯))
      (pullback.snd f prod.fst) =
    𝟙 (pullback (Y := prod.{v, u} Y Z) f prod.fst) ≫ pullback.snd f prod.fst
have h₂ : CategoryStruct.comp (Y := prod.{v, u} Y Z)
    (CategoryStruct.comp (Y := pullback (Y := prod.{v, u} Y Z) f prod.fst)
      (CategoryStruct.comp (Y := prod.{v, u} X Z)
        (prod.lift (pullback.fst f prod.fst) (pullback.snd f prod.fst ≫ prod.snd))
        (pullback.lift prod.fst (prod.map f (𝟙 Z)) sorry))
      (pullback.snd f prod.fst))
    prod.snd =
  (𝟙 (pullback (Y := prod.{v, u} Y Z) f prod.fst) ≫ pullback.snd f prod.fst) ≫ prod.snd
Tactic: apply prod.hom_ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.HasPullback (goal)
Goal:
C : Type u
inst : Category.{v, u} C
W X_1 Y_1 Z_1 X Y : C
f : X ⟶ Y
Z : C
inst_1 : HasBinaryProduct.{v, u} Z Y
inst_2 : HasBinaryProduct.{v, u} Z X
inst_3 : HasPullback (X := prod.{v, u} Z Y) prod.snd f
⊢ CategoryStruct.comp (Y := prod.{v, u} Z X) (prod.lift (pullback.fst prod.snd f ≫ prod.fst) (pullback.snd prod.snd f))
      (pullback.lift (prod.map (𝟙 Z) f) prod.snd ⋯) =
    𝟙 (pullback (X := prod.{v, u} Z Y) prod.snd f)
have h₀ : CategoryStruct.comp (Y := pullback (X := prod.{v, u} Z Y) prod.snd f)
    (CategoryStruct.comp (Y := prod.{v, u} Z X)
      (prod.lift (pullback.fst prod.snd f ≫ prod.fst) (pullback.snd prod.snd f))
      (pullback.lift (prod.map (𝟙 Z) f) prod.snd sorry))
    (pullback.fst prod.snd f) =
  𝟙 (pullback (X := prod.{v, u} Z Y) prod.snd f) ≫ pullback.fst prod.snd f
Tactic: apply pullback.hom_ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.HasPullback (goal)
Goal:
C : Type u
inst : Category.{v, u} C
W X_1 Y_1 Z_1 X Y : C
f : X ⟶ Y
Z : C
inst_1 : HasBinaryProduct.{v, u} Z Y
inst_2 : HasBinaryProduct.{v, u} Z X
inst_3 : HasPullback (X := prod.{v, u} Z Y) prod.snd f
h₀ :
  CategoryStruct.comp (Y := pullback (X := prod.{v, u} Z Y) prod.snd f)
      (CategoryStruct.comp (Y := prod.{v, u} Z X)
        (prod.lift (pullback.fst prod.snd f ≫ prod.fst) (pullback.snd prod.snd f))
        (pullback.lift (prod.map (𝟙 Z) f) prod.snd ⋯))
      (pullback.fst prod.snd f) =
    𝟙 (pullback (X := prod.{v, u} Z Y) prod.snd f) ≫ pullback.fst prod.snd f
⊢ CategoryStruct.comp (Y := prod.{v, u} Z X) (prod.lift (pullback.fst prod.snd f ≫ prod.fst) (pullback.snd prod.snd f))
      (pullback.lift (prod.map (𝟙 Z) f) prod.snd ⋯) =
    𝟙 (pullback (X := prod.{v, u} Z Y) prod.snd f)
have h₁ : CategoryStruct.comp (Y := pullback (X := prod.{v, u} Z Y) prod.snd f)
    (CategoryStruct.comp (Y := prod.{v, u} Z X)
      (prod.lift (pullback.fst prod.snd f ≫ prod.fst) (pullback.snd prod.snd f))
      (pullback.lift (prod.map (𝟙 Z) f) prod.snd sorry))
    (pullback.snd prod.snd f) =
  𝟙 (pullback (X := prod.{v, u} Z Y) prod.snd f) ≫ pullback.snd prod.snd f
Tactic: apply pullback.hom_ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.HasPullback (goal)
Goal:
C : Type u
inst : Category.{v, u} C
W X_1 Y_1 Z_1 X Y : C
f : X ⟶ Y
Z : C
inst_1 : HasBinaryProduct.{v, u} Z Y
inst_2 : HasBinaryProduct.{v, u} Z X
inst_3 : HasPullback (X := prod.{v, u} Z Y) prod.snd f
⊢ CategoryStruct.comp (Y := pullback (X := prod.{v, u} Z Y) prod.snd f)
      (CategoryStruct.comp (Y := prod.{v, u} Z X)
        (prod.lift (pullback.fst prod.snd f ≫ prod.fst) (pullback.snd prod.snd f))
        (pullback.lift (prod.map (𝟙 Z) f) prod.snd ⋯))
      (pullback.fst prod.snd f) =
    𝟙 (pullback (X := prod.{v, u} Z Y) prod.snd f) ≫ pullback.fst prod.snd f
have h₀ : CategoryStruct.comp (Y := prod.{v, u} Z Y)
    (CategoryStruct.comp (Y := pullback (X := prod.{v, u} Z Y) prod.snd f)
      (CategoryStruct.comp (Y := prod.{v, u} Z X)
        (prod.lift (pullback.fst prod.snd f ≫ prod.fst) (pullback.snd prod.snd f))
        (pullback.lift (prod.map (𝟙 Z) f) prod.snd sorry))
      (pullback.fst prod.snd f))
    prod.fst =
  (𝟙 (pullback (X := prod.{v, u} Z Y) prod.snd f) ≫ pullback.fst prod.snd f) ≫ prod.fst
Tactic: apply prod.hom_ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.HasPullback (goal)
Goal:
C : Type u
inst : Category.{v, u} C
W X_1 Y_1 Z_1 X Y : C
f : X ⟶ Y
Z : C
inst_1 : HasBinaryProduct.{v, u} Z Y
inst_2 : HasBinaryProduct.{v, u} Z X
inst_3 : HasPullback (X := prod.{v, u} Z Y) prod.snd f
h₀ :
  CategoryStruct.comp (Y := prod.{v, u} Z Y)
      (CategoryStruct.comp (Y := pullback (X := prod.{v, u} Z Y) prod.snd f)
        (CategoryStruct.comp (Y := prod.{v, u} Z X)
          (prod.lift (pullback.fst prod.snd f ≫ prod.fst) (pullback.snd prod.snd f))
          (pullback.lift (prod.map (𝟙 Z) f) prod.snd ⋯))
        (pullback.fst prod.snd f))
      prod.fst =
    (𝟙 (pullback (X := prod.{v, u} Z Y) prod.snd f) ≫ pullback.fst prod.snd f) ≫ prod.fst
⊢ CategoryStruct.comp (Y := pullback (X := prod.{v, u} Z Y) prod.snd f)
      (CategoryStruct.comp (Y := prod.{v, u} Z X)
        (prod.lift (pullback.fst prod.snd f ≫ prod.fst) (pullback.snd prod.snd f))
        (pullback.lift (prod.map (𝟙 Z) f) prod.snd ⋯))
      (pullback.fst prod.snd f) =
    𝟙 (pullback (X := prod.{v, u} Z Y) prod.snd f) ≫ pullback.fst prod.snd f
have h₁ : CategoryStruct.comp (Y := prod.{v, u} Z Y)
    (CategoryStruct.comp (Y := pullback (X := prod.{v, u} Z Y) prod.snd f)
      (CategoryStruct.comp (Y := prod.{v, u} Z X)
        (prod.lift (pullback.fst prod.snd f ≫ prod.fst) (pullback.snd prod.snd f))
        (pullback.lift (prod.map (𝟙 Z) f) prod.snd sorry))
      (pullback.fst prod.snd f))
    prod.snd =
  (𝟙 (pullback (X := prod.{v, u} Z Y) prod.snd f) ≫ pullback.fst prod.snd f) ≫ prod.snd
Tactic: apply prod.hom_ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
P X Y Z : C
fst : P ⟶ X
snd : P ⟶ Y
f : X ⟶ Z
g : Y ⟶ Z
inst_1 : IsIso fst
inst_2 : Mono g
sq : CommSq fst snd f g
⊢ IsLimit sq.cone
have _ : ∀ (s : PullbackCone f g), (fun (s : PullbackCone f g) ↦ s.fst ≫ inv fst) s ≫ snd = s.snd
Tactic: refine
        PullbackCone.IsLimit.mk _ (fun s => s.fst ≫ inv fst) (by simp)
          (fun s => ?_) (by cat_disch)