-- 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 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:
dsimp only [PushoutCocone.inr, PushoutCocone.mk]

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.inl
            { pt := YE,
              ι := { app := fun j => Option.rec (f ≫ iY) (fun val => WalkingPair.rec iY fE val) j, naturality := ⋯ } } ≫
          l =
        s.inl ∧
      fE ≫ l = s.ι.app WalkingSpan.right ∧
        ∀ {m : YE ⟶ s.pt},
          PushoutCocone.inl
                  { pt := YE,
                    ι :=
                      { app := fun j => Option.rec (f ≫ iY) (fun val => WalkingPair.rec iY fE val) j,
                        naturality := ⋯ } } ≫
                m =
              s.inl →
            fE ≫ m = s.ι.app WalkingSpan.right → m = l }

Proof state:
case mp.intro.refine_1.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 : IsColimit (BinaryCofan.mk (c.inr ≫ fE) iY)
s : PushoutCocone f c.inl
⊢ c.inr ≫ fE ≫ h.desc (BinaryCofan.mk (c.inr ≫ s.inr) s.inl) = c.inr ≫ s.ι.app WalkingSpan.right

Tactic:
rw [← Category.assoc]

Result:
case mp.intro.refine_1.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 : IsColimit (BinaryCofan.mk (c.inr ≫ fE) iY)
s : PushoutCocone f c.inl
⊢ (c.inr ≫ fE) ≫ h.desc (BinaryCofan.mk (c.inr ≫ s.inr) s.inl) = c.inr ≫ s.ι.app WalkingSpan.right

Proof state:
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 = H.isColimit.desc (PushoutCocone.mk s.inr (hc.desc (BinaryCofan.mk (f ≫ s.inr) s.inl)) ⋯)

Tactic:
intro s m e₁ e₂

Result:
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
e₁ : (c.inr ≫ fE) ≫ m = s.inl
e₂ : iY ≫ m = s.inr
⊢ m = H.isColimit.desc (PushoutCocone.mk s.inr (hc.desc (BinaryCofan.mk (f ≫ s.inr) s.inl)) ⋯)

Proof state:
case mp.intro.refine_1.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 : IsColimit (BinaryCofan.mk (c.inr ≫ fE) iY)
s : PushoutCocone f c.inl
⊢ f ≫ (BinaryCofan.mk (c.inr ≫ s.inr) s.inl).ι.app { as := WalkingPair.right } = c.inl ≫ s.ι.app WalkingSpan.right

Tactic:
exact s.condition

Result:
no goals

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
⊢ c.inl ≫ H.cocone.inr ≫ m =
    c.inl ≫ (PushoutCocone.mk s.inr (hc.desc (BinaryCofan.mk (f ≫ s.inr) s.inl)) ⋯).ι.app WalkingSpan.right

Tactic:
erw [hc.fac, ← H.w_assoc, e₂]

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
⊢ f ≫ s.inr = (BinaryCofan.mk (f ≫ s.inr) s.inl).ι.app { as := WalkingPair.left }

Proof state:
case mpr.uniq.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
⊢ H.cocone.inl ≫ m =
    H.cocone.inl ≫ H.isColimit.desc (PushoutCocone.mk s.inr (hc.desc (BinaryCofan.mk (f ≫ s.inr) s.inl)) ⋯)

Tactic:
symm

Result:
case mpr.uniq.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
⊢ H.cocone.inl ≫ H.isColimit.desc (PushoutCocone.mk s.inr (hc.desc (BinaryCofan.mk (f ≫ s.inr) s.inl)) ⋯) =
    H.cocone.inl ≫ m

Proof state:
case mp.intro.refine_1.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 : IsColimit (BinaryCofan.mk (c.inr ≫ fE) iY)
s : PushoutCocone f c.inl
⊢ c.inl ≫ fE ≫ h.desc (BinaryCofan.mk (c.inr ≫ s.inr) s.inl) = c.inl ≫ s.ι.app WalkingSpan.right

Tactic:
rw [← H.w_assoc]

Result:
case mp.intro.refine_1.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 : IsColimit (BinaryCofan.mk (c.inr ≫ fE) iY)
s : PushoutCocone f c.inl
⊢ f ≫ iY ≫ h.desc (BinaryCofan.mk (c.inr ≫ s.inr) s.inl) = c.inl ≫ s.ι.app WalkingSpan.right