-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Types.ColimitTypeFiltered (goal)
Goal:
J : Type u
inst : Category.{v, u} J
inst_1 : IsFiltered.{v, u} J
F : Functor.{v, w₀, u, w₀ + 1} J (Type w₀)
c : CoconeTypes.{w₁, w₀, v, u} F
mp :
  (∀ (j j' : J) (x : F.obj j) (x' : F.obj j'),
      c.ι j x = c.ι j' x' →
        ∃ (k : J) (f : j ⟶ k) (f' : j' ⟶ k),
          Eq (α := (fun (X : Type w₀) ↦ X) (F.obj k))
            ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f) :
                  (a : (fun (X : Type w₀) ↦ X) (F.obj j)) → (fun (X : Type w₀) ↦ X) (F.obj k))
                x :
              (fun (X : Type w₀) ↦ X) (F.obj k))
            ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f') :
                  (a : (fun (X : Type w₀) ↦ X) (F.obj j')) → (fun (X : Type w₀) ↦ X) (F.obj k))
                x' :
              (fun (X : Type w₀) ↦ X) (F.obj k))) →
    ∀ (j : J) (x x' : F.obj j),
      c.ι j x = c.ι j x' →
        ∃ (k : J) (f : j ⟶ k),
          Eq (α := (fun (X : Type w₀) ↦ X) (F.obj k))
            ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f) :
                  (a : (fun (X : Type w₀) ↦ X) (F.obj j)) → (fun (X : Type w₀) ↦ X) (F.obj k))
                x :
              (fun (X : Type w₀) ↦ X) (F.obj k))
            ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f) :
                  (a : (fun (X : Type w₀) ↦ X) (F.obj j)) → (fun (X : Type w₀) ↦ X) (F.obj k))
                x' :
              (fun (X : Type w₀) ↦ X) (F.obj k))
⊢ (∀ (j j' : J) (x : F.obj j) (x' : F.obj j'),
      c.ι j x = c.ι j' x' →
        ∃ (k : J) (f : j ⟶ k) (f' : j' ⟶ k),
          Eq (α := (fun (X : Type w₀) ↦ X) (F.obj k))
            ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f) :
                  (a : (fun (X : Type w₀) ↦ X) (F.obj j)) → (fun (X : Type w₀) ↦ X) (F.obj k))
                x :
              (fun (X : Type w₀) ↦ X) (F.obj k))
            ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f') :
                  (a : (fun (X : Type w₀) ↦ X) (F.obj j')) → (fun (X : Type w₀) ↦ X) (F.obj k))
                x' :
              (fun (X : Type w₀) ↦ X) (F.obj k))) ↔
    ∀ (j : J) (x x' : F.obj j),
      c.ι j x = c.ι j x' →
        ∃ (k : J) (f : j ⟶ k),
          Eq (α := (fun (X : Type w₀) ↦ X) (F.obj k))
            ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f) :
                  (a : (fun (X : Type w₀) ↦ X) (F.obj j)) → (fun (X : Type w₀) ↦ X) (F.obj k))
                x :
              (fun (X : Type w₀) ↦ X) (F.obj k))
            ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f) :
                  (a : (fun (X : Type w₀) ↦ X) (F.obj j)) → (fun (X : Type w₀) ↦ X) (F.obj k))
                x' :
              (fun (X : Type w₀) ↦ X) (F.obj k))
have mpr : (∀ (j : J) (x x' : F.obj j),
    c.ι j x = c.ι j x' →
      ∃ (k : J) (f : j ⟶ k),
        Eq (α := (fun (X : Type w₀) ↦ X) (F.obj k))
          ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f) :
                (a : (fun (X : Type w₀) ↦ X) (F.obj j)) → (fun (X : Type w₀) ↦ X) (F.obj k))
              x :
            (fun (X : Type w₀) ↦ X) (F.obj k))
          ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f) :
                (a : (fun (X : Type w₀) ↦ X) (F.obj j)) → (fun (X : Type w₀) ↦ X) (F.obj k))
              x' :
            (fun (X : Type w₀) ↦ X) (F.obj k))) →
  ∀ (j j' : J) (x : F.obj j) (x' : F.obj j'),
    c.ι j x = c.ι j' x' →
      ∃ (k : J) (f : j ⟶ k) (f' : j' ⟶ k),
        Eq (α := (fun (X : Type w₀) ↦ X) (F.obj k))
          ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f) :
                (a : (fun (X : Type w₀) ↦ X) (F.obj j)) → (fun (X : Type w₀) ↦ X) (F.obj k))
              x :
            (fun (X : Type w₀) ↦ X) (F.obj k))
          ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f') :
                (a : (fun (X : Type w₀) ↦ X) (F.obj j')) → (fun (X : Type w₀) ↦ X) (F.obj k))
              x' :
            (fun (X : Type w₀) ↦ X) (F.obj k))
Tactic: constructor