-- Module: Mathlib.Algebra.Category.MonCat.FilteredColimits
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 ≫ β
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, α, γ