exact ⟨s₂, hs₂⟩
case mp.intro.refine'_1.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
hspace : K₁.space = K₂.space
hsubdiv : ∀ ⦃s₁ : Finset E⦄, s₁ ∈ K₁ → ∃ s₂ ∈ K₂, (convexHull ℝ) ↑s₁ ⊆ (convexHull ℝ) ↑s₂
s₁ : Finset E
hs₁ : s₁ ∈ K₁.faces
s₂ : Finset E
hs₂ : s₂ ∈ K₂
⊢ K₂.faces.Nonempty
no goals