case mp
J : Type v'
inst✝¹ : Category J
C : Type u
inst✝ : Category C
W X✝ Y✝ Z : C
f✝ : W ⟶ X✝
g : W ⟶ Y✝
h : X✝ ⟶ Z
i : Y✝ ⟶ Z
X E Y YE : C
c : BinaryCofan X E
hc : IsColimit c
f : X ⟶ Y
iY : Y ⟶ YE
fE : c.pt ⟶ YE
H : CommSq f (BinaryCofan.inl c) iY fE
⊢ Nonempty (IsColimit (BinaryCofan.mk (BinaryCofan.inr c ≫ fE) iY)) → IsPushout f (BinaryCofan.inl c) iY fE

case mpr
J : Type v'
inst✝¹ : Category J
C : Type u
inst✝ : Category C
W X✝ Y✝ Z : C
f✝ : W ⟶ X✝
g : W ⟶ Y✝
h : X✝ ⟶ Z
i : Y✝ ⟶ Z
X E Y YE : C
c : BinaryCofan X E
hc : IsColimit c
f : X ⟶ Y
iY : Y ⟶ YE
fE : c.pt ⟶ YE
H : CommSq f (BinaryCofan.inl c) iY fE
⊢ IsPushout f (BinaryCofan.inl c) iY fE → Nonempty (IsColimit (BinaryCofan.mk (BinaryCofan.inr c ≫ fE) iY))
J : Type v'
inst✝¹ : Category J
C : Type u
inst✝ : Category C
W X✝ Y✝ Z : C
f✝ : W ⟶ X✝
g : W ⟶ Y✝
h : X✝ ⟶ Z
i : Y✝ ⟶ Z
X E Y YE : C
c : BinaryCofan X E
hc : IsColimit c
f : X ⟶ Y
iY : Y ⟶ YE
fE : c.pt ⟶ YE
H : CommSq f (BinaryCofan.inl c) iY fE
⊢ Nonempty (IsColimit (BinaryCofan.mk (BinaryCofan.inr c ≫ fE) iY)) ↔ IsPushout f (BinaryCofan.inl c) iY fE
constructor
case mp.intro
J : Type v'
inst✝¹ : Category J
C : Type u
inst✝ : Category C
W X✝ Y✝ Z : C
f✝ : W ⟶ X✝
g : W ⟶ Y✝
h✝ : X✝ ⟶ Z
i : Y✝ ⟶ Z
X E Y YE : C
c : BinaryCofan X E
hc : IsColimit c
f : X ⟶ Y
iY : Y ⟶ YE
fE : c.pt ⟶ YE
H : CommSq f (BinaryCofan.inl c) iY fE
h : IsColimit (BinaryCofan.mk (BinaryCofan.inr c ≫ fE) iY)
⊢ IsPushout f (BinaryCofan.inl c) iY fE
case mp
J : Type v'
inst✝¹ : Category J
C : Type u
inst✝ : Category C
W X✝ Y✝ Z : C
f✝ : W ⟶ X✝
g : W ⟶ Y✝
h : X✝ ⟶ Z
i : Y✝ ⟶ Z
X E Y YE : C
c : BinaryCofan X E
hc : IsColimit c
f : X ⟶ Y
iY : Y ⟶ YE
fE : c.pt ⟶ YE
H : CommSq f (BinaryCofan.inl c) iY fE
⊢ Nonempty (IsColimit (BinaryCofan.mk (BinaryCofan.inr c ≫ fE) iY)) → IsPushout f (BinaryCofan.inl c) iY fE
rintro ⟨h⟩
case mp.intro
J : Type v'
inst✝¹ : Category J
C : Type u
inst✝ : Category C
W X✝ Y✝ Z : C
f✝ : W ⟶ X✝
g : W ⟶ Y✝
h✝ : X✝ ⟶ Z
i : Y✝ ⟶ Z
X E Y YE : C
c : BinaryCofan X E
hc : IsColimit c
f : X ⟶ Y
iY : Y ⟶ YE
fE : c.pt ⟶ YE
H : CommSq f (BinaryCofan.inl c) iY fE
h : IsColimit (BinaryCofan.mk (BinaryCofan.inr c ≫ fE) iY)
⊢ (s : PushoutCocone f (BinaryCofan.inl c)) →
    { l //
      PushoutCocone.inl (PushoutCocone.mk iY fE (_ : f ≫ iY = BinaryCofan.inl c ≫ fE)) ≫ l = PushoutCocone.inl s ∧
        PushoutCocone.inr (PushoutCocone.mk iY fE (_ : f ≫ iY = BinaryCofan.inl c ≫ fE)) ≫ l = PushoutCocone.inr s ∧
          ∀ {m : (PushoutCocone.mk iY fE (_ : f ≫ iY = BinaryCofan.inl c ≫ fE)).pt ⟶ s.pt},
            PushoutCocone.inl (PushoutCocone.mk iY fE (_ : f ≫ iY = BinaryCofan.inl c ≫ fE)) ≫ m = PushoutCocone.inl s →
              PushoutCocone.inr (PushoutCocone.mk iY fE (_ : f ≫ iY = BinaryCofan.inl c ≫ fE)) ≫ m =
                  PushoutCocone.inr s →
                m = l }
case mp.intro
J : Type v'
inst✝¹ : Category J
C : Type u
inst✝ : Category C
W X✝ Y✝ Z : C
f✝ : W ⟶ X✝
g : W ⟶ Y✝
h✝ : X✝ ⟶ Z
i : Y✝ ⟶ Z
X E Y YE : C
c : BinaryCofan X E
hc : IsColimit c
f : X ⟶ Y
iY : Y ⟶ YE
fE : c.pt ⟶ YE
H : CommSq f (BinaryCofan.inl c) iY fE
h : IsColimit (BinaryCofan.mk (BinaryCofan.inr c ≫ fE) iY)
⊢ IsPushout f (BinaryCofan.inl c) iY fE
refine' ⟨H, ⟨Limits.PushoutCocone.isColimitAux' _ _⟩⟩
case mp.intro
J : Type v'
inst✝¹ : Category J
C : Type u
inst✝ : Category C
W X✝ Y✝ Z : C
f✝ : W ⟶ X✝
g : W ⟶ Y✝
h✝ : X✝ ⟶ Z
i : Y✝ ⟶ Z
X E Y YE : C
c : BinaryCofan X E
hc : IsColimit c
f : X ⟶ Y
iY : Y ⟶ YE
fE : c.pt ⟶ YE
H : CommSq f (BinaryCofan.inl c) iY fE
h : IsColimit (BinaryCofan.mk (BinaryCofan.inr c ≫ fE) iY)
s : PushoutCocone f (BinaryCofan.inl c)
⊢ { l //
    PushoutCocone.inl (PushoutCocone.mk iY fE (_ : f ≫ iY = BinaryCofan.inl c ≫ fE)) ≫ l = PushoutCocone.inl s ∧
      PushoutCocone.inr (PushoutCocone.mk iY fE (_ : f ≫ iY = BinaryCofan.inl c ≫ fE)) ≫ l = PushoutCocone.inr s ∧
        ∀ {m : (PushoutCocone.mk iY fE (_ : f ≫ iY = BinaryCofan.inl c ≫ fE)).pt ⟶ s.pt},
          PushoutCocone.inl (PushoutCocone.mk iY fE (_ : f ≫ iY = BinaryCofan.inl c ≫ fE)) ≫ m = PushoutCocone.inl s →
            PushoutCocone.inr (PushoutCocone.mk iY fE (_ : f ≫ iY = BinaryCofan.inl c ≫ fE)) ≫ m = PushoutCocone.inr s →
              m = l }
case mp.intro
J : Type v'
inst✝¹ : Category J
C : Type u
inst✝ : Category C
W X✝ Y✝ Z : C
f✝ : W ⟶ X✝
g : W ⟶ Y✝
h✝ : X✝ ⟶ Z
i : Y✝ ⟶ Z
X E Y YE : C
c : BinaryCofan X E
hc : IsColimit c
f : X ⟶ Y
iY : Y ⟶ YE
fE : c.pt ⟶ YE
H : CommSq f (BinaryCofan.inl c) iY fE
h : IsColimit (BinaryCofan.mk (BinaryCofan.inr c ≫ fE) iY)
⊢ (s : PushoutCocone f (BinaryCofan.inl c)) →
    { l //
      PushoutCocone.inl (PushoutCocone.mk iY fE (_ : f ≫ iY = BinaryCofan.inl c ≫ fE)) ≫ l = PushoutCocone.inl s ∧
        PushoutCocone.inr (PushoutCocone.mk iY fE (_ : f ≫ iY = BinaryCofan.inl c ≫ fE)) ≫ l = PushoutCocone.inr s ∧
          ∀ {m : (PushoutCocone.mk iY fE (_ : f ≫ iY = BinaryCofan.inl c ≫ fE)).pt ⟶ s.pt},
            PushoutCocone.inl (PushoutCocone.mk iY fE (_ : f ≫ iY = BinaryCofan.inl c ≫ fE)) ≫ m = PushoutCocone.inl s →
              PushoutCocone.inr (PushoutCocone.mk iY fE (_ : f ≫ iY = BinaryCofan.inl c ≫ fE)) ≫ m =
                  PushoutCocone.inr s →
                m = l }
intro s
case mp.intro
J : Type v'
inst✝¹ : Category J
C : Type u
inst✝ : Category C
W X✝ Y✝ Z : C
f✝ : W ⟶ X✝
g : W ⟶ Y✝
h✝ : X✝ ⟶ Z
i : Y✝ ⟶ Z
X E Y YE : C
c : BinaryCofan X E
hc : IsColimit c
f : X ⟶ Y
iY : Y ⟶ YE
fE : c.pt ⟶ YE
H : CommSq f (BinaryCofan.inl c) iY fE
h : IsColimit (BinaryCofan.mk (BinaryCofan.inr c ≫ fE) iY)
s : PushoutCocone f (BinaryCofan.inl c)
⊢ { l //
    PushoutCocone.inl
            { pt := YE, ι := NatTrans.mk fun j => Option.rec (f ≫ iY) (fun val => WalkingPair.rec iY fE val) j } ≫
          l =
        PushoutCocone.inl s ∧
      fE ≫ l = s.ι.app WalkingSpan.right ∧
        ∀ {m : YE ⟶ s.pt},
          PushoutCocone.inl
                  { pt := YE, ι := NatTrans.mk fun j => Option.rec (f ≫ iY) (fun val => WalkingPair.rec iY fE val) j } ≫
                m =
              PushoutCocone.inl s →
            fE ≫ m = s.ι.app WalkingSpan.right → m = l }
case mp.intro
J : Type v'
inst✝¹ : Category J
C : Type u
inst✝ : Category C
W X✝ Y✝ Z : C
f✝ : W ⟶ X✝
g : W ⟶ Y✝
h✝ : X✝ ⟶ Z
i : Y✝ ⟶ Z
X E Y YE : C
c : BinaryCofan X E
hc : IsColimit c
f : X ⟶ Y
iY : Y ⟶ YE
fE : c.pt ⟶ YE
H : CommSq f (BinaryCofan.inl c) iY fE
h : IsColimit (BinaryCofan.mk (BinaryCofan.inr c ≫ fE) iY)
s : PushoutCocone f (BinaryCofan.inl c)
⊢ { l //
    PushoutCocone.inl (PushoutCocone.mk iY fE (_ : f ≫ iY = BinaryCofan.inl c ≫ fE)) ≫ l = PushoutCocone.inl s ∧
      PushoutCocone.inr (PushoutCocone.mk iY fE (_ : f ≫ iY = BinaryCofan.inl c ≫ fE)) ≫ l = PushoutCocone.inr s ∧
        ∀ {m : (PushoutCocone.mk iY fE (_ : f ≫ iY = BinaryCofan.inl c ≫ fE)).pt ⟶ s.pt},
          PushoutCocone.inl (PushoutCocone.mk iY fE (_ : f ≫ iY = BinaryCofan.inl c ≫ fE)) ≫ m = PushoutCocone.inl s →
            PushoutCocone.inr (PushoutCocone.mk iY fE (_ : f ≫ iY = BinaryCofan.inl c ≫ fE)) ≫ m = PushoutCocone.inr s →
              m = l }
dsimp only [PushoutCocone.inr, PushoutCocone.mk]
case mp.intro.refine'_1
J : Type v'
inst✝¹ : Category J
C : Type u
inst✝ : Category C
W X✝ Y✝ Z : C
f✝ : W ⟶ X✝
g : W ⟶ Y✝
h✝ : X✝ ⟶ Z
i : Y✝ ⟶ Z
X E Y YE : C
c : BinaryCofan X E
hc : IsColimit c
f : X ⟶ Y
iY : Y ⟶ YE
fE : c.pt ⟶ YE
H : CommSq f (BinaryCofan.inl c) iY fE
h : IsColimit (BinaryCofan.mk (BinaryCofan.inr c ≫ fE) iY)
s : PushoutCocone f (BinaryCofan.inl c)
⊢ fE ≫ IsColimit.desc h (BinaryCofan.mk (BinaryCofan.inr c ≫ PushoutCocone.inr s) (PushoutCocone.inl s)) =
    s.ι.app WalkingSpan.right

case mp.intro.refine'_2
J : Type v'
inst✝¹ : Category J
C : Type u
inst✝ : Category C
W X✝ Y✝ Z : C
f✝ : W ⟶ X✝
g : W ⟶ Y✝
h✝ : X✝ ⟶ Z
i : Y✝ ⟶ Z
X E Y YE : C
c : BinaryCofan X E
hc : IsColimit c
f : X ⟶ Y
iY : Y ⟶ YE
fE : c.pt ⟶ YE
H : CommSq f (BinaryCofan.inl c) iY fE
h : IsColimit (BinaryCofan.mk (BinaryCofan.inr c ≫ fE) iY)
s : PushoutCocone f (BinaryCofan.inl c)
⊢ ∀ {m : YE ⟶ s.pt},
    PushoutCocone.inl
            { pt := YE, ι := NatTrans.mk fun j => Option.rec (f ≫ iY) (fun val => WalkingPair.rec iY fE val) j } ≫
          m =
        PushoutCocone.inl s →
      fE ≫ m = s.ι.app WalkingSpan.right →
        m = IsColimit.desc h (BinaryCofan.mk (BinaryCofan.inr c ≫ PushoutCocone.inr s) (PushoutCocone.inl s))
case mp.intro
J : Type v'
inst✝¹ : Category J
C : Type u
inst✝ : Category C
W X✝ Y✝ Z : C
f✝ : W ⟶ X✝
g : W ⟶ Y✝
h✝ : X✝ ⟶ Z
i : Y✝ ⟶ Z
X E Y YE : C
c : BinaryCofan X E
hc : IsColimit c
f : X ⟶ Y
iY : Y ⟶ YE
fE : c.pt ⟶ YE
H : CommSq f (BinaryCofan.inl c) iY fE
h : IsColimit (BinaryCofan.mk (BinaryCofan.inr c ≫ fE) iY)
s : PushoutCocone f (BinaryCofan.inl c)
⊢ { l //
    PushoutCocone.inl
            { pt := YE, ι := NatTrans.mk fun j => Option.rec (f ≫ iY) (fun val => WalkingPair.rec iY fE val) j } ≫
          l =
        PushoutCocone.inl s ∧
      fE ≫ l = s.ι.app WalkingSpan.right ∧
        ∀ {m : YE ⟶ s.pt},
          PushoutCocone.inl
                  { pt := YE, ι := NatTrans.mk fun j => Option.rec (f ≫ iY) (fun val => WalkingPair.rec iY fE val) j } ≫
                m =
              PushoutCocone.inl s →
            fE ≫ m = s.ι.app WalkingSpan.right → m = l }
refine' ⟨h.desc (BinaryCofan.mk (c.inr ≫ s.inr) s.inl), h.fac _ ⟨WalkingPair.right⟩, _, _⟩
case mp.intro.refine'_1.h₁
J : Type v'
inst✝¹ : Category J
C : Type u
inst✝ : Category C
W X✝ Y✝ Z : C
f✝ : W ⟶ X✝
g : W ⟶ Y✝
h✝ : X✝ ⟶ Z
i : Y✝ ⟶ Z
X E Y YE : C
c : BinaryCofan X E
hc : IsColimit c
f : X ⟶ Y
iY : Y ⟶ YE
fE : c.pt ⟶ YE
H : CommSq f (BinaryCofan.inl c) iY fE
h : IsColimit (BinaryCofan.mk (BinaryCofan.inr c ≫ fE) iY)
s : PushoutCocone f (BinaryCofan.inl c)
⊢ BinaryCofan.inl c ≫
      fE ≫ IsColimit.desc h (BinaryCofan.mk (BinaryCofan.inr c ≫ PushoutCocone.inr s) (PushoutCocone.inl s)) =
    BinaryCofan.inl c ≫ s.ι.app WalkingSpan.right

case mp.intro.refine'_1.h₂
J : Type v'
inst✝¹ : Category J
C : Type u
inst✝ : Category C
W X✝ Y✝ Z : C
f✝ : W ⟶ X✝
g : W ⟶ Y✝
h✝ : X✝ ⟶ Z
i : Y✝ ⟶ Z
X E Y YE : C
c : BinaryCofan X E
hc : IsColimit c
f : X ⟶ Y
iY : Y ⟶ YE
fE : c.pt ⟶ YE
H : CommSq f (BinaryCofan.inl c) iY fE
h : IsColimit (BinaryCofan.mk (BinaryCofan.inr c ≫ fE) iY)
s : PushoutCocone f (BinaryCofan.inl c)
⊢ BinaryCofan.inr c ≫
      fE ≫ IsColimit.desc h (BinaryCofan.mk (BinaryCofan.inr c ≫ PushoutCocone.inr s) (PushoutCocone.inl s)) =
    BinaryCofan.inr c ≫ s.ι.app WalkingSpan.right
case mp.intro.refine'_1
J : Type v'
inst✝¹ : Category J
C : Type u
inst✝ : Category C
W X✝ Y✝ Z : C
f✝ : W ⟶ X✝
g : W ⟶ Y✝
h✝ : X✝ ⟶ Z
i : Y✝ ⟶ Z
X E Y YE : C
c : BinaryCofan X E
hc : IsColimit c
f : X ⟶ Y
iY : Y ⟶ YE
fE : c.pt ⟶ YE
H : CommSq f (BinaryCofan.inl c) iY fE
h : IsColimit (BinaryCofan.mk (BinaryCofan.inr c ≫ fE) iY)
s : PushoutCocone f (BinaryCofan.inl c)
⊢ fE ≫ IsColimit.desc h (BinaryCofan.mk (BinaryCofan.inr c ≫ PushoutCocone.inr s) (PushoutCocone.inl s)) =
    s.ι.app WalkingSpan.right
apply BinaryCofan.IsColimit.hom_ext hc
case mp.intro.refine'_1.h₁
J : Type v'
inst✝¹ : Category J
C : Type u
inst✝ : Category C
W X✝ Y✝ Z : C
f✝ : W ⟶ X✝
g : W ⟶ Y✝
h✝ : X✝ ⟶ Z
i : Y✝ ⟶ Z
X E Y YE : C
c : BinaryCofan X E
hc : IsColimit c
f : X ⟶ Y
iY : Y ⟶ YE
fE : c.pt ⟶ YE
H : CommSq f (BinaryCofan.inl c) iY fE
h : IsColimit (BinaryCofan.mk (BinaryCofan.inr c ≫ fE) iY)
s : PushoutCocone f (BinaryCofan.inl c)
⊢ f ≫ iY ≫ IsColimit.desc h (BinaryCofan.mk (BinaryCofan.inr c ≫ PushoutCocone.inr s) (PushoutCocone.inl s)) =
    BinaryCofan.inl c ≫ s.ι.app WalkingSpan.right
case mp.intro.refine'_1.h₁
J : Type v'
inst✝¹ : Category J
C : Type u
inst✝ : Category C
W X✝ Y✝ Z : C
f✝ : W ⟶ X✝
g : W ⟶ Y✝
h✝ : X✝ ⟶ Z
i : Y✝ ⟶ Z
X E Y YE : C
c : BinaryCofan X E
hc : IsColimit c
f : X ⟶ Y
iY : Y ⟶ YE
fE : c.pt ⟶ YE
H : CommSq f (BinaryCofan.inl c) iY fE
h : IsColimit (BinaryCofan.mk (BinaryCofan.inr c ≫ fE) iY)
s : PushoutCocone f (BinaryCofan.inl c)
⊢ BinaryCofan.inl c ≫
      fE ≫ IsColimit.desc h (BinaryCofan.mk (BinaryCofan.inr c ≫ PushoutCocone.inr s) (PushoutCocone.inl s)) =
    BinaryCofan.inl c ≫ s.ι.app WalkingSpan.right
rw [← H.w_assoc]
case mp.intro.refine'_1.h₁
J : Type v'
inst✝¹ : Category J
C : Type u
inst✝ : Category C
W X✝ Y✝ Z : C
f✝ : W ⟶ X✝
g : W ⟶ Y✝
h✝ : X✝ ⟶ Z
i : Y✝ ⟶ Z
X E Y YE : C
c : BinaryCofan X E
hc : IsColimit c
f : X ⟶ Y
iY : Y ⟶ YE
fE : c.pt ⟶ YE
H : CommSq f (BinaryCofan.inl c) iY fE
h : IsColimit (BinaryCofan.mk (BinaryCofan.inr c ≫ fE) iY)
s : PushoutCocone f (BinaryCofan.inl c)
⊢ f ≫
      (BinaryCofan.mk (BinaryCofan.inr c ≫ PushoutCocone.inr s) (PushoutCocone.inl s)).ι.app
        { as := WalkingPair.right } =
    BinaryCofan.inl c ≫ s.ι.app WalkingSpan.right
case mp.intro.refine'_1.h₁
J : Type v'
inst✝¹ : Category J
C : Type u
inst✝ : Category C
W X✝ Y✝ Z : C
f✝ : W ⟶ X✝
g : W ⟶ Y✝
h✝ : X✝ ⟶ Z
i : Y✝ ⟶ Z
X E Y YE : C
c : BinaryCofan X E
hc : IsColimit c
f : X ⟶ Y
iY : Y ⟶ YE
fE : c.pt ⟶ YE
H : CommSq f (BinaryCofan.inl c) iY fE
h : IsColimit (BinaryCofan.mk (BinaryCofan.inr c ≫ fE) iY)
s : PushoutCocone f (BinaryCofan.inl c)
⊢ f ≫ iY ≫ IsColimit.desc h (BinaryCofan.mk (BinaryCofan.inr c ≫ PushoutCocone.inr s) (PushoutCocone.inl s)) =
    BinaryCofan.inl c ≫ s.ι.app WalkingSpan.right
erw [h.fac _ ⟨WalkingPair.right⟩]
no goals
case mp.intro.refine'_1.h₁
J : Type v'
inst✝¹ : Category J
C : Type u
inst✝ : Category C
W X✝ Y✝ Z : C
f✝ : W ⟶ X✝
g : W ⟶ Y✝
h✝ : X✝ ⟶ Z
i : Y✝ ⟶ Z
X E Y YE : C
c : BinaryCofan X E
hc : IsColimit c
f : X ⟶ Y
iY : Y ⟶ YE
fE : c.pt ⟶ YE
H : CommSq f (BinaryCofan.inl c) iY fE
h : IsColimit (BinaryCofan.mk (BinaryCofan.inr c ≫ fE) iY)
s : PushoutCocone f (BinaryCofan.inl c)
⊢ f ≫
      (BinaryCofan.mk (BinaryCofan.inr c ≫ PushoutCocone.inr s) (PushoutCocone.inl s)).ι.app
        { as := WalkingPair.right } =
    BinaryCofan.inl c ≫ s.ι.app WalkingSpan.right
exact s.condition
case mp.intro.refine'_1.h₂
J : Type v'
inst✝¹ : Category J
C : Type u
inst✝ : Category C
W X✝ Y✝ Z : C
f✝ : W ⟶ X✝
g : W ⟶ Y✝
h✝ : X✝ ⟶ Z
i : Y✝ ⟶ Z
X E Y YE : C
c : BinaryCofan X E
hc : IsColimit c
f : X ⟶ Y
iY : Y ⟶ YE
fE : c.pt ⟶ YE
H : CommSq f (BinaryCofan.inl c) iY fE
h : IsColimit (BinaryCofan.mk (BinaryCofan.inr c ≫ fE) iY)
s : PushoutCocone f (BinaryCofan.inl c)
⊢ (BinaryCofan.inr c ≫ fE) ≫
      IsColimit.desc h (BinaryCofan.mk (BinaryCofan.inr c ≫ PushoutCocone.inr s) (PushoutCocone.inl s)) =
    BinaryCofan.inr c ≫ s.ι.app WalkingSpan.right
case mp.intro.refine'_1.h₂
J : Type v'
inst✝¹ : Category J
C : Type u
inst✝ : Category C
W X✝ Y✝ Z : C
f✝ : W ⟶ X✝
g : W ⟶ Y✝
h✝ : X✝ ⟶ Z
i : Y✝ ⟶ Z
X E Y YE : C
c : BinaryCofan X E
hc : IsColimit c
f : X ⟶ Y
iY : Y ⟶ YE
fE : c.pt ⟶ YE
H : CommSq f (BinaryCofan.inl c) iY fE
h : IsColimit (BinaryCofan.mk (BinaryCofan.inr c ≫ fE) iY)
s : PushoutCocone f (BinaryCofan.inl c)
⊢ BinaryCofan.inr c ≫
      fE ≫ IsColimit.desc h (BinaryCofan.mk (BinaryCofan.inr c ≫ PushoutCocone.inr s) (PushoutCocone.inl s)) =
    BinaryCofan.inr c ≫ s.ι.app WalkingSpan.right
rw [← Category.assoc]
no goals
case mp.intro.refine'_1.h₂
J : Type v'
inst✝¹ : Category J
C : Type u
inst✝ : Category C
W X✝ Y✝ Z : C
f✝ : W ⟶ X✝
g : W ⟶ Y✝
h✝ : X✝ ⟶ Z
i : Y✝ ⟶ Z
X E Y YE : C
c : BinaryCofan X E
hc : IsColimit c
f : X ⟶ Y
iY : Y ⟶ YE
fE : c.pt ⟶ YE
H : CommSq f (BinaryCofan.inl c) iY fE
h : IsColimit (BinaryCofan.mk (BinaryCofan.inr c ≫ fE) iY)
s : PushoutCocone f (BinaryCofan.inl c)
⊢ (BinaryCofan.inr c ≫ fE) ≫
      IsColimit.desc h (BinaryCofan.mk (BinaryCofan.inr c ≫ PushoutCocone.inr s) (PushoutCocone.inl s)) =
    BinaryCofan.inr c ≫ s.ι.app WalkingSpan.right
exact h.fac _ ⟨WalkingPair.left⟩
case mp.intro.refine'_2
J : Type v'
inst✝¹ : Category J
C : Type u
inst✝ : Category C
W X✝ Y✝ Z : C
f✝ : W ⟶ X✝
g : W ⟶ Y✝
h✝ : X✝ ⟶ Z
i : Y✝ ⟶ Z
X E Y YE : C
c : BinaryCofan X E
hc : IsColimit c
f : X ⟶ Y
iY : Y ⟶ YE
fE : c.pt ⟶ YE
H : CommSq f (BinaryCofan.inl c) iY fE
h : IsColimit (BinaryCofan.mk (BinaryCofan.inr c ≫ fE) iY)
s : PushoutCocone f (BinaryCofan.inl c)
m : YE ⟶ s.pt
e₁ :
  PushoutCocone.inl
        { pt := YE, ι := NatTrans.mk fun j => Option.rec (f ≫ iY) (fun val => WalkingPair.rec iY fE val) j } ≫
      m =
    PushoutCocone.inl s
e₂ : fE ≫ m = s.ι.app WalkingSpan.right
⊢ m = IsColimit.desc h (BinaryCofan.mk (BinaryCofan.inr c ≫ PushoutCocone.inr s) (PushoutCocone.inl s))
case mp.intro.refine'_2
J : Type v'
inst✝¹ : Category J
C : Type u
inst✝ : Category C
W X✝ Y✝ Z : C
f✝ : W ⟶ X✝
g : W ⟶ Y✝
h✝ : X✝ ⟶ Z
i : Y✝ ⟶ Z
X E Y YE : C
c : BinaryCofan X E
hc : IsColimit c
f : X ⟶ Y
iY : Y ⟶ YE
fE : c.pt ⟶ YE
H : CommSq f (BinaryCofan.inl c) iY fE
h : IsColimit (BinaryCofan.mk (BinaryCofan.inr c ≫ fE) iY)
s : PushoutCocone f (BinaryCofan.inl c)
⊢ ∀ {m : YE ⟶ s.pt},
    PushoutCocone.inl
            { pt := YE, ι := NatTrans.mk fun j => Option.rec (f ≫ iY) (fun val => WalkingPair.rec iY fE val) j } ≫
          m =
        PushoutCocone.inl s →
      fE ≫ m = s.ι.app WalkingSpan.right →
        m = IsColimit.desc h (BinaryCofan.mk (BinaryCofan.inr c ≫ PushoutCocone.inr s) (PushoutCocone.inl s))
intro m e₁ e₂
case mp.intro.refine'_2.h₁
J : Type v'
inst✝¹ : Category J
C : Type u
inst✝ : Category C
W X✝ Y✝ Z : C
f✝ : W ⟶ X✝
g : W ⟶ Y✝
h✝ : X✝ ⟶ Z
i : Y✝ ⟶ Z
X E Y YE : C
c : BinaryCofan X E
hc : IsColimit c
f : X ⟶ Y
iY : Y ⟶ YE
fE : c.pt ⟶ YE
H : CommSq f (BinaryCofan.inl c) iY fE
h : IsColimit (BinaryCofan.mk (BinaryCofan.inr c ≫ fE) iY)
s : PushoutCocone f (BinaryCofan.inl c)
m : YE ⟶ s.pt
e₁ :
  PushoutCocone.inl
        { pt := YE, ι := NatTrans.mk fun j => Option.rec (f ≫ iY) (fun val => WalkingPair.rec iY fE val) j } ≫
      m =
    PushoutCocone.inl s
e₂ : fE ≫ m = s.ι.app WalkingSpan.right
⊢ BinaryCofan.inl (BinaryCofan.mk (BinaryCofan.inr c ≫ fE) iY) ≫ m =
    BinaryCofan.inl (BinaryCofan.mk (BinaryCofan.inr c ≫ fE) iY) ≫
      IsColimit.desc h (BinaryCofan.mk (BinaryCofan.inr c ≫ PushoutCocone.inr s) (PushoutCocone.inl s))

case mp.intro.refine'_2.h₂
J : Type v'
inst✝¹ : Category J
C : Type u
inst✝ : Category C
W X✝ Y✝ Z : C
f✝ : W ⟶ X✝
g : W ⟶ Y✝
h✝ : X✝ ⟶ Z
i : Y✝ ⟶ Z
X E Y YE : C
c : BinaryCofan X E
hc : IsColimit c
f : X ⟶ Y
iY : Y ⟶ YE
fE : c.pt ⟶ YE
H : CommSq f (BinaryCofan.inl c) iY fE
h : IsColimit (BinaryCofan.mk (BinaryCofan.inr c ≫ fE) iY)
s : PushoutCocone f (BinaryCofan.inl c)
m : YE ⟶ s.pt
e₁ :
  PushoutCocone.inl
        { pt := YE, ι := NatTrans.mk fun j => Option.rec (f ≫ iY) (fun val => WalkingPair.rec iY fE val) j } ≫
      m =
    PushoutCocone.inl s
e₂ : fE ≫ m = s.ι.app WalkingSpan.right
⊢ BinaryCofan.inr (BinaryCofan.mk (BinaryCofan.inr c ≫ fE) iY) ≫ m =
    BinaryCofan.inr (BinaryCofan.mk (BinaryCofan.inr c ≫ fE) iY) ≫
      IsColimit.desc h (BinaryCofan.mk (BinaryCofan.inr c ≫ PushoutCocone.inr s) (PushoutCocone.inl s))
case mp.intro.refine'_2
J : Type v'
inst✝¹ : Category J
C : Type u
inst✝ : Category C
W X✝ Y✝ Z : C
f✝ : W ⟶ X✝
g : W ⟶ Y✝
h✝ : X✝ ⟶ Z
i : Y✝ ⟶ Z
X E Y YE : C
c : BinaryCofan X E
hc : IsColimit c
f : X ⟶ Y
iY : Y ⟶ YE
fE : c.pt ⟶ YE
H : CommSq f (BinaryCofan.inl c) iY fE
h : IsColimit (BinaryCofan.mk (BinaryCofan.inr c ≫ fE) iY)
s : PushoutCocone f (BinaryCofan.inl c)
m : YE ⟶ s.pt
e₁ :
  PushoutCocone.inl
        { pt := YE, ι := NatTrans.mk fun j => Option.rec (f ≫ iY) (fun val => WalkingPair.rec iY fE val) j } ≫
      m =
    PushoutCocone.inl s
e₂ : fE ≫ m = s.ι.app WalkingSpan.right
⊢ m = IsColimit.desc h (BinaryCofan.mk (BinaryCofan.inr c ≫ PushoutCocone.inr s) (PushoutCocone.inl s))
apply BinaryCofan.IsColimit.hom_ext h
case mp.intro.refine'_2.h₁
J : Type v'
inst✝¹ : Category J
C : Type u
inst✝ : Category C
W X✝ Y✝ Z : C
f✝ : W ⟶ X✝
g : W ⟶ Y✝
h✝ : X✝ ⟶ Z
i : Y✝ ⟶ Z
X E Y YE : C
c : BinaryCofan X E
hc : IsColimit c
f : X ⟶ Y
iY : Y ⟶ YE
fE : c.pt ⟶ YE
H : CommSq f (BinaryCofan.inl c) iY fE
h : IsColimit (BinaryCofan.mk (BinaryCofan.inr c ≫ fE) iY)
s : PushoutCocone f (BinaryCofan.inl c)
m : YE ⟶ s.pt
e₁ :
  PushoutCocone.inl
        { pt := YE, ι := NatTrans.mk fun j => Option.rec (f ≫ iY) (fun val => WalkingPair.rec iY fE val) j } ≫
      m =
    PushoutCocone.inl s
e₂ : fE ≫ m = s.ι.app WalkingSpan.right
⊢ BinaryCofan.inl
        { pt := YE,
          ι :=
            NatTrans.mk fun x =>
              WalkingPair.rec (motive := fun t =>
                x.as = t →
                  ((pair ((pair X E).obj { as := WalkingPair.right }) Y).obj { as := x.as } ⟶
                    ((Functor.const (Discrete WalkingPair)).obj YE).obj { as := x.as }))
                (fun h => (_ : WalkingPair.left = x.as) ▸ BinaryCofan.inr c ≫ fE)
                (fun h => (_ : WalkingPair.right = x.as) ▸ iY) x.as (_ : x.as = x.as) } ≫
      m =
    BinaryCofan.inl
        { pt := YE,
          ι :=
            NatTrans.mk fun x =>
              WalkingPair.rec (motive := fun t =>
                x.as = t →
                  ((pair ((pair X E).obj { as := WalkingPair.right }) Y).obj { as := x.as } ⟶
                    ((Functor.const (Discrete WalkingPair)).obj YE).obj { as := x.as }))
                (fun h => (_ : WalkingPair.left = x.as) ▸ BinaryCofan.inr c ≫ fE)
                (fun h => (_ : WalkingPair.right = x.as) ▸ iY) x.as (_ : x.as = x.as) } ≫
      IsColimit.desc h
        { pt := s.pt,
          ι :=
            NatTrans.mk fun x =>
              WalkingPair.rec (motive := fun t =>
                x.as = t →
                  ((pair ((pair X E).obj { as := WalkingPair.right }) Y).obj { as := x.as } ⟶
                    ((Functor.const (Discrete WalkingPair)).obj s.pt).obj { as := x.as }))
                (fun h => (_ : WalkingPair.left = x.as) ▸ BinaryCofan.inr c ≫ PushoutCocone.inr s)
                (fun h => (_ : WalkingPair.right = x.as) ▸ PushoutCocone.inl s) x.as (_ : x.as = x.as) }
case mp.intro.refine'_2.h₁
J : Type v'
inst✝¹ : Category J
C : Type u
inst✝ : Category C
W X✝ Y✝ Z : C
f✝ : W ⟶ X✝
g : W ⟶ Y✝
h✝ : X✝ ⟶ Z
i : Y✝ ⟶ Z
X E Y YE : C
c : BinaryCofan X E
hc : IsColimit c
f : X ⟶ Y
iY : Y ⟶ YE
fE : c.pt ⟶ YE
H : CommSq f (BinaryCofan.inl c) iY fE
h : IsColimit (BinaryCofan.mk (BinaryCofan.inr c ≫ fE) iY)
s : PushoutCocone f (BinaryCofan.inl c)
m : YE ⟶ s.pt
e₁ :
  PushoutCocone.inl
        { pt := YE, ι := NatTrans.mk fun j => Option.rec (f ≫ iY) (fun val => WalkingPair.rec iY fE val) j } ≫
      m =
    PushoutCocone.inl s
e₂ : fE ≫ m = s.ι.app WalkingSpan.right
⊢ BinaryCofan.inl (BinaryCofan.mk (BinaryCofan.inr c ≫ fE) iY) ≫ m =
    BinaryCofan.inl (BinaryCofan.mk (BinaryCofan.inr c ≫ fE) iY) ≫
      IsColimit.desc h (BinaryCofan.mk (BinaryCofan.inr c ≫ PushoutCocone.inr s) (PushoutCocone.inl s))
dsimp only [BinaryCofan.mk, id]
case mp.intro.refine'_2.h₁
J : Type v'
inst✝¹ : Category J
C : Type u
inst✝ : Category C
W X✝ Y✝ Z : C
f✝ : W ⟶ X✝
g : W ⟶ Y✝
h✝ : X✝ ⟶ Z
i : Y✝ ⟶ Z
X E Y YE : C
c : BinaryCofan X E
hc : IsColimit c
f : X ⟶ Y
iY : Y ⟶ YE
fE : c.pt ⟶ YE
H : CommSq f (BinaryCofan.inl c) iY fE
h : IsColimit (BinaryCofan.mk (BinaryCofan.inr c ≫ fE) iY)
s : PushoutCocone f (BinaryCofan.inl c)
m : YE ⟶ s.pt
e₁ :
  PushoutCocone.inl
        { pt := YE, ι := NatTrans.mk fun j => Option.rec (f ≫ iY) (fun val => WalkingPair.rec iY fE val) j } ≫
      m =
    PushoutCocone.inl s
e₂ : fE ≫ m = s.ι.app WalkingSpan.right
⊢ BinaryCofan.inl
        { pt := YE,
          ι :=
            NatTrans.mk fun x =>
              WalkingPair.rec (motive := fun t =>
                x.as = t →
                  ((pair ((pair X E).obj { as := WalkingPair.right }) Y).obj { as := x.as } ⟶
                    ((Functor.const (Discrete WalkingPair)).obj YE).obj { as := x.as }))
                (fun h => (_ : WalkingPair.left = x.as) ▸ BinaryCofan.inr c ≫ fE)
                (fun h => (_ : WalkingPair.right = x.as) ▸ iY) x.as (_ : x.as = x.as) } ≫
      IsColimit.desc h
        { pt := s.pt,
          ι :=
            NatTrans.mk fun x =>
              WalkingPair.rec (motive := fun t =>
                x.as = t →
                  ((pair ((pair X E).obj { as := WalkingPair.right }) Y).obj { as := x.as } ⟶
                    ((Functor.const (Discrete WalkingPair)).obj s.pt).obj { as := x.as }))
                (fun h => (_ : WalkingPair.left = x.as) ▸ BinaryCofan.inr c ≫ PushoutCocone.inr s)
                (fun h => (_ : WalkingPair.right = x.as) ▸ PushoutCocone.inl s) x.as (_ : x.as = x.as) } =
    BinaryCofan.inr c ≫ s.ι.app WalkingSpan.right
case mp.intro.refine'_2.h₁
J : Type v'
inst✝¹ : Category J
C : Type u
inst✝ : Category C
W X✝ Y✝ Z : C
f✝ : W ⟶ X✝
g : W ⟶ Y✝
h✝ : X✝ ⟶ Z
i : Y✝ ⟶ Z
X E Y YE : C
c : BinaryCofan X E
hc : IsColimit c
f : X ⟶ Y
iY : Y ⟶ YE
fE : c.pt ⟶ YE
H : CommSq f (BinaryCofan.inl c) iY fE
h : IsColimit (BinaryCofan.mk (BinaryCofan.inr c ≫ fE) iY)
s : PushoutCocone f (BinaryCofan.inl c)
m : YE ⟶ s.pt
e₁ :
  PushoutCocone.inl
        { pt := YE, ι := NatTrans.mk fun j => Option.rec (f ≫ iY) (fun val => WalkingPair.rec iY fE val) j } ≫
      m =
    PushoutCocone.inl s
e₂ : fE ≫ m = s.ι.app WalkingSpan.right
⊢ BinaryCofan.inl
        { pt := YE,
          ι :=
            NatTrans.mk fun x =>
              WalkingPair.rec (motive := fun t =>
                x.as = t →
                  ((pair ((pair X E).obj { as := WalkingPair.right }) Y).obj { as := x.as } ⟶
                    ((Functor.const (Discrete WalkingPair)).obj YE).obj { as := x.as }))
                (fun h => (_ : WalkingPair.left = x.as) ▸ BinaryCofan.inr c ≫ fE)
                (fun h => (_ : WalkingPair.right = x.as) ▸ iY) x.as (_ : x.as = x.as) } ≫
      m =
    BinaryCofan.inl
        { pt := YE,
          ι :=
            NatTrans.mk fun x =>
              WalkingPair.rec (motive := fun t =>
                x.as = t →
                  ((pair ((pair X E).obj { as := WalkingPair.right }) Y).obj { as := x.as } ⟶
                    ((Functor.const (Discrete WalkingPair)).obj YE).obj { as := x.as }))
                (fun h => (_ : WalkingPair.left = x.as) ▸ BinaryCofan.inr c ≫ fE)
                (fun h => (_ : WalkingPair.right = x.as) ▸ iY) x.as (_ : x.as = x.as) } ≫
      IsColimit.desc h
        { pt := s.pt,
          ι :=
            NatTrans.mk fun x =>
              WalkingPair.rec (motive := fun t =>
                x.as = t →
                  ((pair ((pair X E).obj { as := WalkingPair.right }) Y).obj { as := x.as } ⟶
                    ((Functor.const (Discrete WalkingPair)).obj s.pt).obj { as := x.as }))
                (fun h => (_ : WalkingPair.left = x.as) ▸ BinaryCofan.inr c ≫ PushoutCocone.inr s)
                (fun h => (_ : WalkingPair.right = x.as) ▸ PushoutCocone.inl s) x.as (_ : x.as = x.as) }
rw [Category.assoc, e₂, eq_comm]
no goals
case mp.intro.refine'_2.h₁
J : Type v'
inst✝¹ : Category J
C : Type u
inst✝ : Category C
W X✝ Y✝ Z : C
f✝ : W ⟶ X✝
g : W ⟶ Y✝
h✝ : X✝ ⟶ Z
i : Y✝ ⟶ Z
X E Y YE : C
c : BinaryCofan X E
hc : IsColimit c
f : X ⟶ Y
iY : Y ⟶ YE
fE : c.pt ⟶ YE
H : CommSq f (BinaryCofan.inl c) iY fE
h : IsColimit (BinaryCofan.mk (BinaryCofan.inr c ≫ fE) iY)
s : PushoutCocone f (BinaryCofan.inl c)
m : YE ⟶ s.pt
e₁ :
  PushoutCocone.inl
        { pt := YE, ι := NatTrans.mk fun j => Option.rec (f ≫ iY) (fun val => WalkingPair.rec iY fE val) j } ≫
      m =
    PushoutCocone.inl s
e₂ : fE ≫ m = s.ι.app WalkingSpan.right
⊢ BinaryCofan.inl
        { pt := YE,
          ι :=
            NatTrans.mk fun x =>
              WalkingPair.rec (motive := fun t =>
                x.as = t →
                  ((pair ((pair X E).obj { as := WalkingPair.right }) Y).obj { as := x.as } ⟶
                    ((Functor.const (Discrete WalkingPair)).obj YE).obj { as := x.as }))
                (fun h => (_ : WalkingPair.left = x.as) ▸ BinaryCofan.inr c ≫ fE)
                (fun h => (_ : WalkingPair.right = x.as) ▸ iY) x.as (_ : x.as = x.as) } ≫
      IsColimit.desc h
        { pt := s.pt,
          ι :=
            NatTrans.mk fun x =>
              WalkingPair.rec (motive := fun t =>
                x.as = t →
                  ((pair ((pair X E).obj { as := WalkingPair.right }) Y).obj { as := x.as } ⟶
                    ((Functor.const (Discrete WalkingPair)).obj s.pt).obj { as := x.as }))
                (fun h => (_ : WalkingPair.left = x.as) ▸ BinaryCofan.inr c ≫ PushoutCocone.inr s)
                (fun h => (_ : WalkingPair.right = x.as) ▸ PushoutCocone.inl s) x.as (_ : x.as = x.as) } =
    BinaryCofan.inr c ≫ s.ι.app WalkingSpan.right
exact h.fac _ ⟨WalkingPair.left⟩
case mp.intro.refine'_2.h₂
J : Type v'
inst✝¹ : Category J
C : Type u
inst✝ : Category C
W X✝ Y✝ Z : C
f✝ : W ⟶ X✝
g : W ⟶ Y✝
h✝ : X✝ ⟶ Z
i : Y✝ ⟶ Z
X E Y YE : C
c : BinaryCofan X E
hc : IsColimit c
f : X ⟶ Y
iY : Y ⟶ YE
fE : c.pt ⟶ YE
H : CommSq f (BinaryCofan.inl c) iY fE
h : IsColimit (BinaryCofan.mk (BinaryCofan.inr c ≫ fE) iY)
s : PushoutCocone f (BinaryCofan.inl c)
m : YE ⟶ s.pt
e₁ :
  PushoutCocone.inl
        { pt := YE, ι := NatTrans.mk fun j => Option.rec (f ≫ iY) (fun val => WalkingPair.rec iY fE val) j } ≫
      m =
    PushoutCocone.inl s
e₂ : fE ≫ m = s.ι.app WalkingSpan.right
⊢ BinaryCofan.inr (BinaryCofan.mk (BinaryCofan.inr c ≫ fE) iY) ≫
      IsColimit.desc h (BinaryCofan.mk (BinaryCofan.inr c ≫ PushoutCocone.inr s) (PushoutCocone.inl s)) =
    PushoutCocone.inl s
case mp.intro.refine'_2.h₂
J : Type v'
inst✝¹ : Category J
C : Type u
inst✝ : Category C
W X✝ Y✝ Z : C
f✝ : W ⟶ X✝
g : W ⟶ Y✝
h✝ : X✝ ⟶ Z
i : Y✝ ⟶ Z
X E Y YE : C
c : BinaryCofan X E
hc : IsColimit c
f : X ⟶ Y
iY : Y ⟶ YE
fE : c.pt ⟶ YE
H : CommSq f (BinaryCofan.inl c) iY fE
h : IsColimit (BinaryCofan.mk (BinaryCofan.inr c ≫ fE) iY)
s : PushoutCocone f (BinaryCofan.inl c)
m : YE ⟶ s.pt
e₁ :
  PushoutCocone.inl
        { pt := YE, ι := NatTrans.mk fun j => Option.rec (f ≫ iY) (fun val => WalkingPair.rec iY fE val) j } ≫
      m =
    PushoutCocone.inl s
e₂ : fE ≫ m = s.ι.app WalkingSpan.right
⊢ BinaryCofan.inr (BinaryCofan.mk (BinaryCofan.inr c ≫ fE) iY) ≫ m =
    BinaryCofan.inr (BinaryCofan.mk (BinaryCofan.inr c ≫ fE) iY) ≫
      IsColimit.desc h (BinaryCofan.mk (BinaryCofan.inr c ≫ PushoutCocone.inr s) (PushoutCocone.inl s))
refine' e₁.trans (Eq.symm _)
no goals
case mp.intro.refine'_2.h₂
J : Type v'
inst✝¹ : Category J
C : Type u
inst✝ : Category C
W X✝ Y✝ Z : C
f✝ : W ⟶ X✝
g : W ⟶ Y✝
h✝ : X✝ ⟶ Z
i : Y✝ ⟶ Z
X E Y YE : C
c : BinaryCofan X E
hc : IsColimit c
f : X ⟶ Y
iY : Y ⟶ YE
fE : c.pt ⟶ YE
H : CommSq f (BinaryCofan.inl c) iY fE
h : IsColimit (BinaryCofan.mk (BinaryCofan.inr c ≫ fE) iY)
s : PushoutCocone f (BinaryCofan.inl c)
m : YE ⟶ s.pt
e₁ :
  PushoutCocone.inl
        { pt := YE, ι := NatTrans.mk fun j => Option.rec (f ≫ iY) (fun val => WalkingPair.rec iY fE val) j } ≫
      m =
    PushoutCocone.inl s
e₂ : fE ≫ m = s.ι.app WalkingSpan.right
⊢ BinaryCofan.inr (BinaryCofan.mk (BinaryCofan.inr c ≫ fE) iY) ≫
      IsColimit.desc h (BinaryCofan.mk (BinaryCofan.inr c ≫ PushoutCocone.inr s) (PushoutCocone.inl s)) =
    PushoutCocone.inl s
exact h.fac _ _
case mpr
J : Type v'
inst✝¹ : Category J
C : Type u
inst✝ : Category C
W X✝ Y✝ Z : C
f✝ : W ⟶ X✝
g : W ⟶ Y✝
h : X✝ ⟶ Z
i : Y✝ ⟶ Z
X E Y YE : C
c : BinaryCofan X E
hc : IsColimit c
f : X ⟶ Y
iY : Y ⟶ YE
fE : c.pt ⟶ YE
H✝ : CommSq f (BinaryCofan.inl c) iY fE
H : IsPushout f (BinaryCofan.inl c) iY fE
⊢ IsColimit (BinaryCofan.mk (BinaryCofan.inr c ≫ fE) iY)
case mpr
J : Type v'
inst✝¹ : Category J
C : Type u
inst✝ : Category C
W X✝ Y✝ Z : C
f✝ : W ⟶ X✝
g : W ⟶ Y✝
h : X✝ ⟶ Z
i : Y✝ ⟶ Z
X E Y YE : C
c : BinaryCofan X E
hc : IsColimit c
f : X ⟶ Y
iY : Y ⟶ YE
fE : c.pt ⟶ YE
H : CommSq f (BinaryCofan.inl c) iY fE
⊢ IsPushout f (BinaryCofan.inl c) iY fE → Nonempty (IsColimit (BinaryCofan.mk (BinaryCofan.inr c ≫ fE) iY))
refine' fun H => ⟨_⟩
case mpr.desc
J : Type v'
inst✝¹ : Category J
C : Type u
inst✝ : Category C
W X✝ Y✝ Z : C
f✝ : W ⟶ X✝
g : W ⟶ Y✝
h : X✝ ⟶ Z
i : Y✝ ⟶ Z
X E Y YE : C
c : BinaryCofan X E
hc : IsColimit c
f : X ⟶ Y
iY : Y ⟶ YE
fE : c.pt ⟶ YE
H✝ : CommSq f (BinaryCofan.inl c) iY fE
H : IsPushout f (BinaryCofan.inl c) iY fE
⊢ (s : BinaryCofan ((pair X E).obj { as := WalkingPair.right }) Y) → YE ⟶ s.pt

case mpr.fac_left
J : Type v'
inst✝¹ : Category J
C : Type u
inst✝ : Category C
W X✝ Y✝ Z : C
f✝ : W ⟶ X✝
g : W ⟶ Y✝
h : X✝ ⟶ Z
i : Y✝ ⟶ Z
X E Y YE : C
c : BinaryCofan X E
hc : IsColimit c
f : X ⟶ Y
iY : Y ⟶ YE
fE : c.pt ⟶ YE
H✝ : CommSq f (BinaryCofan.inl c) iY fE
H : IsPushout f (BinaryCofan.inl c) iY fE
⊢ ∀ (s : BinaryCofan ((pair X E).obj { as := WalkingPair.right }) Y),
    (BinaryCofan.inr c ≫ fE) ≫ ?mpr.desc s = BinaryCofan.inl s

case mpr.fac_right
J : Type v'
inst✝¹ : Category J
C : Type u
inst✝ : Category C
W X✝ Y✝ Z : C
f✝ : W ⟶ X✝
g : W ⟶ Y✝
h : X✝ ⟶ Z
i : Y✝ ⟶ Z
X E Y YE : C
c : BinaryCofan X E
hc : IsColimit c
f : X ⟶ Y
iY : Y ⟶ YE
fE : c.pt ⟶ YE
H✝ : CommSq f (BinaryCofan.inl c) iY fE
H : IsPushout f (BinaryCofan.inl c) iY fE
⊢ ∀ (s : BinaryCofan ((pair X E).obj { as := WalkingPair.right }) Y), iY ≫ ?mpr.desc s = BinaryCofan.inr s

case mpr.uniq
J : Type v'
inst✝¹ : Category J
C : Type u
inst✝ : Category C
W X✝ Y✝ Z : C
f✝ : W ⟶ X✝
g : W ⟶ Y✝
h : X✝ ⟶ Z
i : Y✝ ⟶ Z
X E Y YE : C
c : BinaryCofan X E
hc : IsColimit c
f : X ⟶ Y
iY : Y ⟶ YE
fE : c.pt ⟶ YE
H✝ : CommSq f (BinaryCofan.inl c) iY fE
H : IsPushout f (BinaryCofan.inl c) iY fE
⊢ ∀ (s : BinaryCofan ((pair X E).obj { as := WalkingPair.right }) Y) (m : YE ⟶ s.pt),
    (BinaryCofan.inr c ≫ fE) ≫ m = BinaryCofan.inl s → iY ≫ m = BinaryCofan.inr s → m = ?mpr.desc s
case mpr
J : Type v'
inst✝¹ : Category J
C : Type u
inst✝ : Category C
W X✝ Y✝ Z : C
f✝ : W ⟶ X✝
g : W ⟶ Y✝
h : X✝ ⟶ Z
i : Y✝ ⟶ Z
X E Y YE : C
c : BinaryCofan X E
hc : IsColimit c
f : X ⟶ Y
iY : Y ⟶ YE
fE : c.pt ⟶ YE
H✝ : CommSq f (BinaryCofan.inl c) iY fE
H : IsPushout f (BinaryCofan.inl c) iY fE
⊢ IsColimit (BinaryCofan.mk (BinaryCofan.inr c ≫ fE) iY)
fapply Limits.BinaryCofan.isColimitMk
no goals
case mpr.desc
J : Type v'
inst✝¹ : Category J
C : Type u
inst✝ : Category C
W X✝ Y✝ Z : C
f✝ : W ⟶ X✝
g : W ⟶ Y✝
h : X✝ ⟶ Z
i : Y✝ ⟶ Z
X E Y YE : C
c : BinaryCofan X E
hc : IsColimit c
f : X ⟶ Y
iY : Y ⟶ YE
fE : c.pt ⟶ YE
H✝ : CommSq f (BinaryCofan.inl c) iY fE
H : IsPushout f (BinaryCofan.inl c) iY fE
⊢ (s : BinaryCofan ((pair X E).obj { as := WalkingPair.right }) Y) → YE ⟶ s.pt
exact fun s => H.isColimit.desc (PushoutCocone.mk s.inr _ <|
  (hc.fac (BinaryCofan.mk (f ≫ s.inr) s.inl) ⟨WalkingPair.left⟩).symm)
case mpr.fac_left
J : Type v'
inst✝¹ : Category J
C : Type u
inst✝ : Category C
W X✝ Y✝ Z : C
f✝ : W ⟶ X✝
g : W ⟶ Y✝
h : X✝ ⟶ Z
i : Y✝ ⟶ Z
X E Y YE : C
c : BinaryCofan X E
hc : IsColimit c
f : X ⟶ Y
iY : Y ⟶ YE
fE : c.pt ⟶ YE
H✝ : CommSq f (BinaryCofan.inl c) iY fE
H : IsPushout f (BinaryCofan.inl c) iY fE
s : BinaryCofan ((pair X E).obj { as := WalkingPair.right }) Y
⊢ (BinaryCofan.inr c ≫ fE) ≫
      IsColimit.desc (IsPushout.isColimit H)
        (PushoutCocone.mk (BinaryCofan.inr s)
          (IsColimit.desc hc (BinaryCofan.mk (f ≫ BinaryCofan.inr s) (BinaryCofan.inl s)))
          (_ :
            (BinaryCofan.mk (f ≫ BinaryCofan.inr s) (BinaryCofan.inl s)).ι.app { as := WalkingPair.left } =
              c.ι.app { as := WalkingPair.left } ≫
                IsColimit.desc hc (BinaryCofan.mk (f ≫ BinaryCofan.inr s) (BinaryCofan.inl s)))) =
    BinaryCofan.inl s
case mpr.fac_left
J : Type v'
inst✝¹ : Category J
C : Type u
inst✝ : Category C
W X✝ Y✝ Z : C
f✝ : W ⟶ X✝
g : W ⟶ Y✝
h : X✝ ⟶ Z
i : Y✝ ⟶ Z
X E Y YE : C
c : BinaryCofan X E
hc : IsColimit c
f : X ⟶ Y
iY : Y ⟶ YE
fE : c.pt ⟶ YE
H✝ : CommSq f (BinaryCofan.inl c) iY fE
H : IsPushout f (BinaryCofan.inl c) iY fE
⊢ ∀ (s : BinaryCofan ((pair X E).obj { as := WalkingPair.right }) Y),
    (BinaryCofan.inr c ≫ fE) ≫
        IsColimit.desc (IsPushout.isColimit H)
          (PushoutCocone.mk (BinaryCofan.inr s)
            (IsColimit.desc hc (BinaryCofan.mk (f ≫ BinaryCofan.inr s) (BinaryCofan.inl s)))
            (_ :
              (BinaryCofan.mk (f ≫ BinaryCofan.inr s) (BinaryCofan.inl s)).ι.app { as := WalkingPair.left } =
                c.ι.app { as := WalkingPair.left } ≫
                  IsColimit.desc hc (BinaryCofan.mk (f ≫ BinaryCofan.inr s) (BinaryCofan.inl s)))) =
      BinaryCofan.inl s
intro s
case mpr.fac_left
J : Type v'
inst✝¹ : Category J
C : Type u
inst✝ : Category C
W X✝ Y✝ Z : C
f✝ : W ⟶ X✝
g : W ⟶ Y✝
h : X✝ ⟶ Z
i : Y✝ ⟶ Z
X E Y YE : C
c : BinaryCofan X E
hc : IsColimit c
f : X ⟶ Y
iY : Y ⟶ YE
fE : c.pt ⟶ YE
H✝ : CommSq f (BinaryCofan.inl c) iY fE
H : IsPushout f (BinaryCofan.inl c) iY fE
s : BinaryCofan ((pair X E).obj { as := WalkingPair.right }) Y
⊢ (BinaryCofan.mk (f ≫ BinaryCofan.inr s) (BinaryCofan.inl s)).ι.app { as := WalkingPair.right } = BinaryCofan.inl s
case mpr.fac_left
J : Type v'
inst✝¹ : Category J
C : Type u
inst✝ : Category C
W X✝ Y✝ Z : C
f✝ : W ⟶ X✝
g : W ⟶ Y✝
h : X✝ ⟶ Z
i : Y✝ ⟶ Z
X E Y YE : C
c : BinaryCofan X E
hc : IsColimit c
f : X ⟶ Y
iY : Y ⟶ YE
fE : c.pt ⟶ YE
H✝ : CommSq f (BinaryCofan.inl c) iY fE
H : IsPushout f (BinaryCofan.inl c) iY fE
s : BinaryCofan ((pair X E).obj { as := WalkingPair.right }) Y
⊢ (BinaryCofan.inr c ≫ fE) ≫
      IsColimit.desc (IsPushout.isColimit H)
        (PushoutCocone.mk (BinaryCofan.inr s)
          (IsColimit.desc hc (BinaryCofan.mk (f ≫ BinaryCofan.inr s) (BinaryCofan.inl s)))
          (_ :
            (BinaryCofan.mk (f ≫ BinaryCofan.inr s) (BinaryCofan.inl s)).ι.app { as := WalkingPair.left } =
              c.ι.app { as := WalkingPair.left } ≫
                IsColimit.desc hc (BinaryCofan.mk (f ≫ BinaryCofan.inr s) (BinaryCofan.inl s)))) =
    BinaryCofan.inl s
erw [Category.assoc, H.isColimit.fac _ WalkingSpan.right, hc.fac]
no goals
case mpr.fac_left
J : Type v'
inst✝¹ : Category J
C : Type u
inst✝ : Category C
W X✝ Y✝ Z : C
f✝ : W ⟶ X✝
g : W ⟶ Y✝
h : X✝ ⟶ Z
i : Y✝ ⟶ Z
X E Y YE : C
c : BinaryCofan X E
hc : IsColimit c
f : X ⟶ Y
iY : Y ⟶ YE
fE : c.pt ⟶ YE
H✝ : CommSq f (BinaryCofan.inl c) iY fE
H : IsPushout f (BinaryCofan.inl c) iY fE
s : BinaryCofan ((pair X E).obj { as := WalkingPair.right }) Y
⊢ (BinaryCofan.mk (f ≫ BinaryCofan.inr s) (BinaryCofan.inl s)).ι.app { as := WalkingPair.right } = BinaryCofan.inl s
rfl
case mpr.fac_right
J : Type v'
inst✝¹ : Category J
C : Type u
inst✝ : Category C
W X✝ Y✝ Z : C
f✝ : W ⟶ X✝
g : W ⟶ Y✝
h : X✝ ⟶ Z
i : Y✝ ⟶ Z
X E Y YE : C
c : BinaryCofan X E
hc : IsColimit c
f : X ⟶ Y
iY : Y ⟶ YE
fE : c.pt ⟶ YE
H✝ : CommSq f (BinaryCofan.inl c) iY fE
H : IsPushout f (BinaryCofan.inl c) iY fE
s : BinaryCofan ((pair X E).obj { as := WalkingPair.right }) Y
⊢ iY ≫
      IsColimit.desc (IsPushout.isColimit H)
        (PushoutCocone.mk (BinaryCofan.inr s)
          (IsColimit.desc hc (BinaryCofan.mk (f ≫ BinaryCofan.inr s) (BinaryCofan.inl s)))
          (_ :
            (BinaryCofan.mk (f ≫ BinaryCofan.inr s) (BinaryCofan.inl s)).ι.app { as := WalkingPair.left } =
              c.ι.app { as := WalkingPair.left } ≫
                IsColimit.desc hc (BinaryCofan.mk (f ≫ BinaryCofan.inr s) (BinaryCofan.inl s)))) =
    BinaryCofan.inr s
case mpr.fac_right
J : Type v'
inst✝¹ : Category J
C : Type u
inst✝ : Category C
W X✝ Y✝ Z : C
f✝ : W ⟶ X✝
g : W ⟶ Y✝
h : X✝ ⟶ Z
i : Y✝ ⟶ Z
X E Y YE : C
c : BinaryCofan X E
hc : IsColimit c
f : X ⟶ Y
iY : Y ⟶ YE
fE : c.pt ⟶ YE
H✝ : CommSq f (BinaryCofan.inl c) iY fE
H : IsPushout f (BinaryCofan.inl c) iY fE
⊢ ∀ (s : BinaryCofan ((pair X E).obj { as := WalkingPair.right }) Y),
    iY ≫
        IsColimit.desc (IsPushout.isColimit H)
          (PushoutCocone.mk (BinaryCofan.inr s)
            (IsColimit.desc hc (BinaryCofan.mk (f ≫ BinaryCofan.inr s) (BinaryCofan.inl s)))
            (_ :
              (BinaryCofan.mk (f ≫ BinaryCofan.inr s) (BinaryCofan.inl s)).ι.app { as := WalkingPair.left } =
                c.ι.app { as := WalkingPair.left } ≫
                  IsColimit.desc hc (BinaryCofan.mk (f ≫ BinaryCofan.inr s) (BinaryCofan.inl s)))) =
      BinaryCofan.inr s
intro s
no goals
case mpr.fac_right
J : Type v'
inst✝¹ : Category J
C : Type u
inst✝ : Category C
W X✝ Y✝ Z : C
f✝ : W ⟶ X✝
g : W ⟶ Y✝
h : X✝ ⟶ Z
i : Y✝ ⟶ Z
X E Y YE : C
c : BinaryCofan X E
hc : IsColimit c
f : X ⟶ Y
iY : Y ⟶ YE
fE : c.pt ⟶ YE
H✝ : CommSq f (BinaryCofan.inl c) iY fE
H : IsPushout f (BinaryCofan.inl c) iY fE
s : BinaryCofan ((pair X E).obj { as := WalkingPair.right }) Y
⊢ iY ≫
      IsColimit.desc (IsPushout.isColimit H)
        (PushoutCocone.mk (BinaryCofan.inr s)
          (IsColimit.desc hc (BinaryCofan.mk (f ≫ BinaryCofan.inr s) (BinaryCofan.inl s)))
          (_ :
            (BinaryCofan.mk (f ≫ BinaryCofan.inr s) (BinaryCofan.inl s)).ι.app { as := WalkingPair.left } =
              c.ι.app { as := WalkingPair.left } ≫
                IsColimit.desc hc (BinaryCofan.mk (f ≫ BinaryCofan.inr s) (BinaryCofan.inl s)))) =
    BinaryCofan.inr s
exact H.isColimit.fac _ WalkingSpan.left
case mpr.uniq
J : Type v'
inst✝¹ : Category J
C : Type u
inst✝ : Category C
W X✝ Y✝ Z : C
f✝ : W ⟶ X✝
g : W ⟶ Y✝
h : X✝ ⟶ Z
i : Y✝ ⟶ Z
X E Y YE : C
c : BinaryCofan X E
hc : IsColimit c
f : X ⟶ Y
iY : Y ⟶ YE
fE : c.pt ⟶ YE
H✝ : CommSq f (BinaryCofan.inl c) iY fE
H : IsPushout f (BinaryCofan.inl c) iY fE
s : BinaryCofan ((pair X E).obj { as := WalkingPair.right }) Y
m : YE ⟶ s.pt
e₁ : (BinaryCofan.inr c ≫ fE) ≫ m = BinaryCofan.inl s
e₂ : iY ≫ m = BinaryCofan.inr s
⊢ m =
    IsColimit.desc (IsPushout.isColimit H)
      (PushoutCocone.mk (BinaryCofan.inr s)
        (IsColimit.desc hc (BinaryCofan.mk (f ≫ BinaryCofan.inr s) (BinaryCofan.inl s)))
        (_ :
          (BinaryCofan.mk (f ≫ BinaryCofan.inr s) (BinaryCofan.inl s)).ι.app { as := WalkingPair.left } =
            c.ι.app { as := WalkingPair.left } ≫
              IsColimit.desc hc (BinaryCofan.mk (f ≫ BinaryCofan.inr s) (BinaryCofan.inl s))))
case mpr.uniq
J : Type v'
inst✝¹ : Category J
C : Type u
inst✝ : Category C
W X✝ Y✝ Z : C
f✝ : W ⟶ X✝
g : W ⟶ Y✝
h : X✝ ⟶ Z
i : Y✝ ⟶ Z
X E Y YE : C
c : BinaryCofan X E
hc : IsColimit c
f : X ⟶ Y
iY : Y ⟶ YE
fE : c.pt ⟶ YE
H✝ : CommSq f (BinaryCofan.inl c) iY fE
H : IsPushout f (BinaryCofan.inl c) iY fE
⊢ ∀ (s : BinaryCofan ((pair X E).obj { as := WalkingPair.right }) Y) (m : YE ⟶ s.pt),
    (BinaryCofan.inr c ≫ fE) ≫ m = BinaryCofan.inl s →
      iY ≫ m = BinaryCofan.inr s →
        m =
          IsColimit.desc (IsPushout.isColimit H)
            (PushoutCocone.mk (BinaryCofan.inr s)
              (IsColimit.desc hc (BinaryCofan.mk (f ≫ BinaryCofan.inr s) (BinaryCofan.inl s)))
              (_ :
                (BinaryCofan.mk (f ≫ BinaryCofan.inr s) (BinaryCofan.inl s)).ι.app { as := WalkingPair.left } =
                  c.ι.app { as := WalkingPair.left } ≫
                    IsColimit.desc hc (BinaryCofan.mk (f ≫ BinaryCofan.inr s) (BinaryCofan.inl s))))
intro s m e₁ e₂
case mpr.uniq.h₀
J : Type v'
inst✝¹ : Category J
C : Type u
inst✝ : Category C
W X✝ Y✝ Z : C
f✝ : W ⟶ X✝
g : W ⟶ Y✝
h : X✝ ⟶ Z
i : Y✝ ⟶ Z
X E Y YE : C
c : BinaryCofan X E
hc : IsColimit c
f : X ⟶ Y
iY : Y ⟶ YE
fE : c.pt ⟶ YE
H✝ : CommSq f (BinaryCofan.inl c) iY fE
H : IsPushout f (BinaryCofan.inl c) iY fE
s : BinaryCofan ((pair X E).obj { as := WalkingPair.right }) Y
m : YE ⟶ s.pt
e₁ : (BinaryCofan.inr c ≫ fE) ≫ m = BinaryCofan.inl s
e₂ : iY ≫ m = BinaryCofan.inr s
⊢ PushoutCocone.inl (IsPushout.cocone H) ≫ m =
    PushoutCocone.inl (IsPushout.cocone H) ≫
      IsColimit.desc (IsPushout.isColimit H)
        (PushoutCocone.mk (BinaryCofan.inr s)
          (IsColimit.desc hc (BinaryCofan.mk (f ≫ BinaryCofan.inr s) (BinaryCofan.inl s)))
          (_ :
            (BinaryCofan.mk (f ≫ BinaryCofan.inr s) (BinaryCofan.inl s)).ι.app { as := WalkingPair.left } =
              c.ι.app { as := WalkingPair.left } ≫
                IsColimit.desc hc (BinaryCofan.mk (f ≫ BinaryCofan.inr s) (BinaryCofan.inl s))))

case mpr.uniq.h₁
J : Type v'
inst✝¹ : Category J
C : Type u
inst✝ : Category C
W X✝ Y✝ Z : C
f✝ : W ⟶ X✝
g : W ⟶ Y✝
h : X✝ ⟶ Z
i : Y✝ ⟶ Z
X E Y YE : C
c : BinaryCofan X E
hc : IsColimit c
f : X ⟶ Y
iY : Y ⟶ YE
fE : c.pt ⟶ YE
H✝ : CommSq f (BinaryCofan.inl c) iY fE
H : IsPushout f (BinaryCofan.inl c) iY fE
s : BinaryCofan ((pair X E).obj { as := WalkingPair.right }) Y
m : YE ⟶ s.pt
e₁ : (BinaryCofan.inr c ≫ fE) ≫ m = BinaryCofan.inl s
e₂ : iY ≫ m = BinaryCofan.inr s
⊢ PushoutCocone.inr (IsPushout.cocone H) ≫ m =
    PushoutCocone.inr (IsPushout.cocone H) ≫
      IsColimit.desc (IsPushout.isColimit H)
        (PushoutCocone.mk (BinaryCofan.inr s)
          (IsColimit.desc hc (BinaryCofan.mk (f ≫ BinaryCofan.inr s) (BinaryCofan.inl s)))
          (_ :
            (BinaryCofan.mk (f ≫ BinaryCofan.inr s) (BinaryCofan.inl s)).ι.app { as := WalkingPair.left } =
              c.ι.app { as := WalkingPair.left } ≫
                IsColimit.desc hc (BinaryCofan.mk (f ≫ BinaryCofan.inr s) (BinaryCofan.inl s))))
case mpr.uniq
J : Type v'
inst✝¹ : Category J
C : Type u
inst✝ : Category C
W X✝ Y✝ Z : C
f✝ : W ⟶ X✝
g : W ⟶ Y✝
h : X✝ ⟶ Z
i : Y✝ ⟶ Z
X E Y YE : C
c : BinaryCofan X E
hc : IsColimit c
f : X ⟶ Y
iY : Y ⟶ YE
fE : c.pt ⟶ YE
H✝ : CommSq f (BinaryCofan.inl c) iY fE
H : IsPushout f (BinaryCofan.inl c) iY fE
s : BinaryCofan ((pair X E).obj { as := WalkingPair.right }) Y
m : YE ⟶ s.pt
e₁ : (BinaryCofan.inr c ≫ fE) ≫ m = BinaryCofan.inl s
e₂ : iY ≫ m = BinaryCofan.inr s
⊢ m =
    IsColimit.desc (IsPushout.isColimit H)
      (PushoutCocone.mk (BinaryCofan.inr s)
        (IsColimit.desc hc (BinaryCofan.mk (f ≫ BinaryCofan.inr s) (BinaryCofan.inl s)))
        (_ :
          (BinaryCofan.mk (f ≫ BinaryCofan.inr s) (BinaryCofan.inl s)).ι.app { as := WalkingPair.left } =
            c.ι.app { as := WalkingPair.left } ≫
              IsColimit.desc hc (BinaryCofan.mk (f ≫ BinaryCofan.inr s) (BinaryCofan.inl s))))
apply PushoutCocone.IsColimit.hom_ext H.isColimit
case mpr.uniq.h₀
J : Type v'
inst✝¹ : Category J
C : Type u
inst✝ : Category C
W X✝ Y✝ Z : C
f✝ : W ⟶ X✝
g : W ⟶ Y✝
h : X✝ ⟶ Z
i : Y✝ ⟶ Z
X E Y YE : C
c : BinaryCofan X E
hc : IsColimit c
f : X ⟶ Y
iY : Y ⟶ YE
fE : c.pt ⟶ YE
H✝ : CommSq f (BinaryCofan.inl c) iY fE
H : IsPushout f (BinaryCofan.inl c) iY fE
s : BinaryCofan ((pair X E).obj { as := WalkingPair.right }) Y
m : YE ⟶ s.pt
e₁ : (BinaryCofan.inr c ≫ fE) ≫ m = BinaryCofan.inl s
e₂ : iY ≫ m = BinaryCofan.inr s
⊢ PushoutCocone.inl (IsPushout.cocone H) ≫
      IsColimit.desc (IsPushout.isColimit H)
        (PushoutCocone.mk (BinaryCofan.inr s)
          (IsColimit.desc hc (BinaryCofan.mk (f ≫ BinaryCofan.inr s) (BinaryCofan.inl s)))
          (_ :
            (BinaryCofan.mk (f ≫ BinaryCofan.inr s) (BinaryCofan.inl s)).ι.app { as := WalkingPair.left } =
              c.ι.app { as := WalkingPair.left } ≫
                IsColimit.desc hc (BinaryCofan.mk (f ≫ BinaryCofan.inr s) (BinaryCofan.inl s)))) =
    PushoutCocone.inl (IsPushout.cocone H) ≫ m
case mpr.uniq.h₀
J : Type v'
inst✝¹ : Category J
C : Type u
inst✝ : Category C
W X✝ Y✝ Z : C
f✝ : W ⟶ X✝
g : W ⟶ Y✝
h : X✝ ⟶ Z
i : Y✝ ⟶ Z
X E Y YE : C
c : BinaryCofan X E
hc : IsColimit c
f : X ⟶ Y
iY : Y ⟶ YE
fE : c.pt ⟶ YE
H✝ : CommSq f (BinaryCofan.inl c) iY fE
H : IsPushout f (BinaryCofan.inl c) iY fE
s : BinaryCofan ((pair X E).obj { as := WalkingPair.right }) Y
m : YE ⟶ s.pt
e₁ : (BinaryCofan.inr c ≫ fE) ≫ m = BinaryCofan.inl s
e₂ : iY ≫ m = BinaryCofan.inr s
⊢ PushoutCocone.inl (IsPushout.cocone H) ≫ m =
    PushoutCocone.inl (IsPushout.cocone H) ≫
      IsColimit.desc (IsPushout.isColimit H)
        (PushoutCocone.mk (BinaryCofan.inr s)
          (IsColimit.desc hc (BinaryCofan.mk (f ≫ BinaryCofan.inr s) (BinaryCofan.inl s)))
          (_ :
            (BinaryCofan.mk (f ≫ BinaryCofan.inr s) (BinaryCofan.inl s)).ι.app { as := WalkingPair.left } =
              c.ι.app { as := WalkingPair.left } ≫
                IsColimit.desc hc (BinaryCofan.mk (f ≫ BinaryCofan.inr s) (BinaryCofan.inl s))))
symm
no goals
case mpr.uniq.h₀
J : Type v'
inst✝¹ : Category J
C : Type u
inst✝ : Category C
W X✝ Y✝ Z : C
f✝ : W ⟶ X✝
g : W ⟶ Y✝
h : X✝ ⟶ Z
i : Y✝ ⟶ Z
X E Y YE : C
c : BinaryCofan X E
hc : IsColimit c
f : X ⟶ Y
iY : Y ⟶ YE
fE : c.pt ⟶ YE
H✝ : CommSq f (BinaryCofan.inl c) iY fE
H : IsPushout f (BinaryCofan.inl c) iY fE
s : BinaryCofan ((pair X E).obj { as := WalkingPair.right }) Y
m : YE ⟶ s.pt
e₁ : (BinaryCofan.inr c ≫ fE) ≫ m = BinaryCofan.inl s
e₂ : iY ≫ m = BinaryCofan.inr s
⊢ PushoutCocone.inl (IsPushout.cocone H) ≫
      IsColimit.desc (IsPushout.isColimit H)
        (PushoutCocone.mk (BinaryCofan.inr s)
          (IsColimit.desc hc (BinaryCofan.mk (f ≫ BinaryCofan.inr s) (BinaryCofan.inl s)))
          (_ :
            (BinaryCofan.mk (f ≫ BinaryCofan.inr s) (BinaryCofan.inl s)).ι.app { as := WalkingPair.left } =
              c.ι.app { as := WalkingPair.left } ≫
                IsColimit.desc hc (BinaryCofan.mk (f ≫ BinaryCofan.inr s) (BinaryCofan.inl s)))) =
    PushoutCocone.inl (IsPushout.cocone H) ≫ m
exact (H.isColimit.fac _ WalkingSpan.left).trans e₂.symm
case mpr.uniq.h₁
J : Type v'
inst✝¹ : Category J
C : Type u
inst✝ : Category C
W X✝ Y✝ Z : C
f✝ : W ⟶ X✝
g : W ⟶ Y✝
h : X✝ ⟶ Z
i : Y✝ ⟶ Z
X E Y YE : C
c : BinaryCofan X E
hc : IsColimit c
f : X ⟶ Y
iY : Y ⟶ YE
fE : c.pt ⟶ YE
H✝ : CommSq f (BinaryCofan.inl c) iY fE
H : IsPushout f (BinaryCofan.inl c) iY fE
s : BinaryCofan ((pair X E).obj { as := WalkingPair.right }) Y
m : YE ⟶ s.pt
e₁ : (BinaryCofan.inr c ≫ fE) ≫ m = BinaryCofan.inl s
e₂ : iY ≫ m = BinaryCofan.inr s
⊢ PushoutCocone.inr (IsPushout.cocone H) ≫ m =
    (PushoutCocone.mk (BinaryCofan.inr s)
            (IsColimit.desc hc (BinaryCofan.mk (f ≫ BinaryCofan.inr s) (BinaryCofan.inl s)))
            (_ :
              (BinaryCofan.mk (f ≫ BinaryCofan.inr s) (BinaryCofan.inl s)).ι.app { as := WalkingPair.left } =
                c.ι.app { as := WalkingPair.left } ≫
                  IsColimit.desc hc (BinaryCofan.mk (f ≫ BinaryCofan.inr s) (BinaryCofan.inl s)))).ι.app
      WalkingSpan.right
case mpr.uniq.h₁
J : Type v'
inst✝¹ : Category J
C : Type u
inst✝ : Category C
W X✝ Y✝ Z : C
f✝ : W ⟶ X✝
g : W ⟶ Y✝
h : X✝ ⟶ Z
i : Y✝ ⟶ Z
X E Y YE : C
c : BinaryCofan X E
hc : IsColimit c
f : X ⟶ Y
iY : Y ⟶ YE
fE : c.pt ⟶ YE
H✝ : CommSq f (BinaryCofan.inl c) iY fE
H : IsPushout f (BinaryCofan.inl c) iY fE
s : BinaryCofan ((pair X E).obj { as := WalkingPair.right }) Y
m : YE ⟶ s.pt
e₁ : (BinaryCofan.inr c ≫ fE) ≫ m = BinaryCofan.inl s
e₂ : iY ≫ m = BinaryCofan.inr s
⊢ PushoutCocone.inr (IsPushout.cocone H) ≫ m =
    PushoutCocone.inr (IsPushout.cocone H) ≫
      IsColimit.desc (IsPushout.isColimit H)
        (PushoutCocone.mk (BinaryCofan.inr s)
          (IsColimit.desc hc (BinaryCofan.mk (f ≫ BinaryCofan.inr s) (BinaryCofan.inl s)))
          (_ :
            (BinaryCofan.mk (f ≫ BinaryCofan.inr s) (BinaryCofan.inl s)).ι.app { as := WalkingPair.left } =
              c.ι.app { as := WalkingPair.left } ≫
                IsColimit.desc hc (BinaryCofan.mk (f ≫ BinaryCofan.inr s) (BinaryCofan.inl s))))
erw [H.isColimit.fac _ WalkingSpan.right]
case mpr.uniq.h₁.h₁
J : Type v'
inst✝¹ : Category J
C : Type u
inst✝ : Category C
W X✝ Y✝ Z : C
f✝ : W ⟶ X✝
g : W ⟶ Y✝
h : X✝ ⟶ Z
i : Y✝ ⟶ Z
X E Y YE : C
c : BinaryCofan X E
hc : IsColimit c
f : X ⟶ Y
iY : Y ⟶ YE
fE : c.pt ⟶ YE
H✝ : CommSq f (BinaryCofan.inl c) iY fE
H : IsPushout f (BinaryCofan.inl c) iY fE
s : BinaryCofan ((pair X E).obj { as := WalkingPair.right }) Y
m : YE ⟶ s.pt
e₁ : (BinaryCofan.inr c ≫ fE) ≫ m = BinaryCofan.inl s
e₂ : iY ≫ m = BinaryCofan.inr s
⊢ BinaryCofan.inl c ≫ PushoutCocone.inr (IsPushout.cocone H) ≫ m =
    BinaryCofan.inl c ≫
      (PushoutCocone.mk (BinaryCofan.inr s)
              (IsColimit.desc hc (BinaryCofan.mk (f ≫ BinaryCofan.inr s) (BinaryCofan.inl s)))
              (_ :
                (BinaryCofan.mk (f ≫ BinaryCofan.inr s) (BinaryCofan.inl s)).ι.app { as := WalkingPair.left } =
                  c.ι.app { as := WalkingPair.left } ≫
                    IsColimit.desc hc (BinaryCofan.mk (f ≫ BinaryCofan.inr s) (BinaryCofan.inl s)))).ι.app
        WalkingSpan.right

case mpr.uniq.h₁.h₂
J : Type v'
inst✝¹ : Category J
C : Type u
inst✝ : Category C
W X✝ Y✝ Z : C
f✝ : W ⟶ X✝
g : W ⟶ Y✝
h : X✝ ⟶ Z
i : Y✝ ⟶ Z
X E Y YE : C
c : BinaryCofan X E
hc : IsColimit c
f : X ⟶ Y
iY : Y ⟶ YE
fE : c.pt ⟶ YE
H✝ : CommSq f (BinaryCofan.inl c) iY fE
H : IsPushout f (BinaryCofan.inl c) iY fE
s : BinaryCofan ((pair X E).obj { as := WalkingPair.right }) Y
m : YE ⟶ s.pt
e₁ : (BinaryCofan.inr c ≫ fE) ≫ m = BinaryCofan.inl s
e₂ : iY ≫ m = BinaryCofan.inr s
⊢ BinaryCofan.inr c ≫ PushoutCocone.inr (IsPushout.cocone H) ≫ m =
    BinaryCofan.inr c ≫
      (PushoutCocone.mk (BinaryCofan.inr s)
              (IsColimit.desc hc (BinaryCofan.mk (f ≫ BinaryCofan.inr s) (BinaryCofan.inl s)))
              (_ :
                (BinaryCofan.mk (f ≫ BinaryCofan.inr s) (BinaryCofan.inl s)).ι.app { as := WalkingPair.left } =
                  c.ι.app { as := WalkingPair.left } ≫
                    IsColimit.desc hc (BinaryCofan.mk (f ≫ BinaryCofan.inr s) (BinaryCofan.inl s)))).ι.app
        WalkingSpan.right
case mpr.uniq.h₁
J : Type v'
inst✝¹ : Category J
C : Type u
inst✝ : Category C
W X✝ Y✝ Z : C
f✝ : W ⟶ X✝
g : W ⟶ Y✝
h : X✝ ⟶ Z
i : Y✝ ⟶ Z
X E Y YE : C
c : BinaryCofan X E
hc : IsColimit c
f : X ⟶ Y
iY : Y ⟶ YE
fE : c.pt ⟶ YE
H✝ : CommSq f (BinaryCofan.inl c) iY fE
H : IsPushout f (BinaryCofan.inl c) iY fE
s : BinaryCofan ((pair X E).obj { as := WalkingPair.right }) Y
m : YE ⟶ s.pt
e₁ : (BinaryCofan.inr c ≫ fE) ≫ m = BinaryCofan.inl s
e₂ : iY ≫ m = BinaryCofan.inr s
⊢ PushoutCocone.inr (IsPushout.cocone H) ≫ m =
    (PushoutCocone.mk (BinaryCofan.inr s)
            (IsColimit.desc hc (BinaryCofan.mk (f ≫ BinaryCofan.inr s) (BinaryCofan.inl s)))
            (_ :
              (BinaryCofan.mk (f ≫ BinaryCofan.inr s) (BinaryCofan.inl s)).ι.app { as := WalkingPair.left } =
                c.ι.app { as := WalkingPair.left } ≫
                  IsColimit.desc hc (BinaryCofan.mk (f ≫ BinaryCofan.inr s) (BinaryCofan.inl s)))).ι.app
      WalkingSpan.right
apply BinaryCofan.IsColimit.hom_ext hc
case mpr.uniq.h₁.h₁
J : Type v'
inst✝¹ : Category J
C : Type u
inst✝ : Category C
W X✝ Y✝ Z : C
f✝ : W ⟶ X✝
g : W ⟶ Y✝
h : X✝ ⟶ Z
i : Y✝ ⟶ Z
X E Y YE : C
c : BinaryCofan X E
hc : IsColimit c
f : X ⟶ Y
iY : Y ⟶ YE
fE : c.pt ⟶ YE
H✝ : CommSq f (BinaryCofan.inl c) iY fE
H : IsPushout f (BinaryCofan.inl c) iY fE
s : BinaryCofan ((pair X E).obj { as := WalkingPair.right }) Y
m : YE ⟶ s.pt
e₁ : (BinaryCofan.inr c ≫ fE) ≫ m = BinaryCofan.inl s
e₂ : iY ≫ m = BinaryCofan.inr s
⊢ f ≫ BinaryCofan.inr s = (BinaryCofan.mk (f ≫ BinaryCofan.inr s) (BinaryCofan.inl s)).ι.app { as := WalkingPair.left }
case mpr.uniq.h₁.h₁
J : Type v'
inst✝¹ : Category J
C : Type u
inst✝ : Category C
W X✝ Y✝ Z : C
f✝ : W ⟶ X✝
g : W ⟶ Y✝
h : X✝ ⟶ Z
i : Y✝ ⟶ Z
X E Y YE : C
c : BinaryCofan X E
hc : IsColimit c
f : X ⟶ Y
iY : Y ⟶ YE
fE : c.pt ⟶ YE
H✝ : CommSq f (BinaryCofan.inl c) iY fE
H : IsPushout f (BinaryCofan.inl c) iY fE
s : BinaryCofan ((pair X E).obj { as := WalkingPair.right }) Y
m : YE ⟶ s.pt
e₁ : (BinaryCofan.inr c ≫ fE) ≫ m = BinaryCofan.inl s
e₂ : iY ≫ m = BinaryCofan.inr s
⊢ BinaryCofan.inl c ≫ PushoutCocone.inr (IsPushout.cocone H) ≫ m =
    BinaryCofan.inl c ≫
      (PushoutCocone.mk (BinaryCofan.inr s)
              (IsColimit.desc hc (BinaryCofan.mk (f ≫ BinaryCofan.inr s) (BinaryCofan.inl s)))
              (_ :
                (BinaryCofan.mk (f ≫ BinaryCofan.inr s) (BinaryCofan.inl s)).ι.app { as := WalkingPair.left } =
                  c.ι.app { as := WalkingPair.left } ≫
                    IsColimit.desc hc (BinaryCofan.mk (f ≫ BinaryCofan.inr s) (BinaryCofan.inl s)))).ι.app
        WalkingSpan.right
erw [hc.fac, ← H.w_assoc, e₂]
no goals
case mpr.uniq.h₁.h₁
J : Type v'
inst✝¹ : Category J
C : Type u
inst✝ : Category C
W X✝ Y✝ Z : C
f✝ : W ⟶ X✝
g : W ⟶ Y✝
h : X✝ ⟶ Z
i : Y✝ ⟶ Z
X E Y YE : C
c : BinaryCofan X E
hc : IsColimit c
f : X ⟶ Y
iY : Y ⟶ YE
fE : c.pt ⟶ YE
H✝ : CommSq f (BinaryCofan.inl c) iY fE
H : IsPushout f (BinaryCofan.inl c) iY fE
s : BinaryCofan ((pair X E).obj { as := WalkingPair.right }) Y
m : YE ⟶ s.pt
e₁ : (BinaryCofan.inr c ≫ fE) ≫ m = BinaryCofan.inl s
e₂ : iY ≫ m = BinaryCofan.inr s
⊢ f ≫ BinaryCofan.inr s = (BinaryCofan.mk (f ≫ BinaryCofan.inr s) (BinaryCofan.inl s)).ι.app { as := WalkingPair.left }
rfl
case mpr.uniq.h₁.h₂
J : Type v'
inst✝¹ : Category J
C : Type u
inst✝ : Category C
W X✝ Y✝ Z : C
f✝ : W ⟶ X✝
g : W ⟶ Y✝
h : X✝ ⟶ Z
i : Y✝ ⟶ Z
X E Y YE : C
c : BinaryCofan X E
hc : IsColimit c
f : X ⟶ Y
iY : Y ⟶ YE
fE : c.pt ⟶ YE
H✝ : CommSq f (BinaryCofan.inl c) iY fE
H : IsPushout f (BinaryCofan.inl c) iY fE
s : BinaryCofan ((pair X E).obj { as := WalkingPair.right }) Y
m : YE ⟶ s.pt
e₁ : (BinaryCofan.inr c ≫ fE) ≫ m = BinaryCofan.inl s
e₂ : iY ≫ m = BinaryCofan.inr s
⊢ BinaryCofan.inl s =
    BinaryCofan.inr c ≫
      (PushoutCocone.mk (BinaryCofan.inr s)
              (IsColimit.desc hc (BinaryCofan.mk (f ≫ BinaryCofan.inr s) (BinaryCofan.inl s)))
              (_ :
                (BinaryCofan.mk (f ≫ BinaryCofan.inr s) (BinaryCofan.inl s)).ι.app { as := WalkingPair.left } =
                  c.ι.app { as := WalkingPair.left } ≫
                    IsColimit.desc hc (BinaryCofan.mk (f ≫ BinaryCofan.inr s) (BinaryCofan.inl s)))).ι.app
        WalkingSpan.right
case mpr.uniq.h₁.h₂
J : Type v'
inst✝¹ : Category J
C : Type u
inst✝ : Category C
W X✝ Y✝ Z : C
f✝ : W ⟶ X✝
g : W ⟶ Y✝
h : X✝ ⟶ Z
i : Y✝ ⟶ Z
X E Y YE : C
c : BinaryCofan X E
hc : IsColimit c
f : X ⟶ Y
iY : Y ⟶ YE
fE : c.pt ⟶ YE
H✝ : CommSq f (BinaryCofan.inl c) iY fE
H : IsPushout f (BinaryCofan.inl c) iY fE
s : BinaryCofan ((pair X E).obj { as := WalkingPair.right }) Y
m : YE ⟶ s.pt
e₁ : (BinaryCofan.inr c ≫ fE) ≫ m = BinaryCofan.inl s
e₂ : iY ≫ m = BinaryCofan.inr s
⊢ BinaryCofan.inr c ≫ PushoutCocone.inr (IsPushout.cocone H) ≫ m =
    BinaryCofan.inr c ≫
      (PushoutCocone.mk (BinaryCofan.inr s)
              (IsColimit.desc hc (BinaryCofan.mk (f ≫ BinaryCofan.inr s) (BinaryCofan.inl s)))
              (_ :
                (BinaryCofan.mk (f ≫ BinaryCofan.inr s) (BinaryCofan.inl s)).ι.app { as := WalkingPair.left } =
                  c.ι.app { as := WalkingPair.left } ≫
                    IsColimit.desc hc (BinaryCofan.mk (f ≫ BinaryCofan.inr s) (BinaryCofan.inl s)))).ι.app
        WalkingSpan.right
refine' ((Category.assoc _ _ _).symm.trans e₁).trans _
case mpr.uniq.h₁.h₂
J : Type v'
inst✝¹ : Category J
C : Type u
inst✝ : Category C
W X✝ Y✝ Z : C
f✝ : W ⟶ X✝
g : W ⟶ Y✝
h : X✝ ⟶ Z
i : Y✝ ⟶ Z
X E Y YE : C
c : BinaryCofan X E
hc : IsColimit c
f : X ⟶ Y
iY : Y ⟶ YE
fE : c.pt ⟶ YE
H✝ : CommSq f (BinaryCofan.inl c) iY fE
H : IsPushout f (BinaryCofan.inl c) iY fE
s : BinaryCofan ((pair X E).obj { as := WalkingPair.right }) Y
m : YE ⟶ s.pt
e₁ : (BinaryCofan.inr c ≫ fE) ≫ m = BinaryCofan.inl s
e₂ : iY ≫ m = BinaryCofan.inr s
⊢ BinaryCofan.inr c ≫
      (PushoutCocone.mk (BinaryCofan.inr s)
              (IsColimit.desc hc (BinaryCofan.mk (f ≫ BinaryCofan.inr s) (BinaryCofan.inl s)))
              (_ :
                (BinaryCofan.mk (f ≫ BinaryCofan.inr s) (BinaryCofan.inl s)).ι.app { as := WalkingPair.left } =
                  c.ι.app { as := WalkingPair.left } ≫
                    IsColimit.desc hc (BinaryCofan.mk (f ≫ BinaryCofan.inr s) (BinaryCofan.inl s)))).ι.app
        WalkingSpan.right =
    BinaryCofan.inl s
case mpr.uniq.h₁.h₂
J : Type v'
inst✝¹ : Category J
C : Type u
inst✝ : Category C
W X✝ Y✝ Z : C
f✝ : W ⟶ X✝
g : W ⟶ Y✝
h : X✝ ⟶ Z
i : Y✝ ⟶ Z
X E Y YE : C
c : BinaryCofan X E
hc : IsColimit c
f : X ⟶ Y
iY : Y ⟶ YE
fE : c.pt ⟶ YE
H✝ : CommSq f (BinaryCofan.inl c) iY fE
H : IsPushout f (BinaryCofan.inl c) iY fE
s : BinaryCofan ((pair X E).obj { as := WalkingPair.right }) Y
m : YE ⟶ s.pt
e₁ : (BinaryCofan.inr c ≫ fE) ≫ m = BinaryCofan.inl s
e₂ : iY ≫ m = BinaryCofan.inr s
⊢ BinaryCofan.inl s =
    BinaryCofan.inr c ≫
      (PushoutCocone.mk (BinaryCofan.inr s)
              (IsColimit.desc hc (BinaryCofan.mk (f ≫ BinaryCofan.inr s) (BinaryCofan.inl s)))
              (_ :
                (BinaryCofan.mk (f ≫ BinaryCofan.inr s) (BinaryCofan.inl s)).ι.app { as := WalkingPair.left } =
                  c.ι.app { as := WalkingPair.left } ≫
                    IsColimit.desc hc (BinaryCofan.mk (f ≫ BinaryCofan.inr s) (BinaryCofan.inl s)))).ι.app
        WalkingSpan.right
symm
no goals
case mpr.uniq.h₁.h₂
J : Type v'
inst✝¹ : Category J
C : Type u
inst✝ : Category C
W X✝ Y✝ Z : C
f✝ : W ⟶ X✝
g : W ⟶ Y✝
h : X✝ ⟶ Z
i : Y✝ ⟶ Z
X E Y YE : C
c : BinaryCofan X E
hc : IsColimit c
f : X ⟶ Y
iY : Y ⟶ YE
fE : c.pt ⟶ YE
H✝ : CommSq f (BinaryCofan.inl c) iY fE
H : IsPushout f (BinaryCofan.inl c) iY fE
s : BinaryCofan ((pair X E).obj { as := WalkingPair.right }) Y
m : YE ⟶ s.pt
e₁ : (BinaryCofan.inr c ≫ fE) ≫ m = BinaryCofan.inl s
e₂ : iY ≫ m = BinaryCofan.inr s
⊢ BinaryCofan.inr c ≫
      (PushoutCocone.mk (BinaryCofan.inr s)
              (IsColimit.desc hc (BinaryCofan.mk (f ≫ BinaryCofan.inr s) (BinaryCofan.inl s)))
              (_ :
                (BinaryCofan.mk (f ≫ BinaryCofan.inr s) (BinaryCofan.inl s)).ι.app { as := WalkingPair.left } =
                  c.ι.app { as := WalkingPair.left } ≫
                    IsColimit.desc hc (BinaryCofan.mk (f ≫ BinaryCofan.inr s) (BinaryCofan.inl s)))).ι.app
        WalkingSpan.right =
    BinaryCofan.inl s
exact hc.fac _ _