-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Finite (goal)
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
⊢ ∃ (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⦌)
        ⋯
have 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 sorry).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)
                sorry :
            (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⦌)
        sorry
Tactic: rw [Subcomplex.mem_nonDegenerate_iff] at h₂
Cleared hypotheses: i, hi