-- Module: Mathlib.Algebra.Category.MonCat.FilteredColimits
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 ≫ β
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)))
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
use s, α, γ