-- 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
x : (↑(F.obj j₁) : Type (max u v))
j₂ : J
y : (↑(F.obj j₂) : Type (max u v))
j₃ : J
x' : (↑(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₁ x) ⟶
    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₃ x') ⟶
    l
hfg :
  Eq (α := (↑(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 f) :
          (a : (↑(F.obj ⟨j₁, x⟩.fst) : Type (max u v))) → (↑(F.obj l) : Type (max u v)))
        x :
      (↑(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₃, x'⟩.fst) : Type (max u v))) → (↑(F.obj l) : Type (max u v)))
        x' :
      (↑(F.obj l) : Type (max u v)))
s : J
α : IsFiltered.max j₁ j₂ ⟶ s
β : l ⟶ s
γ : IsFiltered.max j₃ j₂ ⟶ s
h₁ : IsFiltered.leftToMax j₁ j₂ ≫ α = f ≫ β
h₂ : IsFiltered.rightToMax j₁ j₂ ≫ α = IsFiltered.rightToMax j₃ j₂ ≫ γ
h₃ : IsFiltered.leftToMax 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, α, γ