rw [disjoint_interiors hs (K₂.down_closed hu hWu _) hxs (htW hxt)]
case mp.intro.refine'_2.h.refine'_1.intro.intro.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
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
hxs : x ∈ combiInterior ℝ s
t : Finset E
ht : t ∈ K₁
hxt : x ∈ combiInterior ℝ t
y : E
hyt : y ∈ combiInterior ℝ t
u : Finset E
hu : u ∈ K₂
htu : (convexHull ℝ) ↑t ⊆ (convexHull ℝ) ↑u
W : Finset E
hWu : W ⊆ u
htW : combiInterior ℝ t ⊆ combiInterior ℝ W
⊢ y ∈ combiInterior ℝ s
case mp.intro.refine'_2.h.refine'_1.intro.intro.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
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
hxs : x ∈ combiInterior ℝ s
t : Finset E
ht : t ∈ K₁
hxt : x ∈ combiInterior ℝ t
y : E
hyt : y ∈ combiInterior ℝ t
u : Finset E
hu : u ∈ K₂
htu : (convexHull ℝ) ↑t ⊆ (convexHull ℝ) ↑u
W : Finset E
hWu : W ⊆ u
htW : combiInterior ℝ t ⊆ combiInterior ℝ W
⊢ y ∈ combiInterior ℝ W

𝕜 : 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
hxs : x ∈ combiInterior ℝ s
t : Finset E
ht : t ∈ K₁
hxt : x ∈ combiInterior ℝ t
y : E
hyt : y ∈ combiInterior ℝ t
u : Finset E
hu : u ∈ K₂
htu : (convexHull ℝ) ↑t ⊆ (convexHull ℝ) ↑u
W : Finset E
hWu : W ⊆ u
htW : combiInterior ℝ t ⊆ combiInterior ℝ W
⊢ W ≠ ∅