rwa [hs.2 ht hst]
case refine'_3.intro.intro.intro
𝕜 : 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 : ∀ ⦃s : Finset E⦄, s ∈ K → ∃ t ∈ K, t.card = n + 1 ∧ s ⊆ t
s : Finset E
hs : s ∈ K.facets
t : Finset E
ht : t ∈ K
htcard : t.card = n + 1
hst : s ⊆ t
⊢ s.card = n + 1
no goals