exact ⟨s₂, hs₂, convexHull_subset_convexHull_of_combiInterior_subset_combiInterior
  (K₁.indep hs₁) (K₂.indep hs₂) hs₁s₂ hx⟩
case refine'_2.intro.intro.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₁
s₂ : Finset E
hs₂ : s₂ ∈ K₂
hs₁s₂ : combiInterior ℝ s₁ ⊆ combiInterior ℝ s₂
⊢ ∃ s ∈ K₂.faces, x ∈ (convexHull ℝ) ↑s
no goals