-- Mathlib/Analysis/Convex/Independent.lean
theorem convexIndependent_iff_not_mem_convexHull_diff {p : ι → E} :
    ConvexIndependent 𝕜 p ↔ ∀ i s, p i ∉ convexHull 𝕜 (p '' (s \ {i}))

Proof state:
case refine_1
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : OrderedSemiring 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : ι → E
hc : ConvexIndependent 𝕜 p
i : ι
s : Set ι
h : p i ∈ (convexHull 𝕜) (p '' (s \ {i}))
⊢ False

Tactic:
rw [hc.mem_convexHull_iff] at h

Result:
case refine_1
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : OrderedSemiring 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : ι → E
hc : ConvexIndependent 𝕜 p
i : ι
s : Set ι
h : i ∈ s \ {i}
⊢ False

Proof state:
case refine_2
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : OrderedSemiring 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : ι → E
h : ∀ (i : ι) (s : Set ι), p i ∉ (convexHull 𝕜) (p '' (s \ {i}))
s : Set ι
i : ι
hi : p i ∈ (convexHull 𝕜) (p '' s)
H : i ∉ s
⊢ False

Tactic:
refine h i s ?_

Result:
case refine_2
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : OrderedSemiring 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : ι → E
h : ∀ (i : ι) (s : Set ι), p i ∉ (convexHull 𝕜) (p '' (s \ {i}))
s : Set ι
i : ι
hi : p i ∈ (convexHull 𝕜) (p '' s)
H : i ∉ s
⊢ p i ∈ (convexHull 𝕜) (p '' (s \ {i}))

Proof state:
case refine_1
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : OrderedSemiring 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : ι → E
hc : ConvexIndependent 𝕜 p
i : ι
s : Set ι
h : i ∈ s \ {i}
⊢ False

Tactic:
exact h.2 (Set.mem_singleton _)

Result:
no goals

Proof state:
case refine_2
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : OrderedSemiring 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : ι → E
h : ∀ (i : ι) (s : Set ι), p i ∉ (convexHull 𝕜) (p '' (s \ {i}))
s : Set ι
i : ι
hi : p i ∈ (convexHull 𝕜) (p '' s)
H : i ∉ s
⊢ p i ∈ (convexHull 𝕜) (p '' (s \ {i}))

Tactic:
rw [Set.diff_singleton_eq_self H]

Result:
case refine_2
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : OrderedSemiring 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : ι → E
h : ∀ (i : ι) (s : Set ι), p i ∉ (convexHull 𝕜) (p '' (s \ {i}))
s : Set ι
i : ι
hi : p i ∈ (convexHull 𝕜) (p '' s)
H : i ∉ s
⊢ p i ∈ (convexHull 𝕜) (p '' s)

Proof state:
case refine_2
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : OrderedSemiring 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : ι → E
h : ∀ (i : ι) (s : Set ι), p i ∉ (convexHull 𝕜) (p '' (s \ {i}))
s : Set ι
i : ι
hi : p i ∈ (convexHull 𝕜) (p '' s)
⊢ i ∈ s

Tactic:
by_contra H

Result:
case refine_2
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : OrderedSemiring 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : ι → E
h : ∀ (i : ι) (s : Set ι), p i ∉ (convexHull 𝕜) (p '' (s \ {i}))
s : Set ι
i : ι
hi : p i ∈ (convexHull 𝕜) (p '' s)
H : i ∉ s
⊢ False

Proof state:
case refine_2
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : OrderedSemiring 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : ι → E
h : ∀ (i : ι) (s : Set ι), p i ∉ (convexHull 𝕜) (p '' (s \ {i}))
s : Set ι
i : ι
hi : p i ∈ (convexHull 𝕜) (p '' s)
H : i ∉ s
⊢ p i ∈ (convexHull 𝕜) (p '' s)

Tactic:
exact hi

Result:
no goals

Proof state:
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : OrderedSemiring 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : ι → E
⊢ ConvexIndependent 𝕜 p ↔ ∀ (i : ι) (s : Set ι), p i ∉ (convexHull 𝕜) (p '' (s \ {i}))

Tactic:
refine ⟨fun hc i s h => ?_, fun h s i hi => ?_⟩

Result:
case refine_1
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : OrderedSemiring 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : ι → E
hc : ConvexIndependent 𝕜 p
i : ι
s : Set ι
h : p i ∈ (convexHull 𝕜) (p '' (s \ {i}))
⊢ False

case refine_2
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : OrderedSemiring 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : ι → E
h : ∀ (i : ι) (s : Set ι), p i ∉ (convexHull 𝕜) (p '' (s \ {i}))
s : Set ι
i : ι
hi : p i ∈ (convexHull 𝕜) (p '' s)
⊢ i ∈ s