Theorem: Geometry.SimplicialComplex.Pure.exists_facet (LeanCamCombi/SimplicialComplex/Pure.lean)

State before:
𝕜 : Type u_1
E : Type u_2
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
a b n k : ℕ
K : SimplicialComplex 𝕜 E
s : Finset E
hK : K.Pure n
hs : s ∈ K
⊢ ∃ t ∈ K.facets, s ⊆ t
Tactic:
sorry
State after:
no goals