-- 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.refine_2.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
m : YE ⟶ s.pt
e₁ :
  PushoutCocone.inl
        { pt := YE,
          ι := { app := fun j => Option.rec (f ≫ iY) (fun val => WalkingPair.rec iY fE val) j, naturality := ⋯ } } ≫
      m =
    s.inl
e₂ : fE ≫ m = s.ι.app WalkingSpan.right
⊢ BinaryCofan.inl
        { pt := YE,
          ι :=
            {
              app := fun x =>
                match x.as with
                | WalkingPair.left => c.inr ≫ fE
                | WalkingPair.right => iY,
              naturality := ⋯ } } ≫
      m =
    BinaryCofan.inl
        { pt := YE,
          ι :=
            {
              app := fun x =>
                match x.as with
                | WalkingPair.left => c.inr ≫ fE
                | WalkingPair.right => iY,
              naturality := ⋯ } } ≫
      h.desc
        { pt := s.pt,
          ι :=
            {
              app := fun x =>
                match x.as with
                | WalkingPair.left => c.inr ≫ s.inr
                | WalkingPair.right => s.inl,
              naturality := ⋯ } }

Tactic:
rw [Category.assoc, e₂, eq_comm]

Result:
case mp.intro.refine_2.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
m : YE ⟶ s.pt
e₁ :
  PushoutCocone.inl
        { pt := YE,
          ι := { app := fun j => Option.rec (f ≫ iY) (fun val => WalkingPair.rec iY fE val) j, naturality := ⋯ } } ≫
      m =
    s.inl
e₂ : fE ≫ m = s.ι.app WalkingSpan.right
⊢ BinaryCofan.inl
        { pt := YE,
          ι :=
            {
              app := fun x =>
                match x.as with
                | WalkingPair.left => c.inr ≫ fE
                | WalkingPair.right => iY,
              naturality := ⋯ } } ≫
      h.desc
        { pt := s.pt,
          ι :=
            {
              app := fun x =>
                match x.as with
                | WalkingPair.left => c.inr ≫ s.inr
                | WalkingPair.right => s.inl,
              naturality := ⋯ } } =
    c.inr ≫ s.ι.app WalkingSpan.right

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 ≫ iY ≫ h.desc (BinaryCofan.mk (c.inr ≫ s.inr) s.inl) = c.inl ≫ s.ι.app WalkingSpan.right

Tactic:
erw [h.fac _ ⟨WalkingPair.right⟩]

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

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

Tactic:
refine ((Category.assoc _ _ _).symm.trans e₁).trans ?_

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

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.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 }

Tactic:
refine ⟨h.desc (BinaryCofan.mk (c.inr ≫ s.inr) s.inl), h.fac _ ⟨WalkingPair.right⟩, ?_, ?_⟩

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

case mp.intro.refine_2
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
⊢ ∀ {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 = h.desc (BinaryCofan.mk (c.inr ≫ s.inr) s.inl)

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:
intro s

Result:
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

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

Tactic:
exact (H.isColimit.fac _ WalkingSpan.left).trans e₂.symm

Result:
no goals