-- Module: Mathlib.AlgebraicTopology.SimplicialSet.HornColimits
Goal:
n : ℕ
X : SSet
i : Fin (n + 2)
f : (j : Fin (n + 2)) → j ≠ i → (Δ[n] ⟶ X)
hf : horn.IsCompatible f
zero :
  ∀ {i : Fin (HAdd.hAdd (α := ℕ) 0 2)} {f : (j : Fin (HAdd.hAdd (α := ℕ) 0 2)) → j ≠ i → (Δ[0] ⟶ X)}
    (hf : horn.IsCompatible f) (a : (MultispanShape.ofLinearOrder (↑{i}ᶜ : Type)).L),
    Eq (α :=
      MultispanIndex.left
          (MultispanIndex.map (CompleteLattice.MulticoequalizerDiagram.multispanIndex ⋯).toLinearOrder
            Subcomplex.toSSetFunctor)
          a ⟶
        X)
      (MultispanIndex.fst
          (MultispanIndex.map (CompleteLattice.MulticoequalizerDiagram.multispanIndex ⋯).toLinearOrder
            Subcomplex.toSSetFunctor)
          a ≫
        (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 a))
      (MultispanIndex.snd
          (MultispanIndex.map (CompleteLattice.MulticoequalizerDiagram.multispanIndex ⋯).toLinearOrder
            Subcomplex.toSSetFunctor)
          a ≫
        (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 a))
succ :
  ∀ (n : ℕ) {i : Fin (n + 1 + 2)} {f : (j : Fin (n + 1 + 2)) → j ≠ i → (Δ[n + 1] ⟶ X)} (hf : horn.IsCompatible f)
    (a : (MultispanShape.ofLinearOrder (↑{i}ᶜ : Type)).L),
    Eq (α :=
      MultispanIndex.left
          (MultispanIndex.map (CompleteLattice.MulticoequalizerDiagram.multispanIndex ⋯).toLinearOrder
            Subcomplex.toSSetFunctor)
          a ⟶
        X)
      (MultispanIndex.fst
          (MultispanIndex.map (CompleteLattice.MulticoequalizerDiagram.multispanIndex ⋯).toLinearOrder
            Subcomplex.toSSetFunctor)
          a ≫
        (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 a))
      (MultispanIndex.snd
          (MultispanIndex.map (CompleteLattice.MulticoequalizerDiagram.multispanIndex ⋯).toLinearOrder
            Subcomplex.toSSetFunctor)
          a ≫
        (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 a))
⊢ ∀ (a : (MultispanShape.ofLinearOrder (↑{i}ᶜ : Type)).L),
    Eq (α :=
      MultispanIndex.left
          (MultispanIndex.map (CompleteLattice.MulticoequalizerDiagram.multispanIndex ⋯).toLinearOrder
            Subcomplex.toSSetFunctor)
          a ⟶
        X)
      (MultispanIndex.fst
          (MultispanIndex.map (CompleteLattice.MulticoequalizerDiagram.multispanIndex ⋯).toLinearOrder
            Subcomplex.toSSetFunctor)
          a ≫
        (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 a))
      (MultispanIndex.snd
          (MultispanIndex.map (CompleteLattice.MulticoequalizerDiagram.multispanIndex ⋯).toLinearOrder
            Subcomplex.toSSetFunctor)
          a ≫
        (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 a))

Tactic:
obtain _ | n := n