Theorem: Geometry.SimplicialComplex.mem_of_mem_convexHull (LeanCamCombi/Mathlib/Analysis/Convex/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 : ℕ
hx : x ∈ K.vertices
hs : s ∈ K
hxs : x ∈ (convexHull 𝕜) ↑s
⊢ x ∈ s
Tactic:
have h := K.inter_subset_convexHull hx hs ⟨by simp, hxs⟩
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 : ℕ
hx : x ∈ K.vertices
hs : s ∈ K
hxs : x ∈ (convexHull 𝕜) ↑s
h : x ∈ (convexHull 𝕜) (↑{x} ∩ ↑s)
⊢ x ∈ s

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 : ℕ
hx : x ∈ K.vertices
hs : s ∈ K
hxs : x ∈ (convexHull 𝕜) ↑s
h : x ∈ (convexHull 𝕜) (↑{x} ∩ ↑s)
⊢ x ∈ s
Tactic:
by_contra H
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 : ℕ
hx : x ∈ K.vertices
hs : s ∈ K
hxs : x ∈ (convexHull 𝕜) ↑s
h : x ∈ (convexHull 𝕜) (↑{x} ∩ ↑s)
H : ¬x ∈ s
⊢ 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 : ℕ
hx : x ∈ K.vertices
hs : s ∈ K
hxs : x ∈ (convexHull 𝕜) ↑s
h : x ∈ (convexHull 𝕜) (↑{x} ∩ ↑s)
H : ¬x ∈ s
⊢ False
Tactic:
rwa [← coe_inter, inter_comm, disjoint_iff_inter_eq_empty.1 (disjoint_singleton_right.2 H),
  coe_empty, convexHull_empty] at h
State after:
no goals

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 : ℕ
hx : x ∈ K.vertices
hs : s ∈ K
hxs : x ∈ (convexHull 𝕜) ↑s
⊢ x ∈ (convexHull 𝕜) ↑{x}
Tactic:
simp
State after:
no goals