-- Mathlib/Analysis/Convex/Independent.lean
theorem convexIndependent_iff_finset {p : ι → E} :
    ConvexIndependent 𝕜 p ↔
      ∀ (s : Finset ι) (x : ι), p x ∈ convexHull 𝕜 (s.image p : Set E) → x ∈ s

Proof state:
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : ι → E
h : ∀ (s : Finset ι) (x : ι), p x ∈ (convexHull 𝕜) ↑(image p s) → x ∈ s
s : Set ι
x : ι
hx : p x ∈ (convexHull 𝕜) (p '' s)
a b : ι
hab : p a = p b
⊢ p a ∈ (convexHull 𝕜) ↑(image p {b})

Tactic:
rw [hab, image_singleton, coe_singleton, convexHull_singleton]

Result:
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : ι → E
h : ∀ (s : Finset ι) (x : ι), p x ∈ (convexHull 𝕜) ↑(image p s) → x ∈ s
s : Set ι
x : ι
hx : p x ∈ (convexHull 𝕜) (p '' s)
a b : ι
hab : p a = p b
⊢ p b ∈ {p b}

Proof state:
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : ι → E
h : ∀ (s : Finset ι) (x : ι), p x ∈ (convexHull 𝕜) ↑(image p s) → x ∈ s
s : Set ι
x : ι
hx : p x ∈ (convexHull 𝕜) (p '' s)
a b : ι
hab : p a = p b
⊢ a = b

Tactic:
rw [← mem_singleton]

Result:
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : ι → E
h : ∀ (s : Finset ι) (x : ι), p x ∈ (convexHull 𝕜) ↑(image p s) → x ∈ s
s : Set ι
x : ι
hx : p x ∈ (convexHull 𝕜) (p '' s)
a b : ι
hab : p a = p b
⊢ a ∈ {b}

Proof state:
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : ι → E
h : ∀ (s : Finset ι) (x : ι), p x ∈ (convexHull 𝕜) ↑(image p s) → x ∈ s
s : Set ι
x : ι
hx : p x ∈ (convexHull 𝕜) (p '' s)
a b : ι
hab : p a = p b
⊢ a ∈ {b}

Tactic:
refine h {b} a ?_

Result:
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : ι → E
h : ∀ (s : Finset ι) (x : ι), p x ∈ (convexHull 𝕜) ↑(image p s) → x ∈ s
s : Set ι
x : ι
hx : p x ∈ (convexHull 𝕜) (p '' s)
a b : ι
hab : p a = p b
⊢ p a ∈ (convexHull 𝕜) ↑(image p {b})

Proof state:
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : ι → E
h : ∀ (s : Finset ι) (x : ι), p x ∈ (convexHull 𝕜) ↑(image p s) → x ∈ s
s : Set ι
x : ι
hx : p x ∈ (convexHull 𝕜) (p '' s)
⊢ Injective p

Tactic:
rintro a b hab

Result:
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : ι → E
h : ∀ (s : Finset ι) (x : ι), p x ∈ (convexHull 𝕜) ↑(image p s) → x ∈ s
s : Set ι
x : ι
hx : p x ∈ (convexHull 𝕜) (p '' s)
a b : ι
hab : p a = p b
⊢ a = b

Proof state:
case refine_2.intro.intro
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : ι → E
h : ∀ (s : Finset ι) (x : ι), p x ∈ (convexHull 𝕜) ↑(image p s) → x ∈ s
s : Set ι
x : ι
hp : Injective p
t : Finset E
ht : ↑t ⊆ p '' s
hx : p x ∈ (convexHull 𝕜) ↑t
⊢ x ∈ s

Tactic:
rw [← hp.mem_set_image]

Result:
case refine_2.intro.intro
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : ι → E
h : ∀ (s : Finset ι) (x : ι), p x ∈ (convexHull 𝕜) ↑(image p s) → x ∈ s
s : Set ι
x : ι
hp : Injective p
t : Finset E
ht : ↑t ⊆ p '' s
hx : p x ∈ (convexHull 𝕜) ↑t
⊢ p x ∈ p '' s

Proof state:
case refine_2.intro.intro
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : ι → E
h : ∀ (s : Finset ι) (x : ι), p x ∈ (convexHull 𝕜) ↑(image p s) → x ∈ s
s : Set ι
x : ι
hp : Injective p
t : Finset E
ht : ↑t ⊆ p '' s
hx : p x ∈ (convexHull 𝕜) ↑t
⊢ p x ∈ p '' s

Tactic:
refine ht ?_

Result:
case refine_2.intro.intro
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : ι → E
h : ∀ (s : Finset ι) (x : ι), p x ∈ (convexHull 𝕜) ↑(image p s) → x ∈ s
s : Set ι
x : ι
hp : Injective p
t : Finset E
ht : ↑t ⊆ p '' s
hx : p x ∈ (convexHull 𝕜) ↑t
⊢ p x ∈ ↑t

Proof state:
case refine_2.intro.intro
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : ι → E
h : ∀ (s : Finset ι) (x : ι), p x ∈ (convexHull 𝕜) ↑(image p s) → x ∈ s
s : Set ι
x : ι
hp : Injective p
t : Finset E
ht : ↑t ⊆ p '' s
hx : p x ∈ (convexHull 𝕜) ↑t
⊢ p x ∈ ↑t

Tactic:
suffices x ∈ t.preimage p hp.injOn by rwa [mem_preimage, ← mem_coe] at this

Result:
case refine_2.intro.intro
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : ι → E
h : ∀ (s : Finset ι) (x : ι), p x ∈ (convexHull 𝕜) ↑(image p s) → x ∈ s
s : Set ι
x : ι
hp : Injective p
t : Finset E
ht : ↑t ⊆ p '' s
hx : p x ∈ (convexHull 𝕜) ↑t
⊢ x ∈ t.preimage p ⋯

Proof state:
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : ι → E
⊢ ConvexIndependent 𝕜 p ↔ ∀ (s : Finset ι) (x : ι), p x ∈ (convexHull 𝕜) ↑(image p s) → x ∈ s

Tactic:
refine ⟨fun hc s x hx => hc s x ?_, fun h s x hx => ?_⟩

Result:
case refine_1
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : ι → E
hc : ConvexIndependent 𝕜 p
s : Finset ι
x : ι
hx : p x ∈ (convexHull 𝕜) ↑(image p s)
⊢ p x ∈ (convexHull 𝕜) (p '' ↑s)

case refine_2
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : ι → E
h : ∀ (s : Finset ι) (x : ι), p x ∈ (convexHull 𝕜) ↑(image p s) → x ∈ s
s : Set ι
x : ι
hx : p x ∈ (convexHull 𝕜) (p '' s)
⊢ x ∈ s

Proof state:
case refine_2
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : ι → E
h : ∀ (s : Finset ι) (x : ι), p x ∈ (convexHull 𝕜) ↑(image p s) → x ∈ s
s : Set ι
x : ι
hx : p x ∈ (convexHull 𝕜) (p '' s)
⊢ x ∈ s

Tactic:
have hp : Injective p := by
  rintro a b hab
  rw [← mem_singleton]
  refine h {b} a ?_
  rw [hab, image_singleton, coe_singleton, convexHull_singleton]
  exact Set.mem_singleton _

Result:
case refine_2
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : ι → E
h : ∀ (s : Finset ι) (x : ι), p x ∈ (convexHull 𝕜) ↑(image p s) → x ∈ s
s : Set ι
x : ι
hx : p x ∈ (convexHull 𝕜) (p '' s)
hp : Injective p
⊢ x ∈ s

Proof state:
case refine_2.intro.intro
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : ι → E
h : ∀ (s : Finset ι) (x : ι), p x ∈ (convexHull 𝕜) ↑(image p s) → x ∈ s
s : Set ι
x : ι
hp : Injective p
t : Finset E
ht : ↑t ⊆ p '' s
hx : p x ∈ (convexHull 𝕜) ↑t
⊢ p x ∈ (convexHull 𝕜) ↑(image p (t.preimage p ⋯))

Tactic:
rwa [t.image_preimage p hp.injOn, filter_true_of_mem]

Result:
case refine_2.intro.intro
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : ι → E
h : ∀ (s : Finset ι) (x : ι), p x ∈ (convexHull 𝕜) ↑(image p s) → x ∈ s
s : Set ι
x : ι
hp : Injective p
t : Finset E
ht : ↑t ⊆ p '' s
hx : p x ∈ (convexHull 𝕜) ↑t
⊢ ∀ x ∈ t, x ∈ Set.range p

Proof state:
case refine_2.intro.intro
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : ι → E
h : ∀ (s : Finset ι) (x : ι), p x ∈ (convexHull 𝕜) ↑(image p s) → x ∈ s
s : Set ι
x : ι
hp : Injective p
t : Finset E
ht : ↑t ⊆ p '' s
hx : p x ∈ (convexHull 𝕜) ↑t
⊢ x ∈ t.preimage p ⋯

Tactic:
refine h _ x ?_

Result:
case refine_2.intro.intro
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : ι → E
h : ∀ (s : Finset ι) (x : ι), p x ∈ (convexHull 𝕜) ↑(image p s) → x ∈ s
s : Set ι
x : ι
hp : Injective p
t : Finset E
ht : ↑t ⊆ p '' s
hx : p x ∈ (convexHull 𝕜) ↑t
⊢ p x ∈ (convexHull 𝕜) ↑(image p (t.preimage p ⋯))