-- 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
inst_2 : SuccOrder ι
inst_3 : NoMaxOrder ι
j : ι
x : SimplexCategoryᵒᵖ
d : ℕ
x₁ x₂ : Functor.obj (CategoryTheory.evaluation SimplexCategoryᵒᵖ (Type u) _⦋d⦌) (f.sigmaStdSimplex j)
hx₁ :
  x₁ ∉
    Set.range (ι :=
      (fun (X : Type u) ↦ X) (Functor.obj (CategoryTheory.evaluation SimplexCategoryᵒᵖ (Type u) _⦋d⦌) (f.sigmaHorn j)))
      (⇑(ConcreteCategory.hom (FC := TypeCat.Fun)
            (CategoryTheory.Functor.map (CategoryTheory.evaluation SimplexCategoryᵒᵖ (Type u) _⦋d⦌) (f.m j))) :
        (a : (fun (X : Type u) ↦ X) (CategoryTheory.evaluation SimplexCategoryᵒᵖ (Type u) _⦋d⦌.obj (f.sigmaHorn j))) →
          (fun (X : Type u) ↦ X) (CategoryTheory.evaluation SimplexCategoryᵒᵖ (Type u) _⦋d⦌.obj (f.sigmaStdSimplex j)))
hx₂ :
  x₂ ∉
    Set.range (ι :=
      (fun (X : Type u) ↦ X) (Functor.obj (CategoryTheory.evaluation SimplexCategoryᵒᵖ (Type u) _⦋d⦌) (f.sigmaHorn j)))
      (⇑(ConcreteCategory.hom (FC := TypeCat.Fun)
            (CategoryTheory.Functor.map (CategoryTheory.evaluation SimplexCategoryᵒᵖ (Type u) _⦋d⦌) (f.m j))) :
        (a : (fun (X : Type u) ↦ X) (CategoryTheory.evaluation SimplexCategoryᵒᵖ (Type u) _⦋d⦌.obj (f.sigmaHorn j))) →
          (fun (X : Type u) ↦ X) (CategoryTheory.evaluation SimplexCategoryᵒᵖ (Type u) _⦋d⦌.obj (f.sigmaStdSimplex j)))
h :
  Eq (α :=
    (fun (X : Type u) ↦ X)
      (Functor.obj (CategoryTheory.evaluation SimplexCategoryᵒᵖ (Type u) _⦋d⦌) (f.filtration (Order.succ j)).toSSet))
    ((ConcreteCategory.hom (FC := TypeCat.Fun)
            (CategoryTheory.Functor.map (CategoryTheory.evaluation SimplexCategoryᵒᵖ (Type u) _⦋d⦌) (f.b j)) :
          (a :
              (fun (X : Type u) ↦ X)
                (CategoryTheory.evaluation SimplexCategoryᵒᵖ (Type u) _⦋d⦌.obj (f.sigmaStdSimplex j))) →
            (fun (X : Type u) ↦ X)
              (CategoryTheory.evaluation SimplexCategoryᵒᵖ (Type u) _⦋d⦌.obj (f.filtration (Order.succ j)).toSSet))
        x₁ :
      (fun (X : Type u) ↦ X)
        (Functor.obj (CategoryTheory.evaluation SimplexCategoryᵒᵖ (Type u) _⦋d⦌) (f.filtration (Order.succ j)).toSSet))
    ((ConcreteCategory.hom (FC := TypeCat.Fun)
            (CategoryTheory.Functor.map (CategoryTheory.evaluation SimplexCategoryᵒᵖ (Type u) _⦋d⦌) (f.b j)) :
          (a :
              (fun (X : Type u) ↦ X)
                (CategoryTheory.evaluation SimplexCategoryᵒᵖ (Type u) _⦋d⦌.obj (f.sigmaStdSimplex j))) →
            (fun (X : Type u) ↦ X)
              (CategoryTheory.evaluation SimplexCategoryᵒᵖ (Type u) _⦋d⦌.obj (f.filtration (Order.succ j)).toSSet))
        x₂ :
      (fun (X : Type u) ↦ X)
        (Functor.obj (CategoryTheory.evaluation SimplexCategoryᵒᵖ (Type u) _⦋d⦌) (f.filtration (Order.succ j)).toSSet))
s₁ : (range (X := f.sigmaHorn j) (f.m j)).N
g₁ : ⦋d⦌ ⟶ ⦋s₁.dim⦌
left : Epi g₁
hg₁ :
  (ConcreteCategory.hom (FC := TypeCat.Fun) ((f.sigmaStdSimplex j).map g₁.op) :
        (a : (fun (X : Type u) ↦ X) (f.sigmaStdSimplex j _⦋s₁.dim⦌)) →
          (fun (X : Type u) ↦ X) (f.sigmaStdSimplex j _⦋d⦌))
      s₁.simplex =
    x₁
s₂ : (range (X := f.sigmaHorn j) (f.m j)).N
g₂ : ⦋d⦌ ⟶ ⦋s₂.dim⦌
left_1 : Epi g₂
hg₂ :
  (ConcreteCategory.hom (FC := TypeCat.Fun) ((f.sigmaStdSimplex j).map g₂.op) :
        (a : (fun (X : Type u) ↦ X) (f.sigmaStdSimplex j _⦋s₂.dim⦌)) →
          (fun (X : Type u) ↦ X) (f.sigmaStdSimplex j _⦋d⦌))
      s₂.simplex =
    x₂
rw :
  Eq.{u + 1} (α := (f.filtration (Order.succ j)).toSSet.Subcomplex)
    (ofSimplex (n := d)
      ((ConcreteCategory.hom (FC := TypeCat.Fun) ((f.filtration (Order.succ j)).toSSet.map g₁.op) :
          (a : (fun (X : Type u) ↦ X) ((f.filtration (Order.succ j)).toSSet _⦋s₁.dim⦌)) →
            (fun (X : Type u) ↦ X) ((f.filtration (Order.succ j)).toSSet _⦋d⦌))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (NatTrans.app (f.b j) (op ⦋s₁.dim⦌)) :
            (a : f.sigmaStdSimplex j _⦋s₁.dim⦌) → (↑((f.filtration (Order.succ j)).obj (op ⦋s₁.dim⦌)) : Type u))
          s₁.simplex)))
    (ofSimplex (n := d)
      ((ConcreteCategory.hom (FC := TypeCat.Fun) ((f.filtration (Order.succ j)).toSSet.map g₂.op) :
          (a : (fun (X : Type u) ↦ X) ((f.filtration (Order.succ j)).toSSet _⦋s₂.dim⦌)) →
            (fun (X : Type u) ↦ X) ((f.filtration (Order.succ j)).toSSet _⦋d⦌))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (NatTrans.app (f.b j) (op ⦋s₂.dim⦌)) :
            (a : f.sigmaStdSimplex j _⦋s₂.dim⦌) → (↑((f.filtration (Order.succ j)).obj (op ⦋s₂.dim⦌)) : Type u))
          s₂.simplex)))
hx :
  Membership.mem (α := (f.filtration (Order.succ j)).toSSet _⦋s₁.dim⦌) (γ :=
    Set ((f.filtration (Order.succ j)).toSSet _⦋s₁.dim⦌)) ((f.filtration (Order.succ j)).toSSet.nonDegenerate s₁.dim)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (NatTrans.app (f.b j) (op ⦋s₁.dim⦌)) :
          (a : f.sigmaStdSimplex j _⦋s₁.dim⦌) → (↑((f.filtration (Order.succ j)).obj (op ⦋s₁.dim⦌)) : Type u))
        s₁.simplex :
      (↑((f.filtration (Order.succ j)).obj (op ⦋s₁.dim⦌)) : Type u))
hy :
  Membership.mem (α := (f.filtration (Order.succ j)).toSSet _⦋s₂.dim⦌) (γ :=
    Set ((f.filtration (Order.succ j)).toSSet _⦋s₂.dim⦌)) ((f.filtration (Order.succ j)).toSSet.nonDegenerate s₂.dim)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (NatTrans.app (f.b j) (op ⦋s₂.dim⦌)) :
          (a : f.sigmaStdSimplex j _⦋s₂.dim⦌) → (↑((f.filtration (Order.succ j)).obj (op ⦋s₂.dim⦌)) : Type u))
        s₂.simplex :
      (↑((f.filtration (Order.succ j)).obj (op ⦋s₂.dim⦌)) : Type u))
⊢ Eq.{u + 1} (α := (f.filtration (Order.succ j)).toSSet.S)
    (S.mk (dim := s₁.dim)
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (NatTrans.app (f.b j) (op ⦋s₁.dim⦌)) :
          (a : f.sigmaStdSimplex j _⦋s₁.dim⦌) → (↑((f.filtration (Order.succ j)).obj (op ⦋s₁.dim⦌)) : Type u))
        s₁.simplex))
    (S.mk (dim := s₂.dim)
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (NatTrans.app (f.b j) (op ⦋s₂.dim⦌)) :
          (a : f.sigmaStdSimplex j _⦋s₂.dim⦌) → (↑((f.filtration (Order.succ j)).obj (op ⦋s₂.dim⦌)) : Type u))
        s₂.simplex))

Tactic:
rw [S.eq_iff_ofSimplex_eq, ← Subcomplex.ofSimplex_map_of_epi g₁,
        ← Subcomplex.ofSimplex_map_of_epi g₂]

Premises used: SSet.Subcomplex.ofSimplex_map_of_epi, SSet.S.eq_iff_ofSimplex_eq