-- 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
i : ι
hi : i ≤ j
c : f.Cell i
hx :
  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)) c.s) : A.N)))) d)
    x
h :
  ∀ (hi : i < j),
    (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
h₁ :
  ∀ (hi : i ≤ i),
    (x ∈ A.obj d ∨
        ∃ i_1 < i,
          ∃ (i : f.Cell i_1),
            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.s) : A.N))))
                d)
              x) ∨
      ∃ (y : (f.sigmaStdSimplex i).obj d),
        (↑((ConcreteCategory.hom (FC := TypeCat.Fun) (NatTrans.app (f.b i) d) :
                  (a : (f.sigmaStdSimplex i).obj d) →
                    (↑(A.obj d ∪
                          (⨆ (j : ι),
                                ⨆ (_ : j < Order.succ i),
                                  ⨆ (c : f.Cell j),
                                    (↑((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
⊢ (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

Tactic:
obtain hi | rfl := hi.lt_or_eq

Premises used: LE.le.lt_or_eq, rfl