-- Module: Mathlib.AlgebraicTopology.SimplicialSet.ProdStdSimplexOne
Goal:
p : ℕ
x : (↑((tensorObj (𝒞 := Functor.category) Δ[p] Δ[1]).nonDegenerate (p + 1)) : Type u)
s₁ : Δ[p] _⦋p + 1⦌
i : Fin (p + 1 + 2)
hs_1 :
  Membership.mem (γ := Set (tensorObj (𝒞 := Functor.category) Δ[p] Δ[1] _⦋p + 1⦌))
    ((tensorObj (𝒞 := Functor.category) Δ[p] Δ[1]).nonDegenerate (p + 1)) (s₁, objMk₁ i)
hs : orderHomOfSimplex (s₁, objMk₁ i) ⋯ = OrderHom.id
refine_2 :
  ∀ (i : Fin (p + 2))
    (hs :
      Membership.mem (γ := Set (tensorObj (𝒞 := Functor.category) Δ[p] Δ[1] _⦋p + 1⦌))
        ((tensorObj (𝒞 := Functor.category) Δ[p] Δ[1]).nonDegenerate (p + 1)) (s₁, objMk₁ i.succ))
    (hs_2 : orderHomOfSimplex (s₁, objMk₁ i.succ) ⋯ = OrderHom.id),
    ∃ (a : Fin (p + 1)),
      (fun (i : Fin (p + 1)) ↦
            (Subtype.mk (p := fun (x : tensorObj (𝒞 := Functor.category) Δ[p] Δ[1] _⦋p + 1⦌) ↦
                Membership.mem (γ := Set (tensorObj (𝒞 := Functor.category) Δ[p] Δ[1] _⦋p + 1⦌))
                  ((tensorObj (𝒞 := Functor.category) Δ[p] Δ[1]).nonDegenerate (p + 1)) x)
                ((Equiv.symm stdSimplex.objEquiv : (a : unop (op ⦋p + 1⦌) ⟶ ⦋p⦌) → Δ[p] _⦋p + 1⦌) (SimplexCategory.σ i),
                  objMk₁ i.succ.castSucc)
                ⋯ :
              { x : tensorObj (𝒞 := Functor.category) Δ[p] Δ[1] _⦋p + 1⦌ //
                Membership.mem (γ := Set (tensorObj (𝒞 := Functor.category) Δ[p] Δ[1] _⦋p + 1⦌))
                  ((tensorObj (𝒞 := Functor.category) Δ[p] Δ[1]).nonDegenerate (p + 1)) x }))
          a =
        Subtype.mk (p := fun (x : tensorObj (𝒞 := Functor.category) Δ[p] Δ[1] _⦋p + 1⦌) ↦
          Membership.mem (γ := Set (tensorObj (𝒞 := Functor.category) Δ[p] Δ[1] _⦋p + 1⦌))
            ((tensorObj (𝒞 := Functor.category) Δ[p] Δ[1]).nonDegenerate (p + 1)) x)
          (s₁, objMk₁ i.succ) hs
⊢ ∃ (a : Fin (p + 1)),
    (fun (i : Fin (p + 1)) ↦
          (Subtype.mk (p := fun (x : tensorObj (𝒞 := Functor.category) Δ[p] Δ[1] _⦋p + 1⦌) ↦
              Membership.mem (γ := Set (tensorObj (𝒞 := Functor.category) Δ[p] Δ[1] _⦋p + 1⦌))
                ((tensorObj (𝒞 := Functor.category) Δ[p] Δ[1]).nonDegenerate (p + 1)) x)
              ((Equiv.symm stdSimplex.objEquiv : (a : unop (op ⦋p + 1⦌) ⟶ ⦋p⦌) → Δ[p] _⦋p + 1⦌) (SimplexCategory.σ i),
                objMk₁ i.succ.castSucc)
              ⋯ :
            { x : tensorObj (𝒞 := Functor.category) Δ[p] Δ[1] _⦋p + 1⦌ //
              Membership.mem (γ := Set (tensorObj (𝒞 := Functor.category) Δ[p] Δ[1] _⦋p + 1⦌))
                ((tensorObj (𝒞 := Functor.category) Δ[p] Δ[1]).nonDegenerate (p + 1)) x }))
        a =
      Subtype.mk (p := fun (x : tensorObj (𝒞 := Functor.category) Δ[p] Δ[1] _⦋p + 1⦌) ↦
        Membership.mem (γ := Set (tensorObj (𝒞 := Functor.category) Δ[p] Δ[1] _⦋p + 1⦌))
          ((tensorObj (𝒞 := Functor.category) Δ[p] Δ[1]).nonDegenerate (p + 1)) x)
        (s₁, objMk₁ i) hs_1

Tactic:
obtain ⟨i, rfl⟩ := Fin.eq_succ_of_ne_zero (i := i) (by
        rintro rfl
        have := DFunLike.congr_fun hs 0
        simp only [orderHomOfSimplex_coe,
          stdSimplex.objMk₁_of_le_castSucc (0 : Fin (p + 3)) 0 (by simp)] at this
        simp at this)

Premises used: Fin.eq_succ_of_ne_zero, rfl