-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.RelativeCellComplex (goal)
Goal:
X : SSet
A : X.Subcomplex
P : A.Pairing
ι : Type v
inst : LinearOrder ι
f : P.RankFunction ι
inst_1 : P.IsProper
j : ι
d : ℕ
x : f.Cell j
s : Δ[x.dim + 1] _⦋d⦌
hs :
  Membership.mem (α := f.sigmaStdSimplex j _⦋d⦌) (γ := Set (f.sigmaStdSimplex j _⦋d⦌))
    ((f.sigmaStdSimplex j).nonDegenerate d)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (x.ιSigmaStdSimplex.app (op ⦋d⦌)) :
          (a : (fun (X : Type u) ↦ X) (Δ[x.dim + 1] _⦋d⦌)) → (fun (X : Type u) ↦ X) (f.sigmaStdSimplex j _⦋d⦌))
        s :
      (fun (X : Type u) ↦ X) (f.sigmaStdSimplex j _⦋d⦌))
hs'_1 :
  ((ConcreteCategory.hom (FC := TypeCat.Fun) (x.ιSigmaStdSimplex.app (op ⦋d⦌)) :
          (a : (fun (X : Type u) ↦ X) (Δ[x.dim + 1] _⦋d⦌)) → (fun (X : Type u) ↦ X) (f.sigmaStdSimplex j _⦋d⦌))
        s :
      (fun (X : Type u) ↦ X) (f.sigmaStdSimplex j _⦋d⦌)) ∉
    (range (X := f.sigmaHorn j) (f.m j)).obj (op ⦋d⦌)
hs' : s ∉ Λ[x.dim + 1, x.index].obj (op ⦋d⦌)
⊢ ∃ (c : f.Cell j),
    N.mk
          ((ConcreteCategory.hom (FC := TypeCat.Fun) (x.ιSigmaStdSimplex.app (op ⦋d⦌)) :
              (a : (fun (X : Type u) ↦ X) (Δ[x.dim + 1] _⦋d⦌)) → (fun (X : Type u) ↦ X) (f.sigmaStdSimplex j _⦋d⦌))
            s)
          hs hs'_1 =
        Cell.type₁ f c ∨
      N.mk
          ((ConcreteCategory.hom (FC := TypeCat.Fun) (x.ιSigmaStdSimplex.app (op ⦋d⦌)) :
              (a : (fun (X : Type u) ↦ X) (Δ[x.dim + 1] _⦋d⦌)) → (fun (X : Type u) ↦ X) (f.sigmaStdSimplex j _⦋d⦌))
            s)
          hs hs'_1 =
        Cell.type₂ f c
have obtain : ∀ (g : unop (op ⦋d⦌) ⟶ ⦋x.dim + 1⦌)
  (hs :
    Membership.mem (α := f.sigmaStdSimplex j _⦋d⦌) (γ := Set (f.sigmaStdSimplex j _⦋d⦌))
      ((f.sigmaStdSimplex j).nonDegenerate d)
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (x.ιSigmaStdSimplex.app (op ⦋d⦌)) :
            (a : (fun (X : Type u) ↦ X) (Δ[x.dim + 1] _⦋d⦌)) → (fun (X : Type u) ↦ X) (f.sigmaStdSimplex j _⦋d⦌))
          ((Equiv.symm stdSimplex.objEquiv : (a : unop (op ⦋d⦌) ⟶ ⦋x.dim + 1⦌) → Δ[x.dim + 1] _⦋d⦌) g :
            Δ[x.dim + 1] _⦋d⦌) :
        (fun (X : Type u) ↦ X) (f.sigmaStdSimplex j _⦋d⦌)))
  (hs' :
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (x.ιSigmaStdSimplex.app (op ⦋d⦌)) :
            (a : (fun (X : Type u) ↦ X) (Δ[x.dim + 1] _⦋d⦌)) → (fun (X : Type u) ↦ X) (f.sigmaStdSimplex j _⦋d⦌))
          ((Equiv.symm stdSimplex.objEquiv : (a : unop (op ⦋d⦌) ⟶ ⦋x.dim + 1⦌) → Δ[x.dim + 1] _⦋d⦌) g :
            Δ[x.dim + 1] _⦋d⦌) :
        (fun (X : Type u) ↦ X) (f.sigmaStdSimplex j _⦋d⦌)) ∉
      (range (X := f.sigmaHorn j) (f.m j)).obj (op ⦋d⦌))
  (hs'_2 :
    ((Equiv.symm stdSimplex.objEquiv : (a : unop (op ⦋d⦌) ⟶ ⦋x.dim + 1⦌) → Δ[x.dim + 1] _⦋d⦌) g : Δ[x.dim + 1] _⦋d⦌) ∉
      Λ[x.dim + 1, x.index].obj (op ⦋d⦌)),
  ∃ (c : f.Cell j),
    N.mk
          ((ConcreteCategory.hom (FC := TypeCat.Fun) (x.ιSigmaStdSimplex.app (op ⦋d⦌)) :
              (a : (fun (X : Type u) ↦ X) (Δ[x.dim + 1] _⦋d⦌)) → (fun (X : Type u) ↦ X) (f.sigmaStdSimplex j _⦋d⦌))
            ((Equiv.symm stdSimplex.objEquiv : (a : unop (op ⦋d⦌) ⟶ ⦋x.dim + 1⦌) → Δ[x.dim + 1] _⦋d⦌) g :
              Δ[x.dim + 1] _⦋d⦌))
          hs hs' =
        Cell.type₁ f c ∨
      N.mk
          ((ConcreteCategory.hom (FC := TypeCat.Fun) (x.ιSigmaStdSimplex.app (op ⦋d⦌)) :
              (a : (fun (X : Type u) ↦ X) (Δ[x.dim + 1] _⦋d⦌)) → (fun (X : Type u) ↦ X) (f.sigmaStdSimplex j _⦋d⦌))
            ((Equiv.symm stdSimplex.objEquiv : (a : unop (op ⦋d⦌) ⟶ ⦋x.dim + 1⦌) → Δ[x.dim + 1] _⦋d⦌) g :
              Δ[x.dim + 1] _⦋d⦌))
          hs hs' =
        Cell.type₂ f c
Tactic: obtain ⟨g, rfl⟩ := stdSimplex.objEquiv.symm.surjective s
Cleared hypotheses: s, hs, hs'_1, hs'