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
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
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) ≫
      ⋯.cone.π.app WalkingCospan.left
⊢ IsPullback (F.map f) (F.map g) (F.map h) (F.map i)
have refine_3 : ((Cone.postcompose (cospanCompIso F h i).hom).obj (F.mapCone s.cone)).π.app WalkingCospan.right =
  Iso.hom (Iso.refl ((Cone.postcompose (cospanCompIso F h i).hom).obj (F.mapCone s.cone)).pt) ≫
    sorry.cone.π.app WalkingCospan.right
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 : PreservesColimit (span f g) F
s : IsPushout f g h i
⊢ IsPushout (F.map f) (F.map g) (F.map h) (F.map i)
have refine_1 : ((Cocone.precompose (spanCompIso F f g).inv).obj (F.mapCocone s.cocone)).pt ≅
  ((Cocone.precompose (spanCompIso F f g).inv).obj (F.mapCocone s.cocone)).pt
Tactic: refine
    IsPushout.of_isColimit' (F.map_commSq s.toCommSq)
      (IsColimit.equivOfNatIsoOfIso (spanCompIso F f g) _ _ (WalkingSpan.ext ?_ ?_ ?_)
        (isColimitOfPreserves F s.isColimit))
-- 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 : PreservesColimit (span f g) F
s : IsPushout f g h i
refine_1 :
  ((Cocone.precompose (spanCompIso F f g).inv).obj (F.mapCocone s.cocone)).pt ≅
    ((Cocone.precompose (spanCompIso F f g).inv).obj (F.mapCocone s.cocone)).pt
⊢ IsPushout (F.map f) (F.map g) (F.map h) (F.map i)
have refine_2 : ((Cocone.precompose (spanCompIso F f g).inv).obj (F.mapCocone s.cocone)).ι.app WalkingCospan.left ≫
    Iso.hom (Iso.refl ((Cocone.precompose (spanCompIso F f g).inv).obj (F.mapCocone s.cocone)).pt) =
  sorry.cocone.ι.app WalkingCospan.left
Tactic: refine
    IsPushout.of_isColimit' (F.map_commSq s.toCommSq)
      (IsColimit.equivOfNatIsoOfIso (spanCompIso F f g) _ _ (WalkingSpan.ext ?_ ?_ ?_)
        (isColimitOfPreserves F s.isColimit))
-- 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 : PreservesColimit (span f g) F
s : IsPushout f g h i
refine_1 :
  ((Cocone.precompose (spanCompIso F f g).inv).obj (F.mapCocone s.cocone)).pt ≅
    ((Cocone.precompose (spanCompIso F f g).inv).obj (F.mapCocone s.cocone)).pt
refine_2 :
  ((Cocone.precompose (spanCompIso F f g).inv).obj (F.mapCocone s.cocone)).ι.app WalkingCospan.left ≫
      Iso.hom (Iso.refl ((Cocone.precompose (spanCompIso F f g).inv).obj (F.mapCocone s.cocone)).pt) =
    ⋯.cocone.ι.app WalkingCospan.left
⊢ IsPushout (F.map f) (F.map g) (F.map h) (F.map i)
have refine_3 : ((Cocone.precompose (spanCompIso F f g).inv).obj (F.mapCocone s.cocone)).ι.app WalkingCospan.right ≫
    Iso.hom (Iso.refl ((Cocone.precompose (spanCompIso F f g).inv).obj (F.mapCocone s.cocone)).pt) =
  sorry.cocone.ι.app WalkingCospan.right
Tactic: refine
    IsPushout.of_isColimit' (F.map_commSq s.toCommSq)
      (IsColimit.equivOfNatIsoOfIso (spanCompIso F f g) _ _ (WalkingSpan.ext ?_ ?_ ?_)
        (isColimitOfPreserves F s.isColimit))
-- 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 : ReflectsLimit (cospan h i) F
e : f ≫ h = g ≫ i
H : IsPullback (F.map f) (F.map g) (F.map h) (F.map i)
⊢ IsPullback f g h i
have refine : IsLimit (F.mapCone (PullbackCone.mk f g sorry))
Tactic: refine ⟨⟨e⟩, ⟨isLimitOfReflects F <| ?_⟩⟩
-- 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 : ReflectsLimit (cospan h i) F
e : f ≫ h = g ≫ i
H : IsPullback (F.map f) (F.map g) (F.map h) (F.map i)
⊢ IsLimit (F.mapCone (PullbackCone.mk f g ⋯))
have refine_1 : ((Cone.postcompose (cospanCompIso F h i).hom).obj (F.mapCone (PullbackCone.mk f g sorry))).pt ≅ H.cone.pt
Tactic: refine
    (IsLimit.equivOfNatIsoOfIso (cospanCompIso F h i) _ _ (WalkingCospan.ext ?_ ?_ ?_)).symm
      H.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 : ReflectsLimit (cospan h i) F
e : f ≫ h = g ≫ i
H : IsPullback (F.map f) (F.map g) (F.map h) (F.map i)
refine_1 : ((Cone.postcompose (cospanCompIso F h i).hom).obj (F.mapCone (PullbackCone.mk f g ⋯))).pt ≅ H.cone.pt
⊢ IsLimit (F.mapCone (PullbackCone.mk f g ⋯))
have refine_2 : ((Cone.postcompose (cospanCompIso F h i).hom).obj (F.mapCone (PullbackCone.mk f g sorry))).π.app WalkingCospan.left =
  Iso.hom (Iso.refl ((Cone.postcompose (cospanCompIso F h i).hom).obj (F.mapCone (PullbackCone.mk f g sorry))).pt) ≫
    H.cone.π.app WalkingCospan.left
Tactic: refine
    (IsLimit.equivOfNatIsoOfIso (cospanCompIso F h i) _ _ (WalkingCospan.ext ?_ ?_ ?_)).symm
      H.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 : ReflectsLimit (cospan h i) F
e : f ≫ h = g ≫ i
H : IsPullback (F.map f) (F.map g) (F.map h) (F.map i)
refine_1 : ((Cone.postcompose (cospanCompIso F h i).hom).obj (F.mapCone (PullbackCone.mk f g ⋯))).pt ≅ H.cone.pt
refine_2 :
  ((Cone.postcompose (cospanCompIso F h i).hom).obj (F.mapCone (PullbackCone.mk f g ⋯))).π.app WalkingCospan.left =
    Iso.hom (Iso.refl ((Cone.postcompose (cospanCompIso F h i).hom).obj (F.mapCone (PullbackCone.mk f g ⋯))).pt) ≫
      H.cone.π.app WalkingCospan.left
⊢ IsLimit (F.mapCone (PullbackCone.mk f g ⋯))
have refine_3 : ((Cone.postcompose (cospanCompIso F h i).hom).obj (F.mapCone (PullbackCone.mk f g sorry))).π.app WalkingCospan.right =
  Iso.hom (Iso.refl ((Cone.postcompose (cospanCompIso F h i).hom).obj (F.mapCone (PullbackCone.mk f g sorry))).pt) ≫
    H.cone.π.app WalkingCospan.right
Tactic: refine
    (IsLimit.equivOfNatIsoOfIso (cospanCompIso F h i) _ _ (WalkingCospan.ext ?_ ?_ ?_)).symm
      H.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 : ReflectsColimit (span f g) F
e : f ≫ h = g ≫ i
H : IsPushout (F.map f) (F.map g) (F.map h) (F.map i)
⊢ IsPushout f g h i
have refine : IsColimit (F.mapCocone (PushoutCocone.mk h i sorry))
Tactic: refine ⟨⟨e⟩, ⟨isColimitOfReflects F <| ?_⟩⟩
-- 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 : ReflectsColimit (span f g) F
e : f ≫ h = g ≫ i
H : IsPushout (F.map f) (F.map g) (F.map h) (F.map i)
⊢ IsColimit (F.mapCocone (PushoutCocone.mk h i ⋯))
have refine_1 : ((Cocone.precompose (spanCompIso F f g).inv).obj (F.mapCocone (PushoutCocone.mk h i sorry))).pt ≅ H.cocone.pt
Tactic: refine
    (IsColimit.equivOfNatIsoOfIso (spanCompIso F f g) _ _ (WalkingSpan.ext ?_ ?_ ?_)).symm
      H.isColimit
-- 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 : ReflectsColimit (span f g) F
e : f ≫ h = g ≫ i
H : IsPushout (F.map f) (F.map g) (F.map h) (F.map i)
refine_1 : ((Cocone.precompose (spanCompIso F f g).inv).obj (F.mapCocone (PushoutCocone.mk h i ⋯))).pt ≅ H.cocone.pt
⊢ IsColimit (F.mapCocone (PushoutCocone.mk h i ⋯))
have refine_2 : ((Cocone.precompose (spanCompIso F f g).inv).obj (F.mapCocone (PushoutCocone.mk h i sorry))).ι.app WalkingCospan.left ≫
    Iso.hom (Iso.refl ((Cocone.precompose (spanCompIso F f g).inv).obj (F.mapCocone (PushoutCocone.mk h i sorry))).pt) =
  H.cocone.ι.app WalkingCospan.left
Tactic: refine
    (IsColimit.equivOfNatIsoOfIso (spanCompIso F f g) _ _ (WalkingSpan.ext ?_ ?_ ?_)).symm
      H.isColimit
-- 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 : ReflectsColimit (span f g) F
e : f ≫ h = g ≫ i
H : IsPushout (F.map f) (F.map g) (F.map h) (F.map i)
refine_1 : ((Cocone.precompose (spanCompIso F f g).inv).obj (F.mapCocone (PushoutCocone.mk h i ⋯))).pt ≅ H.cocone.pt
refine_2 :
  ((Cocone.precompose (spanCompIso F f g).inv).obj (F.mapCocone (PushoutCocone.mk h i ⋯))).ι.app WalkingCospan.left ≫
      Iso.hom (Iso.refl ((Cocone.precompose (spanCompIso F f g).inv).obj (F.mapCocone (PushoutCocone.mk h i ⋯))).pt) =
    H.cocone.ι.app WalkingCospan.left
⊢ IsColimit (F.mapCocone (PushoutCocone.mk h i ⋯))
have refine_3 : ((Cocone.precompose (spanCompIso F f g).inv).obj (F.mapCocone (PushoutCocone.mk h i sorry))).ι.app WalkingCospan.right ≫
    Iso.hom (Iso.refl ((Cocone.precompose (spanCompIso F f g).inv).obj (F.mapCocone (PushoutCocone.mk h i sorry))).pt) =
  H.cocone.ι.app WalkingCospan.right
Tactic: refine
    (IsColimit.equivOfNatIsoOfIso (spanCompIso F f g) _ _ (WalkingSpan.ext ?_ ?_ ?_)).symm
      H.isColimit
-- 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
P X Y Z : C
fst : P ⟶ X
snd : P ⟶ Y
f : X ⟶ Z
g : Y ⟶ Z
h : IsPullback fst snd f g
⊢ PreservesLimit (cospan f g) F ↔ IsPullback (F.map fst) (F.map snd) (F.map f) (F.map g)
have refine : ∀ (hF : IsPullback (F.map fst) (F.map snd) (F.map f) (F.map g)), PreservesLimit (cospan f g) F
Tactic: refine ⟨fun _ ↦ h.map _, fun hF ↦ ?_⟩
-- 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
P X Y Z : C
fst : P ⟶ X
snd : P ⟶ Y
f : X ⟶ Z
g : Y ⟶ Z
h : IsPullback fst snd f g
hF : IsPullback (F.map fst) (F.map snd) (F.map f) (F.map g)
⊢ PreservesLimit (cospan f g) F
have apply : IsLimit (F.mapCone h.cone)
Tactic: apply preservesLimit_of_preserves_limit_cone h.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
P X Y Z : C
inl : X ⟶ P
inr : Y ⟶ P
f : Z ⟶ X
g : Z ⟶ Y
h : IsPushout f g inl inr
⊢ PreservesColimit (span f g) F ↔ IsPushout (F.map f) (F.map g) (F.map inl) (F.map inr)
have refine : ∀ (hF : IsPushout (F.map f) (F.map g) (F.map inl) (F.map inr)), PreservesColimit (span f g) F
Tactic: refine ⟨fun _ ↦ h.map _, fun hF ↦ ?_⟩
-- 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
P X Y Z : C
inl : X ⟶ P
inr : Y ⟶ P
f : Z ⟶ X
g : Z ⟶ Y
h : IsPushout f g inl inr
hF : IsPushout (F.map f) (F.map g) (F.map inl) (F.map inr)
⊢ PreservesColimit (span f g) F
have apply : IsColimit (F.mapCocone h.cocone)
Tactic: apply preservesColimit_of_preserves_colimit_cocone h.isColimit
-- 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
H :
  ∀ ⦃X Y Z : C⦄ (f : X ⟶ Z) (g : Y ⟶ Z) [HasPullback f g],
    ∃ (P : C) (fst : P ⟶ X) (snd : P ⟶ Y),
      IsPullback fst snd f g ∧ IsPullback (F.map fst) (F.map snd) (F.map f) (F.map g)
⊢ PreservesLimitsOfShape WalkingCospan F
have suffices : ∀ {X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z), PreservesLimit (cospan f g) F
Tactic: suffices h : ∀ {X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z), PreservesLimit (cospan f g) F from
    ⟨fun {K} ↦ preservesLimit_of_iso_diagram _ (Limits.diagramIsoCospan K).symm⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic (hypothesis)
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
H :
  ∀ ⦃X Y Z : C⦄ (f : X ⟶ Z) (g : Y ⟶ Z) [HasPullback f g],
    ∃ (P : C) (fst : P ⟶ X) (snd : P ⟶ Y),
      IsPullback fst snd f g ∧ IsPullback (F.map fst) (F.map snd) (F.map f) (F.map g)
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
⊢ PreservesLimit (cospan f g) F
have h : HasLimit (cospan f g)
Tactic: refine .mk' fun h ↦ ?_
-- 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
H :
  ∀ ⦃X Y Z : C⦄ (f : X ⟶ Z) (g : Y ⟶ Z) [HasPullback f g],
    ∃ (P : C) (fst : P ⟶ X) (snd : P ⟶ Y),
      IsPullback fst snd f g ∧ IsPullback (F.map fst) (F.map snd) (F.map f) (F.map g)
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
h : HasLimit (cospan f g)
⊢ PreservesLimit (cospan f g) F
have obtain : ∀ (P : C) (fst : P ⟶ X) (snd : P ⟶ Y) (h : IsPullback fst snd f g)
  (h' : IsPullback (F.map fst) (F.map snd) (F.map f) (F.map g)), PreservesLimit (cospan f g) F
Tactic: obtain ⟨P, fst, snd, h, h'⟩ := H f g
-- 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
H :
  ∀ ⦃X Y Z : C⦄ (f : Z ⟶ X) (g : Z ⟶ Y) [HasPushout f g],
    ∃ (P : C) (inl : X ⟶ P) (inr : Y ⟶ P), IsPushout f g inl inr ∧ IsPushout (F.map f) (F.map g) (F.map inl) (F.map inr)
⊢ PreservesColimitsOfShape WalkingSpan F
have suffices : ∀ {X Y Z : C} (f : Z ⟶ X) (g : Z ⟶ Y), PreservesColimit (span f g) F
Tactic: suffices h : ∀ {X Y Z : C} (f : Z ⟶ X) (g : Z ⟶ Y), PreservesColimit (span f g) F from
    ⟨fun {K} ↦ preservesColimit_of_iso_diagram _ (diagramIsoSpan K).symm⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic (hypothesis)
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
H :
  ∀ ⦃X Y Z : C⦄ (f : Z ⟶ X) (g : Z ⟶ Y) [HasPushout f g],
    ∃ (P : C) (inl : X ⟶ P) (inr : Y ⟶ P), IsPushout f g inl inr ∧ IsPushout (F.map f) (F.map g) (F.map inl) (F.map inr)
X Y Z : C
f : Z ⟶ X
g : Z ⟶ Y
⊢ PreservesColimit (span f g) F
have h : HasColimit (span f g)
Tactic: refine .mk' fun h ↦ ?_
-- 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
H :
  ∀ ⦃X Y Z : C⦄ (f : Z ⟶ X) (g : Z ⟶ Y) [HasPushout f g],
    ∃ (P : C) (inl : X ⟶ P) (inr : Y ⟶ P), IsPushout f g inl inr ∧ IsPushout (F.map f) (F.map g) (F.map inl) (F.map inr)
X Y Z : C
f : Z ⟶ X
g : Z ⟶ Y
h : HasColimit (span f g)
⊢ PreservesColimit (span f g) F
have obtain : ∀ (P : C) (fst : X ⟶ P) (snd : Y ⟶ P) (h : IsPushout f g fst snd)
  (h' : IsPushout (F.map f) (F.map g) (F.map fst) (F.map snd)), PreservesColimit (span f g) F
Tactic: obtain ⟨P, fst, snd, h, h'⟩ := H f g
-- 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₁ F₂ F₃ F₄ : Functor.{v₁, v₂, u₁, u₂} C D
f₁ : F₁ ⟶ F₂
f₂ : F₁ ⟶ F₃
f₃ : F₂ ⟶ F₄
f₄ : F₃ ⟶ F₄
h : ∀ (X : C), IsPullback (f₁.app X) (f₂.app X) (f₃.app X) (f₄.app X)
⊢ f₁ ≫ f₃ = f₂ ≫ f₄
have w : ∀ (X : C), (f₁ ≫ f₃).app X = (f₂ ≫ f₄).app X
Tactic: ext X
-- 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₁ F₂ F₃ F₄ : Functor.{v₁, v₂, u₁, u₂} C D
f₁ : F₁ ⟶ F₂
f₂ : F₁ ⟶ F₃
f₃ : F₂ ⟶ F₄
f₄ : F₃ ⟶ F₄
h : ∀ (X : C), IsPushout (f₁.app X) (f₂.app X) (f₃.app X) (f₄.app X)
⊢ f₁ ≫ f₃ = f₂ ≫ f₄
have w : ∀ (X : C), (f₁ ≫ f₃).app X = (f₂ ≫ f₄).app X
Tactic: ext X
-- 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 : X ⟶ Z
g : Y ⟶ Z
inst_1 : HasPullbacksAlong g
P : C
p : P ⟶ X
q : P ⟶ Y
⊢ IsPullback p q f g ↔
    ∃ (e : Over.mk p ≅ Over.mk (Y := pullback f g) (pullback.fst f g)), q = Over.Hom.left e.hom ≫ pullback.snd f g
have mp : IsPullback p q f g →
  ∃ (e : Over.mk p ≅ Over.mk (Y := pullback f g) (pullback.fst f g)), q = Over.Hom.left e.hom ≫ pullback.snd f g
Tactic: constructor
-- 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 : X ⟶ Z
g : Y ⟶ Z
inst_1 : HasPullbacksAlong g
P : C
p : P ⟶ X
q : P ⟶ Y
mp :
  IsPullback p q f g →
    ∃ (e : Over.mk p ≅ Over.mk (Y := pullback f g) (pullback.fst f g)), q = Over.Hom.left e.hom ≫ pullback.snd f g
⊢ IsPullback p q f g ↔
    ∃ (e : Over.mk p ≅ Over.mk (Y := pullback f g) (pullback.fst f g)), q = Over.Hom.left e.hom ≫ pullback.snd f g
have mpr : (∃ (e : Over.mk p ≅ Over.mk (Y := pullback f g) (pullback.fst f g)), q = Over.Hom.left e.hom ≫ pullback.snd f g) →
  IsPullback p q f g
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.BicartesianSq (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : HasZeroObject.{v₁, u₁} C
inst_2 : HasZeroMorphisms.{v₁, u₁} C
X Y : C
inst_3 : HasBinaryProduct.{v₁, u₁} X Y
⊢ IsPullback.{v₁, u₁} (C := C) (P := Limits.prod.{v₁, u₁} X Y) (Z := 0) prod.fst prod.snd 0 0
have h : X = Functor.obj.{0, v₁, 0, u₁} (pair X Y) { as := WalkingPair.left : Discrete WalkingPair } →
  Eq.{v₁ + 1} (α := X ⟶ 0) 0
    (IsTerminal.from HasZeroObject.zeroIsTerminal
      (Functor.obj.{0, v₁, 0, u₁} (pair X Y) { as := WalkingPair.left : Discrete WalkingPair }))
Tactic: convert! @of_is_product _ _ X Y 0 _ (limit.isLimit _) HasZeroObject.zeroIsTerminal
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.BicartesianSq (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : HasZeroObject.{v₁, u₁} C
inst_2 : HasZeroMorphisms.{v₁, u₁} C
X Y : C
inst_3 : HasBinaryProduct.{v₁, u₁} X Y
h :
  X = Functor.obj.{0, v₁, 0, u₁} (pair X Y) { as := WalkingPair.left : Discrete WalkingPair } →
    Eq.{v₁ + 1} (α := X ⟶ 0) 0
      (IsTerminal.from HasZeroObject.zeroIsTerminal
        (Functor.obj.{0, v₁, 0, u₁} (pair X Y) { as := WalkingPair.left : Discrete WalkingPair }))
⊢ IsPullback.{v₁, u₁} (C := C) (P := Limits.prod.{v₁, u₁} X Y) (Z := 0) prod.fst prod.snd 0 0
have h₁ : Y = Functor.obj.{0, v₁, 0, u₁} (pair X Y) { as := WalkingPair.right : Discrete WalkingPair } →
  Eq.{v₁ + 1} (α := Y ⟶ 0) 0
    (IsTerminal.from HasZeroObject.zeroIsTerminal
      (Functor.obj.{0, v₁, 0, u₁} (pair X Y) { as := WalkingPair.right : Discrete WalkingPair }))
Tactic: convert! @of_is_product _ _ X Y 0 _ (limit.isLimit _) HasZeroObject.zeroIsTerminal
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.BicartesianSq (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : HasZeroObject.{v₁, u₁} C
inst_2 : HasZeroMorphisms.{v₁, u₁} C
X Y : C
b : BinaryBicone.{v₁, u₁} X Y
h : b.IsBilimit
⊢ IsPullback (Z := 0) b.fst b.snd 0 0
have h₁ : Eq.{v₁ + 1} (α := X ⟶ 0) 0 (IsTerminal.from HasZeroObject.zeroIsTerminal X)
Tactic: convert! IsPullback.of_is_product' h.isLimit HasZeroObject.zeroIsTerminal
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.BicartesianSq (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : HasZeroObject.{v₁, u₁} C
inst_2 : HasZeroMorphisms.{v₁, u₁} C
X Y : C
b : BinaryBicone.{v₁, u₁} X Y
h : b.IsBilimit
h₁ : Eq.{v₁ + 1} (α := X ⟶ 0) 0 (IsTerminal.from HasZeroObject.zeroIsTerminal X)
⊢ IsPullback (Z := 0) b.fst b.snd 0 0
have h₂ : Eq.{v₁ + 1} (α := Y ⟶ 0) 0 (IsTerminal.from HasZeroObject.zeroIsTerminal Y)
Tactic: convert! IsPullback.of_is_product' h.isLimit HasZeroObject.zeroIsTerminal
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.BicartesianSq (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : HasZeroObject.{v₁, u₁} C
inst_2 : HasZeroMorphisms.{v₁, u₁} C
X Y : C
b : BinaryBicone.{v₁, u₁} X Y
h : b.IsBilimit
⊢ IsPullback (Y := 0) b.inl 0 b.snd 0
have refine : IsPullback (Y := 0) (Z := 0) (b.inl ≫ b.fst) 0 0 (CategoryStruct.comp (Y := Y) 0 0)
Tactic: refine of_right ?_ (by simp) (of_isBilimit h)
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.BicartesianSq (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : HasZeroObject.{v₁, u₁} C
inst_2 : HasZeroMorphisms.{v₁, u₁} C
X Y : C
b : BinaryBicone.{v₁, u₁} X Y
h : b.IsBilimit
⊢ IsPullback (Y := 0) b.inr 0 b.fst 0
have h₁ : IsPullback (X := 0) 0 b.inr 0 b.fst
Tactic: apply flip
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.BicartesianSq (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : HasZeroObject.{v₁, u₁} C
inst_2 : HasZeroMorphisms.{v₁, u₁} C
X Y : C
b : BinaryBicone.{v₁, u₁} X Y
h : b.IsBilimit
⊢ IsPullback (X := 0) 0 b.inr 0 b.fst
have h₁ : IsPullback (X := 0) (Z := 0) 0 (b.inr ≫ b.snd) (CategoryStruct.comp (Y := X) 0 0) 0
Tactic: refine of_bot ?_ (by simp) (of_isBilimit h)
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.BicartesianSq (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : HasZeroObject.{v₁, u₁} C
inst_2 : HasZeroMorphisms.{v₁, u₁} C
X Y : C
b : BinaryBicone.{v₁, u₁} X Y
h : b.IsBilimit
⊢ IsPullback (P := 0) 0 0 b.inl b.inr
have refine : IsPullback (P := 0) (X := 0) (CategoryStruct.comp (Y := X) 0 0) 0 0 (b.inr ≫ b.snd)
Tactic: refine IsPullback.of_right ?_ (by simp) (IsPullback.inl_snd' h).flip
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.BicartesianSq (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : HasZeroObject.{v₁, u₁} C
inst_2 : HasZeroMorphisms.{v₁, u₁} C
X Y : C
inst_3 : HasBinaryCoproduct.{v₁, u₁} X Y
⊢ IsPushout.{v₁, u₁} (C := C) (Z := 0) (X := X) (Y := Y) (P := coprod.{v₁, u₁} X Y) 0 0 coprod.inl coprod.inr
have h : X = Functor.obj.{0, v₁, 0, u₁} (pair X Y) { as := WalkingPair.left : Discrete WalkingPair } →
  Eq.{v₁ + 1} (α := 0 ⟶ X) 0
    (IsInitial.to HasZeroObject.zeroIsInitial
      (Functor.obj.{0, v₁, 0, u₁} (pair X Y) { as := WalkingPair.left : Discrete WalkingPair }))
Tactic: convert! @of_is_coproduct _ _ 0 X Y _ (colimit.isColimit _) HasZeroObject.zeroIsInitial