-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Skeleton (goal)
Goal:
X Y : SSet
i : X ⟶ Y
d : ℕ
x : SimplexCategoryᵒᵖ
n : ℕ
c₁ : Cell i d
f₁ : ⦋n⦌ ⟶ ⦋d⦌
w : Epi f₁
hx₁ :
  ((ConcreteCategory.hom (FC := TypeCat.Fun) (c₁.ιSigmaStdSimplex.app (op ⦋n⦌)) :
          (a : (fun (X : Type u) ↦ X) (Δ[d] _⦋n⦌)) → (fun (X : Type u) ↦ X) (sigmaStdSimplex i d _⦋n⦌))
        ((Equiv.symm stdSimplex.objEquiv : (a : unop (op ⦋n⦌) ⟶ ⦋d⦌) → Δ[d] _⦋n⦌) f₁ : Δ[d] _⦋n⦌) :
      (fun (X : Type u) ↦ X) (sigmaStdSimplex i d _⦋n⦌)) ∉
    Set.range (ι := sigmaBoundary i d _⦋n⦌)
      (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) ((l i d).app (op ⦋n⦌))) :
        (a : sigmaBoundary i d _⦋n⦌) → sigmaStdSimplex i d _⦋n⦌)
c₂ : Cell i d
f₂ : ⦋n⦌ ⟶ ⦋d⦌
w_1 : Epi f₂
hx₂ :
  ((ConcreteCategory.hom (FC := TypeCat.Fun) (c₂.ιSigmaStdSimplex.app (op ⦋n⦌)) :
          (a : (fun (X : Type u) ↦ X) (Δ[d] _⦋n⦌)) → (fun (X : Type u) ↦ X) (sigmaStdSimplex i d _⦋n⦌))
        ((Equiv.symm stdSimplex.objEquiv : (a : unop (op ⦋n⦌) ⟶ ⦋d⦌) → Δ[d] _⦋n⦌) f₂ : Δ[d] _⦋n⦌) :
      (fun (X : Type u) ↦ X) (sigmaStdSimplex i d _⦋n⦌)) ∉
    Set.range (ι := sigmaBoundary i d _⦋n⦌)
      (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) ((l i d).app (op ⦋n⦌))) :
        (a : sigmaBoundary i d _⦋n⦌) → sigmaStdSimplex i d _⦋n⦌)
h :
  Eq (α := (fun (X : Type u) ↦ X) (Y _⦋n⦌))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (Y.map f₁.op) :
          (a : (fun (X : Type u) ↦ X) (Y _⦋d⦌)) → (fun (X : Type u) ↦ X) (Y _⦋n⦌))
        c₁.simplex :
      (fun (X : Type u) ↦ X) (Y _⦋n⦌))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (Y.map f₂.op) :
          (a : (fun (X : Type u) ↦ X) (Y _⦋d⦌)) → (fun (X : Type u) ↦ X) (Y _⦋n⦌))
        c₂.simplex :
      (fun (X : Type u) ↦ X) (Y _⦋n⦌))
⊢ Eq (α := sigmaStdSimplex i d _⦋n⦌)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (c₁.ιSigmaStdSimplex.app (op ⦋n⦌)) :
          (a : (fun (X : Type u) ↦ X) (Δ[d] _⦋n⦌)) → (fun (X : Type u) ↦ X) (sigmaStdSimplex i d _⦋n⦌))
        ((Equiv.symm stdSimplex.objEquiv : (a : unop (op ⦋n⦌) ⟶ ⦋d⦌) → Δ[d] _⦋n⦌) f₁ : Δ[d] _⦋n⦌) :
      (fun (X : Type u) ↦ X) (sigmaStdSimplex i d _⦋n⦌))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (c₂.ιSigmaStdSimplex.app (op ⦋n⦌)) :
          (a : (fun (X : Type u) ↦ X) (Δ[d] _⦋n⦌)) → (fun (X : Type u) ↦ X) (sigmaStdSimplex i d _⦋n⦌))
        ((Equiv.symm stdSimplex.objEquiv : (a : unop (op ⦋n⦌) ⟶ ⦋d⦌) → Δ[d] _⦋n⦌) f₂ : Δ[d] _⦋n⦌) :
      (fun (X : Type u) ↦ X) (sigmaStdSimplex i d _⦋n⦌))
have refine_3 : ∀
  (hx₂ :
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (c₁.ιSigmaStdSimplex.app (op ⦋n⦌)) :
            (a : (fun (X : Type u) ↦ X) (Δ[d] _⦋n⦌)) → (fun (X : Type u) ↦ X) (sigmaStdSimplex i d _⦋n⦌))
          ((Equiv.symm stdSimplex.objEquiv : (a : unop (op ⦋n⦌) ⟶ ⦋d⦌) → Δ[d] _⦋n⦌) f₂ : Δ[d] _⦋n⦌) :
        (fun (X : Type u) ↦ X) (sigmaStdSimplex i d _⦋n⦌)) ∉
      Set.range (ι := sigmaBoundary i d _⦋n⦌)
        (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) ((l i d).app (op ⦋n⦌))) :
          (a : sigmaBoundary i d _⦋n⦌) → sigmaStdSimplex i d _⦋n⦌))
  (h :
    Eq (α := (fun (X : Type u) ↦ X) (Y _⦋n⦌))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (Y.map f₁.op) :
            (a : (fun (X : Type u) ↦ X) (Y _⦋d⦌)) → (fun (X : Type u) ↦ X) (Y _⦋n⦌))
          c₁.simplex :
        (fun (X : Type u) ↦ X) (Y _⦋n⦌))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (Y.map f₂.op) :
            (a : (fun (X : Type u) ↦ X) (Y _⦋d⦌)) → (fun (X : Type u) ↦ X) (Y _⦋n⦌))
          c₁.simplex :
        (fun (X : Type u) ↦ X) (Y _⦋n⦌))),
  Eq (α := sigmaStdSimplex i d _⦋n⦌)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (c₁.ιSigmaStdSimplex.app (op ⦋n⦌)) :
          (a : (fun (X : Type u) ↦ X) (Δ[d] _⦋n⦌)) → (fun (X : Type u) ↦ X) (sigmaStdSimplex i d _⦋n⦌))
        ((Equiv.symm stdSimplex.objEquiv : (a : unop (op ⦋n⦌) ⟶ ⦋d⦌) → Δ[d] _⦋n⦌) f₁ : Δ[d] _⦋n⦌) :
      (fun (X : Type u) ↦ X) (sigmaStdSimplex i d _⦋n⦌))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (c₁.ιSigmaStdSimplex.app (op ⦋n⦌)) :
          (a : (fun (X : Type u) ↦ X) (Δ[d] _⦋n⦌)) → (fun (X : Type u) ↦ X) (sigmaStdSimplex i d _⦋n⦌))
        ((Equiv.symm stdSimplex.objEquiv : (a : unop (op ⦋n⦌) ⟶ ⦋d⦌) → Δ[d] _⦋n⦌) f₂ : Δ[d] _⦋n⦌) :
      (fun (X : Type u) ↦ X) (sigmaStdSimplex i d _⦋n⦌))
Tactic: obtain rfl : c₁ = c₂ := by
        ext
        exact Subtype.ext_iff.mp
          (Y.unique_nonDegenerate_simplex _ f₁ ⟨_, c₁.nonDegenerate⟩ rfl
            f₂ ⟨_, c₂.nonDegenerate⟩ h)
Cleared hypotheses: c₂, hx₂, h