Theorem: Geometry.SimplicialComplex.subset_of_combiInterior_inter_convexHull_nonempty (LeanCamCombi/SimplicialComplex/Basic.lean)

State before:
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
K K₁ K₂ : SimplicialComplex 𝕜 E
x y : E
s t : Finset E
A : Set (Finset E)
m n : ℕ
hs : s ∈ K
ht : t ∈ K
hst : (combiInterior 𝕜 s ∩ (convexHull 𝕜) ↑t).Nonempty
⊢ s ⊆ t
Tactic:
obtain ⟨x, hxs, hxt⟩ := hst
State after:
case intro.intro
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
K K₁ K₂ : SimplicialComplex 𝕜 E
x✝ y : E
s t : Finset E
A : Set (Finset E)
m n : ℕ
hs : s ∈ K
ht : t ∈ K
x : E
hxs : x ∈ combiInterior 𝕜 s
hxt : x ∈ (convexHull 𝕜) ↑t
⊢ s ⊆ t

State before:
case intro.intro
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
K K₁ K₂ : SimplicialComplex 𝕜 E
x✝ y : E
s t : Finset E
A : Set (Finset E)
m n : ℕ
hs : s ∈ K
ht : t ∈ K
x : E
hxs : x ∈ combiInterior 𝕜 s
hxt : x ∈ (convexHull 𝕜) ↑t
⊢ s ⊆ t
Tactic:
obtain ⟨u, hut, hxu⟩ := mem_convexHull_iff.1 hxt
State after:
case intro.intro.intro.intro
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
K K₁ K₂ : SimplicialComplex 𝕜 E
x✝ y : E
s t : Finset E
A : Set (Finset E)
m n : ℕ
hs : s ∈ K
ht : t ∈ K
x : E
hxs : x ∈ combiInterior 𝕜 s
hxt : x ∈ (convexHull 𝕜) ↑t
u : Finset E
hut : u ⊆ t
hxu : x ∈ combiInterior 𝕜 u
⊢ s ⊆ t

State before:
case intro.intro.intro.intro
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
K K₁ K₂ : SimplicialComplex 𝕜 E
x✝ y : E
s t : Finset E
A : Set (Finset E)
m n : ℕ
hs : s ∈ K
ht : t ∈ K
x : E
hxs : x ∈ combiInterior 𝕜 s
hxt : x ∈ (convexHull 𝕜) ↑t
u : Finset E
hut : u ⊆ t
hxu : x ∈ combiInterior 𝕜 u
⊢ s ⊆ t
Tactic:
rw [disjoint_interiors hs (K.down_closed' ht hut <| nonempty_of_ne_empty _) hxs hxu]
State after:
case intro.intro.intro.intro
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
K K₁ K₂ : SimplicialComplex 𝕜 E
x✝ y : E
s t : Finset E
A : Set (Finset E)
m n : ℕ
hs : s ∈ K
ht : t ∈ K
x : E
hxs : x ∈ combiInterior 𝕜 s
hxt : x ∈ (convexHull 𝕜) ↑t
u : Finset E
hut : u ⊆ t
hxu : x ∈ combiInterior 𝕜 u
⊢ u ⊆ t

𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
K K₁ K₂ : SimplicialComplex 𝕜 E
x✝ y : E
s t : Finset E
A : Set (Finset E)
m n : ℕ
hs : s ∈ K
ht : t ∈ K
x : E
hxs : x ∈ combiInterior 𝕜 s
hxt : x ∈ (convexHull 𝕜) ↑t
u : Finset E
hut : u ⊆ t
hxu : x ∈ combiInterior 𝕜 u
⊢ u ≠ ∅

State before:
case intro.intro.intro.intro
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
K K₁ K₂ : SimplicialComplex 𝕜 E
x✝ y : E
s t : Finset E
A : Set (Finset E)
m n : ℕ
hs : s ∈ K
ht : t ∈ K
x : E
hxs : x ∈ combiInterior 𝕜 s
hxt : x ∈ (convexHull 𝕜) ↑t
u : Finset E
hut : u ⊆ t
hxu : x ∈ combiInterior 𝕜 u
⊢ u ⊆ t

𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
K K₁ K₂ : SimplicialComplex 𝕜 E
x✝ y : E
s t : Finset E
A : Set (Finset E)
m n : ℕ
hs : s ∈ K
ht : t ∈ K
x : E
hxs : x ∈ combiInterior 𝕜 s
hxt : x ∈ (convexHull 𝕜) ↑t
u : Finset E
hut : u ⊆ t
hxu : x ∈ combiInterior 𝕜 u
⊢ u ≠ ∅
Tactic:
exact hut
State after:
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
K K₁ K₂ : SimplicialComplex 𝕜 E
x✝ y : E
s t : Finset E
A : Set (Finset E)
m n : ℕ
hs : s ∈ K
ht : t ∈ K
x : E
hxs : x ∈ combiInterior 𝕜 s
hxt : x ∈ (convexHull 𝕜) ↑t
u : Finset E
hut : u ⊆ t
hxu : x ∈ combiInterior 𝕜 u
⊢ u ≠ ∅

State before:
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
K K₁ K₂ : SimplicialComplex 𝕜 E
x✝ y : E
s t : Finset E
A : Set (Finset E)
m n : ℕ
hs : s ∈ K
ht : t ∈ K
x : E
hxs : x ∈ combiInterior 𝕜 s
hxt : x ∈ (convexHull 𝕜) ↑t
u : Finset E
hut : u ⊆ t
hxu : x ∈ combiInterior 𝕜 u
⊢ u ≠ ∅
Tactic:
rintro rfl
State after:
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
K K₁ K₂ : SimplicialComplex 𝕜 E
x✝ y : E
s t : Finset E
A : Set (Finset E)
m n : ℕ
hs : s ∈ K
ht : t ∈ K
x : E
hxs : x ∈ combiInterior 𝕜 s
hxt : x ∈ (convexHull 𝕜) ↑t
hut : ∅ ⊆ t
hxu : x ∈ combiInterior 𝕜 ∅
⊢ False

State before:
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
K K₁ K₂ : SimplicialComplex 𝕜 E
x✝ y : E
s t : Finset E
A : Set (Finset E)
m n : ℕ
hs : s ∈ K
ht : t ∈ K
x : E
hxs : x ∈ combiInterior 𝕜 s
hxt : x ∈ (convexHull 𝕜) ↑t
hut : ∅ ⊆ t
hxu : x ∈ combiInterior 𝕜 ∅
⊢ False
Tactic:
rwa [combiInterior_empty] at hxu
State after:
no goals