-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.HornColimits (hypothesis)
Goal:
X : SSet
n : ℕ
i : Fin (n + 1 + 2)
f : (j : Fin (n + 1 + 2)) → j ≠ i → (Δ[n + 1] ⟶ X)
hf : horn.IsCompatible f
a : Fin (n + 1 + 1 + 1)
ha : Membership.mem (γ := Set (Fin (n + 1 + 1 + 1))) {i}ᶜ a
b : Fin (n + 1 + 1 + 1)
hb : Membership.mem (γ := Set (Fin (n + 1 + 1 + 1))) {i}ᶜ b
hab : a < b
⊢ Eq (α :=
    MultispanIndex.left (J := MultispanShape.ofLinearOrder (↑{i}ᶜ : Type))
        (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)
          (Subtype.mk (p := fun (x : Fin (n + 1 + 1 + 1)) ↦ Membership.mem (γ := Set (Fin (n + 1 + 1 + 1))) {i}ᶜ x) a
              ha,
            Subtype.mk (p := fun (x : Fin (n + 1 + 1 + 1)) ↦ Membership.mem (γ := Set (Fin (n + 1 + 1 + 1))) {i}ᶜ x) b
              hb)
          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)
          (Subtype.mk (p := fun (x : Fin (n + 1 + 1 + 1)) ↦ Membership.mem (γ := Set (Fin (n + 1 + 1 + 1))) {i}ᶜ x) a
              ha,
            Subtype.mk (p := fun (x : Fin (n + 1 + 1 + 1)) ↦ Membership.mem (γ := Set (Fin (n + 1 + 1 + 1))) {i}ᶜ x) b
              hb)
          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)
            (Subtype.mk (p := fun (x : Fin (n + 1 + 1 + 1)) ↦ Membership.mem (γ := Set (Fin (n + 1 + 1 + 1))) {i}ᶜ x) a
                ha,
              Subtype.mk (p := fun (x : Fin (n + 1 + 1 + 1)) ↦ Membership.mem (γ := Set (Fin (n + 1 + 1 + 1))) {i}ᶜ x) b
                hb)
            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)
          (Subtype.mk (p := fun (x : Fin (n + 1 + 1 + 1)) ↦ Membership.mem (γ := Set (Fin (n + 1 + 1 + 1))) {i}ᶜ x) a
              ha,
            Subtype.mk (p := fun (x : Fin (n + 1 + 1 + 1)) ↦ Membership.mem (γ := Set (Fin (n + 1 + 1 + 1))) {i}ᶜ x) b
              hb)
          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)
            (Subtype.mk (p := fun (x : Fin (n + 1 + 1 + 1)) ↦ Membership.mem (γ := Set (Fin (n + 1 + 1 + 1))) {i}ᶜ x) a
                ha,
              Subtype.mk (p := fun (x : Fin (n + 1 + 1 + 1)) ↦ Membership.mem (γ := Set (Fin (n + 1 + 1 + 1))) {i}ᶜ x) b
                hb)
            hab)))
have ha₁ : ¬a = i
Tactic: simp only [Set.mem_compl_iff, Set.mem_singleton_iff] at ha hb