-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.ProdStdSimplexOne (goal)
Goal:
p : ℕ
refine_1 :
  ∀ (x x_1 : Fin (p + 1))
    (h :
      Eq.{u + 1} (α := (↑((tensorObj (𝒞 := Functor.category) Δ[p] Δ[1]).nonDegenerate (p + 1)) : Type u))
        ((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 }))
          x)
        ((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 }))
          x_1)),
    x = x_1
⊢ Function.Bijective.{1, u + 1} (β := (↑((tensorObj (𝒞 := Functor.category) Δ[p] Δ[1]).nonDegenerate (p + 1)) : Type u))
    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)
      ⋯
have refine_2 : ∀ (x : (↑((tensorObj (𝒞 := Functor.category) Δ[p] Δ[1]).nonDegenerate (p + 1)) : Type u)) (s₁ : Δ[p] _⦋p + 1⦌)
  (s₂ : Δ[1] _⦋p + 1⦌)
  (hs :
    Membership.mem (γ := Set (tensorObj (𝒞 := Functor.category) Δ[p] Δ[1] _⦋p + 1⦌))
      ((tensorObj (𝒞 := Functor.category) Δ[p] Δ[1]).nonDegenerate (p + 1)) (s₁, s₂)),
  ∃ (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)
              sorry :
            { 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₁, s₂) hs
Tactic: refine ⟨fun _ _ h ↦ ?_, fun ⟨⟨s₁, s₂⟩, hs⟩ ↦ ?_⟩