-- 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 : ι
d : SimplexCategoryᵒᵖ
x : X.obj d
hx : x ∈ (f.filtration (Order.succ j)).obj d
h :
  ∀
    (hx :
      x ∈ A.obj d ∨
        ∃ i ≤ j,
          ∃ (i_1 : f.Cell i),
            Membership.mem (γ := Set (X.obj d))
              (Subfunctor.obj
                (S.subcomplex
                  (N.toS (N.toN (A := A) (↑((P.p : (a : (↑P.II : Type u)) → (↑P.I : Type u)) i_1.s) : A.N))))
                d)
              x),
    (x ∈ A.obj d ∨
        ∃ i < j,
          ∃ (i_1 : f.Cell i),
            Membership.mem (γ := Set (X.obj d))
              (Subfunctor.obj
                (S.subcomplex
                  (N.toS (N.toN (A := A) (↑((P.p : (a : (↑P.II : Type u)) → (↑P.I : Type u)) i_1.s) : A.N))))
                d)
              x) ∨
      ∃ (y : (f.sigmaStdSimplex j).obj d),
        (↑((ConcreteCategory.hom (FC := TypeCat.Fun) (NatTrans.app (f.b j) d) :
                  (a : (f.sigmaStdSimplex j).obj d) →
                    (↑(A.obj d ∪
                          (⨆ (j_1 : ι),
                                ⨆ (_ : j_1 < Order.succ j),
                                  ⨆ (c : f.Cell j_1),
                                    (↑((P.p : (a : (↑P.II : Type u)) → (↑P.I : Type u)) c.s) : A.N).subcomplex).obj
                            d) :
                      Type u))
                y) :
            X.obj d) =
          x
⊢ Membership.mem (γ := Set ((fun (X : Type u) ↦ X) ((f.filtration (Order.succ j)).toSSet.obj d)))
      (Set.range (ι := (fun (X : Type u) ↦ X) ((f.filtration j).toSSet.obj d))
          (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (NatTrans.app (homOfLE ⋯) d)) :
            (a : (fun (X : Type u) ↦ X) ((f.filtration j).toSSet.obj d)) →
              (fun (X : Type u) ↦ X) ((f.filtration (Order.succ j)).toSSet.obj d)) ⊔
        Set.range (ι := (fun (X : Type u) ↦ X) ((f.sigmaStdSimplex j).obj d))
          (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (NatTrans.app (f.b j) d)) :
            (a : (fun (X : Type u) ↦ X) ((f.sigmaStdSimplex j).obj d)) →
              (fun (X : Type u) ↦ X) ((f.filtration (Order.succ j)).toSSet.obj d)))
      (Subtype.mk (p := fun (x : X.obj d) ↦ x ∈ (f.filtration (Order.succ j)).obj d) x hx) ↔
    Membership.mem (γ := Set ((fun (X : Type u) ↦ X) ((f.filtration (Order.succ j)).toSSet.obj d))) Set.univ
      (Subtype.mk (p := fun (x : X.obj d) ↦ x ∈ (f.filtration (Order.succ j)).obj d) x hx)

Tactic:
simp only [filtration_def, Order.lt_succ_iff, Subfunctor.max_obj, Subfunctor.iSup_obj,
    Set.mem_union, Set.mem_iUnion, exists_prop, Subfunctor.toFunctor_obj, Subfunctor.homOfLe_app,
    TypeCat.hom_ofHom, TypeCat.Fun.coe_mk, Set.sup_eq_union, Set.mem_range, Subtype.ext_iff,
    Subtype.exists, exists_eq_right, Set.mem_univ, iff_true] at hx ⊢

Premises used: Set.mem_union, CategoryTheory.Subfunctor.homOfLe_app, Set.mem_range, CategoryTheory.Subfunctor.toFunctor_obj, CategoryTheory.Subfunctor.max_obj, Set.mem_iUnion, iff_true, TypeCat.Fun.coe_mk, Subtype.exists, Set.sup_eq_union, exists_eq_right, TypeCat.hom_ofHom, exists_prop, SSet.Subcomplex.Pairing.RankFunction.filtration_def, Subtype.ext_iff, Order.lt_succ_iff, Set.mem_univ, CategoryTheory.Subfunctor.iSup_obj