-- Module: Mathlib.AlgebraicTopology.SimplicialSet.Finite
Goal:
X : SSet
ι : Type u_1
inst : Finite ι
A : ι → X.Subcomplex
h : ∀ (i : ι), SSet.Finite.{u} (A i).toSSet
d : ℕ
s : X _⦋d⦌
h₁ : Membership.mem (γ := Set (X _⦋d⦌)) (Subfunctor.obj (⨆ (i : ι), A i) (Opposite.op ⦋d⦌)) s
h₂ :
  Membership.mem (γ := Set (Subcomplex.toSSet (X := X) (⨆ (i : ι), A i) _⦋d⦌))
    ((Subcomplex.toSSet (X := X) (⨆ (i : ι), A i)).nonDegenerate d)
    (Subtype.mk (p := fun (x : X _⦋d⦌) ↦
      Membership.mem (γ := Set (X _⦋d⦌)) (Subfunctor.obj (⨆ (i : ι), A i) (Opposite.op ⦋d⦌)) x) s h₁)
i : ι
hi : Membership.mem (γ := Set (X _⦋d⦌)) ((A i).obj (Opposite.op ⦋d⦌)) s
rw :
  ∀
    (h₂_1 :
      (↑(Subtype.mk (p := fun (x : X _⦋d⦌) ↦
              Membership.mem (γ := Set (X _⦋d⦌)) (Subfunctor.obj (⨆ (i : ι), A i) (Opposite.op ⦋d⦌)) x) s h₁) :
          X _⦋d⦌) ∈
        X.nonDegenerate d)
    (i : ι) (hi : Membership.mem (γ := Set (X _⦋d⦌)) ((A i).obj (Opposite.op ⦋d⦌)) s),
    ∃ (a : (i : ι) × (A i).toSSet.N),
      (fun (x : (i : ι) × (A i).toSSet.N) ↦
            (match (motive := (i : ι) × (A i).toSSet.N → (Subcomplex.toSSet (X := X) (⨆ (i : ι), A i)).N) x with
              | ⟨i, s⟩ =>
                N.mk
                  ((ConcreteCategory.hom (FC := TypeCat.Fun) ((Subcomplex.homOfLE ⋯).app (Opposite.op ⦋s.dim⦌)) :
                      (a : (fun (X : Type u) ↦ X) ((A i).toSSet _⦋s.dim⦌)) →
                        (fun (X : Type u) ↦ X) ((iSup A).toSSet _⦋s.dim⦌))
                    s.simplex)
                  ⋯ :
              (Subcomplex.toSSet (X := X) (⨆ (i : ι), A i)).N))
          a =
        N.mk
          (↑(Subtype.mk (p := fun (x : Subcomplex.toSSet (X := X) (⨆ (i : ι), A i) _⦋d⦌) ↦
                Membership.mem (γ := Set (Subcomplex.toSSet (X := X) (⨆ (i : ι), A i) _⦋d⦌))
                  ((Subcomplex.toSSet (X := X) (⨆ (i : ι), A i)).nonDegenerate d) x)
                (Subtype.mk (p := fun (x : X _⦋d⦌) ↦
                  Membership.mem (γ := Set (X _⦋d⦌)) (Subfunctor.obj (⨆ (i : ι), A i) (Opposite.op ⦋d⦌)) x) s h₁)
                h₂) :
            (⨆ (i : ι), A i).toSSet _⦋d⦌)
          ⋯
⊢ ∃ (a : (i : ι) × (A i).toSSet.N),
    (fun (x : (i : ι) × (A i).toSSet.N) ↦
          (match (motive := (i : ι) × (A i).toSSet.N → (Subcomplex.toSSet (X := X) (⨆ (i : ι), A i)).N) x with
            | ⟨i, s⟩ =>
              N.mk
                ((ConcreteCategory.hom (FC := TypeCat.Fun) ((Subcomplex.homOfLE ⋯).app (Opposite.op ⦋s.dim⦌)) :
                    (a : (fun (X : Type u) ↦ X) ((A i).toSSet _⦋s.dim⦌)) →
                      (fun (X : Type u) ↦ X) ((iSup A).toSSet _⦋s.dim⦌))
                  s.simplex)
                ⋯ :
            (Subcomplex.toSSet (X := X) (⨆ (i : ι), A i)).N))
        a =
      N.mk
        (↑(Subtype.mk (p := fun (x : Subcomplex.toSSet (X := X) (⨆ (i : ι), A i) _⦋d⦌) ↦
              Membership.mem (γ := Set (Subcomplex.toSSet (X := X) (⨆ (i : ι), A i) _⦋d⦌))
                ((Subcomplex.toSSet (X := X) (⨆ (i : ι), A i)).nonDegenerate d) x)
              (Subtype.mk (p := fun (x : X _⦋d⦌) ↦
                Membership.mem (γ := Set (X _⦋d⦌)) (Subfunctor.obj (⨆ (i : ι), A i) (Opposite.op ⦋d⦌)) x) s h₁)
              h₂) :
          (⨆ (i : ι), A i).toSSet _⦋d⦌)
        ⋯

Tactic:
rw [Subcomplex.mem_nonDegenerate_iff] at h₂

Premises used: SSet.Subcomplex.mem_nonDegenerate_iff