[GOAL]
C : Type u_1
inst✝² : Category.{?u.599, u_1} C
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
X : C
⊢ ∀ (s : BinaryFan 0 X), (fun s => BinaryFan.snd s) s ≫ 0 = BinaryFan.fst s
[PROOFSTEP]
aesop_cat
[GOAL]
C : Type u_1
inst✝² : Category.{?u.599, u_1} C
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
X : C
⊢ ∀ (s : BinaryFan 0 X), (fun s => BinaryFan.snd s) s ≫ 𝟙 X = BinaryFan.snd s
[PROOFSTEP]
aesop_cat
[GOAL]
C : Type u_1
inst✝² : Category.{?u.599, u_1} C
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
X : C
s : BinaryFan 0 X
m : s.pt ⟶ X
x✝ : m ≫ 0 = BinaryFan.fst s
h₂ : m ≫ 𝟙 X = BinaryFan.snd s
⊢ m = (fun s => BinaryFan.snd s) s
[PROOFSTEP]
simpa using h₂
[GOAL]
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
X : C
⊢ (zeroProdIso X).inv ≫ prod.snd = 𝟙 X
[PROOFSTEP]
dsimp [zeroProdIso, binaryFanZeroLeft]
[GOAL]
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
X : C
⊢ (limit.isoLimitCone { cone := BinaryFan.mk 0 (𝟙 X), isLimit := binaryFanZeroLeftIsLimit X }).inv ≫ prod.snd = 𝟙 X
[PROOFSTEP]
simp
[GOAL]
C : Type u_1
inst✝² : Category.{?u.6030, u_1} C
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
X : C
⊢ ∀ (s : BinaryFan X 0), (fun s => BinaryFan.fst s) s ≫ 𝟙 X = BinaryFan.fst s
[PROOFSTEP]
aesop_cat
[GOAL]
C : Type u_1
inst✝² : Category.{?u.6030, u_1} C
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
X : C
⊢ ∀ (s : BinaryFan X 0), (fun s => BinaryFan.fst s) s ≫ 0 = BinaryFan.snd s
[PROOFSTEP]
aesop_cat
[GOAL]
C : Type u_1
inst✝² : Category.{?u.6030, u_1} C
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
X : C
s : BinaryFan X 0
m : s.pt ⟶ X
h₁ : m ≫ 𝟙 X = BinaryFan.fst s
x✝ : m ≫ 0 = BinaryFan.snd s
⊢ m = (fun s => BinaryFan.fst s) s
[PROOFSTEP]
simpa using h₁
[GOAL]
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
X : C
⊢ (prodZeroIso X).inv ≫ prod.fst = 𝟙 X
[PROOFSTEP]
dsimp [prodZeroIso, binaryFanZeroRight]
[GOAL]
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
X : C
⊢ (limit.isoLimitCone { cone := BinaryFan.mk (𝟙 X) 0, isLimit := binaryFanZeroRightIsLimit X }).inv ≫ prod.fst = 𝟙 X
[PROOFSTEP]
simp
[GOAL]
C : Type u_1
inst✝² : Category.{?u.11453, u_1} C
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
X : C
⊢ ∀ (s : BinaryCofan 0 X), 0 ≫ (fun s => BinaryCofan.inr s) s = BinaryCofan.inl s
[PROOFSTEP]
aesop_cat
[GOAL]
C : Type u_1
inst✝² : Category.{?u.11453, u_1} C
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
X : C
⊢ ∀ (s : BinaryCofan 0 X), 𝟙 X ≫ (fun s => BinaryCofan.inr s) s = BinaryCofan.inr s
[PROOFSTEP]
aesop_cat
[GOAL]
C : Type u_1
inst✝² : Category.{?u.11453, u_1} C
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
X : C
s : BinaryCofan 0 X
m : X ⟶ s.pt
x✝ : 0 ≫ m = BinaryCofan.inl s
h₂ : 𝟙 X ≫ m = BinaryCofan.inr s
⊢ m = (fun s => BinaryCofan.inr s) s
[PROOFSTEP]
simpa using h₂
[GOAL]
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
X : C
⊢ coprod.inr ≫ (zeroCoprodIso X).hom = 𝟙 X
[PROOFSTEP]
dsimp [zeroCoprodIso, binaryCofanZeroLeft]
[GOAL]
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
X : C
⊢ coprod.inr ≫
      (colimit.isoColimitCocone { cocone := BinaryCofan.mk 0 (𝟙 X), isColimit := binaryCofanZeroLeftIsColimit X }).hom =
    𝟙 X
[PROOFSTEP]
simp
[GOAL]
C : Type u_1
inst✝² : Category.{?u.17161, u_1} C
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
X : C
⊢ ∀ (s : BinaryCofan X 0), 𝟙 X ≫ (fun s => BinaryCofan.inl s) s = BinaryCofan.inl s
[PROOFSTEP]
aesop_cat
[GOAL]
C : Type u_1
inst✝² : Category.{?u.17161, u_1} C
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
X : C
⊢ ∀ (s : BinaryCofan X 0), 0 ≫ (fun s => BinaryCofan.inl s) s = BinaryCofan.inr s
[PROOFSTEP]
aesop_cat
[GOAL]
C : Type u_1
inst✝² : Category.{?u.17161, u_1} C
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
X : C
s : BinaryCofan X 0
m : X ⟶ s.pt
h₁ : 𝟙 X ≫ m = BinaryCofan.inl s
x✝ : 0 ≫ m = BinaryCofan.inr s
⊢ m = (fun s => BinaryCofan.inl s) s
[PROOFSTEP]
simpa using h₁
[GOAL]
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
X : C
⊢ coprod.inl ≫ (coprodZeroIso X).hom = 𝟙 X
[PROOFSTEP]
dsimp [coprodZeroIso, binaryCofanZeroRight]
[GOAL]
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
X : C
⊢ coprod.inl ≫
      (colimit.isoColimitCocone
          { cocone := BinaryCofan.mk (𝟙 X) 0, isColimit := binaryCofanZeroRightIsColimit X }).hom =
    𝟙 X
[PROOFSTEP]
simp
[GOAL]
C : Type u_1
inst✝³ : Category.{u_2, u_1} C
inst✝² : HasZeroObject C
inst✝¹ : HasZeroMorphisms C
X Y : C
inst✝ : HasBinaryProduct X Y
⊢ (pullbackZeroZeroIso X Y).inv ≫ pullback.fst = prod.fst
[PROOFSTEP]
dsimp [pullbackZeroZeroIso]
[GOAL]
C : Type u_1
inst✝³ : Category.{u_2, u_1} C
inst✝² : HasZeroObject C
inst✝¹ : HasZeroMorphisms C
X Y : C
inst✝ : HasBinaryProduct X Y
⊢ (limit.isoLimitCone
          { cone := PullbackCone.mk prod.fst prod.snd (_ : prod.fst ≫ 0 = prod.snd ≫ 0),
            isLimit :=
              isPullbackOfIsTerminalIsProduct 0 0 prod.fst prod.snd HasZeroObject.zeroIsTerminal
                (prodIsProd X Y) }).inv ≫
      pullback.fst =
    prod.fst
[PROOFSTEP]
simp
[GOAL]
C : Type u_1
inst✝³ : Category.{u_2, u_1} C
inst✝² : HasZeroObject C
inst✝¹ : HasZeroMorphisms C
X Y : C
inst✝ : HasBinaryProduct X Y
⊢ (pullbackZeroZeroIso X Y).inv ≫ pullback.snd = prod.snd
[PROOFSTEP]
dsimp [pullbackZeroZeroIso]
[GOAL]
C : Type u_1
inst✝³ : Category.{u_2, u_1} C
inst✝² : HasZeroObject C
inst✝¹ : HasZeroMorphisms C
X Y : C
inst✝ : HasBinaryProduct X Y
⊢ (limit.isoLimitCone
          { cone := PullbackCone.mk prod.fst prod.snd (_ : prod.fst ≫ 0 = prod.snd ≫ 0),
            isLimit :=
              isPullbackOfIsTerminalIsProduct 0 0 prod.fst prod.snd HasZeroObject.zeroIsTerminal
                (prodIsProd X Y) }).inv ≫
      pullback.snd =
    prod.snd
[PROOFSTEP]
simp
[GOAL]
C : Type u_1
inst✝³ : Category.{u_2, u_1} C
inst✝² : HasZeroObject C
inst✝¹ : HasZeroMorphisms C
X Y : C
inst✝ : HasBinaryProduct X Y
⊢ (pullbackZeroZeroIso X Y).hom ≫ prod.fst = pullback.fst
[PROOFSTEP]
simp [← Iso.eq_inv_comp]
[GOAL]
C : Type u_1
inst✝³ : Category.{u_2, u_1} C
inst✝² : HasZeroObject C
inst✝¹ : HasZeroMorphisms C
X Y : C
inst✝ : HasBinaryProduct X Y
⊢ (pullbackZeroZeroIso X Y).hom ≫ prod.snd = pullback.snd
[PROOFSTEP]
simp [← Iso.eq_inv_comp]
[GOAL]
C : Type u_1
inst✝³ : Category.{u_2, u_1} C
inst✝² : HasZeroObject C
inst✝¹ : HasZeroMorphisms C
X Y : C
inst✝ : HasBinaryCoproduct X Y
⊢ pushout.inl ≫ (pushoutZeroZeroIso X Y).hom = coprod.inl
[PROOFSTEP]
dsimp [pushoutZeroZeroIso]
[GOAL]
C : Type u_1
inst✝³ : Category.{u_2, u_1} C
inst✝² : HasZeroObject C
inst✝¹ : HasZeroMorphisms C
X Y : C
inst✝ : HasBinaryCoproduct X Y
⊢ pushout.inl ≫
      (colimit.isoColimitCocone
          { cocone := PushoutCocone.mk coprod.inl coprod.inr (_ : 0 ≫ coprod.inl = 0 ≫ coprod.inr),
            isColimit :=
              isPushoutOfIsInitialIsCoproduct coprod.inl coprod.inr 0 0 HasZeroObject.zeroIsInitial
                (coprodIsCoprod X Y) }).hom =
    coprod.inl
[PROOFSTEP]
simp
[GOAL]
C : Type u_1
inst✝³ : Category.{u_2, u_1} C
inst✝² : HasZeroObject C
inst✝¹ : HasZeroMorphisms C
X Y : C
inst✝ : HasBinaryCoproduct X Y
⊢ pushout.inr ≫ (pushoutZeroZeroIso X Y).hom = coprod.inr
[PROOFSTEP]
dsimp [pushoutZeroZeroIso]
[GOAL]
C : Type u_1
inst✝³ : Category.{u_2, u_1} C
inst✝² : HasZeroObject C
inst✝¹ : HasZeroMorphisms C
X Y : C
inst✝ : HasBinaryCoproduct X Y
⊢ pushout.inr ≫
      (colimit.isoColimitCocone
          { cocone := PushoutCocone.mk coprod.inl coprod.inr (_ : 0 ≫ coprod.inl = 0 ≫ coprod.inr),
            isColimit :=
              isPushoutOfIsInitialIsCoproduct coprod.inl coprod.inr 0 0 HasZeroObject.zeroIsInitial
                (coprodIsCoprod X Y) }).hom =
    coprod.inr
[PROOFSTEP]
simp
[GOAL]
C : Type u_1
inst✝³ : Category.{u_2, u_1} C
inst✝² : HasZeroObject C
inst✝¹ : HasZeroMorphisms C
X Y : C
inst✝ : HasBinaryCoproduct X Y
⊢ coprod.inl ≫ (pushoutZeroZeroIso X Y).inv = pushout.inl
[PROOFSTEP]
simp [Iso.comp_inv_eq]
[GOAL]
C : Type u_1
inst✝³ : Category.{u_2, u_1} C
inst✝² : HasZeroObject C
inst✝¹ : HasZeroMorphisms C
X Y : C
inst✝ : HasBinaryCoproduct X Y
⊢ coprod.inr ≫ (pushoutZeroZeroIso X Y).inv = pushout.inr
[PROOFSTEP]
simp [Iso.comp_inv_eq]
