-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Skeleton
Goal:
X Y : SSet
i : X ⟶ Y
d : ℕ
n : SimplexCategory
x : Y.obj (op n)
hx_1 :
  Membership.mem (γ := Set (Y.obj (op n))) (Subfunctor.obj ((skeletonOfMono i : (a : ℕ) → Y.Subcomplex) (d + 1)) (op n))
    x
h :
  Membership.mem (γ :=
    Set ((Subcomplex.toSSet (X := Y) ((skeletonOfMono i : (a : ℕ) → Y.Subcomplex) (d + 1))).obj (op n)))
    (Subfunctor.obj ⊤ (op n))
    (Subtype.mk (p := fun (x : Y.obj (op n)) ↦
      Membership.mem (γ := Set (Y.obj (op n)))
        (Subfunctor.obj ((skeletonOfMono i : (a : ℕ) → Y.Subcomplex) (d + 1)) (op n)) x)
      x hx_1)
hx :
  Membership.mem (γ := Set (Y.obj (op n))) (Subfunctor.obj ((skeletonOfMono i : (a : ℕ) → Y.Subcomplex) d) (op n)) x ∨
    ∃ i_1 ∈ Y.nonDegenerate d,
      (∀ (x : X _⦋d⦌), ¬(ConcreteCategory.hom (FC := TypeCat.Fun) (i.app (op ⦋d⦌)) : (a : X _⦋d⦌) → Y _⦋d⦌) x = i_1) ∧
        Membership.mem (γ := Set (Y.obj (op n))) ((Subcomplex.ofSimplex i_1).obj (op n)) x
inl :
  ∀
    (hx :
      Membership.mem (γ := Set (Y.obj (op n))) (Subfunctor.obj ((skeletonOfMono i : (a : ℕ) → Y.Subcomplex) d) (op n))
        x),
    Membership.mem (γ := Set (↑(Subfunctor.obj ((skeletonOfMono i : (a : ℕ) → Y.Subcomplex) (d + 1)) (op n)) : Type u))
      (Set.range (ι := (↑(Subfunctor.obj ((skeletonOfMono i : (a : ℕ) → Y.Subcomplex) d) (op n)) : Type u))
          (⇑{
                toFun := fun (x : (↑(Subfunctor.obj ((skeletonOfMono i : (a : ℕ) → Y.Subcomplex) d) (op n)) : Type u)) ↦
                  Subtype.mk (p := fun (x : Y.obj (op n)) ↦
                    Membership.mem (γ := Set (Y.obj (op n)))
                      (Subfunctor.obj ((skeletonOfMono i : (a : ℕ) → Y.Subcomplex) (d + 1)) (op n)) x)
                    (↑x : Y.obj (op n)) ⋯ } :
            (a : (↑(((skeletonOfMono i : (a : ℕ) → Y.Subcomplex) d).obj (op n)) : Type u)) →
              (↑(((skeletonOfMono i : (a : ℕ) → Y.Subcomplex) (d + 1)).obj (op n)) : Type u)) ∪
        Set.range (ι := (sigmaStdSimplex i d).obj (op n))
          (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) ((b i d).app (op n))) :
            (a : (sigmaStdSimplex i d).obj (op n)) →
              (↑(((skeletonOfMono i : (a : ℕ) → Y.Subcomplex) (d + 1)).obj (op n)) : Type u)))
      (Subtype.mk (p := fun (x : Y.obj (op n)) ↦
        Membership.mem (γ := Set (Y.obj (op n)))
          (Subfunctor.obj ((skeletonOfMono i : (a : ℕ) → Y.Subcomplex) (d + 1)) (op n)) x)
        x hx_1)
inr :
  ∀ (y : Y _⦋d⦌) (hy₁ : y ∈ Y.nonDegenerate d)
    (hy₂ : ∀ (x : X _⦋d⦌), ¬(ConcreteCategory.hom (FC := TypeCat.Fun) (i.app (op ⦋d⦌)) : (a : X _⦋d⦌) → Y _⦋d⦌) x = y)
    (f : op ⦋d⦌ ⟶ op n)
    (hx :
      Membership.mem (α := Y.obj (op n)) (γ := Set (Y.obj (op n)))
        (Subfunctor.obj ((skeletonOfMono i : (a : ℕ) → Y.Subcomplex) (d + 1)) (op n))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (Y.map f) :
              (a : (fun (X : Type u) ↦ X) (Y _⦋d⦌)) → (fun (X : Type u) ↦ X) (Y.obj (op n)))
            y :
          (fun (X : Type u) ↦ X) (Y.obj (op n)))),
    Membership.mem (α := (Subcomplex.toSSet (X := Y) ((skeletonOfMono i : (a : ℕ) → Y.Subcomplex) (d + 1))).obj (op n))
        (γ := Set ((Subcomplex.toSSet (X := Y) ((skeletonOfMono i : (a : ℕ) → Y.Subcomplex) (d + 1))).obj (op n)))
        (Subfunctor.obj ⊤ (op n))
        (Subtype.mk (p := fun (x : Y.obj (op n)) ↦
            Membership.mem (γ := Set (Y.obj (op n)))
              (Subfunctor.obj ((skeletonOfMono i : (a : ℕ) → Y.Subcomplex) (d + 1)) (op n)) x)
            ((ConcreteCategory.hom (FC := TypeCat.Fun) (Y.map f) :
                (a : (fun (X : Type u) ↦ X) (Y _⦋d⦌)) → (fun (X : Type u) ↦ X) (Y.obj (op n)))
              y)
            hx :
          { x : Y.obj (op n) //
            Membership.mem (γ := Set (Y.obj (op n)))
              (Subfunctor.obj ((skeletonOfMono i : (a : ℕ) → Y.Subcomplex) (d + 1)) (op n)) x }) →
      Membership.mem (α := (↑(Subfunctor.obj ((skeletonOfMono i : (a : ℕ) → Y.Subcomplex) (d + 1)) (op n)) : Type u))
        (γ := Set (↑(Subfunctor.obj ((skeletonOfMono i : (a : ℕ) → Y.Subcomplex) (d + 1)) (op n)) : Type u))
        (Set.range (ι := (↑(Subfunctor.obj ((skeletonOfMono i : (a : ℕ) → Y.Subcomplex) d) (op n)) : Type u))
            (⇑{
                  toFun :=
                    fun (x : (↑(Subfunctor.obj ((skeletonOfMono i : (a : ℕ) → Y.Subcomplex) d) (op n)) : Type u)) ↦
                    Subtype.mk (p := fun (x : Y.obj (op n)) ↦
                      Membership.mem (γ := Set (Y.obj (op n)))
                        (Subfunctor.obj ((skeletonOfMono i : (a : ℕ) → Y.Subcomplex) (d + 1)) (op n)) x)
                      (↑x : Y.obj (op n)) ⋯ } :
              (a : (↑(((skeletonOfMono i : (a : ℕ) → Y.Subcomplex) d).obj (op n)) : Type u)) →
                (↑(((skeletonOfMono i : (a : ℕ) → Y.Subcomplex) (d + 1)).obj (op n)) : Type u)) ∪
          Set.range (ι := (sigmaStdSimplex i d).obj (op n))
            (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) ((b i d).app (op n))) :
              (a : (sigmaStdSimplex i d).obj (op n)) →
                (↑(((skeletonOfMono i : (a : ℕ) → Y.Subcomplex) (d + 1)).obj (op n)) : Type u)))
        (Subtype.mk (p := fun (x : Y.obj (op n)) ↦
            Membership.mem (γ := Set (Y.obj (op n)))
              (Subfunctor.obj ((skeletonOfMono i : (a : ℕ) → Y.Subcomplex) (d + 1)) (op n)) x)
            ((ConcreteCategory.hom (FC := TypeCat.Fun) (Y.map f) :
                (a : (fun (X : Type u) ↦ X) (Y _⦋d⦌)) → (fun (X : Type u) ↦ X) (Y.obj (op n)))
              y)
            hx :
          { x : Y.obj (op n) //
            Membership.mem (γ := Set (Y.obj (op n)))
              (Subfunctor.obj ((skeletonOfMono i : (a : ℕ) → Y.Subcomplex) (d + 1)) (op n)) x })
⊢ Membership.mem (γ := Set (↑(Subfunctor.obj ((skeletonOfMono i : (a : ℕ) → Y.Subcomplex) (d + 1)) (op n)) : Type u))
    (Set.range (ι := (↑(Subfunctor.obj ((skeletonOfMono i : (a : ℕ) → Y.Subcomplex) d) (op n)) : Type u))
        (⇑{
              toFun := fun (x : (↑(Subfunctor.obj ((skeletonOfMono i : (a : ℕ) → Y.Subcomplex) d) (op n)) : Type u)) ↦
                Subtype.mk (p := fun (x : Y.obj (op n)) ↦
                  Membership.mem (γ := Set (Y.obj (op n)))
                    (Subfunctor.obj ((skeletonOfMono i : (a : ℕ) → Y.Subcomplex) (d + 1)) (op n)) x)
                  (↑x : Y.obj (op n)) ⋯ } :
          (a : (↑(((skeletonOfMono i : (a : ℕ) → Y.Subcomplex) d).obj (op n)) : Type u)) →
            (↑(((skeletonOfMono i : (a : ℕ) → Y.Subcomplex) (d + 1)).obj (op n)) : Type u)) ∪
      Set.range (ι := (sigmaStdSimplex i d).obj (op n))
        (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) ((b i d).app (op n))) :
          (a : (sigmaStdSimplex i d).obj (op n)) →
            (↑(((skeletonOfMono i : (a : ℕ) → Y.Subcomplex) (d + 1)).obj (op n)) : Type u)))
    (Subtype.mk (p := fun (x : Y.obj (op n)) ↦
      Membership.mem (γ := Set (Y.obj (op n)))
        (Subfunctor.obj ((skeletonOfMono i : (a : ℕ) → Y.Subcomplex) (d + 1)) (op n)) x)
      x hx_1)

Tactic:
obtain hx | ⟨y, hy₁, hy₂, f, rfl⟩ := hx

Premises used: rfl