refine' ⟨fun s hs => hK.1 <| skeleton_le hs, fun s hs => _⟩
case inr
𝕜 : Type u_1
E : Type u_2
inst✝³ : LinearOrderedField 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : FiniteDimensional 𝕜 E
m n k : ℕ
K : SimplicialComplex 𝕜 E
s t : Finset E
A : Set (Finset E)
hK : K.Pure n
hn : n ≤ k
⊢ (K.skeleton k).Pure n
case inr
𝕜 : Type u_1
E : Type u_2
inst✝³ : LinearOrderedField 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : FiniteDimensional 𝕜 E
m n k : ℕ
K : SimplicialComplex 𝕜 E
s✝ t : Finset E
A : Set (Finset E)
hK : K.Pure n
hn : n ≤ k
s : Finset E
hs : s ∈ (K.skeleton k).facets
⊢ s.card = n + 1