obtain ⟨t, ht, hst⟩ := h.2 hs
case refine'_1
𝕜 : 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₁.Subdivides K₂
s : Finset E
hs : s ∈ K₁
⊢ ∃ s₂ ∈ K₂, combiInterior ℝ s ⊆ combiInterior ℝ s₂
case refine'_1.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₁.Subdivides K₂
s : Finset E
hs : s ∈ K₁
t : Finset E
ht : t ∈ K₂
hst : (convexHull ℝ) ↑s ⊆ (convexHull ℝ) ↑t
⊢ ∃ s₂ ∈ K₂, combiInterior ℝ s ⊆ combiInterior ℝ s₂