refine' ⟨fun s hs => hs.2, _⟩
𝕜 : Type u_1
E : Type u_2
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
m n k : ℕ
K : SimplicialComplex 𝕜 E
s t : Finset E
A : Set (Finset E)
hK : K.Pure n
h : k ≤ n
⊢ (K.skeleton k).Pure k
𝕜 : Type u_1
E : Type u_2
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
m n k : ℕ
K : SimplicialComplex 𝕜 E
s t : Finset E
A : Set (Finset E)
hK : K.Pure n
h : k ≤ n
⊢ Set.Sized (k + 1) (K.skeleton k).facets