awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
refine : IsPullback (Y := 0) (Z := 0) (b.inl ≫ b.fst) 0 0 (CategoryStruct.comp (Y := Y) 0 0)
⊢ IsPullback (Y := 0) b.inl 0 b.snd 0

Tactic:
refine of_right ?_ (by simp) (of_isBilimit h)

Premises used: CategoryTheory.IsPullback.of_isBilimit, CategoryTheory.IsPullback.of_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 (Y := 0) (Z := 0) (b.inl ≫ b.fst) 0 0 (CategoryStruct.comp (Y := Y) 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 Y : C
inst_3 : HasBinaryBiproduct.{v₁, u₁} X Y
⊢ IsPullback.{v₁, u₁} (C := C) (P := X) (X := biprod.{v₁, u₁} X Y) (Y := 0) biprod.inl 0 biprod.snd 0

Tactic:
inl_snd' (BinaryBiproduct.isBilimit X Y)

Premises used: CategoryTheory.IsPullback.inl_snd', 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
h₁ : IsPullback (X := 0) 0 b.inr 0 b.fst
⊢ IsPullback (Y := 0) b.inr 0 b.fst 0

Tactic:
apply flip

Premises used: 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 Y : C
b : BinaryBicone.{v₁, u₁} X Y
h : b.IsBilimit
⊢ CategoryStruct.comp (Y := 0) 0 0 = b.inr ≫ b.fst

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 Y : C
b : BinaryBicone.{v₁, u₁} X Y
h : b.IsBilimit
h₁ : IsPullback (X := 0) (Z := 0) 0 (b.inr ≫ b.snd) (CategoryStruct.comp (Y := X) 0 0) 0
⊢ IsPullback (X := 0) 0 b.inr 0 b.fst

Tactic:
refine of_bot ?_ (by simp) (of_isBilimit h)

Premises used: CategoryTheory.IsPullback.of_bot, CategoryTheory.IsPullback.of_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
⊢ IsPullback (X := 0) (Z := 0) 0 (b.inr ≫ b.snd) (CategoryStruct.comp (Y := X) 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 Y : C
inst_3 : HasBinaryBiproduct.{v₁, u₁} X Y
⊢ IsPullback.{v₁, u₁} (C := C) (P := Y) (X := biprod.{v₁, u₁} X Y) (Y := 0) biprod.inr 0 biprod.fst 0

Tactic:
inr_fst' (BinaryBiproduct.isBilimit X Y)

Premises used: CategoryTheory.IsPullback.inr_fst', 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
⊢ Eq (α := 0 ⟶ b.pt) (0 ≫ b.inl) (0 ≫ b.inr)

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 Y : C
b : BinaryBicone.{v₁, u₁} X Y
h : b.IsBilimit
refine : IsPullback (P := 0) (X := 0) (CategoryStruct.comp (Y := X) 0 0) 0 0 (b.inr ≫ b.snd)
⊢ IsPullback (P := 0) 0 0 b.inl b.inr

Tactic:
refine IsPullback.of_right ?_ (by simp) (IsPullback.inl_snd' h).flip

Premises used: CategoryTheory.IsPullback.inl_snd', CategoryTheory.IsPullback.flip, CategoryTheory.IsPullback.of_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 (P := 0) (X := 0) (CategoryStruct.comp (Y := X) 0 0) 0 0 (b.inr ≫ b.snd)

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 Y : C
inst_3 : HasBinaryBiproduct.{v₁, u₁} X Y
⊢ IsPullback.{v₁, u₁} (C := C) (P := 0) (X := X) (Y := Y) (Z := biprod.{v₁, u₁} X Y) 0 0 biprod.inl biprod.inr

Tactic:
of_is_bilimit' (BinaryBiproduct.isBilimit X Y)

Premises used: CategoryTheory.IsPullback.of_is_bilimit', 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
P X Y Z : C
fst : P ⟶ X
snd : P ⟶ Y
f : X ⟶ Z
g : Y ⟶ Z
inst_3 : HasBinaryBiproduct.{v₁, u₁} X Y
⊢ HasPullback.{v₁, u₁} (C := C) (X := X) (Y := Y) (Z := biprod.{v₁, u₁} X Y) biprod.inl biprod.inr

Tactic:
HasLimit.mk ⟨_, (of_hasBinaryBiproduct X Y).isLimit⟩

Premises used: CategoryTheory.IsPullback.of_hasBinaryBiproduct, CategoryTheory.Limits.HasLimit.mk, CategoryTheory.Limits.LimitCone.mk, CategoryTheory.IsPullback.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
inst_3 : HasBinaryCoproduct.{v₁, u₁} X Y
⊢ IsPushout (Z := 0) (P :=
    Functor.obj.{0, v₁, 0, u₁}
      (Functor.obj (Functor.const (Discrete WalkingPair))
        (Cocone.pt.{0, v₁, 0, u₁} (F := pair X Y) (colimit.cocone (pair X Y))))
      { as := WalkingPair.left : Discrete WalkingPair })
    (IsInitial.to HasZeroObject.zeroIsInitial
      (Functor.obj.{0, v₁, 0, u₁} (pair X Y) { as := WalkingPair.left : Discrete WalkingPair }))
    (IsInitial.to HasZeroObject.zeroIsInitial
      (Functor.obj.{0, v₁, 0, u₁} (pair X Y) { as := WalkingPair.right : Discrete WalkingPair }))
    (BinaryCofan.inl (colimit.cocone (pair X Y))) (BinaryCofan.inr (colimit.cocone (pair X Y)))

Tactic:
@of_is_coproduct _ _ 0 X Y _ (colimit.isColimit _) HasZeroObject.zeroIsInitial

Premises used: CategoryTheory.Limits.HasZeroObject.zeroIsInitial, CategoryTheory.Limits.colimit.isColimit, CategoryTheory.IsPushout.of_is_coproduct
-- 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 : HasBinaryCoproduct.{v₁, u₁} X Y
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 }))
h₁ :
  Y = Functor.obj.{0, v₁, 0, u₁} (pair X Y) { as := WalkingPair.right : Discrete WalkingPair } →
    Eq.{v₁ + 1} (α := 0 ⟶ Y) 0
      (IsInitial.to HasZeroObject.zeroIsInitial
        (Functor.obj.{0, v₁, 0, u₁} (pair X Y) { as := WalkingPair.right : Discrete WalkingPair }))
⊢ IsPushout.{v₁, u₁} (C := C) (Z := 0) (X := X) (Y := Y) (P := coprod.{v₁, u₁} X Y) 0 0 coprod.inl coprod.inr

Tactic:
convert! @of_is_coproduct _ _ 0 X Y _ (colimit.isColimit _) HasZeroObject.zeroIsInitial

Premises used: CategoryTheory.Limits.HasZeroObject.zeroIsInitial, CategoryTheory.Limits.colimit.isColimit, CategoryTheory.IsPushout.of_is_coproduct
-- 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 : HasBinaryCoproduct.{v₁, u₁} X Y
e_4 : 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:
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 : HasBinaryCoproduct.{v₁, u₁} X Y
e_5 : Y = Functor.obj.{0, v₁, 0, u₁} (pair X Y) { as := WalkingPair.right : Discrete WalkingPair }
⊢ Eq.{v₁ + 1} (α := 0 ⟶ Y) 0
    (IsInitial.to HasZeroObject.zeroIsInitial
      (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} (α := X ⟶ 0) (CategoryStruct.comp (Y := 0) 0 0) (𝟙 X ≫ 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 : Cocone.{0, v₁, 0, u₁} (span (Y := 0) 0 (𝟙 X))
⊢ PushoutCocone.inl s ≫ 0 = PushoutCocone.inl s ≫ 𝟙 s.pt

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
s : Cocone.{0, v₁, 0, u₁} (span (Y := 0) 0 (𝟙 X))
⊢ PushoutCocone.inr s ≫ 0 = PushoutCocone.inr s ≫ 𝟙 s.pt

Tactic:
simpa using PushoutCocone.condition s

Premises used: CategoryTheory.Limits.PushoutCocone.condition
-- 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 : Cocone.{0, v₁, 0, u₁} (span (Y := 0) 0 (𝟙 X))
⊢ ∀ (j : WalkingSpan), s.ι.app j ≫ 0 = s.ι.app j ≫ 𝟙 s.pt

Tactic:
have c :=
              @PushoutCocone.coequalizer_ext _ _ _ _ _ _ _ s _ 0 (𝟙 _)
                (by simp [eq_iff_true_of_subsingleton]) (by simpa using PushoutCocone.condition s)
-- 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 : Cocone.{0, v₁, 0, u₁} (span (Y := 0) 0 (𝟙 X))
c : ∀ (j : WalkingSpan), s.ι.app j ≫ 0 = s.ι.app j ≫ 𝟙 s.pt
⊢ ∀ (j : WalkingSpan),
    CategoryStruct.comp (Y :=
        Functor.obj.{0, v₁, 0, u₁}
          (Functor.obj (Functor.const WalkingSpan)
            (Cocone.pt.{0, v₁, 0, u₁} (F := span (Y := 0) 0 (𝟙 X)) (PushoutCocone.mk (W := 0) 0 0 ⋯)))
          j)
        (NatTrans.app (Cocone.ι (PushoutCocone.mk (W := 0) 0 0 ⋯)) j) 0 =
      s.ι.app j

Tactic:
simpa using c
-- 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
⊢ IsPushout.{v₁, u₁} (Y := 0) (P := 0) (𝟙 X) 0 0 0

Tactic:
(zero_right X).flip

Premises used: CategoryTheory.IsPushout.flip, CategoryTheory.IsPushout.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 : C
⊢ CommSq.{v₁, u₁} (W := 0) (Y := 0) 0 0 (𝟙 X) 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 ⟶ pushout.{v₁, u₁} (X := 0) (Y := X) (Z := 0) 0 0)
    (𝟙 X ≫
        Iso.hom
          (Iso.trans (Y := coprod.{v₁, u₁} X 0) (Iso.symm (coprodZeroIso X) : X ≅ coprod.{v₁, u₁} X 0)
            (Iso.symm (pushoutZeroZeroIso X 0) :
              coprod.{v₁, u₁} X 0 ≅ pushout.{v₁, u₁} (X := 0) (Y := X) (Z := 0) 0 0)) :
      X ⟶ pushout.{v₁, u₁} (X := 0) (Y := X) (Z := 0) 0 0)
    (pushout.inl 0 0 : X ⟶ pushout.{v₁, u₁} (X := 0) (Y := X) (Z := 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
⊢ Eq.{v₁ + 1} (α := Quiver.Hom.{v₁, u₁} (V := C) 0 (pushout.{v₁, u₁} (X := 0) (Y := X) (Z := 0) 0 0))
    (0 ≫
        Iso.hom
          (Iso.trans (Y := coprod.{v₁, u₁} X 0) (Iso.symm (coprodZeroIso X) : X ≅ coprod.{v₁, u₁} X 0)
            (Iso.symm (pushoutZeroZeroIso X 0) :
              coprod.{v₁, u₁} X 0 ≅ pushout.{v₁, u₁} (X := 0) (Y := X) (Z := 0) 0 0)) :
      Quiver.Hom.{v₁, u₁} (V := C) 0 (pushout.{v₁, u₁} (X := 0) (Y := X) (Z := 0) 0 0))
    (pushout.inr 0 0 : Quiver.Hom.{v₁, u₁} (V := C) 0 (pushout.{v₁, u₁} (X := 0) (Y := X) (Z := 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
⊢ IsPushout.{v₁, u₁} (Z := 0) (X := 0) 0 0 0 (𝟙 X)

Tactic:
(zero_left X).flip

Premises used: CategoryTheory.IsPushout.zero_left, CategoryTheory.IsPushout.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 Y : C
b : BinaryBicone.{v₁, u₁} X Y
h : b.IsBilimit
⊢ IsPushout (Z := 0) (IsInitial.to HasZeroObject.zeroIsInitial X) (IsInitial.to HasZeroObject.zeroIsInitial Y) b.inl
    b.inr

Tactic:
IsPushout.of_is_coproduct' h.isColimit HasZeroObject.zeroIsInitial

Premises used: CategoryTheory.Limits.HasZeroObject.zeroIsInitial, CategoryTheory.IsPushout.of_is_coproduct', CategoryTheory.Limits.BinaryBicone.IsBilimit.isColimit
-- 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} (α := 0 ⟶ X) 0 (IsInitial.to HasZeroObject.zeroIsInitial X)
h₂ : Eq.{v₁ + 1} (α := 0 ⟶ Y) 0 (IsInitial.to HasZeroObject.zeroIsInitial Y)
⊢ IsPushout (Z := 0) 0 0 b.inl b.inr

Tactic:
convert! IsPushout.of_is_coproduct' h.isColimit HasZeroObject.zeroIsInitial

Premises used: CategoryTheory.Limits.HasZeroObject.zeroIsInitial, CategoryTheory.IsPushout.of_is_coproduct', CategoryTheory.Limits.BinaryBicone.IsBilimit.isColimit
-- 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} (α := 0 ⟶ X) 0 (IsInitial.to HasZeroObject.zeroIsInitial 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} (α := 0 ⟶ Y) 0 (IsInitial.to HasZeroObject.zeroIsInitial 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
⊢ IsPushout.{v₁, u₁} (C := C) (Z := 0) (X := X) (Y := Y) (P := biprod.{v₁, u₁} X Y) 0 0 biprod.inl biprod.inr

Tactic:
of_isBilimit (BinaryBiproduct.isBilimit X Y)

Premises used: CategoryTheory.IsPushout.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
h₁ : IsPushout (X := 0) 0 b.inl 0 b.snd
⊢ IsPushout (Y := 0) b.inl 0 b.snd 0

Tactic:
apply flip

Premises used: CategoryTheory.IsPushout.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 Y : C
b : BinaryBicone.{v₁, u₁} X Y
h : b.IsBilimit
⊢ CategoryStruct.comp (Y := 0) 0 0 = b.inl ≫ b.snd

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 Y : C
b : BinaryBicone.{v₁, u₁} X Y
h : b.IsBilimit
h₁ : IsPushout (Z := 0) (X := 0) (CategoryStruct.comp (Y := X) 0 0) 0 0 (b.inr ≫ b.snd)
⊢ IsPushout (X := 0) 0 b.inl 0 b.snd

Tactic:
refine of_left ?_ (by simp) (of_isBilimit h)

Premises used: CategoryTheory.IsPushout.of_left, CategoryTheory.IsPushout.of_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
⊢ IsPushout (Z := 0) (X := 0) (CategoryStruct.comp (Y := X) 0 0) 0 0 (b.inr ≫ b.snd)

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 Y : C
inst_3 : HasBinaryBiproduct.{v₁, u₁} X Y
⊢ IsPushout.{v₁, u₁} (C := C) (Z := X) (X := biprod.{v₁, u₁} X Y) (Y := 0) biprod.inl 0 biprod.snd 0

Tactic:
inl_snd' (BinaryBiproduct.isBilimit X Y)

Premises used: CategoryTheory.IsPushout.inl_snd', 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.inr ≫ b.fst = 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 Y : C
b : BinaryBicone.{v₁, u₁} X Y
h : b.IsBilimit
refine : IsPushout (Z := 0) (Y := 0) 0 (CategoryStruct.comp (Y := Y) 0 0) (b.inl ≫ b.fst) 0
⊢ IsPushout (Y := 0) b.inr 0 b.fst 0

Tactic:
refine of_top ?_ (by simp) (of_isBilimit h)

Premises used: CategoryTheory.IsPushout.of_top, CategoryTheory.IsPushout.of_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
⊢ IsPushout (Z := 0) (Y := 0) 0 (CategoryStruct.comp (Y := Y) 0 0) (b.inl ≫ b.fst) 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 Y : C
inst_3 : HasBinaryBiproduct.{v₁, u₁} X Y
⊢ IsPushout.{v₁, u₁} (C := C) (Z := Y) (X := biprod.{v₁, u₁} X Y) (Y := 0) biprod.inr 0 biprod.fst 0

Tactic:
inr_fst' (BinaryBiproduct.isBilimit X Y)

Premises used: CategoryTheory.IsPushout.inr_fst', 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
⊢ Eq (α := b.pt ⟶ 0) (b.fst ≫ 0) (b.snd ≫ 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 Y : C
b : BinaryBicone.{v₁, u₁} X Y
h : b.IsBilimit
refine : IsPushout (Y := 0) (P := 0) (b.inl ≫ b.fst) 0 0 (CategoryStruct.comp (Y := Y) 0 0)
⊢ IsPushout (P := 0) b.fst b.snd 0 0

Tactic:
refine IsPushout.of_left ?_ (by simp) (IsPushout.inl_snd' h)

Premises used: CategoryTheory.IsPushout.inl_snd', CategoryTheory.IsPushout.of_left
-- 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
⊢ IsPushout (Y := 0) (P := 0) (b.inl ≫ b.fst) 0 0 (CategoryStruct.comp (Y := Y) 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 Y : C
inst_3 : HasBinaryBiproduct.{v₁, u₁} X Y
⊢ IsPushout.{v₁, u₁} (C := C) (Z := biprod.{v₁, u₁} X Y) (P := 0) biprod.fst biprod.snd 0 0

Tactic:
of_is_bilimit' (BinaryBiproduct.isBilimit X Y)

Premises used: CategoryTheory.IsPushout.of_is_bilimit', 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
Z X Y P : C
f : Z ⟶ X
g : Z ⟶ Y
inl : X ⟶ P
inr : Y ⟶ P
inst_3 : HasBinaryBiproduct.{v₁, u₁} X Y
⊢ HasPushout.{v₁, u₁} (C := C) (X := biprod.{v₁, u₁} X Y) biprod.fst biprod.snd

Tactic:
HasColimit.mk ⟨_, (of_hasBinaryBiproduct X Y).isColimit⟩

Premises used: CategoryTheory.Limits.HasColimit.mk, CategoryTheory.Limits.ColimitCocone.mk, CategoryTheory.IsPushout.of_hasBinaryBiproduct, CategoryTheory.IsPushout.isColimit
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.BicartesianSq
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
W X Y Z : C
f : W ⟶ X
g : W ⟶ Y
h : X ⟶ Z
i : Y ⟶ Z
p₁ : IsPullback f g h i
p₂ : IsPushout f g h i
⊢ BicartesianSq f g h i

Tactic:
BicartesianSq.mk p₁ p₂.isColimit'

Premises used: CategoryTheory.IsPushout.isColimit', CategoryTheory.BicartesianSq.mk
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.BicartesianSq
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
W X Y Z : C
f : W ⟶ X
g : W ⟶ Y
h : X ⟶ Z
i : Y ⟶ Z
p : BicartesianSq f g h i
⊢ BicartesianSq g f i h

Tactic:
of_isPullback_isPushout p.toIsPullback.flip p.toIsPushout.flip

Premises used: CategoryTheory.BicartesianSq.toIsPushout, CategoryTheory.BicartesianSq.of_isPullback_isPushout, CategoryTheory.IsPushout.flip, CategoryTheory.IsPullback.flip, CategoryTheory.BicartesianSq.toIsPullback
-- 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
⊢ BicartesianSq (Z := 0) b.fst b.snd 0 0

Tactic:
of_isPullback_isPushout (IsPullback.of_isBilimit h) (IsPushout.of_is_bilimit' h)

Premises used: CategoryTheory.IsPushout.of_is_bilimit', CategoryTheory.BicartesianSq.of_isPullback_isPushout, CategoryTheory.IsPullback.of_isBilimit