Theorem: combiFrontier_singleton (LeanCamCombi/SimplicialComplex/Simplex.lean)

State before:
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t : Finset E
x : E
⊢ combiFrontier 𝕜 {x} = ∅
Tactic:
refine eq_empty_of_subset_empty fun y hy ↦ ?_
State after:
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t : Finset E
x y : E
hy : y ∈ combiFrontier 𝕜 {x}
⊢ y ∈ ∅

State before:
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t : Finset E
x y : E
hy : y ∈ combiFrontier 𝕜 {x}
⊢ y ∈ ∅
Tactic:
rw [mem_combiFrontier_iff] at hy
State after:
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t : Finset E
x y : E
hy : ∃ t ⊂ {x}, y ∈ (convexHull 𝕜) ↑t
⊢ y ∈ ∅

State before:
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t : Finset E
x y : E
hy : ∃ t ⊂ {x}, y ∈ (convexHull 𝕜) ↑t
⊢ y ∈ ∅
Tactic:
obtain ⟨s, hs, hys⟩ := hy
State after:
case intro.intro
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s✝ t : Finset E
x y : E
s : Finset E
hs : s ⊂ {x}
hys : y ∈ (convexHull 𝕜) ↑s
⊢ y ∈ ∅

State before:
case intro.intro
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s✝ t : Finset E
x y : E
s : Finset E
hs : s ⊂ {x}
hys : y ∈ (convexHull 𝕜) ↑s
⊢ y ∈ ∅
Tactic:
rw [Finset.eq_empty_of_ssubset_singleton hs] at hys
State after:
case intro.intro
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s✝ t : Finset E
x y : E
s : Finset E
hs : s ⊂ {x}
hys : y ∈ (convexHull 𝕜) ↑∅
⊢ y ∈ ∅

State before:
case intro.intro
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s✝ t : Finset E
x y : E
s : Finset E
hs : s ⊂ {x}
hys : y ∈ (convexHull 𝕜) ↑∅
⊢ y ∈ ∅
Tactic:
simp at hys
State after:
no goals