-- 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.mk (c.inr ≫ fE) iY).inl ≫ m =
    (BinaryCofan.mk (c.inr ≫ fE) iY).inl ≫ h.desc (BinaryCofan.mk (c.inr ≫ s.inr) s.inl)

Tactic:
dsimp only [BinaryCofan.mk, id]

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 := ⋯ } } ≫
      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 := ⋯ } }

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

Tactic:
rfl

Result:
no goals

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.mk (c.inr ≫ fE) iY).inr ≫ m =
    (BinaryCofan.mk (c.inr ≫ fE) iY).inr ≫ h.desc (BinaryCofan.mk (c.inr ≫ s.inr) s.inl)

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

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

Tactic:
exact h.fac _ ⟨WalkingPair.left⟩

Result:
no goals

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

Tactic:
exact h.fac _ _

Result:
no goals

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
⊢ IsPushout f c.inl iY fE → Nonempty (IsColimit (BinaryCofan.mk (c.inr ≫ fE) iY))

Tactic:
refine fun H => ⟨?_⟩

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

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 := ⋯ } } ≫
      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

Tactic:
exact h.fac _ ⟨WalkingPair.left⟩

Result:
no goals