-- Lean 4 proof step from Mathlib.AlgebraicTopology.Quasicategory.StrictSegal (goal)
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 : ℕ) ⋯
m : Fin (HAdd.hAdd (α := ℕ) 1 1)
h :
  Eq (α := Fin (n + 1 + 2 + 1))
    (((↑(((horn.spineId i h₀ hₙ).interval (↑k : ℕ) 2 ⋯).arrow
              ((fun (i : Fin (⦋1⦌.len + 1)) ↦ i) (⟨0, ⋯⟩ : Fin (⦋1⦌.len + 1)))) :
          Δ[n + 1 + 2] _⦋1⦌) :
        (a : Fin (1 + 1)) → Fin (n + 1 + 2 + 1))
      ((fun (i : Fin (⦋1⦌.len + 1)) ↦ i) ⟨0, ⋯⟩))
    ((((↑(Subtype.mk (p := fun (x : Δ[n + 1 + 2] _⦋1⦌) ↦
                Membership.mem (γ := Set (Δ[n + 1 + 2] _⦋1⦌)) (Λ[n + 1 + 2, i].obj (Opposite.op ⦋1⦌)) x)
                ((ConcreteCategory.hom (FC := TypeCat.Fun)
                      (Δ[n + 1 + 2].map
                        (Quiver.Hom.op (mkOfSucc ((fun (i : Fin (⦋1⦌.len + 1)) ↦ i) (⟨0, ⋯⟩ : Fin (⦋1⦌.len + 1)))))) :
                    (a : Δ[n + 1 + 2] _⦋2⦌) → Δ[n + 1 + 2] _⦋1⦌)
                  (↑triangle : Δ[n + 1 + 2] _⦋2⦌))
                ⋯) :
            Δ[n + 1 + 2] _⦋1⦌) :
          Δ[n + 1 + 2] _⦋1⦌) :
        (a : Fin (1 + 1)) → Fin (n + 1 + 2 + 1))
      ((fun (i : Fin (⦋1⦌.len + 1)) ↦ i) ⟨0, ⋯⟩))
⊢ Eq (α := Fin (n + 1 + 2 + 1))
    (((↑(((horn.spineId i h₀ hₙ).interval (↑k : ℕ) 2 ⋯).arrow m) : Δ[n + 1 + 2] _⦋1⦌) :
        (a : Fin (1 + 1)) → Fin (n + 1 + 2 + 1))
      ((fun (i : Fin (⦋1⦌.len + 1)) ↦ i) ⟨0, ⋯⟩))
    ((((↑(Subtype.mk (p := fun (x : Δ[n + 1 + 2] _⦋1⦌) ↦
                Membership.mem (γ := Set (Δ[n + 1 + 2] _⦋1⦌)) (Λ[n + 1 + 2, i].obj (Opposite.op ⦋1⦌)) x)
                ((ConcreteCategory.hom (FC := TypeCat.Fun) (Δ[n + 1 + 2].map (mkOfSucc m).op) :
                    (a : Δ[n + 1 + 2] _⦋2⦌) → Δ[n + 1 + 2] _⦋1⦌)
                  (↑triangle : Δ[n + 1 + 2] _⦋2⦌))
                ⋯) :
            Δ[n + 1 + 2] _⦋1⦌) :
          Δ[n + 1 + 2] _⦋1⦌) :
        (a : Fin (1 + 1)) → Fin (n + 1 + 2 + 1))
      ((fun (i : Fin (⦋1⦌.len + 1)) ↦ i) ⟨0, ⋯⟩))
have h₁ : Eq (α := Fin (n + 1 + 2 + 1))
  (((↑(((horn.spineId i h₀ hₙ).interval (↑k : ℕ) 2 sorry).arrow
            ((fun (i : Fin (⦋1⦌.len + 1)) ↦ i) (⟨1, sorry⟩ : Fin (⦋1⦌.len + 1)))) :
        Δ[n + 1 + 2] _⦋1⦌) :
      (a : Fin (1 + 1)) → Fin (n + 1 + 2 + 1))
    ((fun (i : Fin (⦋1⦌.len + 1)) ↦ i) ⟨0, sorry⟩))
  ((((↑(Subtype.mk (p := fun (x : Δ[n + 1 + 2] _⦋1⦌) ↦
              Membership.mem (γ := Set (Δ[n + 1 + 2] _⦋1⦌)) (Λ[n + 1 + 2, i].obj (Opposite.op ⦋1⦌)) x)
              ((ConcreteCategory.hom (FC := TypeCat.Fun)
                    (Δ[n + 1 + 2].map
                      (Quiver.Hom.op (mkOfSucc ((fun (i : Fin (⦋1⦌.len + 1)) ↦ i) (⟨1, sorry⟩ : Fin (⦋1⦌.len + 1)))))) :
                  (a : Δ[n + 1 + 2] _⦋2⦌) → Δ[n + 1 + 2] _⦋1⦌)
                (↑triangle : Δ[n + 1 + 2] _⦋2⦌))
              sorry) :
          Δ[n + 1 + 2] _⦋1⦌) :
        Δ[n + 1 + 2] _⦋1⦌) :
      (a : Fin (1 + 1)) → Fin (n + 1 + 2 + 1))
    ((fun (i : Fin (⦋1⦌.len + 1)) ↦ i) ⟨0, sorry⟩))
Tactic: fin_cases m
Cleared hypotheses: m