-- Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.RelativeCellComplex
Goal:
X : SSet
A : X.Subcomplex
P : A.Pairing
ι : Type v
inst : LinearOrder ι
f : P.RankFunction ι
inst_1 : P.IsProper
j : ι
x : f.Cell j
g : unop (op ⦋x.dim + 1⦌) ⟶ ⦋x.dim + 1⦌
hs_1 :
  Membership.mem (α := f.sigmaStdSimplex j _⦋x.dim + 1⦌) (γ := Set (f.sigmaStdSimplex j _⦋x.dim + 1⦌))
    ((f.sigmaStdSimplex j).nonDegenerate (x.dim + 1))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (x.ιSigmaStdSimplex.app (op ⦋x.dim + 1⦌)) :
          (a : (fun (X : Type u) ↦ X) (Δ[x.dim + 1] _⦋x.dim + 1⦌)) →
            (fun (X : Type u) ↦ X) (f.sigmaStdSimplex j _⦋x.dim + 1⦌))
        ((Equiv.symm stdSimplex.objEquiv : (a : unop (op ⦋x.dim + 1⦌) ⟶ ⦋x.dim + 1⦌) → Δ[x.dim + 1] _⦋x.dim + 1⦌) g :
          Δ[x.dim + 1] _⦋x.dim + 1⦌) :
      (fun (X : Type u) ↦ X) (f.sigmaStdSimplex j _⦋x.dim + 1⦌))
hs : Mono g
hs'_1 :
  ((ConcreteCategory.hom (FC := TypeCat.Fun) (x.ιSigmaStdSimplex.app (op ⦋x.dim + 1⦌)) :
          (a : (fun (X : Type u) ↦ X) (Δ[x.dim + 1] _⦋x.dim + 1⦌)) →
            (fun (X : Type u) ↦ X) (f.sigmaStdSimplex j _⦋x.dim + 1⦌))
        ((Equiv.symm stdSimplex.objEquiv : (a : unop (op ⦋x.dim + 1⦌) ⟶ ⦋x.dim + 1⦌) → Δ[x.dim + 1] _⦋x.dim + 1⦌) g :
          Δ[x.dim + 1] _⦋x.dim + 1⦌) :
      (fun (X : Type u) ↦ X) (f.sigmaStdSimplex j _⦋x.dim + 1⦌)) ∉
    (range (X := f.sigmaHorn j) (f.m j)).obj (op ⦋x.dim + 1⦌)
hs' :
  ((Equiv.symm stdSimplex.objEquiv : (a : unop (op ⦋x.dim + 1⦌) ⟶ ⦋x.dim + 1⦌) → Δ[x.dim + 1] _⦋x.dim + 1⦌) g :
      Δ[x.dim + 1] _⦋x.dim + 1⦌) ∉
    Λ[x.dim + 1, x.index].obj (op ⦋x.dim + 1⦌)
inr :
  ∀
    (hs :
      Membership.mem (α := f.sigmaStdSimplex j _⦋x.dim + 1⦌) (γ := Set (f.sigmaStdSimplex j _⦋x.dim + 1⦌))
        ((f.sigmaStdSimplex j).nonDegenerate (x.dim + 1))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (x.ιSigmaStdSimplex.app (op ⦋x.dim + 1⦌)) :
              (a : (fun (X : Type u) ↦ X) (Δ[x.dim + 1] _⦋x.dim + 1⦌)) →
                (fun (X : Type u) ↦ X) (f.sigmaStdSimplex j _⦋x.dim + 1⦌))
            ((Equiv.symm stdSimplex.objEquiv : (a : unop (op ⦋x.dim + 1⦌) ⟶ ⦋x.dim + 1⦌) → Δ[x.dim + 1] _⦋x.dim + 1⦌)
                (𝟙 (unop (op ⦋x.dim + 1⦌))) :
              Δ[x.dim + 1] _⦋x.dim + 1⦌) :
          (fun (X : Type u) ↦ X) (f.sigmaStdSimplex j _⦋x.dim + 1⦌)))
    (hs_2 : Mono (𝟙 (unop (op ⦋x.dim + 1⦌))))
    (hs' :
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (x.ιSigmaStdSimplex.app (op ⦋x.dim + 1⦌)) :
              (a : (fun (X : Type u) ↦ X) (Δ[x.dim + 1] _⦋x.dim + 1⦌)) →
                (fun (X : Type u) ↦ X) (f.sigmaStdSimplex j _⦋x.dim + 1⦌))
            ((Equiv.symm stdSimplex.objEquiv : (a : unop (op ⦋x.dim + 1⦌) ⟶ ⦋x.dim + 1⦌) → Δ[x.dim + 1] _⦋x.dim + 1⦌)
                (𝟙 (unop (op ⦋x.dim + 1⦌))) :
              Δ[x.dim + 1] _⦋x.dim + 1⦌) :
          (fun (X : Type u) ↦ X) (f.sigmaStdSimplex j _⦋x.dim + 1⦌)) ∉
        (range (X := f.sigmaHorn j) (f.m j)).obj (op ⦋x.dim + 1⦌))
    (hs'_2 :
      ((Equiv.symm stdSimplex.objEquiv : (a : unop (op ⦋x.dim + 1⦌) ⟶ ⦋x.dim + 1⦌) → Δ[x.dim + 1] _⦋x.dim + 1⦌)
            (𝟙 (unop (op ⦋x.dim + 1⦌))) :
          Δ[x.dim + 1] _⦋x.dim + 1⦌) ∉
        Λ[x.dim + 1, x.index].obj (op ⦋x.dim + 1⦌)),
    ∃ (c : f.Cell j),
      N.mk
            ((ConcreteCategory.hom (FC := TypeCat.Fun) (x.ιSigmaStdSimplex.app (op ⦋x.dim + 1⦌)) :
                (a : (fun (X : Type u) ↦ X) (Δ[x.dim + 1] _⦋x.dim + 1⦌)) →
                  (fun (X : Type u) ↦ X) (f.sigmaStdSimplex j _⦋x.dim + 1⦌))
              ((Equiv.symm stdSimplex.objEquiv : (a : unop (op ⦋x.dim + 1⦌) ⟶ ⦋x.dim + 1⦌) → Δ[x.dim + 1] _⦋x.dim + 1⦌)
                  (𝟙 (unop (op ⦋x.dim + 1⦌))) :
                Δ[x.dim + 1] _⦋x.dim + 1⦌))
            hs hs' =
          Cell.type₁ f c ∨
        N.mk
            ((ConcreteCategory.hom (FC := TypeCat.Fun) (x.ιSigmaStdSimplex.app (op ⦋x.dim + 1⦌)) :
                (a : (fun (X : Type u) ↦ X) (Δ[x.dim + 1] _⦋x.dim + 1⦌)) →
                  (fun (X : Type u) ↦ X) (f.sigmaStdSimplex j _⦋x.dim + 1⦌))
              ((Equiv.symm stdSimplex.objEquiv : (a : unop (op ⦋x.dim + 1⦌) ⟶ ⦋x.dim + 1⦌) → Δ[x.dim + 1] _⦋x.dim + 1⦌)
                  (𝟙 (unop (op ⦋x.dim + 1⦌))) :
                Δ[x.dim + 1] _⦋x.dim + 1⦌))
            hs hs' =
          Cell.type₂ f c
⊢ ∃ (c : f.Cell j),
    N.mk
          ((ConcreteCategory.hom (FC := TypeCat.Fun) (x.ιSigmaStdSimplex.app (op ⦋x.dim + 1⦌)) :
              (a : (fun (X : Type u) ↦ X) (Δ[x.dim + 1] _⦋x.dim + 1⦌)) →
                (fun (X : Type u) ↦ X) (f.sigmaStdSimplex j _⦋x.dim + 1⦌))
            ((Equiv.symm stdSimplex.objEquiv : (a : unop (op ⦋x.dim + 1⦌) ⟶ ⦋x.dim + 1⦌) → Δ[x.dim + 1] _⦋x.dim + 1⦌)
                g :
              Δ[x.dim + 1] _⦋x.dim + 1⦌))
          hs_1 hs'_1 =
        Cell.type₁ f c ∨
      N.mk
          ((ConcreteCategory.hom (FC := TypeCat.Fun) (x.ιSigmaStdSimplex.app (op ⦋x.dim + 1⦌)) :
              (a : (fun (X : Type u) ↦ X) (Δ[x.dim + 1] _⦋x.dim + 1⦌)) →
                (fun (X : Type u) ↦ X) (f.sigmaStdSimplex j _⦋x.dim + 1⦌))
            ((Equiv.symm stdSimplex.objEquiv : (a : unop (op ⦋x.dim + 1⦌) ⟶ ⦋x.dim + 1⦌) → Δ[x.dim + 1] _⦋x.dim + 1⦌)
                g :
              Δ[x.dim + 1] _⦋x.dim + 1⦌))
          hs_1 hs'_1 =
        Cell.type₂ f c

Tactic:
obtain rfl := SimplexCategory.eq_id_of_mono g

Premises used: SimplexCategory.eq_id_of_mono, rfl