awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
A B : C
f : A ⟶ B
X : C
inst_1 : HasBinaryCoproduct.{v₁, u₁} A X
inst_2 : HasBinaryCoproduct.{v₁, u₁} B X
s : PushoutCocone (Y := coprod.{v₁, u₁} A X) coprod.inl f
refine_1 :
  CategoryStruct.comp (Y :=
      Cocone.pt (F := span (Y := coprod.{v₁, u₁} A X) coprod.inl f)
        (PushoutCocone.mk (W := coprod.{v₁, u₁} B X) (coprod.map f (𝟙 X)) coprod.inl ⋯))
      (PushoutCocone.inl (PushoutCocone.mk (W := coprod.{v₁, u₁} B X) (coprod.map f (𝟙 X)) coprod.inl ⋯))
      (coprod.desc s.inr (coprod.inr ≫ s.inl)) =
    s.inl
⊢ { l :
    Cocone.pt (F := span (Y := coprod.{v₁, u₁} A X) coprod.inl f)
        (PushoutCocone.mk (W := coprod.{v₁, u₁} B X) (coprod.map f (𝟙 X)) coprod.inl ⋯) ⟶
      s.pt //
    PushoutCocone.inl (PushoutCocone.mk (W := coprod.{v₁, u₁} B X) (coprod.map f (𝟙 X)) coprod.inl ⋯) ≫ l = s.inl ∧
      PushoutCocone.inr (PushoutCocone.mk (W := coprod.{v₁, u₁} B X) (coprod.map f (𝟙 X)) coprod.inl ⋯) ≫ l = s.inr ∧
        ∀
          {m :
            Cocone.pt (F := span (Y := coprod.{v₁, u₁} A X) coprod.inl f)
                (PushoutCocone.mk (W := coprod.{v₁, u₁} B X) (coprod.map f (𝟙 X)) coprod.inl ⋯) ⟶
              s.pt},
          PushoutCocone.inl (PushoutCocone.mk (W := coprod.{v₁, u₁} B X) (coprod.map f (𝟙 X)) coprod.inl ⋯) ≫ m =
              s.inl →
            PushoutCocone.inr (PushoutCocone.mk (W := coprod.{v₁, u₁} B X) (coprod.map f (𝟙 X)) coprod.inl ⋯) ≫ m =
                s.inr →
              m = l }
have refine_2 : CategoryStruct.comp (Y :=
    Cocone.pt (F := span (Y := coprod.{v₁, u₁} A X) coprod.inl f)
      (PushoutCocone.mk (W := coprod.{v₁, u₁} B X) (coprod.map f (𝟙 X)) coprod.inl sorry))
    (PushoutCocone.inr (PushoutCocone.mk (W := coprod.{v₁, u₁} B X) (coprod.map f (𝟙 X)) coprod.inl sorry))
    (coprod.desc s.inr (coprod.inr ≫ s.inl)) =
  s.inr
Tactic: refine ⟨coprod.desc s.inr (coprod.inr ≫ s.inl), ?_, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
A B : C
f : A ⟶ B
X : C
inst_1 : HasBinaryCoproduct.{v₁, u₁} A X
inst_2 : HasBinaryCoproduct.{v₁, u₁} B X
s : PushoutCocone (Y := coprod.{v₁, u₁} A X) coprod.inl f
refine_1 :
  CategoryStruct.comp (Y :=
      Cocone.pt (F := span (Y := coprod.{v₁, u₁} A X) coprod.inl f)
        (PushoutCocone.mk (W := coprod.{v₁, u₁} B X) (coprod.map f (𝟙 X)) coprod.inl ⋯))
      (PushoutCocone.inl (PushoutCocone.mk (W := coprod.{v₁, u₁} B X) (coprod.map f (𝟙 X)) coprod.inl ⋯))
      (coprod.desc s.inr (coprod.inr ≫ s.inl)) =
    s.inl
refine_2 :
  CategoryStruct.comp (Y :=
      Cocone.pt (F := span (Y := coprod.{v₁, u₁} A X) coprod.inl f)
        (PushoutCocone.mk (W := coprod.{v₁, u₁} B X) (coprod.map f (𝟙 X)) coprod.inl ⋯))
      (PushoutCocone.inr (PushoutCocone.mk (W := coprod.{v₁, u₁} B X) (coprod.map f (𝟙 X)) coprod.inl ⋯))
      (coprod.desc s.inr (coprod.inr ≫ s.inl)) =
    s.inr
⊢ { l :
    Cocone.pt (F := span (Y := coprod.{v₁, u₁} A X) coprod.inl f)
        (PushoutCocone.mk (W := coprod.{v₁, u₁} B X) (coprod.map f (𝟙 X)) coprod.inl ⋯) ⟶
      s.pt //
    PushoutCocone.inl (PushoutCocone.mk (W := coprod.{v₁, u₁} B X) (coprod.map f (𝟙 X)) coprod.inl ⋯) ≫ l = s.inl ∧
      PushoutCocone.inr (PushoutCocone.mk (W := coprod.{v₁, u₁} B X) (coprod.map f (𝟙 X)) coprod.inl ⋯) ≫ l = s.inr ∧
        ∀
          {m :
            Cocone.pt (F := span (Y := coprod.{v₁, u₁} A X) coprod.inl f)
                (PushoutCocone.mk (W := coprod.{v₁, u₁} B X) (coprod.map f (𝟙 X)) coprod.inl ⋯) ⟶
              s.pt},
          PushoutCocone.inl (PushoutCocone.mk (W := coprod.{v₁, u₁} B X) (coprod.map f (𝟙 X)) coprod.inl ⋯) ≫ m =
              s.inl →
            PushoutCocone.inr (PushoutCocone.mk (W := coprod.{v₁, u₁} B X) (coprod.map f (𝟙 X)) coprod.inl ⋯) ≫ m =
                s.inr →
              m = l }
have refine_3 : ∀
  {m :
    Cocone.pt (F := span (Y := coprod.{v₁, u₁} A X) coprod.inl f)
        (PushoutCocone.mk (W := coprod.{v₁, u₁} B X) (coprod.map f (𝟙 X)) coprod.inl sorry) ⟶
      s.pt},
  PushoutCocone.inl (PushoutCocone.mk (W := coprod.{v₁, u₁} B X) (coprod.map f (𝟙 X)) coprod.inl sorry) ≫ m = s.inl →
    PushoutCocone.inr (PushoutCocone.mk (W := coprod.{v₁, u₁} B X) (coprod.map f (𝟙 X)) coprod.inl sorry) ≫ m = s.inr →
      m = coprod.desc s.inr (coprod.inr ≫ s.inl)
Tactic: refine ⟨coprod.desc s.inr (coprod.inr ≫ s.inl), ?_, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
A B : C
f : A ⟶ B
X : C
inst_1 : HasBinaryCoproduct.{v₁, u₁} A X
inst_2 : HasBinaryCoproduct.{v₁, u₁} B X
s : PushoutCocone (Y := coprod.{v₁, u₁} A X) coprod.inl f
⊢ CategoryStruct.comp (Y :=
      Cocone.pt (F := span (Y := coprod.{v₁, u₁} A X) coprod.inl f)
        (PushoutCocone.mk (W := coprod.{v₁, u₁} B X) (coprod.map f (𝟙 X)) coprod.inl ⋯))
      (PushoutCocone.inl (PushoutCocone.mk (W := coprod.{v₁, u₁} B X) (coprod.map f (𝟙 X)) coprod.inl ⋯))
      (coprod.desc s.inr (coprod.inr ≫ s.inl)) =
    s.inl
have refine_1 : CategoryStruct.comp (Y := coprod.{v₁, u₁} A X) coprod.inl
    (CategoryStruct.comp (Y :=
      Cocone.pt (F := span (Y := coprod.{v₁, u₁} A X) coprod.inl f)
        (PushoutCocone.mk (W := coprod.{v₁, u₁} B X) (coprod.map f (𝟙 X)) coprod.inl sorry))
      (PushoutCocone.inl (PushoutCocone.mk (W := coprod.{v₁, u₁} B X) (coprod.map f (𝟙 X)) coprod.inl sorry))
      (coprod.desc s.inr (coprod.inr ≫ s.inl))) =
  coprod.inl ≫ s.inl
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
A B : C
f : A ⟶ B
X : C
inst_1 : HasBinaryCoproduct.{v₁, u₁} A X
inst_2 : HasBinaryCoproduct.{v₁, u₁} B X
s : PushoutCocone (Y := coprod.{v₁, u₁} A X) coprod.inl f
refine_1 :
  CategoryStruct.comp (Y := coprod.{v₁, u₁} A X) coprod.inl
      (CategoryStruct.comp (Y :=
        Cocone.pt (F := span (Y := coprod.{v₁, u₁} A X) coprod.inl f)
          (PushoutCocone.mk (W := coprod.{v₁, u₁} B X) (coprod.map f (𝟙 X)) coprod.inl ⋯))
        (PushoutCocone.inl (PushoutCocone.mk (W := coprod.{v₁, u₁} B X) (coprod.map f (𝟙 X)) coprod.inl ⋯))
        (coprod.desc s.inr (coprod.inr ≫ s.inl))) =
    coprod.inl ≫ s.inl
⊢ CategoryStruct.comp (Y :=
      Cocone.pt (F := span (Y := coprod.{v₁, u₁} A X) coprod.inl f)
        (PushoutCocone.mk (W := coprod.{v₁, u₁} B X) (coprod.map f (𝟙 X)) coprod.inl ⋯))
      (PushoutCocone.inl (PushoutCocone.mk (W := coprod.{v₁, u₁} B X) (coprod.map f (𝟙 X)) coprod.inl ⋯))
      (coprod.desc s.inr (coprod.inr ≫ s.inl)) =
    s.inl
have refine_1₁ : CategoryStruct.comp (Y := coprod.{v₁, u₁} A X) coprod.inr
    (CategoryStruct.comp (Y :=
      Cocone.pt (F := span (Y := coprod.{v₁, u₁} A X) coprod.inl f)
        (PushoutCocone.mk (W := coprod.{v₁, u₁} B X) (coprod.map f (𝟙 X)) coprod.inl sorry))
      (PushoutCocone.inl (PushoutCocone.mk (W := coprod.{v₁, u₁} B X) (coprod.map f (𝟙 X)) coprod.inl sorry))
      (coprod.desc s.inr (coprod.inr ≫ s.inl))) =
  coprod.inr ≫ s.inl
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
A B : C
f : A ⟶ B
X : C
inst_1 : HasBinaryCoproduct.{v₁, u₁} A X
inst_2 : HasBinaryCoproduct.{v₁, u₁} B X
s : PushoutCocone (Y := coprod.{v₁, u₁} A X) coprod.inl f
m : coprod.{v₁, u₁} B X ⟶ s.pt
h₁ : coprod.map f (𝟙 X) ≫ m = s.inl
h₂ : coprod.inl ≫ m = s.inr
⊢ m = coprod.desc s.inr (coprod.inr ≫ s.inl)
have refine_3 : coprod.inl ≫ m = CategoryStruct.comp (Y := coprod.{v₁, u₁} B X) coprod.inl (coprod.desc s.inr (coprod.inr ≫ s.inl))
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
A B : C
f : A ⟶ B
X : C
inst_1 : HasBinaryCoproduct.{v₁, u₁} A X
inst_2 : HasBinaryCoproduct.{v₁, u₁} B X
s : PushoutCocone (Y := coprod.{v₁, u₁} A X) coprod.inl f
m : coprod.{v₁, u₁} B X ⟶ s.pt
h₁ : coprod.map f (𝟙 X) ≫ m = s.inl
h₂ : coprod.inl ≫ m = s.inr
refine_3 :
  coprod.inl ≫ m = CategoryStruct.comp (Y := coprod.{v₁, u₁} B X) coprod.inl (coprod.desc s.inr (coprod.inr ≫ s.inl))
⊢ m = coprod.desc s.inr (coprod.inr ≫ s.inl)
have refine_3₁ : coprod.inr ≫ m = CategoryStruct.comp (Y := coprod.{v₁, u₁} B X) coprod.inr (coprod.desc s.inr (coprod.inr ≫ s.inl))
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y : C
c : BinaryCofan.{v₁, u₁} X Y
hc : IsColimit c
I : C
hI : IsInitial.{v₁, u₁} I
s :
  PushoutCocone (Y := Functor.obj.{0, v₁, 0, u₁} (pair X Y) { as := WalkingPair.right : Discrete WalkingPair }) (Z :=
    Functor.obj.{0, v₁, 0, u₁} (pair X Y) { as := WalkingPair.left : Discrete WalkingPair })
    (hI.to (Functor.obj.{0, v₁, 0, u₁} (pair X Y) { as := WalkingPair.right : Discrete WalkingPair }))
    (hI.to (Functor.obj.{0, v₁, 0, u₁} (pair X Y) { as := WalkingPair.left : Discrete WalkingPair }))
m :
  Functor.obj.{0, v₁, 0, u₁} (Functor.obj (Functor.const (Discrete WalkingPair)) c.pt)
      { as := WalkingPair.right : Discrete WalkingPair } ⟶
    s.pt
h₁ : c.inr ≫ m = s.inl
h₂ : c.inl ≫ m = s.inr
⊢ m =
    (fun
          (s :
            PushoutCocone (Y :=
              Functor.obj.{0, v₁, 0, u₁} (pair X Y) { as := WalkingPair.right : Discrete WalkingPair }) (Z :=
              Functor.obj.{0, v₁, 0, u₁} (pair X Y) { as := WalkingPair.left : Discrete WalkingPair })
              (hI.to (Functor.obj.{0, v₁, 0, u₁} (pair X Y) { as := WalkingPair.right : Discrete WalkingPair }))
              (hI.to (Functor.obj.{0, v₁, 0, u₁} (pair X Y) { as := WalkingPair.left : Discrete WalkingPair }))) ↦
        BinaryCofan.IsColimit.desc hc s.inr s.inl)
      s
have h₃ : c.inl ≫ m =
  c.inl ≫
    (fun
          (s :
            PushoutCocone (Y :=
              Functor.obj.{0, v₁, 0, u₁} (pair X Y) { as := WalkingPair.right : Discrete WalkingPair }) (Z :=
              Functor.obj.{0, v₁, 0, u₁} (pair X Y) { as := WalkingPair.left : Discrete WalkingPair })
              (hI.to (Functor.obj.{0, v₁, 0, u₁} (pair X Y) { as := WalkingPair.right : Discrete WalkingPair }))
              (hI.to (Functor.obj.{0, v₁, 0, u₁} (pair X Y) { as := WalkingPair.left : Discrete WalkingPair }))) ↦
        BinaryCofan.IsColimit.desc hc s.inr s.inl)
      s
Tactic: apply BinaryCofan.IsColimit.hom_ext hc
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y : C
c : BinaryCofan.{v₁, u₁} X Y
hc : IsColimit c
I : C
hI : IsInitial.{v₁, u₁} I
s :
  PushoutCocone (Y := Functor.obj.{0, v₁, 0, u₁} (pair X Y) { as := WalkingPair.right : Discrete WalkingPair }) (Z :=
    Functor.obj.{0, v₁, 0, u₁} (pair X Y) { as := WalkingPair.left : Discrete WalkingPair })
    (hI.to (Functor.obj.{0, v₁, 0, u₁} (pair X Y) { as := WalkingPair.right : Discrete WalkingPair }))
    (hI.to (Functor.obj.{0, v₁, 0, u₁} (pair X Y) { as := WalkingPair.left : Discrete WalkingPair }))
m :
  Functor.obj.{0, v₁, 0, u₁} (Functor.obj (Functor.const (Discrete WalkingPair)) c.pt)
      { as := WalkingPair.right : Discrete WalkingPair } ⟶
    s.pt
h₁ : c.inr ≫ m = s.inl
h₂ : c.inl ≫ m = s.inr
h₃ :
  c.inl ≫ m =
    c.inl ≫
      (fun
            (s :
              PushoutCocone (Y :=
                Functor.obj.{0, v₁, 0, u₁} (pair X Y) { as := WalkingPair.right : Discrete WalkingPair }) (Z :=
                Functor.obj.{0, v₁, 0, u₁} (pair X Y) { as := WalkingPair.left : Discrete WalkingPair })
                (hI.to (Functor.obj.{0, v₁, 0, u₁} (pair X Y) { as := WalkingPair.right : Discrete WalkingPair }))
                (hI.to (Functor.obj.{0, v₁, 0, u₁} (pair X Y) { as := WalkingPair.left : Discrete WalkingPair }))) ↦
          BinaryCofan.IsColimit.desc hc s.inr s.inl)
        s
⊢ m =
    (fun
          (s :
            PushoutCocone (Y :=
              Functor.obj.{0, v₁, 0, u₁} (pair X Y) { as := WalkingPair.right : Discrete WalkingPair }) (Z :=
              Functor.obj.{0, v₁, 0, u₁} (pair X Y) { as := WalkingPair.left : Discrete WalkingPair })
              (hI.to (Functor.obj.{0, v₁, 0, u₁} (pair X Y) { as := WalkingPair.right : Discrete WalkingPair }))
              (hI.to (Functor.obj.{0, v₁, 0, u₁} (pair X Y) { as := WalkingPair.left : Discrete WalkingPair }))) ↦
        BinaryCofan.IsColimit.desc hc s.inr s.inl)
      s
have h₄ : c.inr ≫ m =
  c.inr ≫
    (fun
          (s :
            PushoutCocone (Y :=
              Functor.obj.{0, v₁, 0, u₁} (pair X Y) { as := WalkingPair.right : Discrete WalkingPair }) (Z :=
              Functor.obj.{0, v₁, 0, u₁} (pair X Y) { as := WalkingPair.left : Discrete WalkingPair })
              (hI.to (Functor.obj.{0, v₁, 0, u₁} (pair X Y) { as := WalkingPair.right : Discrete WalkingPair }))
              (hI.to (Functor.obj.{0, v₁, 0, u₁} (pair X Y) { as := WalkingPair.left : Discrete WalkingPair }))) ↦
        BinaryCofan.IsColimit.desc hc s.inr s.inl)
      s
Tactic: apply BinaryCofan.IsColimit.hom_ext hc
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y Z : C
f f' : X ⟶ Y
g g' : Y ⟶ Z
H : IsPullback f f g g'
⊢ IsLimit (Fork.ofι f ⋯)
have lift : (s : Fork g g') → s.pt ⟶ (Fork.ofι f sorry).pt
Tactic: fapply Fork.IsLimit.mk
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y Z : C
f f' : X ⟶ Y
g g' : Y ⟶ Z
H : IsPullback f f g g'
lift : (s : Fork g g') → s.pt ⟶ (Fork.ofι f ⋯).pt
⊢ IsLimit (Fork.ofι f ⋯)
have fac : ∀ (s : Fork g g'), H.isLimit.lift (PullbackCone.mk s.ι s.ι sorry) ≫ (Fork.ofι f sorry).ι = s.ι
Tactic: fapply Fork.IsLimit.mk
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y Z : C
f f' : X ⟶ Y
g g' : Y ⟶ Z
H : IsPullback f f g g'
lift : (s : Fork g g') → s.pt ⟶ (Fork.ofι f ⋯).pt
fac : ∀ (s : Fork g g'), H.isLimit.lift (PullbackCone.mk s.ι s.ι ⋯) ≫ (Fork.ofι f ⋯).ι = s.ι
⊢ IsLimit (Fork.ofι f ⋯)
have uniq : ∀ (s : Fork g g') (m : s.pt ⟶ (Fork.ofι f sorry).pt),
  m ≫ (Fork.ofι f sorry).ι = s.ι → m = H.isLimit.lift (PullbackCone.mk s.ι s.ι sorry)
Tactic: fapply Fork.IsLimit.mk
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y Z : C
f f' : X ⟶ Y
g g' : Y ⟶ Z
H : IsPullback f f g g'
s : Fork g g'
m : s.pt ⟶ (Fork.ofι f ⋯).pt
e : m ≫ (Fork.ofι f ⋯).ι = s.ι
⊢ m = H.isLimit.lift (PullbackCone.mk s.ι s.ι ⋯)
have uniq : m ≫ H.cone.fst = H.isLimit.lift (PullbackCone.mk s.ι s.ι sorry) ≫ H.cone.fst
Tactic: apply PullbackCone.IsLimit.hom_ext H.isLimit
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y Z : C
f f' : X ⟶ Y
g g' : Y ⟶ Z
H : IsPullback f f g g'
s : Fork g g'
m : s.pt ⟶ (Fork.ofι f ⋯).pt
e : m ≫ (Fork.ofι f ⋯).ι = s.ι
uniq : m ≫ H.cone.fst = H.isLimit.lift (PullbackCone.mk s.ι s.ι ⋯) ≫ H.cone.fst
⊢ m = H.isLimit.lift (PullbackCone.mk s.ι s.ι ⋯)
have uniq₁ : m ≫ H.cone.snd = H.isLimit.lift (PullbackCone.mk s.ι s.ι sorry) ≫ H.cone.snd
Tactic: apply PullbackCone.IsLimit.hom_ext H.isLimit
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y Z : C
f f' : X ⟶ Y
g g' : Y ⟶ Z
H : IsPullback f f g g'
s : Fork g g'
m : s.pt ⟶ (Fork.ofι f ⋯).pt
e : m ≫ (Fork.ofι f ⋯).ι = s.ι
⊢ m ≫ H.cone.fst = H.isLimit.lift (PullbackCone.mk s.ι s.ι ⋯) ≫ H.cone.fst
have uniq : s.ι = H.isLimit.lift (PullbackCone.mk s.ι s.ι sorry) ≫ H.cone.fst
Tactic: refine e.trans ?_
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y Z : C
f f' : X ⟶ Y
g g' : Y ⟶ Z
H : IsPullback f f g g'
s : Fork g g'
m : s.pt ⟶ (Fork.ofι f ⋯).pt
e : m ≫ (Fork.ofι f ⋯).ι = s.ι
⊢ m ≫ H.cone.snd = H.isLimit.lift (PullbackCone.mk s.ι s.ι ⋯) ≫ H.cone.snd
have uniq : s.ι = H.isLimit.lift (PullbackCone.mk s.ι s.ι sorry) ≫ H.cone.snd
Tactic: refine e.trans ?_
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y Z : C
f f' : X ⟶ Y
g g' : Y ⟶ Z
H : IsPullback f f g g'
s : Fork g g'
m : s.pt ⟶ (Fork.ofι f ⋯).pt
e : m ≫ (Fork.ofι f ⋯).ι = s.ι
⊢ s.ι = H.isLimit.lift (PullbackCone.mk s.ι s.ι ⋯) ≫ H.cone.fst
have uniq : H.isLimit.lift (PullbackCone.mk s.ι s.ι sorry) ≫ H.cone.fst = s.ι
Tactic: symm
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y Z : C
f f' : X ⟶ Y
g g' : Y ⟶ Z
H : IsPullback f f g g'
s : Fork g g'
m : s.pt ⟶ (Fork.ofι f ⋯).pt
e : m ≫ (Fork.ofι f ⋯).ι = s.ι
⊢ s.ι = H.isLimit.lift (PullbackCone.mk s.ι s.ι ⋯) ≫ H.cone.snd
have uniq : H.isLimit.lift (PullbackCone.mk s.ι s.ι sorry) ≫ H.cone.snd = s.ι
Tactic: symm
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y Z : C
f f' : X ⟶ Y
g g' : Y ⟶ Z
H : IsPushout f f' g g
⊢ IsColimit (Cofork.ofπ g ⋯)
have desc : (s : Cofork f f') → (Cofork.ofπ g sorry).pt ⟶ s.pt
Tactic: fapply Cofork.IsColimit.mk
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y Z : C
f f' : X ⟶ Y
g g' : Y ⟶ Z
H : IsPushout f f' g g
desc : (s : Cofork f f') → (Cofork.ofπ g ⋯).pt ⟶ s.pt
⊢ IsColimit (Cofork.ofπ g ⋯)
have fac : ∀ (s : Cofork f f'), (Cofork.ofπ g sorry).π ≫ H.isColimit.desc (PushoutCocone.mk s.π s.π sorry) = s.π
Tactic: fapply Cofork.IsColimit.mk
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y Z : C
f f' : X ⟶ Y
g g' : Y ⟶ Z
H : IsPushout f f' g g
desc : (s : Cofork f f') → (Cofork.ofπ g ⋯).pt ⟶ s.pt
fac : ∀ (s : Cofork f f'), (Cofork.ofπ g ⋯).π ≫ H.isColimit.desc (PushoutCocone.mk s.π s.π ⋯) = s.π
⊢ IsColimit (Cofork.ofπ g ⋯)
have uniq : ∀ (s : Cofork f f') (m : (Cofork.ofπ g sorry).pt ⟶ s.pt),
  (Cofork.ofπ g sorry).π ≫ m = s.π → m = H.isColimit.desc (PushoutCocone.mk s.π s.π sorry)
Tactic: fapply Cofork.IsColimit.mk
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y Z : C
f f' : X ⟶ Y
g g' : Y ⟶ Z
H : IsPushout f f' g g
s : Cofork f f'
m : (Cofork.ofπ g ⋯).pt ⟶ s.pt
e : (Cofork.ofπ g ⋯).π ≫ m = s.π
⊢ m = H.isColimit.desc (PushoutCocone.mk s.π s.π ⋯)
have uniq : H.cocone.inl ≫ m = H.cocone.inl ≫ H.isColimit.desc (PushoutCocone.mk s.π s.π sorry)
Tactic: apply PushoutCocone.IsColimit.hom_ext H.isColimit
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y Z : C
f f' : X ⟶ Y
g g' : Y ⟶ Z
H : IsPushout f f' g g
s : Cofork f f'
m : (Cofork.ofπ g ⋯).pt ⟶ s.pt
e : (Cofork.ofπ g ⋯).π ≫ m = s.π
uniq : H.cocone.inl ≫ m = H.cocone.inl ≫ H.isColimit.desc (PushoutCocone.mk s.π s.π ⋯)
⊢ m = H.isColimit.desc (PushoutCocone.mk s.π s.π ⋯)
have uniq₁ : H.cocone.inr ≫ m = H.cocone.inr ≫ H.isColimit.desc (PushoutCocone.mk s.π s.π sorry)
Tactic: apply PushoutCocone.IsColimit.hom_ext H.isColimit
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y Z : C
f f' : X ⟶ Y
g g' : Y ⟶ Z
H : IsPushout f f' g g
s : Cofork f f'
m : (Cofork.ofπ g ⋯).pt ⟶ s.pt
e : (Cofork.ofπ g ⋯).π ≫ m = s.π
⊢ H.cocone.inl ≫ m = H.cocone.inl ≫ H.isColimit.desc (PushoutCocone.mk s.π s.π ⋯)
have uniq : s.π = H.cocone.inl ≫ H.isColimit.desc (PushoutCocone.mk s.π s.π sorry)
Tactic: refine e.trans ?_
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y Z : C
f f' : X ⟶ Y
g g' : Y ⟶ Z
H : IsPushout f f' g g
s : Cofork f f'
m : (Cofork.ofπ g ⋯).pt ⟶ s.pt
e : (Cofork.ofπ g ⋯).π ≫ m = s.π
⊢ H.cocone.inr ≫ m = H.cocone.inr ≫ H.isColimit.desc (PushoutCocone.mk s.π s.π ⋯)
have uniq : s.π = H.cocone.inr ≫ H.isColimit.desc (PushoutCocone.mk s.π s.π sorry)
Tactic: refine e.trans ?_
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y Z : C
f f' : X ⟶ Y
g g' : Y ⟶ Z
H : IsPushout f f' g g
s : Cofork f f'
m : (Cofork.ofπ g ⋯).pt ⟶ s.pt
e : (Cofork.ofπ g ⋯).π ≫ m = s.π
⊢ s.π = H.cocone.inl ≫ H.isColimit.desc (PushoutCocone.mk s.π s.π ⋯)
have uniq : H.cocone.inl ≫ H.isColimit.desc (PushoutCocone.mk s.π s.π sorry) = s.π
Tactic: symm
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y Z : C
f f' : X ⟶ Y
g g' : Y ⟶ Z
H : IsPushout f f' g g
s : Cofork f f'
m : (Cofork.ofπ g ⋯).pt ⟶ s.pt
e : (Cofork.ofπ g ⋯).π ≫ m = s.π
⊢ s.π = H.cocone.inr ≫ H.isColimit.desc (PushoutCocone.mk s.π s.π ⋯)
have uniq : H.cocone.inr ≫ H.isColimit.desc (PushoutCocone.mk s.π s.π sorry) = s.π
Tactic: symm
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
W X Y Z : C
f : W ⟶ X
g : W ⟶ Y
h : X ⟶ Z
i : Y ⟶ Z
inst_2 : PreservesLimit (cospan h i) F
s : IsPullback f g h i
⊢ IsPullback (F.map f) (F.map g) (F.map h) (F.map i)
have refine_1 : ((Cone.postcompose (cospanCompIso F h i).hom).obj (F.mapCone s.cone)).pt ≅
  ((Cone.postcompose (cospanCompIso F h i).hom).obj (F.mapCone s.cone)).pt
Tactic: refine
    IsPullback.of_isLimit' (F.map_commSq s.toCommSq)
      (IsLimit.equivOfNatIsoOfIso (cospanCompIso F h i) _ _ (WalkingCospan.ext ?_ ?_ ?_)
        (isLimitOfPreserves F s.isLimit))
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
W X Y Z : C
f : W ⟶ X
g : W ⟶ Y
h : X ⟶ Z
i : Y ⟶ Z
inst_2 : PreservesLimit (cospan h i) F
s : IsPullback f g h i
refine_1 :
  ((Cone.postcompose (cospanCompIso F h i).hom).obj (F.mapCone s.cone)).pt ≅
    ((Cone.postcompose (cospanCompIso F h i).hom).obj (F.mapCone s.cone)).pt
⊢ IsPullback (F.map f) (F.map g) (F.map h) (F.map i)
have refine_2 : ((Cone.postcompose (cospanCompIso F h i).hom).obj (F.mapCone s.cone)).π.app WalkingCospan.left =
  Iso.hom (Iso.refl ((Cone.postcompose (cospanCompIso F h i).hom).obj (F.mapCone s.cone)).pt) ≫
    sorry.cone.π.app WalkingCospan.left
Tactic: refine
    IsPullback.of_isLimit' (F.map_commSq s.toCommSq)
      (IsLimit.equivOfNatIsoOfIso (cospanCompIso F h i) _ _ (WalkingCospan.ext ?_ ?_ ?_)
        (isLimitOfPreserves F s.isLimit))