refine' fun s hs => ⟨h hs.1, fun t ht hst => Finset.eq_of_subset_of_card_le hst _⟩
𝕜 : 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
K₁ K₂ : SimplicialComplex 𝕜 E
h : K₁ ≤ K₂
hK₁ : K₁.Pure n
hK₂ : K₂.Pure n
⊢ K₁.facets ⊆ K₂.facets
𝕜 : 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
K₁ K₂ : SimplicialComplex 𝕜 E
h : K₁ ≤ K₂
hK₁ : K₁.Pure n
hK₂ : K₂.Pure n
s : Finset E
hs : s ∈ K₁.facets
t : Finset E
ht : t ∈ K₂.faces
hst : s ⊆ t
⊢ t.card ≤ s.card