-- Lean 4 proof step from Mathlib.Algebra.Category.MonCat.FilteredColimits (goal)
Goal:
J : Type v
inst : SmallCategory J
F : J ⥤ MonCat
inst_1 : IsFiltered J
j : J
⊢ ∃ (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)))
have 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 sorry) 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 sorry) 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 sorry) 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 sorry) 1))
              j)) :
        (a : (↑(F.obj ⟨sorry.some, 1⟩.fst) : Type (max u v))) →
          (↑(F.obj (IsFiltered.max ⟨sorry.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 sorry) 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 sorry) 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 sorry) 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 sorry) 1))
              j)) :
        (a : (↑(F.obj ⟨j, 1⟩.fst) : Type (max u v))) → (↑(F.obj (IsFiltered.max ⟨sorry.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 sorry) 1))
            j)) :
      Type (max u v)))
Tactic: refine ⟨max' _ j, IsFiltered.leftToMax _ j, IsFiltered.rightToMax _ j, ?_⟩