-- Mathlib/CategoryTheory/Adhesive.lean
theorem is_coprod_iff_isPushout {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 c.inl iY fE) :
    Nonempty (IsColimit (BinaryCofan.mk (c.inr ≫ fE) iY)) ↔ IsPushout f c.inl iY fE

Proof state:
case mpr.uniq.h₁.h₁
C : Type u
inst✝ : Category.{v, u} C
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 c.inl iY fE
H : IsPushout f c.inl iY fE
s : BinaryCofan ((pair X E).obj { as := WalkingPair.right }) Y
m : YE ⟶ s.pt
e₁ : (c.inr ≫ fE) ≫ m = s.inl
e₂ : iY ≫ m = s.inr
⊢ f ≫ s.inr = (BinaryCofan.mk (f ≫ s.inr) s.inl).ι.app { as := WalkingPair.left }

Tactic:
rfl

Result:
no goals

Proof state:
case mp.intro
C : Type u
inst✝ : Category.{v, u} C
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 c.inl iY fE
h : IsColimit (BinaryCofan.mk (c.inr ≫ fE) iY)
⊢ (s : PushoutCocone f c.inl) →
    { l //
      (PushoutCocone.mk iY fE ⋯).inl ≫ l = s.inl ∧
        (PushoutCocone.mk iY fE ⋯).inr ≫ l = s.inr ∧
          ∀ {m : (PushoutCocone.mk iY fE ⋯).pt ⟶ s.pt},
            (PushoutCocone.mk iY fE ⋯).inl ≫ m = s.inl → (PushoutCocone.mk iY fE ⋯).inr ≫ m = s.inr → m = l }

Tactic:
intro s

Result:
case mp.intro
C : Type u
inst✝ : Category.{v, u} C
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 c.inl iY fE
h : IsColimit (BinaryCofan.mk (c.inr ≫ fE) iY)
s : PushoutCocone f c.inl
⊢ { l //
    (PushoutCocone.mk iY fE ⋯).inl ≫ l = s.inl ∧
      (PushoutCocone.mk iY fE ⋯).inr ≫ l = s.inr ∧
        ∀ {m : (PushoutCocone.mk iY fE ⋯).pt ⟶ s.pt},
          (PushoutCocone.mk iY fE ⋯).inl ≫ m = s.inl → (PushoutCocone.mk iY fE ⋯).inr ≫ m = s.inr → m = l }

Proof state:
case mpr
C : Type u
inst✝ : Category.{v, u} C
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 c.inl iY fE
H : IsPushout f c.inl iY fE
⊢ IsColimit (BinaryCofan.mk (c.inr ≫ fE) iY)

Tactic:
fapply Limits.BinaryCofan.isColimitMk

Result:
case mpr.desc
C : Type u
inst✝ : Category.{v, u} C
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 c.inl iY fE
H : IsPushout f c.inl iY fE
⊢ (s : BinaryCofan ((pair X E).obj { as := WalkingPair.right }) Y) → YE ⟶ s.pt

case mpr.fac_left
C : Type u
inst✝ : Category.{v, u} C
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 c.inl iY fE
H : IsPushout f c.inl iY fE
⊢ ∀ (s : BinaryCofan ((pair X E).obj { as := WalkingPair.right }) Y), (c.inr ≫ fE) ≫ ?mpr.desc s = s.inl

case mpr.fac_right
C : Type u
inst✝ : Category.{v, u} C
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 c.inl iY fE
H : IsPushout f c.inl iY fE
⊢ ∀ (s : BinaryCofan ((pair X E).obj { as := WalkingPair.right }) Y), iY ≫ ?mpr.desc s = s.inr

case mpr.uniq
C : Type u
inst✝ : Category.{v, u} C
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 c.inl iY fE
H : IsPushout f c.inl iY fE
⊢ ∀ (s : BinaryCofan ((pair X E).obj { as := WalkingPair.right }) Y) (m : YE ⟶ s.pt),
    (c.inr ≫ fE) ≫ m = s.inl → iY ≫ m = s.inr → m = ?mpr.desc s

Proof state:
case mpr.fac_right
C : Type u
inst✝ : Category.{v, u} C
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 c.inl iY fE
H : IsPushout f c.inl iY fE
s : BinaryCofan ((pair X E).obj { as := WalkingPair.right }) Y
⊢ iY ≫ H.isColimit.desc (PushoutCocone.mk s.inr (hc.desc (BinaryCofan.mk (f ≫ s.inr) s.inl)) ⋯) = s.inr

Tactic:
exact H.isColimit.fac _ WalkingSpan.left

Result:
no goals

Proof state:
case mpr.fac_left
C : Type u
inst✝ : Category.{v, u} C
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 c.inl iY fE
H : IsPushout f c.inl iY fE
s : BinaryCofan ((pair X E).obj { as := WalkingPair.right }) Y
⊢ (c.inr ≫ fE) ≫ H.isColimit.desc (PushoutCocone.mk s.inr (hc.desc (BinaryCofan.mk (f ≫ s.inr) s.inl)) ⋯) = s.inl

Tactic:
erw [Category.assoc, H.isColimit.fac _ WalkingSpan.right, hc.fac]

Result:
case mpr.fac_left
C : Type u
inst✝ : Category.{v, u} C
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 c.inl iY fE
H : IsPushout f c.inl iY fE
s : BinaryCofan ((pair X E).obj { as := WalkingPair.right }) Y
⊢ (BinaryCofan.mk (f ≫ s.inr) s.inl).ι.app { as := WalkingPair.right } = s.inl

Proof state:
case mpr.fac_left
C : Type u
inst✝ : Category.{v, u} C
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 c.inl iY fE
H : IsPushout f c.inl iY fE
⊢ ∀ (s : BinaryCofan ((pair X E).obj { as := WalkingPair.right }) Y),
    (c.inr ≫ fE) ≫ H.isColimit.desc (PushoutCocone.mk s.inr (hc.desc (BinaryCofan.mk (f ≫ s.inr) s.inl)) ⋯) = s.inl

Tactic:
intro s

Result:
case mpr.fac_left
C : Type u
inst✝ : Category.{v, u} C
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 c.inl iY fE
H : IsPushout f c.inl iY fE
s : BinaryCofan ((pair X E).obj { as := WalkingPair.right }) Y
⊢ (c.inr ≫ fE) ≫ H.isColimit.desc (PushoutCocone.mk s.inr (hc.desc (BinaryCofan.mk (f ≫ s.inr) s.inl)) ⋯) = s.inl

Proof state:
C : Type u
inst✝ : Category.{v, u} C
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 c.inl iY fE
⊢ Nonempty (IsColimit (BinaryCofan.mk (c.inr ≫ fE) iY)) ↔ IsPushout f c.inl iY fE

Tactic:
constructor

Result:
case mp
C : Type u
inst✝ : Category.{v, u} C
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 c.inl iY fE
⊢ Nonempty (IsColimit (BinaryCofan.mk (c.inr ≫ fE) iY)) → IsPushout f c.inl iY fE

case mpr
C : Type u
inst✝ : Category.{v, u} C
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 c.inl iY fE
⊢ IsPushout f c.inl iY fE → Nonempty (IsColimit (BinaryCofan.mk (c.inr ≫ fE) iY))

Proof state:
case mpr.uniq.h₁.h₂
C : Type u
inst✝ : Category.{v, u} C
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 c.inl iY fE
H : IsPushout f c.inl iY fE
s : BinaryCofan ((pair X E).obj { as := WalkingPair.right }) Y
m : YE ⟶ s.pt
e₁ : (c.inr ≫ fE) ≫ m = s.inl
e₂ : iY ≫ m = s.inr
⊢ s.inl = c.inr ≫ (PushoutCocone.mk s.inr (hc.desc (BinaryCofan.mk (f ≫ s.inr) s.inl)) ⋯).ι.app WalkingSpan.right

Tactic:
symm

Result:
case mpr.uniq.h₁.h₂
C : Type u
inst✝ : Category.{v, u} C
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 c.inl iY fE
H : IsPushout f c.inl iY fE
s : BinaryCofan ((pair X E).obj { as := WalkingPair.right }) Y
m : YE ⟶ s.pt
e₁ : (c.inr ≫ fE) ≫ m = s.inl
e₂ : iY ≫ m = s.inr
⊢ c.inr ≫ (PushoutCocone.mk s.inr (hc.desc (BinaryCofan.mk (f ≫ s.inr) s.inl)) ⋯).ι.app WalkingSpan.right = s.inl