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
S : C
g : Y ⟶ X
f : X ⟶ S
i : pullback (g ≫ f) f ≅ pullback (g ≫ f) (𝟙 X ≫ f) := congrHom ⋯ ⋯
h₀ :
  (map (g ≫ f) (𝟙 X ≫ f) f f g (𝟙 X) (𝟙 S) ⋯ ⋯ ≫ 𝟙 (diagonalObj f)) ≫ fst f f =
    CategoryStruct.comp (Y := pullback f f) (i.inv ≫ map (g ≫ f) f f f g (𝟙 X) (𝟙 S) ⋯ ⋯) (fst f f)
⊢ map (g ≫ f) (𝟙 X ≫ f) f f g (𝟙 X) (𝟙 S) ⋯ ⋯ ≫ 𝟙 (diagonalObj f) = i.inv ≫ map (g ≫ f) f f f g (𝟙 X) (𝟙 S) ⋯ ⋯
have h₁ : (map (g ≫ f) (𝟙 X ≫ f) f f g (𝟙 X) (𝟙 S) sorry sorry ≫ 𝟙 (diagonalObj f)) ≫ snd f f =
  CategoryStruct.comp (Y := pullback f f) (i.inv ≫ map (g ≫ f) f f f g (𝟙 X) (𝟙 S) 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 : C
inst_1 : HasPullbacks.{v_1, u_1} C
S : C
g : Y ⟶ X
f : X ⟶ S
i : pullback (g ≫ f) f ≅ pullback (g ≫ f) (𝟙 X ≫ f) := congrHom ⋯ ⋯
e : pullback (Y := pullback (g ≫ f) f) (Z := diagonalObj f) (diagonal f) (map (g ≫ f) f f f g (𝟙 X) (𝟙 S) ⋯ ⋯) ≅
  pullback (Y := pullback (g ≫ f) (𝟙 X ≫ f)) (Z := diagonalObj f) (diagonal f)
    (map (g ≫ f) (𝟙 X ≫ f) f f g (𝟙 X) (𝟙 S) ⋯ ⋯) :=
  Iso.symm
    (asIso
      (map (diagonal f) (map (g ≫ f) (𝟙 X ≫ f) f f g (𝟙 X) (𝟙 S) ⋯ ⋯) (diagonal f) (map (g ≫ f) f f f g (𝟙 X) (𝟙 S) ⋯ ⋯)
        (𝟙 X) i.inv (𝟙 (diagonalObj f)) ⋯ ⋯))
⊢ IsPullback (Y := pullback (g ≫ f) f) (Z := diagonalObj f) g (lift (𝟙 Y) g ⋯) (diagonal f)
    (map (g ≫ f) f f f g (𝟙 X) (𝟙 S) ⋯ ⋯)
have w₁ : (e ≪≫ Iso.trans (Y := pullback g (𝟙 X)) (pullbackDiagonalMapIdIso g (𝟙 X) f) (asIso (fst g (𝟙 X)))).symm.hom ≫
    fst (diagonal f) (map (g ≫ f) f f f g (𝟙 X) (𝟙 S) sorry sorry) =
  g
Tactic: apply IsPullback.of_iso_pullback _
      (e ≪≫ pullbackDiagonalMapIdIso (T := X) (S := S) g (𝟙 X) f ≪≫ asIso (pullback.fst _ _)).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 : C
g : Y ⟶ X
f : X ⟶ S
i : pullback (g ≫ f) f ≅ pullback (g ≫ f) (𝟙 X ≫ f) := congrHom ⋯ ⋯
e : pullback (Y := pullback (g ≫ f) f) (Z := diagonalObj f) (diagonal f) (map (g ≫ f) f f f g (𝟙 X) (𝟙 S) ⋯ ⋯) ≅
  pullback (Y := pullback (g ≫ f) (𝟙 X ≫ f)) (Z := diagonalObj f) (diagonal f)
    (map (g ≫ f) (𝟙 X ≫ f) f f g (𝟙 X) (𝟙 S) ⋯ ⋯) :=
  Iso.symm
    (asIso
      (map (diagonal f) (map (g ≫ f) (𝟙 X ≫ f) f f g (𝟙 X) (𝟙 S) ⋯ ⋯) (diagonal f) (map (g ≫ f) f f f g (𝟙 X) (𝟙 S) ⋯ ⋯)
        (𝟙 X) i.inv (𝟙 (diagonalObj f)) ⋯ ⋯))
w₁ :
  (e ≪≫ Iso.trans (Y := pullback g (𝟙 X)) (pullbackDiagonalMapIdIso g (𝟙 X) f) (asIso (fst g (𝟙 X)))).symm.hom ≫
      fst (diagonal f) (map (g ≫ f) f f f g (𝟙 X) (𝟙 S) ⋯ ⋯) =
    g
⊢ IsPullback (Y := pullback (g ≫ f) f) (Z := diagonalObj f) g (lift (𝟙 Y) g ⋯) (diagonal f)
    (map (g ≫ f) f f f g (𝟙 X) (𝟙 S) ⋯ ⋯)
have w₂ : (e ≪≫ Iso.trans (Y := pullback g (𝟙 X)) (pullbackDiagonalMapIdIso g (𝟙 X) f) (asIso (fst g (𝟙 X)))).symm.hom ≫
    snd (diagonal f) (map (g ≫ f) f f f g (𝟙 X) (𝟙 S) sorry sorry) =
  lift (𝟙 Y) g sorry
Tactic: apply IsPullback.of_iso_pullback _
      (e ≪≫ pullbackDiagonalMapIdIso (T := X) (S := S) g (𝟙 X) f ≪≫ asIso (pullback.fst _ _)).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 : C
g : Y ⟶ X
f : X ⟶ S
i : pullback (g ≫ f) f ≅ pullback (g ≫ f) (𝟙 X ≫ f) := congrHom ⋯ ⋯
e : pullback (Y := pullback (g ≫ f) f) (Z := diagonalObj f) (diagonal f) (map (g ≫ f) f f f g (𝟙 X) (𝟙 S) ⋯ ⋯) ≅
  pullback (Y := pullback (g ≫ f) (𝟙 X ≫ f)) (Z := diagonalObj f) (diagonal f)
    (map (g ≫ f) (𝟙 X ≫ f) f f g (𝟙 X) (𝟙 S) ⋯ ⋯) :=
  Iso.symm
    (asIso
      (map (diagonal f) (map (g ≫ f) (𝟙 X ≫ f) f f g (𝟙 X) (𝟙 S) ⋯ ⋯) (diagonal f) (map (g ≫ f) f f f g (𝟙 X) (𝟙 S) ⋯ ⋯)
        (𝟙 X) i.inv (𝟙 (diagonalObj f)) ⋯ ⋯))
w₁ :
  (e ≪≫ Iso.trans (Y := pullback g (𝟙 X)) (pullbackDiagonalMapIdIso g (𝟙 X) f) (asIso (fst g (𝟙 X)))).symm.hom ≫
      fst (diagonal f) (map (g ≫ f) f f f g (𝟙 X) (𝟙 S) ⋯ ⋯) =
    g
w₂ :
  (e ≪≫ Iso.trans (Y := pullback g (𝟙 X)) (pullbackDiagonalMapIdIso g (𝟙 X) f) (asIso (fst g (𝟙 X)))).symm.hom ≫
      snd (diagonal f) (map (g ≫ f) f f f g (𝟙 X) (𝟙 S) ⋯ ⋯) =
    lift (𝟙 Y) g ⋯
⊢ IsPullback (Y := pullback (g ≫ f) f) (Z := diagonalObj f) g (lift (𝟙 Y) g ⋯) (diagonal f)
    (map (g ≫ f) f f f g (𝟙 X) (𝟙 S) ⋯ ⋯)
have apply : CommSq (Y := pullback (g ≫ f) f) (Z := diagonalObj f) g (lift (𝟙 Y) g sorry) (diagonal f)
  (map (g ≫ f) f f f g (𝟙 X) (𝟙 S) sorry sorry)
Tactic: apply IsPullback.of_iso_pullback _
      (e ≪≫ pullbackDiagonalMapIdIso (T := X) (S := S) g (𝟙 X) f ≪≫ asIso (pullback.fst _ _)).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 : C
g : Y ⟶ X
f : X ⟶ S
i : pullback (g ≫ f) f ≅ pullback (g ≫ f) (𝟙 X ≫ f) := congrHom ⋯ ⋯
e : pullback (Y := pullback (g ≫ f) f) (Z := diagonalObj f) (diagonal f) (map (g ≫ f) f f f g (𝟙 X) (𝟙 S) ⋯ ⋯) ≅
  pullback (Y := pullback (g ≫ f) (𝟙 X ≫ f)) (Z := diagonalObj f) (diagonal f)
    (map (g ≫ f) (𝟙 X ≫ f) f f g (𝟙 X) (𝟙 S) ⋯ ⋯) :=
  Iso.symm
    (asIso
      (map (diagonal f) (map (g ≫ f) (𝟙 X ≫ f) f f g (𝟙 X) (𝟙 S) ⋯ ⋯) (diagonal f) (map (g ≫ f) f f f g (𝟙 X) (𝟙 S) ⋯ ⋯)
        (𝟙 X) i.inv (𝟙 (diagonalObj f)) ⋯ ⋯))
⊢ (e ≪≫ Iso.trans (Y := pullback g (𝟙 X)) (pullbackDiagonalMapIdIso g (𝟙 X) f) (asIso (fst g (𝟙 X)))).symm.hom ≫
      snd (diagonal f) (map (g ≫ f) f f f g (𝟙 X) (𝟙 S) ⋯ ⋯) =
    lift (𝟙 Y) g ⋯
have w₂ : ((e ≪≫ Iso.trans (Y := pullback g (𝟙 X)) (pullbackDiagonalMapIdIso g (𝟙 X) f) (asIso (fst g (𝟙 X)))).symm.hom ≫
      snd (diagonal f) (map (g ≫ f) f f f g (𝟙 X) (𝟙 S) sorry sorry)) ≫
    fst (g ≫ f) f =
  CategoryStruct.comp (Y := pullback (g ≫ f) f) (lift (𝟙 Y) g sorry) (fst (g ≫ 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 : C
inst_1 : HasPullbacks.{v_1, u_1} C
S : C
g : Y ⟶ X
f : X ⟶ S
i : pullback (g ≫ f) f ≅ pullback (g ≫ f) (𝟙 X ≫ f) := congrHom ⋯ ⋯
e : pullback (Y := pullback (g ≫ f) f) (Z := diagonalObj f) (diagonal f) (map (g ≫ f) f f f g (𝟙 X) (𝟙 S) ⋯ ⋯) ≅
  pullback (Y := pullback (g ≫ f) (𝟙 X ≫ f)) (Z := diagonalObj f) (diagonal f)
    (map (g ≫ f) (𝟙 X ≫ f) f f g (𝟙 X) (𝟙 S) ⋯ ⋯) :=
  Iso.symm
    (asIso
      (map (diagonal f) (map (g ≫ f) (𝟙 X ≫ f) f f g (𝟙 X) (𝟙 S) ⋯ ⋯) (diagonal f) (map (g ≫ f) f f f g (𝟙 X) (𝟙 S) ⋯ ⋯)
        (𝟙 X) i.inv (𝟙 (diagonalObj f)) ⋯ ⋯))
w₂ :
  ((e ≪≫ Iso.trans (Y := pullback g (𝟙 X)) (pullbackDiagonalMapIdIso g (𝟙 X) f) (asIso (fst g (𝟙 X)))).symm.hom ≫
        snd (diagonal f) (map (g ≫ f) f f f g (𝟙 X) (𝟙 S) ⋯ ⋯)) ≫
      fst (g ≫ f) f =
    CategoryStruct.comp (Y := pullback (g ≫ f) f) (lift (𝟙 Y) g ⋯) (fst (g ≫ f) f)
⊢ (e ≪≫ Iso.trans (Y := pullback g (𝟙 X)) (pullbackDiagonalMapIdIso g (𝟙 X) f) (asIso (fst g (𝟙 X)))).symm.hom ≫
      snd (diagonal f) (map (g ≫ f) f f f g (𝟙 X) (𝟙 S) ⋯ ⋯) =
    lift (𝟙 Y) g ⋯
have w₃ : ((e ≪≫ Iso.trans (Y := pullback g (𝟙 X)) (pullbackDiagonalMapIdIso g (𝟙 X) f) (asIso (fst g (𝟙 X)))).symm.hom ≫
      snd (diagonal f) (map (g ≫ f) f f f g (𝟙 X) (𝟙 S) sorry sorry)) ≫
    snd (g ≫ f) f =
  CategoryStruct.comp (Y := pullback (g ≫ f) f) (lift (𝟙 Y) g sorry) (snd (g ≫ 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 : C
inst_1 : HasPullbacks.{v_1, u_1} C
S : C
g : Y ⟶ X
f : X ⟶ S
i : pullback (g ≫ f) f ≅ pullback (g ≫ f) (𝟙 X ≫ f) := congrHom ⋯ ⋯
e : pullback (Y := pullback (g ≫ f) f) (Z := diagonalObj f) (diagonal f) (map (g ≫ f) f f f g (𝟙 X) (𝟙 S) ⋯ ⋯) ≅
  pullback (Y := pullback (g ≫ f) (𝟙 X ≫ f)) (Z := diagonalObj f) (diagonal f)
    (map (g ≫ f) (𝟙 X ≫ f) f f g (𝟙 X) (𝟙 S) ⋯ ⋯) :=
  Iso.symm
    (asIso
      (map (diagonal f) (map (g ≫ f) (𝟙 X ≫ f) f f g (𝟙 X) (𝟙 S) ⋯ ⋯) (diagonal f) (map (g ≫ f) f f f g (𝟙 X) (𝟙 S) ⋯ ⋯)
        (𝟙 X) i.inv (𝟙 (diagonalObj f)) ⋯ ⋯))
⊢ CommSq (Y := pullback (g ≫ f) f) (Z := diagonalObj f) g (lift (𝟙 Y) g ⋯) (diagonal f)
    (map (g ≫ f) f f f g (𝟙 X) (𝟙 S) ⋯ ⋯)
have w : autoParam
  (Eq (α := Y ⟶ diagonalObj f) (g ≫ diagonal f)
    (CategoryStruct.comp (Y := pullback (g ≫ f) f) (lift (𝟙 Y) g sorry) (map (g ≫ f) f f f g (𝟙 X) (𝟙 S) sorry sorry)))
  CommSq.w._autoParam
Tactic: constructor
-- 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 : C
g : Y ⟶ X
f : X ⟶ S
i : pullback (g ≫ f) f ≅ pullback (g ≫ f) (𝟙 X ≫ f) := congrHom ⋯ ⋯
e : pullback (Y := pullback (g ≫ f) f) (Z := diagonalObj f) (diagonal f) (map (g ≫ f) f f f g (𝟙 X) (𝟙 S) ⋯ ⋯) ≅
  pullback (Y := pullback (g ≫ f) (𝟙 X ≫ f)) (Z := diagonalObj f) (diagonal f)
    (map (g ≫ f) (𝟙 X ≫ f) f f g (𝟙 X) (𝟙 S) ⋯ ⋯) :=
  Iso.symm
    (asIso
      (map (diagonal f) (map (g ≫ f) (𝟙 X ≫ f) f f g (𝟙 X) (𝟙 S) ⋯ ⋯) (diagonal f) (map (g ≫ f) f f f g (𝟙 X) (𝟙 S) ⋯ ⋯)
        (𝟙 X) i.inv (𝟙 (diagonalObj f)) ⋯ ⋯))
⊢ autoParam
    (Eq (α := Y ⟶ diagonalObj f) (g ≫ diagonal f)
      (CategoryStruct.comp (Y := pullback (g ≫ f) f) (lift (𝟙 Y) g ⋯) (map (g ≫ f) f f f g (𝟙 X) (𝟙 S) ⋯ ⋯)))
    CommSq.w._autoParam
have w : CategoryStruct.comp (Y := pullback f f) (g ≫ diagonal f) (fst f f) =
  CategoryStruct.comp (Y := pullback f f)
    (CategoryStruct.comp (Y := pullback (g ≫ f) f) (lift (𝟙 Y) g sorry) (map (g ≫ f) f f f g (𝟙 X) (𝟙 S) sorry sorry)) (fst 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 : C
inst_1 : HasPullbacks.{v_1, u_1} C
S : C
g : Y ⟶ X
f : X ⟶ S
i : pullback (g ≫ f) f ≅ pullback (g ≫ f) (𝟙 X ≫ f) := congrHom ⋯ ⋯
e : pullback (Y := pullback (g ≫ f) f) (Z := diagonalObj f) (diagonal f) (map (g ≫ f) f f f g (𝟙 X) (𝟙 S) ⋯ ⋯) ≅
  pullback (Y := pullback (g ≫ f) (𝟙 X ≫ f)) (Z := diagonalObj f) (diagonal f)
    (map (g ≫ f) (𝟙 X ≫ f) f f g (𝟙 X) (𝟙 S) ⋯ ⋯) :=
  Iso.symm
    (asIso
      (map (diagonal f) (map (g ≫ f) (𝟙 X ≫ f) f f g (𝟙 X) (𝟙 S) ⋯ ⋯) (diagonal f) (map (g ≫ f) f f f g (𝟙 X) (𝟙 S) ⋯ ⋯)
        (𝟙 X) i.inv (𝟙 (diagonalObj f)) ⋯ ⋯))
w :
  CategoryStruct.comp (Y := pullback f f) (g ≫ diagonal f) (fst f f) =
    CategoryStruct.comp (Y := pullback f f)
      (CategoryStruct.comp (Y := pullback (g ≫ f) f) (lift (𝟙 Y) g ⋯) (map (g ≫ f) f f f g (𝟙 X) (𝟙 S) ⋯ ⋯)) (fst f f)
⊢ autoParam
    (Eq (α := Y ⟶ diagonalObj f) (g ≫ diagonal f)
      (CategoryStruct.comp (Y := pullback (g ≫ f) f) (lift (𝟙 Y) g ⋯) (map (g ≫ f) f f f g (𝟙 X) (𝟙 S) ⋯ ⋯)))
    CommSq.w._autoParam
have w₁ : CategoryStruct.comp (Y := pullback f f) (g ≫ diagonal f) (snd f f) =
  CategoryStruct.comp (Y := pullback f f)
    (CategoryStruct.comp (Y := pullback (g ≫ f) f) (lift (𝟙 Y) g sorry) (map (g ≫ f) f f f g (𝟙 X) (𝟙 S) 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
inst_1 : HasPullbacks.{v_1, u_1} C
X Y S X' Y' S' : C
f : X ⟶ S
g : Y ⟶ S
f' : X' ⟶ S'
g' : Y' ⟶ S'
i₁ : X ⟶ X'
i₂ : Y ⟶ Y'
i₃ : S ⟶ S'
e₁ : f ≫ i₃ = i₁ ≫ f'
e₂ : g ≫ i₃ = i₂ ≫ g'
inst_2 : Mono i₃
⊢ Eq (α := pullback f g ⟶ pullback f' g')
    (CategoryStruct.comp (Y := pullback (X := pullback f' g') (fst f' g') i₁)
      (lift (map f g f' g' i₁ i₂ i₃ e₁ e₂) (fst f g) ⋯) (fst (fst f' g') i₁))
    (CategoryStruct.comp (Y := pullback (X := pullback f' g') (snd f' g') i₂)
      (lift (map f g f' g' i₁ i₂ i₃ e₁ e₂) (snd f g) ⋯) (fst (snd f' g') i₂))
have rw : Eq (α := pullback f g ⟶ pullback f' g') (map f g f' g' i₁ i₂ i₃ e₁ e₂)
  (CategoryStruct.comp (Y := pullback (X := pullback f' g') (snd f' g') i₂)
    (lift (map f g f' g' i₁ i₂ i₃ e₁ e₂) (snd f g) sorry) (fst (snd f' g') i₂))
Tactic: rw [lift_fst, lift_fst]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Diagonal (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasPullbacks.{v_1, u_1} C
X Y S X' Y' S' : C
f : X ⟶ S
g : Y ⟶ S
f' : X' ⟶ S'
g' : Y' ⟶ S'
i₁ : X ⟶ X'
i₂ : Y ⟶ Y'
i₃ : S ⟶ S'
e₁ : f ≫ i₃ = i₁ ≫ f'
e₂ : g ≫ i₃ = i₂ ≫ g'
inst_2 : Mono i₃
rw :
  Eq (α := pullback f g ⟶ pullback f' g') (map f g f' g' i₁ i₂ i₃ e₁ e₂)
    (CategoryStruct.comp (Y := pullback (X := pullback f' g') (snd f' g') i₂)
      (lift (map f g f' g' i₁ i₂ i₃ e₁ e₂) (snd f g) ⋯) (fst (snd f' g') i₂))
⊢ Eq (α := pullback f g ⟶ pullback f' g')
    (CategoryStruct.comp (Y := pullback (X := pullback f' g') (fst f' g') i₁)
      (lift (map f g f' g' i₁ i₂ i₃ e₁ e₂) (fst f g) ⋯) (fst (fst f' g') i₁))
    (CategoryStruct.comp (Y := pullback (X := pullback f' g') (snd f' g') i₂)
      (lift (map f g f' g' i₁ i₂ i₃ e₁ e₂) (snd f g) ⋯) (fst (snd f' g') i₂))
have rw₁ : Eq (α := pullback f g ⟶ pullback f' g') (map f g f' g' i₁ i₂ i₃ e₁ e₂) (map f g f' g' i₁ i₂ i₃ e₁ e₂)
Tactic: rw [lift_fst, lift_fst]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Diagonal (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasPullbacks.{v_1, u_1} C
X Y Z S : C
f : X ⟶ S
g : Y ⟶ S
h : Z ⟶ S
⊢ IsPullback (P := pullback (X := pullback f g) (Y := pullback f h) (fst f g) (fst f h)) (X := pullback g h)
    (map (fst f g) (fst f h) g h (snd f g) (snd f h) f ⋯ ⋯) (fst (fst f g) (fst f h)) (fst g h) (snd f g)
have refine_1 : (s : PullbackCone (X := pullback g h) (Y := pullback f g) (fst g h) (snd f g)) →
  s.pt ⟶ pullback (X := pullback f g) (Y := pullback f h) (fst f g) (fst f h)
Tactic: refine ⟨⟨by simp⟩, ⟨PullbackCone.IsLimit.mk _ ?_ ?_ ?_ ?_⟩⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Diagonal (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasPullbacks.{v_1, u_1} C
X Y Z S : C
f : X ⟶ S
g : Y ⟶ S
h : Z ⟶ S
refine_1 :
  (s : PullbackCone (X := pullback g h) (Y := pullback f g) (fst g h) (snd f g)) →
    s.pt ⟶ pullback (X := pullback f g) (Y := pullback f h) (fst f g) (fst f h)
⊢ IsPullback (P := pullback (X := pullback f g) (Y := pullback f h) (fst f g) (fst f h)) (X := pullback g h)
    (map (fst f g) (fst f h) g h (snd f g) (snd f h) f ⋯ ⋯) (fst (fst f g) (fst f h)) (fst g h) (snd f g)
have refine_2 : ∀ (s : PullbackCone (X := pullback g h) (Y := pullback f g) (fst g h) (snd f g)),
  CategoryStruct.comp (Y := pullback (X := pullback f g) (Y := pullback f h) (fst f g) (fst f h))
      (lift s.snd (lift (s.snd ≫ fst f g) (s.fst ≫ snd g h) sorry) sorry)
      (map (fst f g) (fst f h) g h (snd f g) (snd f h) f sorry sorry) =
    s.fst
Tactic: refine ⟨⟨by simp⟩, ⟨PullbackCone.IsLimit.mk _ ?_ ?_ ?_ ?_⟩⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Diagonal (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasPullbacks.{v_1, u_1} C
X Y Z S : C
f : X ⟶ S
g : Y ⟶ S
h : Z ⟶ S
refine_1 :
  (s : PullbackCone (X := pullback g h) (Y := pullback f g) (fst g h) (snd f g)) →
    s.pt ⟶ pullback (X := pullback f g) (Y := pullback f h) (fst f g) (fst f h)
refine_2 :
  ∀ (s : PullbackCone (X := pullback g h) (Y := pullback f g) (fst g h) (snd f g)),
    CategoryStruct.comp (Y := pullback (X := pullback f g) (Y := pullback f h) (fst f g) (fst f h))
        (lift s.snd (lift (s.snd ≫ fst f g) (s.fst ≫ snd g h) ⋯) ⋯)
        (map (fst f g) (fst f h) g h (snd f g) (snd f h) f ⋯ ⋯) =
      s.fst
⊢ IsPullback (P := pullback (X := pullback f g) (Y := pullback f h) (fst f g) (fst f h)) (X := pullback g h)
    (map (fst f g) (fst f h) g h (snd f g) (snd f h) f ⋯ ⋯) (fst (fst f g) (fst f h)) (fst g h) (snd f g)
have refine_3 : ∀ (s : PullbackCone (X := pullback g h) (Y := pullback f g) (fst g h) (snd f g)),
  CategoryStruct.comp (Y := pullback (X := pullback f g) (Y := pullback f h) (fst f g) (fst f h))
      (lift s.snd (lift (s.snd ≫ fst f g) (s.fst ≫ snd g h) sorry) sorry) (fst (fst f g) (fst f h)) =
    s.snd
Tactic: refine ⟨⟨by simp⟩, ⟨PullbackCone.IsLimit.mk _ ?_ ?_ ?_ ?_⟩⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Diagonal (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasPullbacks.{v_1, u_1} C
X Y Z S : C
f : X ⟶ S
g : Y ⟶ S
h : Z ⟶ S
refine_1 :
  (s : PullbackCone (X := pullback g h) (Y := pullback f g) (fst g h) (snd f g)) →
    s.pt ⟶ pullback (X := pullback f g) (Y := pullback f h) (fst f g) (fst f h)
refine_2 :
  ∀ (s : PullbackCone (X := pullback g h) (Y := pullback f g) (fst g h) (snd f g)),
    CategoryStruct.comp (Y := pullback (X := pullback f g) (Y := pullback f h) (fst f g) (fst f h))
        (lift s.snd (lift (s.snd ≫ fst f g) (s.fst ≫ snd g h) ⋯) ⋯)
        (map (fst f g) (fst f h) g h (snd f g) (snd f h) f ⋯ ⋯) =
      s.fst
refine_3 :
  ∀ (s : PullbackCone (X := pullback g h) (Y := pullback f g) (fst g h) (snd f g)),
    CategoryStruct.comp (Y := pullback (X := pullback f g) (Y := pullback f h) (fst f g) (fst f h))
        (lift s.snd (lift (s.snd ≫ fst f g) (s.fst ≫ snd g h) ⋯) ⋯) (fst (fst f g) (fst f h)) =
      s.snd
⊢ IsPullback (P := pullback (X := pullback f g) (Y := pullback f h) (fst f g) (fst f h)) (X := pullback g h)
    (map (fst f g) (fst f h) g h (snd f g) (snd f h) f ⋯ ⋯) (fst (fst f g) (fst f h)) (fst g h) (snd f g)
have refine_4 : ∀ (s : PullbackCone (X := pullback g h) (Y := pullback f g) (fst g h) (snd f g))
  (m : s.pt ⟶ pullback (X := pullback f g) (Y := pullback f h) (fst f g) (fst f h)),
  m ≫ map (fst f g) (fst f h) g h (snd f g) (snd f h) f sorry sorry = s.fst →
    m ≫ fst (fst f g) (fst f h) = s.snd → m = lift s.snd (lift (s.snd ≫ fst f g) (s.fst ≫ snd g h) sorry) sorry
Tactic: refine ⟨⟨by simp⟩, ⟨PullbackCone.IsLimit.mk _ ?_ ?_ ?_ ?_⟩⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Diagonal (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasPullbacks.{v_1, u_1} C
X Y Z S : C
f : X ⟶ S
g : Y ⟶ S
h : Z ⟶ S
c : PullbackCone (X := pullback g h) (Y := pullback f g) (fst g h) (snd f g)
⊢ c.pt ⟶ pullback (X := pullback f g) (Y := pullback f h) (fst f g) (fst f h)
have refine_1 : (c.snd ≫ fst f g) ≫ f = (c.fst ≫ snd g h) ≫ h
Tactic: refine pullback.lift c.snd
        (pullback.lift (c.snd ≫ pullback.fst _ _) (c.fst ≫ pullback.snd _ _) ?_) ?_
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Diagonal (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasPullbacks.{v_1, u_1} C
X Y Z S : C
f : X ⟶ S
g : Y ⟶ S
h : Z ⟶ S
c : PullbackCone (X := pullback g h) (Y := pullback f g) (fst g h) (snd f g)
refine_1 : (c.snd ≫ fst f g) ≫ f = (c.fst ≫ snd g h) ≫ h
⊢ c.pt ⟶ pullback (X := pullback f g) (Y := pullback f h) (fst f g) (fst f h)
have refine_1₁ : c.snd ≫ fst f g = CategoryStruct.comp (Y := pullback f h) (lift (c.snd ≫ fst f g) (c.fst ≫ snd g h) sorry) (fst f h)
Tactic: refine pullback.lift c.snd
        (pullback.lift (c.snd ≫ pullback.fst _ _) (c.fst ≫ pullback.snd _ _) ?_) ?_
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Diagonal (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasPullbacks.{v_1, u_1} C
X Y Z S : C
f : X ⟶ S
g : Y ⟶ S
h : Z ⟶ S
c : PullbackCone (X := pullback g h) (Y := pullback f g) (fst g h) (snd f g)
⊢ CategoryStruct.comp (Y := pullback (X := pullback f g) (Y := pullback f h) (fst f g) (fst f h))
      (lift c.snd (lift (c.snd ≫ fst f g) (c.fst ≫ snd g h) ⋯) ⋯)
      (map (fst f g) (fst f h) g h (snd f g) (snd f h) f ⋯ ⋯) =
    c.fst
have refine_2 : CategoryStruct.comp (Y := pullback g h)
    (CategoryStruct.comp (Y := pullback (X := pullback f g) (Y := pullback f h) (fst f g) (fst f h))
      (lift c.snd (lift (c.snd ≫ fst f g) (c.fst ≫ snd g h) sorry) sorry)
      (map (fst f g) (fst f h) g h (snd f g) (snd f h) f sorry sorry))
    (fst g h) =
  c.fst ≫ fst g h
Tactic: apply pullback.hom_ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Diagonal (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasPullbacks.{v_1, u_1} C
X Y Z S : C
f : X ⟶ S
g : Y ⟶ S
h : Z ⟶ S
c : PullbackCone (X := pullback g h) (Y := pullback f g) (fst g h) (snd f g)
refine_2 :
  CategoryStruct.comp (Y := pullback g h)
      (CategoryStruct.comp (Y := pullback (X := pullback f g) (Y := pullback f h) (fst f g) (fst f h))
        (lift c.snd (lift (c.snd ≫ fst f g) (c.fst ≫ snd g h) ⋯) ⋯)
        (map (fst f g) (fst f h) g h (snd f g) (snd f h) f ⋯ ⋯))
      (fst g h) =
    c.fst ≫ fst g h
⊢ CategoryStruct.comp (Y := pullback (X := pullback f g) (Y := pullback f h) (fst f g) (fst f h))
      (lift c.snd (lift (c.snd ≫ fst f g) (c.fst ≫ snd g h) ⋯) ⋯)
      (map (fst f g) (fst f h) g h (snd f g) (snd f h) f ⋯ ⋯) =
    c.fst
have refine_2₁ : CategoryStruct.comp (Y := pullback g h)
    (CategoryStruct.comp (Y := pullback (X := pullback f g) (Y := pullback f h) (fst f g) (fst f h))
      (lift c.snd (lift (c.snd ≫ fst f g) (c.fst ≫ snd g h) sorry) sorry)
      (map (fst f g) (fst f h) g h (snd f g) (snd f h) f sorry sorry))
    (snd g h) =
  c.fst ≫ snd g h
Tactic: apply pullback.hom_ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Diagonal (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasPullbacks.{v_1, u_1} C
X Y Z S : C
f : X ⟶ S
g : Y ⟶ S
h : Z ⟶ S
c : PullbackCone (X := pullback g h) (Y := pullback f g) (fst g h) (snd f g)
⊢ CategoryStruct.comp (Y := pullback (X := pullback f g) (Y := pullback f h) (fst f g) (fst f h))
      (lift c.snd (lift (c.snd ≫ fst f g) (c.fst ≫ snd g h) ⋯) ⋯) (fst (fst f g) (fst f h)) =
    c.snd
have refine_3 : CategoryStruct.comp (Y := pullback (X := pullback f g) (Y := pullback f h) (fst f g) (fst f h))
      (lift c.snd (lift (c.snd ≫ fst f g) (c.fst ≫ snd g h) sorry) sorry) (fst (fst f g) (fst f h)) ≫
    fst f g =
  c.snd ≫ fst f g
Tactic: apply pullback.hom_ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Diagonal (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasPullbacks.{v_1, u_1} C
X Y Z S : C
f : X ⟶ S
g : Y ⟶ S
h : Z ⟶ S
c : PullbackCone (X := pullback g h) (Y := pullback f g) (fst g h) (snd f g)
refine_3 :
  CategoryStruct.comp (Y := pullback (X := pullback f g) (Y := pullback f h) (fst f g) (fst f h))
        (lift c.snd (lift (c.snd ≫ fst f g) (c.fst ≫ snd g h) ⋯) ⋯) (fst (fst f g) (fst f h)) ≫
      fst f g =
    c.snd ≫ fst f g
⊢ CategoryStruct.comp (Y := pullback (X := pullback f g) (Y := pullback f h) (fst f g) (fst f h))
      (lift c.snd (lift (c.snd ≫ fst f g) (c.fst ≫ snd g h) ⋯) ⋯) (fst (fst f g) (fst f h)) =
    c.snd
have refine_3₁ : CategoryStruct.comp (Y := pullback (X := pullback f g) (Y := pullback f h) (fst f g) (fst f h))
      (lift c.snd (lift (c.snd ≫ fst f g) (c.fst ≫ snd g h) sorry) sorry) (fst (fst f g) (fst f h)) ≫
    snd f g =
  c.snd ≫ snd f g
Tactic: apply pullback.hom_ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Diagonal (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasPullbacks.{v_1, u_1} C
X Y Z S : C
f : X ⟶ S
g : Y ⟶ S
h : Z ⟶ S
c : PullbackCone (X := pullback g h) (Y := pullback f g) (fst g h) (snd f g)
m : c.pt ⟶ pullback (X := pullback f g) (Y := pullback f h) (fst f g) (fst f h)
hfst : m ≫ map (fst f g) (fst f h) g h (snd f g) (snd f h) f ⋯ ⋯ = c.fst
hsnd : m ≫ fst (fst f g) (fst f h) = c.snd
⊢ m = lift c.snd (lift (c.snd ≫ fst f g) (c.fst ≫ snd g h) ⋯) ⋯
have refine_4 : m ≫ snd (fst f g) (fst f h) =
  CategoryStruct.comp (Y := pullback (X := pullback f g) (Y := pullback f h) (fst f g) (fst f h))
    (lift c.snd (lift (c.snd ≫ fst f g) (c.fst ≫ snd g h) sorry) sorry) (snd (fst f g) (fst f h))
Tactic: refine pullback.hom_ext (by simpa) ?_