-- Lean 4 proof step from Mathlib.AlgebraicTopology.Quasicategory.StrictSegal (goal)
Goal:
X : SSet
sx : X.StrictSegal
i : Fin (HAdd.hAdd (α := ℕ) 0 3)
σ₀ : Λ[HAdd.hAdd (α := ℕ) 0 2, i].toSSet ⟶ X
h₀ : 0 < i
hₙ : i < Fin.last (HAdd.hAdd (α := ℕ) 0 2)
j : Fin (HAdd.hAdd (α := ℕ) 0 3)
hj : j ≠ i
ksucc : Fin (HAdd.hAdd (α := ℕ) 0 1 + 1 + 1) := Fin.castSucc (Fin.succ 0)
heq : j = ksucc
h :
  ∀
    (σ₀ :
      Subcomplex.toSSet (X := Δ[HAdd.hAdd (α := ℕ) 0 2])
          Λ[HAdd.hAdd (α := ℕ) 0 2, (fun (i : Fin (⦋2⦌.len + 1)) ↦ i) (⟨0, ⋯⟩ : Fin (⦋2⦌.len + 1))] ⟶
        X)
    (h₀ : LT.lt (α := Fin (HAdd.hAdd (α := ℕ) 0 3)) 0 ((fun (i : Fin (⦋2⦌.len + 1)) ↦ i) ⟨0, ⋯⟩))
    (hₙ :
      LT.lt (α := Fin (HAdd.hAdd (α := ℕ) 0 3)) ((fun (i : Fin (⦋2⦌.len + 1)) ↦ i) ⟨0, ⋯⟩)
        (Fin.last (HAdd.hAdd (α := ℕ) 0 2)))
    (hj : j ≠ (fun (i : Fin (⦋2⦌.len + 1)) ↦ i) ⟨0, ⋯⟩),
    Eq (α := X _⦋1⦌)
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (Quiver.Hom.op (mkOfSucc 0))) : (a : X _⦋0 + 1⦌) → X _⦋1⦌)
          ((ConcreteCategory.hom (FC := TypeCat.Fun) (SimplicialObject.δ X j) : (a : X _⦋0 + 1 + 1⦌) → X _⦋0 + 1⦌)
              (sx.spineToSimplex
                ((horn.spineId ((fun (i : Fin (⦋2⦌.len + 1)) ↦ i) (⟨0, ⋯⟩ : Fin (⦋2⦌.len + 1))) h₀ hₙ).map σ₀)) :
            X _⦋HAdd.hAdd (α := ℕ) 0 1⦌) :
        X _⦋1⦌)
      ((ConcreteCategory.hom (FC := TypeCat.Fun)
              ((Subcomplex.toSSet (X := Δ[HAdd.hAdd (α := ℕ) 0 2])
                      Λ[HAdd.hAdd (α := ℕ) 0 2, (fun (i : Fin (⦋2⦌.len + 1)) ↦ i) (⟨0, ⋯⟩ : Fin (⦋2⦌.len + 1))]).map
                  (Quiver.Hom.op (mkOfSucc 0)) ≫
                σ₀.app (Opposite.op ⦋1⦌)) :
            (a : (fun (X : Type u) ↦ X) (Λ[0 + 2, (fun (i : Fin (⦋2⦌.len + 1)) ↦ i) ⟨0, ⋯⟩].toSSet _⦋0 + 1⦌)) →
              (fun (X : Type u) ↦ X) (X _⦋1⦌))
          (horn.face ((fun (i : Fin (⦋2⦌.len + 1)) ↦ i) (⟨0, ⋯⟩ : Fin (⦋2⦌.len + 1))) j hj) :
        (fun (X : Type u) ↦ X) (X _⦋1⦌))
h₁ :
  ∀
    (σ₀ :
      Subcomplex.toSSet (X := Δ[HAdd.hAdd (α := ℕ) 0 2])
          Λ[HAdd.hAdd (α := ℕ) 0 2, (fun (i : Fin (⦋2⦌.len + 1)) ↦ i) (⟨1, ⋯⟩ : Fin (⦋2⦌.len + 1))] ⟶
        X)
    (h₀ : LT.lt (α := Fin (HAdd.hAdd (α := ℕ) 0 3)) 0 ((fun (i : Fin (⦋2⦌.len + 1)) ↦ i) ⟨1, ⋯⟩))
    (hₙ :
      LT.lt (α := Fin (HAdd.hAdd (α := ℕ) 0 3)) ((fun (i : Fin (⦋2⦌.len + 1)) ↦ i) ⟨1, ⋯⟩)
        (Fin.last (HAdd.hAdd (α := ℕ) 0 2)))
    (hj : j ≠ (fun (i : Fin (⦋2⦌.len + 1)) ↦ i) ⟨1, ⋯⟩),
    Eq (α := X _⦋1⦌)
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (Quiver.Hom.op (mkOfSucc 0))) : (a : X _⦋0 + 1⦌) → X _⦋1⦌)
          ((ConcreteCategory.hom (FC := TypeCat.Fun) (SimplicialObject.δ X j) : (a : X _⦋0 + 1 + 1⦌) → X _⦋0 + 1⦌)
              (sx.spineToSimplex
                ((horn.spineId ((fun (i : Fin (⦋2⦌.len + 1)) ↦ i) (⟨1, ⋯⟩ : Fin (⦋2⦌.len + 1))) h₀ hₙ).map σ₀)) :
            X _⦋HAdd.hAdd (α := ℕ) 0 1⦌) :
        X _⦋1⦌)
      ((ConcreteCategory.hom (FC := TypeCat.Fun)
              ((Subcomplex.toSSet (X := Δ[HAdd.hAdd (α := ℕ) 0 2])
                      Λ[HAdd.hAdd (α := ℕ) 0 2, (fun (i : Fin (⦋2⦌.len + 1)) ↦ i) (⟨1, ⋯⟩ : Fin (⦋2⦌.len + 1))]).map
                  (Quiver.Hom.op (mkOfSucc 0)) ≫
                σ₀.app (Opposite.op ⦋1⦌)) :
            (a : (fun (X : Type u) ↦ X) (Λ[0 + 2, (fun (i : Fin (⦋2⦌.len + 1)) ↦ i) ⟨1, ⋯⟩].toSSet _⦋0 + 1⦌)) →
              (fun (X : Type u) ↦ X) (X _⦋1⦌))
          (horn.face ((fun (i : Fin (⦋2⦌.len + 1)) ↦ i) (⟨1, ⋯⟩ : Fin (⦋2⦌.len + 1))) j hj) :
        (fun (X : Type u) ↦ X) (X _⦋1⦌))
⊢ Eq (α := X _⦋1⦌)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (Quiver.Hom.op (mkOfSucc 0))) : (a : X _⦋0 + 1⦌) → X _⦋1⦌)
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (SimplicialObject.δ X j) : (a : X _⦋0 + 1 + 1⦌) → X _⦋0 + 1⦌)
            (sx.spineToSimplex ((horn.spineId i h₀ hₙ).map σ₀)) :
          X _⦋HAdd.hAdd (α := ℕ) 0 1⦌) :
      X _⦋1⦌)
    ((ConcreteCategory.hom (FC := TypeCat.Fun)
            (Λ[HAdd.hAdd (α := ℕ) 0 2, i].toSSet.map (Quiver.Hom.op (mkOfSucc 0)) ≫ σ₀.app (Opposite.op ⦋1⦌)) :
          (a : (fun (X : Type u) ↦ X) (Λ[0 + 2, i].toSSet _⦋0 + 1⦌)) → (fun (X : Type u) ↦ X) (X _⦋1⦌))
        (horn.face i j hj) :
      (fun (X : Type u) ↦ X) (X _⦋1⦌))
have h₂ : ∀
  (σ₀ :
    Subcomplex.toSSet (X := Δ[HAdd.hAdd (α := ℕ) 0 2])
        Λ[HAdd.hAdd (α := ℕ) 0 2, (fun (i : Fin (⦋2⦌.len + 1)) ↦ i) (⟨2, sorry⟩ : Fin (⦋2⦌.len + 1))] ⟶
      X)
  (h₀ : LT.lt (α := Fin (HAdd.hAdd (α := ℕ) 0 3)) 0 ((fun (i : Fin (⦋2⦌.len + 1)) ↦ i) ⟨2, sorry⟩))
  (hₙ :
    LT.lt (α := Fin (HAdd.hAdd (α := ℕ) 0 3)) ((fun (i : Fin (⦋2⦌.len + 1)) ↦ i) ⟨2, sorry⟩)
      (Fin.last (HAdd.hAdd (α := ℕ) 0 2)))
  (hj : j ≠ (fun (i : Fin (⦋2⦌.len + 1)) ↦ i) ⟨2, sorry⟩),
  Eq (α := X _⦋1⦌)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (X.map (Quiver.Hom.op (mkOfSucc 0))) : (a : X _⦋0 + 1⦌) → X _⦋1⦌)
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (SimplicialObject.δ X j) : (a : X _⦋0 + 1 + 1⦌) → X _⦋0 + 1⦌)
            (sx.spineToSimplex
              ((horn.spineId ((fun (i : Fin (⦋2⦌.len + 1)) ↦ i) (⟨2, sorry⟩ : Fin (⦋2⦌.len + 1))) h₀ hₙ).map σ₀)) :
          X _⦋HAdd.hAdd (α := ℕ) 0 1⦌) :
      X _⦋1⦌)
    ((ConcreteCategory.hom (FC := TypeCat.Fun)
            ((Subcomplex.toSSet (X := Δ[HAdd.hAdd (α := ℕ) 0 2])
                    Λ[HAdd.hAdd (α := ℕ) 0 2, (fun (i : Fin (⦋2⦌.len + 1)) ↦ i) (⟨2, sorry⟩ : Fin (⦋2⦌.len + 1))]).map
                (Quiver.Hom.op (mkOfSucc 0)) ≫
              σ₀.app (Opposite.op ⦋1⦌)) :
          (a : (fun (X : Type u) ↦ X) (Λ[0 + 2, (fun (i : Fin (⦋2⦌.len + 1)) ↦ i) ⟨2, sorry⟩].toSSet _⦋0 + 1⦌)) →
            (fun (X : Type u) ↦ X) (X _⦋1⦌))
        (horn.face ((fun (i : Fin (⦋2⦌.len + 1)) ↦ i) (⟨2, sorry⟩ : Fin (⦋2⦌.len + 1))) j hj) :
      (fun (X : Type u) ↦ X) (X _⦋1⦌))
Tactic: fin_cases i
Cleared hypotheses: i, σ₀, h₀, hₙ, hj