-- Module: Mathlib.Algebra.Category.MonCat.FilteredColimits
Goal:
J : Type v
inst : SmallCategory J
F : J ⥤ MonCat
inst_1 : IsFiltered J
j : J
h :
  Eq (α :=
    (↑(F.obj
          (IsFiltered.max
            (Sigma.fst (β := fun (j : J) ↦ (↑(F.obj j) : Type (max u v)))
              (Sigma.mk (β := fun (j : J) ↦ (↑(F.obj j) : Type (max u v))) (Nonempty.some ⋯) 1))
            j)) :
      Type (max u v)))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : MonCat) ↦ (↑x1 : Type (max u v)) →* (↑x2 : Type (max u v))) (CC :=
            carrier) (X :=
            F.obj
              (Sigma.fst (β := fun (j : J) ↦ (↑(F.obj j) : Type (max u v)))
                (Sigma.mk (β := fun (j : J) ↦ (↑(F.obj j) : Type (max u v))) (Nonempty.some ⋯) 1)))
            (Y :=
            F.obj
              (IsFiltered.max
                (Sigma.fst (β := fun (j : J) ↦ (↑(F.obj j) : Type (max u v)))
                  (Sigma.mk (β := fun (j : J) ↦ (↑(F.obj j) : Type (max u v))) (Nonempty.some ⋯) 1))
                j))
            (F.map
              (IsFiltered.leftToMax
                (Sigma.fst (β := fun (j : J) ↦ (↑(F.obj j) : Type (max u v)))
                  (Sigma.mk (β := fun (j : J) ↦ (↑(F.obj j) : Type (max u v))) (Nonempty.some ⋯) 1))
                j)) :
          (a : (↑(F.obj ⟨⋯.some, 1⟩.fst) : Type (max u v))) →
            (↑(F.obj (IsFiltered.max ⟨⋯.some, 1⟩.fst j)) : Type (max u v)))
        (Sigma.snd (β := fun (j : J) ↦ (↑(F.obj j) : Type (max u v)))
          (Sigma.mk (β := fun (j : J) ↦ (↑(F.obj j) : Type (max u v))) (Nonempty.some ⋯) 1)) :
      (↑(F.obj
            (IsFiltered.max
              (Sigma.fst (β := fun (j : J) ↦ (↑(F.obj j) : Type (max u v)))
                (Sigma.mk (β := fun (j : J) ↦ (↑(F.obj j) : Type (max u v))) (Nonempty.some ⋯) 1))
              j)) :
        Type (max u v)))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : MonCat) ↦ (↑x1 : Type (max u v)) →* (↑x2 : Type (max u v))) (CC :=
            carrier) (Y :=
            F.obj
              (IsFiltered.max
                (Sigma.fst (β := fun (j : J) ↦ (↑(F.obj j) : Type (max u v)))
                  (Sigma.mk (β := fun (j : J) ↦ (↑(F.obj j) : Type (max u v))) (Nonempty.some ⋯) 1))
                j))
            (F.map
              (IsFiltered.rightToMax
                (Sigma.fst (β := fun (j : J) ↦ (↑(F.obj j) : Type (max u v)))
                  (Sigma.mk (β := fun (j : J) ↦ (↑(F.obj j) : Type (max u v))) (Nonempty.some ⋯) 1))
                j)) :
          (a : (↑(F.obj ⟨j, 1⟩.fst) : Type (max u v))) → (↑(F.obj (IsFiltered.max ⟨⋯.some, 1⟩.fst j)) : Type (max u v)))
        (Sigma.snd (β := fun (j : J) ↦ (↑(F.obj j) : Type (max u v)))
          (Sigma.mk (β := fun (j : J) ↦ (↑(F.obj j) : Type (max u v))) j 1)) :
      (↑(F.obj
            (IsFiltered.max
              (Sigma.fst (β := fun (j : J) ↦ (↑(F.obj j) : Type (max u v)))
                (Sigma.mk (β := fun (j : J) ↦ (↑(F.obj j) : Type (max u v))) (Nonempty.some ⋯) 1))
              j)) :
        Type (max u v)))
⊢ ∃ (k : J) (f :
    Sigma.fst (β := fun (j : J) ↦ (↑(F.obj j) : Type (max u v)))
        (Sigma.mk (β := fun (j : J) ↦ (↑(F.obj j) : Type (max u v))) (Nonempty.some ⋯) 1) ⟶
      k)
    (g :
    Sigma.fst (β := fun (j : J) ↦ (↑(F.obj j) : Type (max u v)))
        (Sigma.mk (β := fun (j : J) ↦ (↑(F.obj j) : Type (max u v))) j 1) ⟶
      k),
    Eq (α := (↑(F.obj k) : Type (max u v)))
      ((ConcreteCategory.hom (FC := fun (x1 x2 : MonCat) ↦ (↑x1 : Type (max u v)) →* (↑x2 : Type (max u v))) (CC :=
              carrier) (F.map f) :
            (a : (↑(F.obj ⟨⋯.some, 1⟩.fst) : Type (max u v))) → (↑(F.obj k) : Type (max u v)))
          (Sigma.snd (β := fun (j : J) ↦ (↑(F.obj j) : Type (max u v)))
            (Sigma.mk (β := fun (j : J) ↦ (↑(F.obj j) : Type (max u v))) (Nonempty.some ⋯) 1)) :
        (↑(F.obj k) : Type (max u v)))
      ((ConcreteCategory.hom (FC := fun (x1 x2 : MonCat) ↦ (↑x1 : Type (max u v)) →* (↑x2 : Type (max u v))) (CC :=
              carrier) (F.map g) :
            (a : (↑(F.obj ⟨j, 1⟩.fst) : Type (max u v))) → (↑(F.obj k) : Type (max u v)))
          (Sigma.snd (β := fun (j : J) ↦ (↑(F.obj j) : Type (max u v)))
            (Sigma.mk (β := fun (j : J) ↦ (↑(F.obj j) : Type (max u v))) j 1)) :
        (↑(F.obj k) : Type (max u v)))

Tactic:
refine ⟨max' _ j, IsFiltered.leftToMax _ j, IsFiltered.rightToMax _ j, ?_⟩