-- Module: Mathlib.AlgebraicTopology.SimplicialSet.HornColimits
Goal:
X : SSet
i : Fin (HAdd.hAdd (α := ℕ) 0 2)
f : (j : Fin (HAdd.hAdd (α := ℕ) 0 2)) → j ≠ i → (Δ[0] ⟶ X)
hf : horn.IsCompatible f
a b : (↑{i}ᶜ : Type)
hab :
  Membership.mem (γ := Set ((↑{i}ᶜ : Type) × (↑{i}ᶜ : Type))) {x : (↑{i}ᶜ : Type) × (↑{i}ᶜ : Type) | x.1 < x.2} (a, b)
⊢ Eq (α :=
    MultispanIndex.left
        (MultispanIndex.map (CompleteLattice.MulticoequalizerDiagram.multispanIndex ⋯).toLinearOrder
          Subcomplex.toSSetFunctor)
        (Subtype.mk (p := fun (x : (↑{i}ᶜ : Type) × (↑{i}ᶜ : Type)) ↦
          Membership.mem (γ := Set ((↑{i}ᶜ : Type) × (↑{i}ᶜ : Type))) {x : (↑{i}ᶜ : Type) × (↑{i}ᶜ : Type) | x.1 < x.2}
            x)
          (a, b) hab) ⟶
      X)
    (MultispanIndex.fst
        (MultispanIndex.map (CompleteLattice.MulticoequalizerDiagram.multispanIndex ⋯).toLinearOrder
          Subcomplex.toSSetFunctor)
        (Subtype.mk (p := fun (x : (↑{i}ᶜ : Type) × (↑{i}ᶜ : Type)) ↦
          Membership.mem (γ := Set ((↑{i}ᶜ : Type) × (↑{i}ᶜ : Type))) {x : (↑{i}ᶜ : Type) × (↑{i}ᶜ : Type) | x.1 < x.2}
            x)
          (a, b) hab) ≫
      (fun (x : (MultispanShape.ofLinearOrder (↑{i}ᶜ : Type)).R) ↦
          (match (motive :=
              (x : (MultispanShape.ofLinearOrder (↑{i}ᶜ : Type)).R) →
                MultispanIndex.right
                    (MultispanIndex.map (CompleteLattice.MulticoequalizerDiagram.multispanIndex ⋯).toLinearOrder
                      Subcomplex.toSSetFunctor)
                    x ⟶
                  X)
              x with
            | ⟨j, hj⟩ => (faceSingletonComplIso j).inv ≫ f j hj :
            MultispanIndex.right
                (MultispanIndex.map (CompleteLattice.MulticoequalizerDiagram.multispanIndex ⋯).toLinearOrder
                  Subcomplex.toSSetFunctor)
                x ⟶
              X))
        ((MultispanShape.ofLinearOrder (↑{i}ᶜ : Type)).fst
          (Subtype.mk (p := fun (x : (↑{i}ᶜ : Type) × (↑{i}ᶜ : Type)) ↦
            Membership.mem (γ := Set ((↑{i}ᶜ : Type) × (↑{i}ᶜ : Type)))
              {x : (↑{i}ᶜ : Type) × (↑{i}ᶜ : Type) | x.1 < x.2} x)
            (a, b) hab)))
    (MultispanIndex.snd
        (MultispanIndex.map (CompleteLattice.MulticoequalizerDiagram.multispanIndex ⋯).toLinearOrder
          Subcomplex.toSSetFunctor)
        (Subtype.mk (p := fun (x : (↑{i}ᶜ : Type) × (↑{i}ᶜ : Type)) ↦
          Membership.mem (γ := Set ((↑{i}ᶜ : Type) × (↑{i}ᶜ : Type))) {x : (↑{i}ᶜ : Type) × (↑{i}ᶜ : Type) | x.1 < x.2}
            x)
          (a, b) hab) ≫
      (fun (x : (MultispanShape.ofLinearOrder (↑{i}ᶜ : Type)).R) ↦
          (match (motive :=
              (x : (MultispanShape.ofLinearOrder (↑{i}ᶜ : Type)).R) →
                MultispanIndex.right
                    (MultispanIndex.map (CompleteLattice.MulticoequalizerDiagram.multispanIndex ⋯).toLinearOrder
                      Subcomplex.toSSetFunctor)
                    x ⟶
                  X)
              x with
            | ⟨j, hj⟩ => (faceSingletonComplIso j).inv ≫ f j hj :
            MultispanIndex.right
                (MultispanIndex.map (CompleteLattice.MulticoequalizerDiagram.multispanIndex ⋯).toLinearOrder
                  Subcomplex.toSSetFunctor)
                x ⟶
              X))
        ((MultispanShape.ofLinearOrder (↑{i}ᶜ : Type)).snd
          (Subtype.mk (p := fun (x : (↑{i}ᶜ : Type) × (↑{i}ᶜ : Type)) ↦
            Membership.mem (γ := Set ((↑{i}ᶜ : Type) × (↑{i}ᶜ : Type)))
              {x : (↑{i}ᶜ : Type) × (↑{i}ᶜ : Type) | x.1 < x.2} x)
            (a, b) hab)))

Tactic:
grind