-- Module: Mathlib.CategoryTheory.Limits.Types.ColimitTypeFiltered
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
h :
  ∀ (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'
eq : c.ι j x = c.ι j' x'
mpr :
  ∀ (k : J) (g : IsFiltered.max.{v, u} j j' ⟶ k)
    (eq :
      Eq (α := (fun (X : Type w₀) ↦ X) (F.obj k))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map g) :
              (a : (fun (X : Type w₀) ↦ X) (F.obj (IsFiltered.max j j'))) → (fun (X : Type w₀) ↦ X) (F.obj k))
            ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (leftToMax j j')) :
                  (a : (fun (X : Type w₀) ↦ X) (F.obj j)) → (fun (X : Type w₀) ↦ X) (F.obj (IsFiltered.max j j')))
                x :
              (fun (X : Type w₀) ↦ X) (F.obj (IsFiltered.max.{v, u} j j'))) :
          (fun (X : Type w₀) ↦ X) (F.obj k))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map g) :
              (a : (fun (X : Type w₀) ↦ X) (F.obj (IsFiltered.max j j'))) → (fun (X : Type w₀) ↦ X) (F.obj k))
            ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (rightToMax j j')) :
                  (a : (fun (X : Type w₀) ↦ X) (F.obj j')) → (fun (X : Type w₀) ↦ X) (F.obj (IsFiltered.max j j')))
                x' :
              (fun (X : Type w₀) ↦ X) (F.obj (IsFiltered.max.{v, u} j j'))) :
          (fun (X : Type w₀) ↦ X) (F.obj k))),
    ∃ (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))
⊢ ∃ (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:
obtain ⟨k, g, eq⟩ := h (max j j') (F.map (leftToMax _ _) x)
      (F.map (rightToMax _ _) x') (by simpa only [c.ι_naturality_apply])

Premises used: CategoryTheory.IsFiltered.rightToMax, CategoryTheory.ConcreteCategory.hom, CategoryTheory.IsFiltered.max, CategoryTheory.Functor.map, CategoryTheory.IsFiltered.leftToMax, DFunLike.coe