-- 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
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 (α :=
    (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₁, x⟩.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₁ x)) :
      (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₃, x'⟩.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₃ x')) :
      (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 (α := (↑(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)))
Tactic: replace hfg : F.map f x = F.map g x' := by simpa
Cleared hypotheses: hfg