rw [mem_iUnion₂]
case mp.intro.refine'_2.h.refine'_2
𝕜 : 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₂
x : E
⊢ x ∈ ⋃ s₁ ∈ {t | t ∈ K₁ ∧ combiInterior ℝ t ⊆ combiInterior ℝ s}, combiInterior ℝ s₁ → x ∈ combiInterior ℝ s
case mp.intro.refine'_2.h.refine'_2
𝕜 : 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₂
x : E
⊢ (∃ i, ∃ (_ : i ∈ {t | t ∈ K₁ ∧ combiInterior ℝ t ⊆ combiInterior ℝ s}), x ∈ combiInterior ℝ i) → x ∈ combiInterior ℝ s