-- Lean 4 proof step from Mathlib.Algebra.Category.MonCat.FilteredColimits (hypothesis)
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 (α :=
    (fun (X : Type (max u v)) ↦ X)
      ((F ⋙
            forget MonCat (FC := fun (x1 x2 : MonCat) ↦ (↑x1 : Type (max u v)) →* (↑x2 : Type (max u v))) (CC :=
              carrier)).obj
        l))
    ((ConcreteCategory.hom (FC := TypeCat.Fun)
            ((F ⋙
                  forget MonCat (FC := fun (x1 x2 : MonCat) ↦ (↑x1 : Type (max u v)) →* (↑x2 : Type (max u v))) (CC :=
                    carrier)).map
              f) :
          (a : (fun (X : Type (max u v)) ↦ X) ((F ⋙ forget MonCat).obj ⟨j₁, y⟩.fst)) →
            (fun (X : Type (max u v)) ↦ X) ((F ⋙ forget MonCat).obj l))
        (Sigma.snd (β := 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)) :
      (fun (X : Type (max u v)) ↦ X)
        ((F ⋙
              forget MonCat (FC := fun (x1 x2 : MonCat) ↦ (↑x1 : Type (max u v)) →* (↑x2 : Type (max u v))) (CC :=
                carrier)).obj
          l))
    ((ConcreteCategory.hom (FC := TypeCat.Fun)
            ((F ⋙
                  forget MonCat (FC := fun (x1 x2 : MonCat) ↦ (↑x1 : Type (max u v)) →* (↑x2 : Type (max u v))) (CC :=
                    carrier)).map
              g) :
          (a : (fun (X : Type (max u v)) ↦ X) ((F ⋙ forget MonCat).obj ⟨j₃, y'⟩.fst)) →
            (fun (X : Type (max u v)) ↦ X) ((F ⋙ forget MonCat).obj l))
        (Sigma.snd (β := 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')) :
      (fun (X : Type (max u v)) ↦ X)
        ((F ⋙
              forget MonCat (FC := fun (x1 x2 : MonCat) ↦ (↑x1 : Type (max u v)) →* (↑x2 : Type (max u v))) (CC :=
                carrier)).obj
          l))
⊢ colimitMulAux F (Sigma.mk (β := fun (j : J) ↦ (↑(F.obj j) : Type (max u v))) j₂ x)
      (Sigma.mk (β := fun (j : J) ↦ (↑(F.obj j) : Type (max u v))) j₁ y) =
    colimitMulAux F (Sigma.mk (β := fun (j : J) ↦ (↑(F.obj j) : Type (max u v))) j₂ x)
      (Sigma.mk (β := fun (j : J) ↦ (↑(F.obj j) : Type (max u v))) j₃ y')
have 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)))
Tactic: simp only [Functor.comp_obj, Functor.comp_map, ConcreteCategory.hom_ofHom,
    TypeCat.Fun.coe_mk] at hfg
Cleared hypotheses: hfg