-- Mathlib/Analysis/Convex/Independent.lean
theorem convexIndependent_set_iff_not_mem_convexHull_diff {s : Set E} :
    ConvexIndependent 𝕜 ((↑) : s → E) ↔ ∀ x ∈ s, x ∉ convexHull 𝕜 (s \ {x})

Proof state:
case mpr.intro
𝕜 : Type u_1
E : Type u_2
inst✝² : OrderedSemiring 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s : Set E
hs : ∀ x ∈ s, x ∉ (convexHull 𝕜) (s \ {x})
t : Set E
ht : t ⊆ s
x : E
hxs : x ∈ s
hxt : x ∈ (convexHull 𝕜) t
⊢ x ∈ t

Tactic:
by_contra h

Result:
case mpr.intro
𝕜 : Type u_1
E : Type u_2
inst✝² : OrderedSemiring 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s : Set E
hs : ∀ x ∈ s, x ∉ (convexHull 𝕜) (s \ {x})
t : Set E
ht : t ⊆ s
x : E
hxs : x ∈ s
hxt : x ∈ (convexHull 𝕜) t
h : x ∉ t
⊢ False

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : OrderedSemiring 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s : Set E
⊢ ConvexIndependent 𝕜 Subtype.val ↔ ∀ x ∈ s, x ∉ (convexHull 𝕜) (s \ {x})

Tactic:
rw [convexIndependent_set_iff_inter_convexHull_subset]

Result:
𝕜 : Type u_1
E : Type u_2
inst✝² : OrderedSemiring 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s : Set E
⊢ (∀ t ⊆ s, s ∩ (convexHull 𝕜) t ⊆ t) ↔ ∀ x ∈ s, x ∉ (convexHull 𝕜) (s \ {x})

Proof state:
case mpr
𝕜 : Type u_1
E : Type u_2
inst✝² : OrderedSemiring 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s : Set E
⊢ (∀ x ∈ s, x ∉ (convexHull 𝕜) (s \ {x})) → ∀ t ⊆ s, s ∩ (convexHull 𝕜) t ⊆ t

Tactic:
rintro hs t ht x ⟨hxs, hxt⟩

Result:
case mpr.intro
𝕜 : Type u_1
E : Type u_2
inst✝² : OrderedSemiring 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s : Set E
hs : ∀ x ∈ s, x ∉ (convexHull 𝕜) (s \ {x})
t : Set E
ht : t ⊆ s
x : E
hxs : x ∈ s
hxt : x ∈ (convexHull 𝕜) t
⊢ x ∈ t

Proof state:
case mp
𝕜 : Type u_1
E : Type u_2
inst✝² : OrderedSemiring 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s : Set E
hs : ∀ t ⊆ s, s ∩ (convexHull 𝕜) t ⊆ t
x : E
hxs : x ∈ s
hx : x ∈ (convexHull 𝕜) (s \ {x})
⊢ False

Tactic:
exact (hs _ Set.diff_subset ⟨hxs, hx⟩).2 (Set.mem_singleton _)

Result:
no goals

Proof state:
case mpr.intro
𝕜 : Type u_1
E : Type u_2
inst✝² : OrderedSemiring 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s : Set E
hs : ∀ x ∈ s, x ∉ (convexHull 𝕜) (s \ {x})
t : Set E
ht : t ⊆ s
x : E
hxs : x ∈ s
hxt : x ∈ (convexHull 𝕜) t
h : x ∉ t
⊢ False

Tactic:
exact hs _ hxs (convexHull_mono (Set.subset_diff_singleton ht h) hxt)

Result:
no goals

Proof state:
case mp
𝕜 : Type u_1
E : Type u_2
inst✝² : OrderedSemiring 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s : Set E
⊢ (∀ t ⊆ s, s ∩ (convexHull 𝕜) t ⊆ t) → ∀ x ∈ s, x ∉ (convexHull 𝕜) (s \ {x})

Tactic:
rintro hs x hxs hx

Result:
case mp
𝕜 : Type u_1
E : Type u_2
inst✝² : OrderedSemiring 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s : Set E
hs : ∀ t ⊆ s, s ∩ (convexHull 𝕜) t ⊆ t
x : E
hxs : x ∈ s
hx : x ∈ (convexHull 𝕜) (s \ {x})
⊢ False

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : OrderedSemiring 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s : Set E
⊢ (∀ t ⊆ s, s ∩ (convexHull 𝕜) t ⊆ t) ↔ ∀ x ∈ s, x ∉ (convexHull 𝕜) (s \ {x})

Tactic:
constructor

Result:
case mp
𝕜 : Type u_1
E : Type u_2
inst✝² : OrderedSemiring 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s : Set E
⊢ (∀ t ⊆ s, s ∩ (convexHull 𝕜) t ⊆ t) → ∀ x ∈ s, x ∉ (convexHull 𝕜) (s \ {x})

case mpr
𝕜 : Type u_1
E : Type u_2
inst✝² : OrderedSemiring 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s : Set E
⊢ (∀ x ∈ s, x ∉ (convexHull 𝕜) (s \ {x})) → ∀ t ⊆ s, s ∩ (convexHull 𝕜) t ⊆ t