-- 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
inst_2 : SuccOrder ι
inst_3 : NoMaxOrder ι
j : ι
d : SimplexCategoryᵒᵖ
x : X.obj d
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
h :
  ∀ (hx : x ∈ A.obj d),
    (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
⊢ (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
have h₁ : ∀ (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),
  (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 hx | ⟨i, hi, c, hx⟩ := hx
Cleared hypotheses: hx