exact hx
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₁
hspace : K₁.space = K₂.space
s : Finset E
hs : s ∈ K₁
hsnonempty : s.Nonempty
x : E
hx : x ∈ combiInterior ℝ s
t : Finset E
ht : t ∈ K₂
hxt : x ∈ combiInterior ℝ t
x' : E
hx' : x' ∈ combiInterior ℝ s
t' : Finset E
ht' : t' ∈ K₂
F : Set (Finset E)
hF : F ⊆ K₁.faces
hinterior : combiInterior ℝ t = ⋃ s₁ ∈ F, combiInterior ℝ s₁
F' : Set (Finset E)
hF' : F' ⊆ K₁.faces
hinterior' : combiInterior ℝ t' = ⋃ s₁ ∈ F', combiInterior ℝ s₁
u : Finset E
hu : u ∈ F'
hxu : x' ∈ combiInterior ℝ u
⊢ x ∈ combiInterior ℝ s
no goals