obtain ⟨s₁, hs₁, hx⟩ := mem_space_iff.1 hx
case refine'_2
𝕜 : Type u_1
E : Type u_2
inst✝² : SeminormedAddCommGroup E
inst✝¹ : T2Space E
inst✝ : NormedSpace ℝ E
s t : Finset E
m : ℕ
K₁ K₂ : SimplicialComplex ℝ E
h : K₂.space ⊆ K₁.space ∧ ∀ s₁ ∈ K₁, ∃ s₂ ∈ K₂, combiInterior ℝ s₁ ⊆ combiInterior ℝ s₂
x : E
hx : x ∈ K₁.space
⊢ x ∈ K₂.space
case refine'_2.intro.intro
𝕜 : Type u_1
E : Type u_2
inst✝² : SeminormedAddCommGroup E
inst✝¹ : T2Space E
inst✝ : NormedSpace ℝ E
s t : Finset E
m : ℕ
K₁ K₂ : SimplicialComplex ℝ E
h : K₂.space ⊆ K₁.space ∧ ∀ s₁ ∈ K₁, ∃ s₂ ∈ K₂, combiInterior ℝ s₁ ⊆ combiInterior ℝ s₂
x : E
hx✝ : x ∈ K₁.space
s₁ : Finset E
hs₁ : s₁ ∈ K₁.faces
hx : x ∈ (convexHull ℝ) ↑s₁
⊢ x ∈ K₂.space