-- Mathlib/CategoryTheory/Limits/Shapes/Types.lean
theorem binaryCofan_isColimit_iff {X Y : Type u} (c : BinaryCofan X Y) :
    Nonempty (IsColimit c) ↔
      Injective c.inl ∧ Injective c.inr ∧ IsCompl (Set.range c.inl) (Set.range c.inr)

Proof state:
case mp.intro
X Y : Type u
c : BinaryCofan X Y
h : IsColimit c
⊢ Injective c.inl ∧ Injective c.inr ∧ IsCompl (Set.range c.inl) (Set.range c.inr)

Tactic:
rw [← show _ = c.inl from
    h.comp_coconePointUniqueUpToIso_inv (binaryCoproductColimit X Y) ⟨WalkingPair.left⟩,
  ← show _ = c.inr from
    h.comp_coconePointUniqueUpToIso_inv (binaryCoproductColimit X Y) ⟨WalkingPair.right⟩]

Result:
case mp.intro
X Y : Type u
c : BinaryCofan X Y
h : IsColimit c
⊢ Injective
      ((binaryCoproductCocone X Y).ι.app { as := left } ≫
        (h.coconePointUniqueUpToIso (binaryCoproductColimit X Y)).inv) ∧
    Injective
        ((binaryCoproductCocone X Y).ι.app { as := right } ≫
          (h.coconePointUniqueUpToIso (binaryCoproductColimit X Y)).inv) ∧
      IsCompl
        (Set.range
          ((binaryCoproductCocone X Y).ι.app { as := left } ≫
            (h.coconePointUniqueUpToIso (binaryCoproductColimit X Y)).inv))
        (Set.range
          ((binaryCoproductCocone X Y).ι.app { as := right } ≫
            (h.coconePointUniqueUpToIso (binaryCoproductColimit X Y)).inv))

Proof state:
case mpr.intro.intro.refine_2
X Y : Type u
c : BinaryCofan X Y
h₁ : Injective c.inl
h₂ : Injective c.inr
h₃ : IsCompl (Set.range c.inl) (Set.range c.inr)
this :
  ∀ (x : ((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := left }),
    x ∈ Set.range c.inl ∨ x ∈ Set.range c.inr
⊢ ∀ {T : Type u} (f : X ⟶ T) (g : Y ⟶ T),
    (c.inl ≫ fun x =>
        if h : x ∈ Set.range c.inl then f ((Equiv.ofInjective c.inl h₁).symm ⟨x, h⟩)
        else g ((Equiv.ofInjective c.inr h₂).symm ⟨x, ⋯⟩)) =
      f

Tactic:
intro T f g

Result:
case mpr.intro.intro.refine_2
X Y : Type u
c : BinaryCofan X Y
h₁ : Injective c.inl
h₂ : Injective c.inr
h₃ : IsCompl (Set.range c.inl) (Set.range c.inr)
this :
  ∀ (x : ((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := left }),
    x ∈ Set.range c.inl ∨ x ∈ Set.range c.inr
T : Type u
f : X ⟶ T
g : Y ⟶ T
⊢ (c.inl ≫ fun x =>
      if h : x ∈ Set.range c.inl then f ((Equiv.ofInjective c.inl h₁).symm ⟨x, h⟩)
      else g ((Equiv.ofInjective c.inr h₂).symm ⟨x, ⋯⟩)) =
    f

Proof state:
case mpr.intro.intro.refine_3.h
X Y : Type u
c : BinaryCofan X Y
h₁ : Injective c.inl
h₂ : Injective c.inr
h₃ : IsCompl (Set.range c.inl) (Set.range c.inr)
this✝ :
  ∀ (x : ((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := left }),
    x ∈ Set.range c.inl ∨ x ∈ Set.range c.inr
T : Type u
f : X ⟶ T
g : Y ⟶ T
x : (pair X Y).obj { as := right }
y : X
e : c.inl y = c.inr x
this : c.inr x ∈ ⊥
⊢ f ((Equiv.ofInjective c.inl h₁).symm ⟨c.inr x, ⋯⟩) = g x

Tactic:
exact this.elim

Result:
no goals

Proof state:
case mpr.intro.intro.refine_4.h
X Y : Type u
c : BinaryCofan X Y
h₁ : Injective c.inl
h₂ : Injective c.inr
h₃ : IsCompl (Set.range c.inl) (Set.range c.inr)
this :
  ∀ (x : ((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := left }),
    x ∈ Set.range c.inl ∨ x ∈ Set.range c.inr
T : Type u
m : c.pt ⟶ T
x : c.pt
⊢ m x =
    if h : x ∈ Set.range c.inl then m (c.inl ((Equiv.ofInjective c.inl h₁).symm ⟨x, h⟩))
    else m (c.inr ((Equiv.ofInjective c.inr h₂).symm ⟨x, ⋯⟩))

Tactic:
split_ifs <;> exact congr_arg _ (Equiv.apply_ofInjective_symm _ ⟨_, _⟩).symm

Result:
no goals

Proof state:
X Y : Type u
c : BinaryCofan X Y
h₁ : Injective c.inl
h₂ : Injective c.inr
h₃ : IsCompl (Set.range c.inl) (Set.range c.inr)
⊢ ∀ (x : ((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := left }),
    x ∈ Set.range c.inl ∨ x ∈ Set.range c.inr

Tactic:
rw [eq_compl_iff_isCompl.mpr h₃.symm]

Result:
X Y : Type u
c : BinaryCofan X Y
h₁ : Injective c.inl
h₂ : Injective c.inr
h₃ : IsCompl (Set.range c.inl) (Set.range c.inr)
⊢ ∀ (x : ((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := left }),
    x ∈ Set.range c.inl ∨ x ∈ (Set.range c.inl)ᶜ

Proof state:
case mpr.intro.intro.refine_3.h
X Y : Type u
c : BinaryCofan X Y
h₁ : Injective c.inl
h₂ : Injective c.inr
h₃ : IsCompl (Set.range c.inl) (Set.range c.inr)
this :
  ∀ (x : ((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := left }),
    x ∈ Set.range c.inl ∨ x ∈ Set.range c.inr
T : Type u
f : X ⟶ T
g : Y ⟶ T
x : (pair X Y).obj { as := right }
y : X
e : c.inl y = c.inr x
⊢ f ((Equiv.ofInjective c.inl h₁).symm ⟨c.inr x, ⋯⟩) = g x

Tactic:
have : c.inr x ∈ Set.range c.inl ⊓ Set.range c.inr := ⟨⟨_, e⟩, ⟨_, rfl⟩⟩

Result:
case mpr.intro.intro.refine_3.h
X Y : Type u
c : BinaryCofan X Y
h₁ : Injective c.inl
h₂ : Injective c.inr
h₃ : IsCompl (Set.range c.inl) (Set.range c.inr)
this✝ :
  ∀ (x : ((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := left }),
    x ∈ Set.range c.inl ∨ x ∈ Set.range c.inr
T : Type u
f : X ⟶ T
g : Y ⟶ T
x : (pair X Y).obj { as := right }
y : X
e : c.inl y = c.inr x
this : c.inr x ∈ Set.range c.inl ⊓ Set.range c.inr
⊢ f ((Equiv.ofInjective c.inl h₁).symm ⟨c.inr x, ⋯⟩) = g x