-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Types.Coproducts (hypothesis)
Goal:
X Y : Type u
c : BinaryCofan X Y
h₁ :
  Injective (α := (fun (X : Type u) ↦ X) (Functor.obj (pair X Y) { as := left : Discrete WalkingPair })) (β :=
    (fun (X : Type u) ↦ X)
      (Functor.obj (Functor.obj (Functor.const (Discrete WalkingPair)) c.pt) { as := left : Discrete WalkingPair }))
    (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) c.inl) :
      (a : (fun (X : Type u) ↦ X) ((pair X Y).obj { as := left })) →
        (fun (X : Type u) ↦ X) (((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := left }))
h₂ :
  Injective (α := (fun (X : Type u) ↦ X) (Functor.obj (pair X Y) { as := right : Discrete WalkingPair })) (β :=
    (fun (X : Type u) ↦ X)
      (Functor.obj (Functor.obj (Functor.const (Discrete WalkingPair)) c.pt) { as := right : Discrete WalkingPair }))
    (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) c.inr) :
      (a : (fun (X : Type u) ↦ X) ((pair X Y).obj { as := right })) →
        (fun (X : Type u) ↦ X) (((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := right }))
h₃ :
  IsCompl (α :=
    Set
      ((fun (X : Type u) ↦ X)
        (Functor.obj (Functor.obj (Functor.const (Discrete WalkingPair)) c.pt) { as := left : Discrete WalkingPair })))
    (Set.range (ι := (fun (X : Type u) ↦ X) (Functor.obj (pair X Y) { as := left : Discrete WalkingPair }))
      (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) c.inl) :
        (a : (fun (X : Type u) ↦ X) ((pair X Y).obj { as := left })) →
          (fun (X : Type u) ↦ X) (((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := left })))
    (Set.range (ι := (fun (X : Type u) ↦ X) (Functor.obj (pair X Y) { as := right : Discrete WalkingPair }))
      (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) c.inr) :
        (a : (fun (X : Type u) ↦ X) ((pair X Y).obj { as := right })) →
          (fun (X : Type u) ↦ X) (((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := right })))
⊢ Nonempty (IsColimit c)
have this : ∀
  (x :
    (fun (X : Type u) ↦ X)
      (Functor.obj (Functor.obj (Functor.const (Discrete WalkingPair)) c.pt) { as := left : Discrete WalkingPair })),
  Membership.mem (γ :=
      Set
        ((fun (X : Type u) ↦ X)
          (Functor.obj (Functor.obj (Functor.const (Discrete WalkingPair)) c.pt)
            { as := left : Discrete WalkingPair })))
      (Set.range (ι := (fun (X : Type u) ↦ X) (Functor.obj (pair X Y) { as := left : Discrete WalkingPair }))
        (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) c.inl) :
          (a : (fun (X : Type u) ↦ X) ((pair X Y).obj { as := left })) →
            (fun (X : Type u) ↦ X) (((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := left })))
      x ∨
    Membership.mem (γ :=
      Set
        ((fun (X : Type u) ↦ X)
          (Functor.obj (Functor.obj (Functor.const (Discrete WalkingPair)) c.pt)
            { as := right : Discrete WalkingPair })))
      (Set.range (ι := (fun (X : Type u) ↦ X) (Functor.obj (pair X Y) { as := right : Discrete WalkingPair }))
        (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) c.inr) :
          (a : (fun (X : Type u) ↦ X) ((pair X Y).obj { as := right })) →
            (fun (X : Type u) ↦ X) (((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := right })))
      x
Tactic: have : ∀ x, x ∈ Set.range c.inl ∨ x ∈ Set.range c.inr := by
        rw [eq_compl_iff_isCompl.mpr h₃.symm]
        exact fun _ => or_not