exact h.subset ht
case refine'_1.faces.h.intro.intro
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝³ : LinearOrderedField 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
K : SimplicialComplex 𝕜 E
x y : E
s✝ t✝ : Finset E
A : Set (Finset E)
m n : ℕ
inst✝ : FiniteDimensional 𝕜 E
h : K.facets = ∅
s : Finset E
hs : s ∈ K.faces
t : Finset E
ht : t ∈ K.facets
⊢ False
no goals