obtain ⟨F, hF, hsint⟩ := hpartition _ hs
case 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
hempty : K₁.faces.Nonempty → K₂.faces.Nonempty
hspace : K₁.space ⊆ K₂.space
hpartition : ∀ s₂ ∈ K₂, ∃ F ⊆ K₁.faces, combiInterior ℝ s₂ = ⋃ s₁ ∈ F, combiInterior ℝ s₁
x : E
s : Finset E
hs : s ∈ K₂
hxs : x ∈ combiInterior ℝ s
⊢ ∃ i, ∃ (_ : i ∈ K₁), x ∈ combiInterior ℝ i
case 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
hempty : K₁.faces.Nonempty → K₂.faces.Nonempty
hspace : K₁.space ⊆ K₂.space
hpartition : ∀ s₂ ∈ K₂, ∃ F ⊆ K₁.faces, combiInterior ℝ s₂ = ⋃ s₁ ∈ F, combiInterior ℝ s₁
x : E
s : Finset E
hs : s ∈ K₂
hxs : x ∈ combiInterior ℝ s
F : Set (Finset E)
hF : F ⊆ K₁.faces
hsint : combiInterior ℝ s = ⋃ s₁ ∈ F, combiInterior ℝ s₁
⊢ ∃ i, ∃ (_ : i ∈ K₁), x ∈ combiInterior ℝ i