by_contra hXY
case pos.intro.intro.intro.intro.refine'_2
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝³ : OrderedRing 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
K K₁ K₂ : SimplicialComplex 𝕜 E
x✝ t✝¹ : E
s✝ t✝ : Finset E
A : Set (Finset E)
m n : ℕ
inst✝ : DecidableEq E
x : E
hx : ¬{s | s ∈ K.faces ∧ x ∈ (convexHull 𝕜) ↑s}.Finite
hxspace : x ∈ K.space
s : Finset E
hX : s ∈ K
hXhull : x ∈ (convexHull 𝕜) ↑s
hXbound : x ∉ combiFrontier 𝕜 s
hXunique : ∀ y ∈ K, x ∈ combiInterior 𝕜 y → y = s
hXlocallyfinite : K.LocallyFiniteAt s
t : Finset E
hY : t ∈ {s | s ∈ K.faces ∧ x ∈ (convexHull 𝕜) ↑s}
hXYhull : x ∈ (convexHull 𝕜) ↑(s ∩ t)
⊢ s ⊆ t
case pos.intro.intro.intro.intro.refine'_2
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝³ : OrderedRing 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
K K₁ K₂ : SimplicialComplex 𝕜 E
x✝ t✝¹ : E
s✝ t✝ : Finset E
A : Set (Finset E)
m n : ℕ
inst✝ : DecidableEq E
x : E
hx : ¬{s | s ∈ K.faces ∧ x ∈ (convexHull 𝕜) ↑s}.Finite
hxspace : x ∈ K.space
s : Finset E
hX : s ∈ K
hXhull : x ∈ (convexHull 𝕜) ↑s
hXbound : x ∉ combiFrontier 𝕜 s
hXunique : ∀ y ∈ K, x ∈ combiInterior 𝕜 y → y = s
hXlocallyfinite : K.LocallyFiniteAt s
t : Finset E
hY : t ∈ {s | s ∈ K.faces ∧ x ∈ (convexHull 𝕜) ↑s}
hXYhull : x ∈ (convexHull 𝕜) ↑(s ∩ t)
hXY : ¬s ⊆ t
⊢ False