-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.HornColimits (goal)
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))
⊢ ∀ (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))
have 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 sorry).toLinearOrder
          Subcomplex.toSSetFunctor)
        a ⟶
      X)
    (MultispanIndex.fst
        (MultispanIndex.map (CompleteLattice.MulticoequalizerDiagram.multispanIndex sorry).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 sorry).toLinearOrder
                      Subcomplex.toSSetFunctor)
                    x ⟶
                  X)
              x with
            | ⟨j, hj⟩ => (faceSingletonComplIso j).inv ≫ f j hj :
            MultispanIndex.right
                (MultispanIndex.map (CompleteLattice.MulticoequalizerDiagram.multispanIndex sorry).toLinearOrder
                  Subcomplex.toSSetFunctor)
                x ⟶
              X))
        ((MultispanShape.ofLinearOrder (↑{i}ᶜ : Type)).fst a))
    (MultispanIndex.snd
        (MultispanIndex.map (CompleteLattice.MulticoequalizerDiagram.multispanIndex sorry).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 sorry).toLinearOrder
                      Subcomplex.toSSetFunctor)
                    x ⟶
                  X)
              x with
            | ⟨j, hj⟩ => (faceSingletonComplIso j).inv ≫ f j hj :
            MultispanIndex.right
                (MultispanIndex.map (CompleteLattice.MulticoequalizerDiagram.multispanIndex sorry).toLinearOrder
                  Subcomplex.toSSetFunctor)
                x ⟶
              X))
        ((MultispanShape.ofLinearOrder (↑{i}ᶜ : Type)).snd a))
Tactic: obtain _ | n := n
Cleared hypotheses: n, i, f, hf