awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic
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
⊢ HasLimit (cospan f g)

Tactic:
refine .mk' fun h ↦ ?_
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic
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)
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
⊢ PreservesLimit (cospan f g) F

Tactic:
obtain ⟨P, fst, snd, h, h'⟩ := H f g
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic
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_1 : HasLimit (cospan f g)
P : C
fst : P ⟶ X
snd : P ⟶ Y
h : IsPullback fst snd f g
h' rwa rwa₁ rwa₂ rwa₃ : IsPullback (F.map fst) (F.map snd) (F.map f) (F.map g)
⊢ PreservesLimit (cospan f g) F

Tactic:
rwa [h.preservesLimit_cospan_iff]

Premises used: CategoryTheory.IsPullback.preservesLimit_cospan_iff
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic
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)
suffices : ∀ {X Y Z : C} (f : Z ⟶ X) (g : Z ⟶ Y), PreservesColimit (span f g) F
⊢ PreservesColimitsOfShape WalkingSpan 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⟩
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic
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

Tactic:
.mk' fun h ↦ ?_

Premises used: CategoryTheory.Limits.PreservesColimit.mk'
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic
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
⊢ HasColimit (span f g)

Tactic:
refine .mk' fun h ↦ ?_
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic
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)
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
⊢ PreservesColimit (span f g) F

Tactic:
obtain ⟨P, fst, snd, h, h'⟩ := H f g
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic
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_1 : HasColimit (span f g)
P : C
fst : X ⟶ P
snd : Y ⟶ P
h : IsPushout f g fst snd
h' rwa rwa₁ rwa₂ rwa₃ : IsPushout (F.map f) (F.map g) (F.map fst) (F.map snd)
⊢ PreservesColimit (span f g) F

Tactic:
rwa [h.preservesColimit_span_iff]

Premises used: CategoryTheory.IsPushout.preservesColimit_span_iff
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
inst_2 : HasPullbacks.{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 : IsPullback f₁ f₂ f₃ f₄
X : C
⊢ IsPullback (f₁.app X) (f₂.app X) (f₃.app X) (f₄.app X)

Tactic:
h.map ((evaluation _ _).obj X)

Premises used: CategoryTheory.evaluation, CategoryTheory.IsPullback.map, CategoryTheory.Functor.obj
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic
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)
w : ∀ (X : C), (f₁ ≫ f₃).app X = (f₂ ≫ f₄).app X
⊢ f₁ ≫ f₃ = f₂ ≫ f₄

Tactic:
ext X
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic
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)
X : C
⊢ (f₁ ≫ f₃).app X = (f₂ ≫ f₄).app X

Tactic:
simpa using (h X).w

Premises used: CategoryTheory.IsPullback.toCommSq, CategoryTheory.CommSq.w
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
inst_2 : HasPullbacks.{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₄
⊢ IsPullback f₁ f₂ f₃ f₄ ↔ ∀ (X : C), IsPullback (f₁.app X) (f₂.app X) (f₃.app X) (f₄.app X)

Tactic:
⟨.app, .of_forall_isPullback_app⟩

Premises used: CategoryTheory.IsPullback.app, CategoryTheory.IsPullback.of_forall_isPullback_app, Iff.intro
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
inst_2 : HasPushouts.{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 : IsPushout f₁ f₂ f₃ f₄
X : C
⊢ IsPushout (f₁.app X) (f₂.app X) (f₃.app X) (f₄.app X)

Tactic:
h.map ((evaluation _ _).obj X)

Premises used: CategoryTheory.IsPushout.map, CategoryTheory.evaluation, CategoryTheory.Functor.obj
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic
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)
w : ∀ (X : C), (f₁ ≫ f₃).app X = (f₂ ≫ f₄).app X
⊢ f₁ ≫ f₃ = f₂ ≫ f₄

Tactic:
ext X
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic
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)
X : C
⊢ (f₁ ≫ f₃).app X = (f₂ ≫ f₄).app X

Tactic:
simpa using (h X).w

Premises used: CategoryTheory.IsPushout.toCommSq, CategoryTheory.CommSq.w
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
inst_2 : HasPushouts.{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₄
⊢ IsPushout f₁ f₂ f₃ f₄ ↔ ∀ (X : C), IsPushout (f₁.app X) (f₂.app X) (f₃.app X) (f₄.app X)

Tactic:
⟨.app, .of_forall_isPushout_app⟩

Premises used: CategoryTheory.IsPushout.app, Iff.intro, CategoryTheory.IsPushout.of_forall_isPushout_app
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic
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
fst : P ⟶ X
snd : P ⟶ Y
h : IsPullback fst snd f g
⊢ Iso.hom (isoIsPullback X Y h ⋯) ≫ (Over.mk (Y := pullback f g) (pullback.fst f g)).hom = (Over.mk fst).hom

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic
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
fst : P ⟶ X
snd : P ⟶ Y
h : IsPullback fst snd f g
⊢ CategoryStruct.comp (Y := pullback f g) (Over.Hom.left (Iso.hom h.isoOverPullback)) (pullback.snd f g) = snd

Tactic:
h.isoIsPullback_hom_snd _ _ (IsPullback.of_hasPullback f g)

Premises used: CategoryTheory.Limits.limit, CategoryTheory.IsPullback.of_hasPullback, CategoryTheory.IsPullback.isoIsPullback_hom_snd
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic
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
e : Over.mk p ≅ Over.mk (Y := pullback f g) (pullback.fst f g)
⊢ CategoryStruct.comp (Y := pullback f g) (Iso.hom (Functor.mapIso (Over.forget X) e)) (pullback.fst f g) =
    p ≫ Iso.hom (Iso.refl X)

Tactic:
simpa using Over.w e.hom

Premises used: CategoryTheory.Over.w, CategoryTheory.Iso.hom
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic
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
e : Over.mk p ≅ Over.mk (Y := pullback f g) (pullback.fst f g)
⊢ CategoryStruct.comp (Y := pullback f g) (Iso.hom (Functor.mapIso (Over.forget X) e)) (pullback.snd f g) =
    (Over.Hom.left e.hom ≫ pullback.snd f g) ≫ Iso.hom (Iso.refl Y)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic
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
e : Over.mk p ≅ Over.mk (Y := pullback f g) (pullback.fst f g)
⊢ Iso.hom (Iso.refl X) ≫ f = f ≫ Iso.hom (Iso.refl Z)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic
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
e : Over.mk p ≅ Over.mk (Y := pullback f g) (pullback.fst f g)
⊢ Iso.hom (Iso.refl Y) ≫ g = g ≫ Iso.hom (Iso.refl Z)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic
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
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
⊢ 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
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic
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
h : IsPullback p q f g
⊢ q =
    CategoryStruct.comp (Y := (Over.mk (Y := pullback f g) (pullback.fst f g)).left)
      (Over.Hom.left (Iso.hom h.isoOverPullback)) (pullback.snd f g)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic
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
h : 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:
exact ⟨h.isoOverPullback, by simp⟩
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic
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
e : Over.mk p ≅ Over.mk (Y := pullback f g) (pullback.fst f g)
⊢ IsPullback p (Over.Hom.left e.hom ≫ pullback.snd f g) f g

Tactic:
of_over_iso e

Premises used: CategoryTheory.IsPullback.of_over_iso
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic
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
e : Over.mk p ≅ Over.mk (Y := pullback f g) (pullback.fst f g)
⊢ IsPullback p (Over.Hom.left e.hom ≫ pullback.snd f g) f g

Tactic:
exact of_over_iso e

Premises used: CategoryTheory.IsPullback.of_over_iso
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.BicartesianSq
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 (P :=
    Functor.obj.{0, v₁, 0, u₁}
      (Functor.obj (Functor.const (Discrete WalkingPair))
        (Cone.pt.{0, v₁, 0, u₁} (F := pair X Y) (limit.cone (pair X Y))))
      { as := WalkingPair.left : Discrete WalkingPair })
    (Z := 0) (BinaryFan.fst (limit.cone (pair X Y))) (BinaryFan.snd (limit.cone (pair X Y)))
    (IsTerminal.from HasZeroObject.zeroIsTerminal
      (Functor.obj.{0, v₁, 0, u₁} (pair X Y) { as := WalkingPair.left : Discrete WalkingPair }))
    (IsTerminal.from HasZeroObject.zeroIsTerminal
      (Functor.obj.{0, v₁, 0, u₁} (pair X Y) { as := WalkingPair.right : Discrete WalkingPair }))

Tactic:
@of_is_product _ _ X Y 0 _ (limit.isLimit _) HasZeroObject.zeroIsTerminal

Premises used: CategoryTheory.Limits.HasZeroObject.zeroIsTerminal, CategoryTheory.Limits.limit.isLimit, CategoryTheory.IsPullback.of_is_product
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.BicartesianSq
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 }))
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 }))
⊢ IsPullback.{v₁, u₁} (C := C) (P := Limits.prod.{v₁, u₁} X Y) (Z := 0) prod.fst prod.snd 0 0

Tactic:
convert! @of_is_product _ _ X Y 0 _ (limit.isLimit _) HasZeroObject.zeroIsTerminal

Premises used: CategoryTheory.Limits.HasZeroObject.zeroIsTerminal, CategoryTheory.Limits.limit.isLimit, CategoryTheory.IsPullback.of_is_product
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.BicartesianSq
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
e_4 : 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:
subsingleton
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.BicartesianSq
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
e_5 : 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:
subsingleton
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.BicartesianSq
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : HasZeroObject.{v₁, u₁} C
inst_2 : HasZeroMorphisms.{v₁, u₁} C
X : C
⊢ Eq.{v₁ + 1} (α := 0 ⟶ X) (0 ≫ 𝟙 X) (CategoryStruct.comp (Y := 0) 0 0)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.BicartesianSq
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : HasZeroObject.{v₁, u₁} C
inst_2 : HasZeroMorphisms.{v₁, u₁} C
X : C
s : Cone.{0, v₁, 0, u₁} (cospan (Y := 0) (𝟙 X) 0)
⊢ 0 ≫ PullbackCone.fst s = 𝟙 s.pt ≫ PullbackCone.fst s

Tactic:
simpa using (PullbackCone.condition s).symm

Premises used: CategoryTheory.Limits.PullbackCone.condition, Eq.symm
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.BicartesianSq
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : HasZeroObject.{v₁, u₁} C
inst_2 : HasZeroMorphisms.{v₁, u₁} C
X : C
s : Cone.{0, v₁, 0, u₁} (cospan (Y := 0) (𝟙 X) 0)
⊢ ∀ (j : WalkingCospan),
    CategoryStruct.comp (Y := Cone.pt.{0, v₁, 0, u₁} (F := cospan (Y := 0) (𝟙 X) 0) (PullbackCone.mk (W := 0) 0 0 ⋯))
        (0 : s.pt ⟶ Cone.pt.{0, v₁, 0, u₁} (F := cospan (Y := 0) (𝟙 X) 0) (PullbackCone.mk (W := 0) 0 0 ⋯))
        (NatTrans.app (Cone.π (PullbackCone.mk (W := 0) 0 0 ⋯)) j :
          Functor.obj.{0, v₁, 0, u₁}
              (Functor.obj (Functor.const WalkingCospan)
                (Cone.pt.{0, v₁, 0, u₁} (F := cospan (Y := 0) (𝟙 X) 0) (PullbackCone.mk (W := 0) 0 0 ⋯)))
              j ⟶
            Functor.obj.{0, v₁, 0, u₁} (cospan (Y := 0) (𝟙 X) 0) j) =
      s.π.app j

Tactic:
simpa [eq_iff_true_of_subsingleton] using
              @PullbackCone.equalizer_ext _ _ _ _ _ _ _ s _ 0 (𝟙 _)
                (by simpa using (PullbackCone.condition s).symm)

Premises used: CategoryTheory.Limits.PullbackCone.equalizer_ext, eq_iff_true_of_subsingleton
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.BicartesianSq
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : HasZeroObject.{v₁, u₁} C
inst_2 : HasZeroMorphisms.{v₁, u₁} C
X : C
⊢ IsPullback.{v₁, u₁} (P := 0) (X := 0) 0 0 0 (𝟙 X)

Tactic:
(zero_left X).flip

Premises used: CategoryTheory.IsPullback.zero_left, CategoryTheory.IsPullback.flip
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.BicartesianSq
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : HasZeroObject.{v₁, u₁} C
inst_2 : HasZeroMorphisms.{v₁, u₁} C
X : C
⊢ CommSq.{v₁, u₁} (X := 0) (Z := 0) 0 (𝟙 X) 0 0

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.BicartesianSq
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : HasZeroObject.{v₁, u₁} C
inst_2 : HasZeroMorphisms.{v₁, u₁} C
X : C
⊢ Eq.{v₁ + 1} (α := X ⟶ 0)
    (CategoryStruct.comp (Y := pullback.{v₁, u₁} (X := 0) (Y := X) (Z := 0) 0 0)
      (Iso.hom
          (Iso.trans (Y := Limits.prod.{v₁, u₁} 0 X) (Iso.symm (zeroProdIso X) : X ≅ Limits.prod.{v₁, u₁} 0 X)
            (Iso.symm (pullbackZeroZeroIso 0 X) :
              Limits.prod.{v₁, u₁} 0 X ≅ pullback.{v₁, u₁} (X := 0) (Y := X) (Z := 0) 0 0)) :
        X ⟶ pullback.{v₁, u₁} (X := 0) (Y := X) (Z := 0) 0 0)
      (pullback.fst 0 0 : Quiver.Hom.{v₁, u₁} (V := C) (pullback.{v₁, u₁} (X := 0) (Y := X) (Z := 0) 0 0) 0))
    0

Tactic:
simp [eq_iff_true_of_subsingleton]

Premises used: eq_iff_true_of_subsingleton
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.BicartesianSq
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : HasZeroObject.{v₁, u₁} C
inst_2 : HasZeroMorphisms.{v₁, u₁} C
X : C
⊢ Eq.{v₁ + 1} (α := X ⟶ X)
    (CategoryStruct.comp (Y := pullback.{v₁, u₁} (X := 0) (Y := X) (Z := 0) 0 0)
      (Iso.hom
          (Iso.trans (Y := Limits.prod.{v₁, u₁} 0 X) (Iso.symm (zeroProdIso X) : X ≅ Limits.prod.{v₁, u₁} 0 X)
            (Iso.symm (pullbackZeroZeroIso 0 X) :
              Limits.prod.{v₁, u₁} 0 X ≅ pullback.{v₁, u₁} (X := 0) (Y := X) (Z := 0) 0 0)) :
        X ⟶ pullback.{v₁, u₁} (X := 0) (Y := X) (Z := 0) 0 0)
      (pullback.snd 0 0 : pullback.{v₁, u₁} (X := 0) (Y := X) (Z := 0) 0 0 ⟶ X))
    (𝟙 X)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.BicartesianSq
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : HasZeroObject.{v₁, u₁} C
inst_2 : HasZeroMorphisms.{v₁, u₁} C
X : C
⊢ IsPullback.{v₁, u₁} (Y := 0) (Z := 0) (𝟙 X) 0 0 0

Tactic:
(zero_right X).flip

Premises used: CategoryTheory.IsPullback.flip, CategoryTheory.IsPullback.zero_right
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.BicartesianSq
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 (IsTerminal.from HasZeroObject.zeroIsTerminal X)
    (IsTerminal.from HasZeroObject.zeroIsTerminal Y)

Tactic:
IsPullback.of_is_product' h.isLimit HasZeroObject.zeroIsTerminal

Premises used: CategoryTheory.Limits.HasZeroObject.zeroIsTerminal, CategoryTheory.IsPullback.of_is_product', CategoryTheory.Limits.BinaryBicone.IsBilimit.isLimit
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.BicartesianSq
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)
h₂ : Eq.{v₁ + 1} (α := Y ⟶ 0) 0 (IsTerminal.from HasZeroObject.zeroIsTerminal Y)
⊢ IsPullback (Z := 0) b.fst b.snd 0 0

Tactic:
convert! IsPullback.of_is_product' h.isLimit HasZeroObject.zeroIsTerminal

Premises used: CategoryTheory.Limits.HasZeroObject.zeroIsTerminal, CategoryTheory.IsPullback.of_is_product', CategoryTheory.Limits.BinaryBicone.IsBilimit.isLimit
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.BicartesianSq
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
⊢ Eq.{v₁ + 1} (α := X ⟶ 0) 0 (IsTerminal.from HasZeroObject.zeroIsTerminal X)

Tactic:
subsingleton
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.BicartesianSq
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
⊢ Eq.{v₁ + 1} (α := Y ⟶ 0) 0 (IsTerminal.from HasZeroObject.zeroIsTerminal Y)

Tactic:
subsingleton
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.BicartesianSq
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 : HasBinaryBiproduct.{v₁, u₁} X Y
⊢ IsPullback.{v₁, u₁} (C := C) (P := biprod.{v₁, u₁} X Y) (Z := 0) biprod.fst biprod.snd 0 0

Tactic:
of_isBilimit (BinaryBiproduct.isBilimit X Y)

Premises used: CategoryTheory.IsPullback.of_isBilimit, CategoryTheory.Limits.BinaryBiproduct.isBilimit
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.BicartesianSq
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
⊢ b.inl ≫ b.snd = CategoryStruct.comp (Y := 0) 0 0

Tactic:
simp