-- 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
y : (↑(F.obj j₁) : Type (max u v))
j₂ : J
x : (↑(F.obj j₂) : Type (max u v))
j₃ : J
y' : (↑(F.obj j₃) : Type (max u v))
l : J
f :
  Sigma.fst (β := fun (j : J) ↦
      (F ⋙
            forget MonCat (FC := fun (x1 x2 : MonCat) ↦ (↑x1 : Type (max u v)) →* (↑x2 : Type (max u v))) (CC :=
              carrier)).obj
        j)
      (Sigma.mk (β := fun (j : J) ↦ (↑(F.obj j) : Type (max u v))) j₁ y) ⟶
    l
g :
  Sigma.fst (β := fun (j : J) ↦
      (F ⋙
            forget MonCat (FC := fun (x1 x2 : MonCat) ↦ (↑x1 : Type (max u v)) →* (↑x2 : Type (max u v))) (CC :=
              carrier)).obj
        j)
      (Sigma.mk (β := fun (j : J) ↦ (↑(F.obj j) : Type (max u v))) j₃ y') ⟶
    l
hfg :
  Eq (α :=
    ToType (FC := fun (x1 x2 : MonCat) ↦ (↑x1 : Type (max u v)) →* (↑x2 : Type (max u v))) (CC := carrier) (F.obj l))
    ((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 j₁) : Type (max u v))) → (↑(F.obj l) : Type (max u v)))
        y :
      (↑(F.obj l) : 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₃) : Type (max u v))) → (↑(F.obj l) : Type (max u v)))
        y' :
      (↑(F.obj l) : Type (max u v)))
s : J
α : IsFiltered.max j₂ j₁ ⟶ s
β : l ⟶ s
γ : IsFiltered.max j₂ j₃ ⟶ s
h₁ : IsFiltered.rightToMax j₂ j₁ ≫ α = f ≫ β
h₂ : IsFiltered.leftToMax j₂ j₁ ≫ α = IsFiltered.leftToMax j₂ j₃ ≫ γ
h₃ : IsFiltered.rightToMax j₂ j₃ ≫ γ = g ≫ β
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
have h : Eq (α := (↑(F.obj s) : 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 α) :
        (a :
            (↑(F.obj
                  ⟨IsFiltered.max ⟨j₂, x⟩.fst ⟨j₁, y⟩.fst,
                      (ConcreteCategory.hom (F.map (IsFiltered.leftToMax ⟨j₂, x⟩.fst ⟨j₁, y⟩.fst)) :
                            (a : (↑(F.obj ⟨j₂, x⟩.fst) : Type (max u v))) →
                              (↑(F.obj (IsFiltered.max ⟨j₂, x⟩.fst ⟨j₁, y⟩.fst)) : Type (max u v)))
                          ⟨j₂, x⟩.snd *
                        (ConcreteCategory.hom (F.map (IsFiltered.rightToMax ⟨j₂, x⟩.fst ⟨j₁, y⟩.fst)) :
                            (a : (↑(F.obj ⟨j₁, y⟩.fst) : Type (max u v))) →
                              (↑(F.obj (IsFiltered.max ⟨j₂, x⟩.fst ⟨j₁, y⟩.fst)) : Type (max u v)))
                          ⟨j₁, y⟩.snd⟩.fst) :
              Type (max u v))) →
          (↑(F.obj s) : 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)))
          (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))) j₂ x))
            (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₁ y)))
          (HMul.hMul (α :=
            (↑(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))) j₂ x))
                    (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₁ y)))) :
              Type (max u v)))
            (β :=
            (↑(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))) j₂ x))
                    (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₁ y)))) :
              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))) j₂ x))
                        (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₁ y))))
                    (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))) j₂ x))
                        (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₁ y)))) :
                  (a : (↑(F.obj ⟨j₂, x⟩.fst) : Type (max u v))) →
                    (↑(F.obj (IsFiltered.max ⟨j₂, x⟩.fst ⟨j₁, y⟩.fst)) : 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₂ x)) :
              (↑(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))) j₂ x))
                      (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₁ y)))) :
                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))) j₁ y)))
                    (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))) j₂ x))
                        (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₁ y))))
                    (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))) j₂ x))
                        (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₁ y)))) :
                  (a : (↑(F.obj ⟨j₁, y⟩.fst) : Type (max u v))) →
                    (↑(F.obj (IsFiltered.max ⟨j₂, x⟩.fst ⟨j₁, y⟩.fst)) : 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₁ 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))) j₂ x))
                      (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₁ y)))) :
                Type (max u v)))))) :
    (↑(F.obj s) : 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 γ) :
        (a :
            (↑(F.obj
                  ⟨IsFiltered.max ⟨j₂, x⟩.fst ⟨j₃, y'⟩.fst,
                      (ConcreteCategory.hom (F.map (IsFiltered.leftToMax ⟨j₂, x⟩.fst ⟨j₃, y'⟩.fst)) :
                            (a : (↑(F.obj ⟨j₂, x⟩.fst) : Type (max u v))) →
                              (↑(F.obj (IsFiltered.max ⟨j₂, x⟩.fst ⟨j₃, y'⟩.fst)) : Type (max u v)))
                          ⟨j₂, x⟩.snd *
                        (ConcreteCategory.hom (F.map (IsFiltered.rightToMax ⟨j₂, x⟩.fst ⟨j₃, y'⟩.fst)) :
                            (a : (↑(F.obj ⟨j₃, y'⟩.fst) : Type (max u v))) →
                              (↑(F.obj (IsFiltered.max ⟨j₂, x⟩.fst ⟨j₃, y'⟩.fst)) : Type (max u v)))
                          ⟨j₃, y'⟩.snd⟩.fst) :
              Type (max u v))) →
          (↑(F.obj s) : 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)))
          (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))) j₂ x))
            (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₃ y')))
          (HMul.hMul (α :=
            (↑(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))) j₂ x))
                    (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₃ y')))) :
              Type (max u v)))
            (β :=
            (↑(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))) j₂ x))
                    (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₃ y')))) :
              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))) j₂ x))
                        (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₃ y'))))
                    (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))) j₂ x))
                        (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₃ y')))) :
                  (a : (↑(F.obj ⟨j₂, x⟩.fst) : Type (max u v))) →
                    (↑(F.obj (IsFiltered.max ⟨j₂, x⟩.fst ⟨j₃, y'⟩.fst)) : 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₂ x)) :
              (↑(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))) j₂ x))
                      (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₃ y')))) :
                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))) j₃ y')))
                    (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))) j₂ x))
                        (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₃ y'))))
                    (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))) j₂ x))
                        (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₃ y')))) :
                  (a : (↑(F.obj ⟨j₃, y'⟩.fst) : Type (max u v))) →
                    (↑(F.obj (IsFiltered.max ⟨j₂, x⟩.fst ⟨j₃, y'⟩.fst)) : 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₃ 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))) j₂ x))
                      (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₃ y')))) :
                Type (max u v)))))) :
    (↑(F.obj s) : Type (max u v)))
Tactic: use s, α, γ