-- Module: Mathlib.AlgebraicTopology.Quasicategory.StrictSegal
Goal:
X : SSet
sx : X.StrictSegal
n : ℕ
i : Fin (n + 1 + 3)
σ₀ : Λ[n + 1 + 2, i].toSSet ⟶ X
h₀ : 0 < i
hₙ : i < Fin.last (n + 1 + 2)
j : Fin (n + 1 + 3)
hj : j ≠ i
k : Fin (n + 1 + 1)
ksucc : Fin (n + 1 + 1 + 1 + 1) := k.succ.castSucc
heq : j = ksucc
triangle : Λ[n + 3, i].toSSet _⦋2⦌ := horn.primitiveTriangle i h₀ hₙ (↑k : ℕ) ⋯
hi :
  ((horn.spineId i h₀ hₙ).map σ₀).interval (↑k : ℕ) 2 ⋯ =
    X.spine 2
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (σ₀.app (Opposite.op ⦋2⦌)) :
          (a : (fun (X : Type u) ↦ X) (Λ[n + 1 + 2, i].toSSet _⦋2⦌)) → (fun (X : Type u) ↦ X) (X _⦋2⦌))
        triangle)
z : Fin (HAdd.hAdd (α := ℕ) 1 1)
h :
  Eq (α := Fin (n + 1 + 2 + 1))
    ((((Equiv.symm stdSimplex.objEquiv : (a : ⦋1⦌ ⟶ ⦋n + 1 + 2⦌) → Δ[n + 1 + 2] _⦋1⦌)
              (CategoryStruct.comp (Y := ⦋2⦌) (diag 2)
                (((stdSimplex.objEquiv : Δ[n + 1 + 2] _⦋2⦌ ≃ (Opposite.unop (Opposite.op ⦋2⦌) ⟶ ⦋n + 1 + 2⦌)) :
                    (a : Δ[n + 1 + 2] _⦋2⦌) → ⦋2⦌ ⟶ ⦋n + 1 + 2⦌)
                  (↑triangle : Δ[n + 1 + 2] _⦋2⦌))) :
            Δ[n + 1 + 2] _⦋1⦌) :
          (a : Fin 2) → Fin (n + 1 + 2 + 1))
        z :
      Fin (n + 1 + 2 + 1))
    ((((Equiv.symm stdSimplex.objEquiv : (a : ⦋1⦌ ⟶ ⦋n + 1 + 2⦌) → Δ[n + 1 + 2] _⦋1⦌)
              (mkOfSucc k ≫
                ((stdSimplex.objEquiv :
                      Δ[n + 1 + 2] _⦋n + 1 + 1⦌ ≃ (Opposite.unop (Opposite.op ⦋n + 1 + 1⦌) ⟶ ⦋n + 1 + 2⦌)) :
                    (a : Δ[n + 1 + 2] _⦋n + 1 + 1⦌) → ⦋n + 1 + 1⦌ ⟶ ⦋n + 1 + 2⦌)
                  ((yonedaEquiv : (a : Δ[n + 1 + 1] ⟶ Δ[n + 1 + 1 + 1]) → Δ[n + 1 + 1 + 1] _⦋n + 1 + 1⦌)
                    (stdSimplex.map (SimplexCategory.δ j)))) :
            Δ[n + 1 + 2] _⦋1⦌) :
          (a : Fin 2) → Fin (n + 1 + 2 + 1))
        z :
      Fin (n + 1 + 2 + 1))
⊢ Eq (α := Fin (n + 1 + 2 + 1))
    ((((Equiv.symm stdSimplex.objEquiv : (a : Opposite.unop (Opposite.op ⦋1⦌) ⟶ ⦋n + 1 + 2⦌) → Δ[n + 1 + 2] _⦋1⦌)
              (CategoryStruct.comp (Y := Opposite.unop (Opposite.op ⦋2⦌)) (diag 2)
                (((stdSimplex.objEquiv : Δ[n + 1 + 2] _⦋2⦌ ≃ (Opposite.unop (Opposite.op ⦋2⦌) ⟶ ⦋n + 1 + 2⦌)) :
                    (a : Δ[n + 1 + 2] _⦋2⦌) → Opposite.unop (Opposite.op ⦋2⦌) ⟶ ⦋n + 1 + 2⦌)
                  (↑triangle : Δ[n + 1 + 2] _⦋2⦌))) :
            Δ[n + 1 + 2] _⦋1⦌) :
          (a : Fin 2) → Fin (n + 1 + 2 + 1))
        z :
      Fin (n + 1 + 2 + 1))
    ((((Equiv.symm stdSimplex.objEquiv : (a : Opposite.unop (Opposite.op ⦋1⦌) ⟶ ⦋n + 1 + 2⦌) → Δ[n + 1 + 2] _⦋1⦌)
              (mkOfSucc k ≫
                ((stdSimplex.objEquiv :
                      Δ[n + 1 + 2] _⦋n + 1 + 1⦌ ≃ (Opposite.unop (Opposite.op ⦋n + 1 + 1⦌) ⟶ ⦋n + 1 + 2⦌)) :
                    (a : Δ[n + 1 + 2] _⦋n + 1 + 1⦌) → Opposite.unop (Opposite.op ⦋n + 1 + 1⦌) ⟶ ⦋n + 1 + 2⦌)
                  ((yonedaEquiv : (a : Δ[n + 1 + 1] ⟶ Δ[n + 1 + 1 + 1]) → Δ[n + 1 + 1 + 1] _⦋n + 1 + 1⦌)
                    (stdSimplex.δ j))) :
            Δ[n + 1 + 2] _⦋1⦌) :
          (a : Fin 2) → Fin (n + 1 + 2 + 1))
        z :
      Fin (n + 1 + 2 + 1))

Tactic:
dsimp [CosimplicialObject.δ]

Premises used: CategoryTheory.CosimplicialObject.δ