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