Theorem: extremePoints_convexHull_eq_iff_convexIndependent (LeanCamCombi/Mathlib/Analysis/Convex/Extreme.lean)

State before:
𝕜 : Type u_1
E : Type u_2
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t : Set E
x : E
⊢ extremePoints 𝕜 ((convexHull 𝕜) s) = s ↔ ConvexIndependent 𝕜 fun p => ↑p
Tactic:
refine' ⟨fun h => _, fun hs => _⟩
State after:
case refine'_1
𝕜 : Type u_1
E : Type u_2
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t : Set E
x : E
h : extremePoints 𝕜 ((convexHull 𝕜) s) = s
⊢ ConvexIndependent 𝕜 fun p => ↑p

case refine'_2
𝕜 : Type u_1
E : Type u_2
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t : Set E
x : E
hs : ConvexIndependent 𝕜 fun p => ↑p
⊢ extremePoints 𝕜 ((convexHull 𝕜) s) = s

State before:
case refine'_2
𝕜 : Type u_1
E : Type u_2
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t : Set E
x : E
hs : ConvexIndependent 𝕜 fun p => ↑p
⊢ extremePoints 𝕜 ((convexHull 𝕜) s) = s
Tactic:
rw [convexIndependent_set_iff_not_mem_convexHull_diff] at hs
State after:
case refine'_2
𝕜 : Type u_1
E : Type u_2
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t : Set E
x : E
hs : ∀ x ∈ s, x ∉ (convexHull 𝕜) (s \ {x})
⊢ extremePoints 𝕜 ((convexHull 𝕜) s) = s

State before:
case refine'_2
𝕜 : Type u_1
E : Type u_2
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t : Set E
x : E
hs : ∀ x ∈ s, x ∉ (convexHull 𝕜) (s \ {x})
⊢ extremePoints 𝕜 ((convexHull 𝕜) s) = s
Tactic:
refine' extremePoints_convexHull_subset.antisymm fun x hxs => ⟨subset_convexHull 𝕜 _ hxs, _⟩
State after:
case refine'_2
𝕜 : Type u_1
E : Type u_2
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t : Set E
x✝ : E
hs : ∀ x ∈ s, x ∉ (convexHull 𝕜) (s \ {x})
x : E
hxs : x ∈ s
⊢ ∀ ⦃x₁ : E⦄, x₁ ∈ (convexHull 𝕜) s → ∀ ⦃x₂ : E⦄, x₂ ∈ (convexHull 𝕜) s → x ∈ openSegment 𝕜 x₁ x₂ → x₁ = x ∧ x₂ = x

State before:
case refine'_2
𝕜 : Type u_1
E : Type u_2
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t : Set E
x✝ : E
hs : ∀ x ∈ s, x ∉ (convexHull 𝕜) (s \ {x})
x : E
hxs : x ∈ s
⊢ ∀ ⦃x₁ : E⦄, x₁ ∈ (convexHull 𝕜) s → ∀ ⦃x₂ : E⦄, x₂ ∈ (convexHull 𝕜) s → x ∈ openSegment 𝕜 x₁ x₂ → x₁ = x ∧ x₂ = x
Tactic:
by_contra! h
State after:
case refine'_2
𝕜 : Type u_1
E : Type u_2
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t : Set E
x✝ : E
hs : ∀ x ∈ s, x ∉ (convexHull 𝕜) (s \ {x})
x : E
hxs : x ∈ s
h : ∃ x₁ ∈ (convexHull 𝕜) s, ∃ x₂ ∈ (convexHull 𝕜) s, x ∈ openSegment 𝕜 x₁ x₂ ∧ (x₁ = x → x₂ ≠ x)
⊢ False

State before:
case refine'_2
𝕜 : Type u_1
E : Type u_2
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t : Set E
x✝ : E
hs : ∀ x ∈ s, x ∉ (convexHull 𝕜) (s \ {x})
x : E
hxs : x ∈ s
h : ∃ x₁ ∈ (convexHull 𝕜) s, ∃ x₂ ∈ (convexHull 𝕜) s, x ∈ openSegment 𝕜 x₁ x₂ ∧ (x₁ = x → x₂ ≠ x)
⊢ False
Tactic:
obtain ⟨x₁, hx₁, x₂, hx₂, hx⟩ := h
State after:
case refine'_2.intro.intro.intro.intro
𝕜 : Type u_1
E : Type u_2
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t : Set E
x✝ : E
hs : ∀ x ∈ s, x ∉ (convexHull 𝕜) (s \ {x})
x : E
hxs : x ∈ s
x₁ : E
hx₁ : x₁ ∈ (convexHull 𝕜) s
x₂ : E
hx₂ : x₂ ∈ (convexHull 𝕜) s
hx : x ∈ openSegment 𝕜 x₁ x₂ ∧ (x₁ = x → x₂ ≠ x)
⊢ False

State before:
case refine'_2.intro.intro.intro.intro
𝕜 : Type u_1
E : Type u_2
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t : Set E
x✝ : E
hs : ∀ x ∈ s, x ∉ (convexHull 𝕜) (s \ {x})
x : E
hxs : x ∈ s
x₁ : E
hx₁ : x₁ ∈ (convexHull 𝕜) s
x₂ : E
hx₂ : x₂ ∈ (convexHull 𝕜) s
hx : x ∈ openSegment 𝕜 x₁ x₂ ∧ (x₁ = x → x₂ ≠ x)
⊢ False
Tactic:
suffices h : x₁ ∈ convexHull 𝕜 (s \ {x}) ∧ x₂ ∈ convexHull 𝕜 (s \ {x}) by
  exact hs _ hxs (convex_iff_openSegment_subset.1 (convex_convexHull 𝕜 _) h.1 h.2 hx.1)
State after:
case refine'_2.intro.intro.intro.intro
𝕜 : Type u_1
E : Type u_2
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t : Set E
x✝ : E
hs : ∀ x ∈ s, x ∉ (convexHull 𝕜) (s \ {x})
x : E
hxs : x ∈ s
x₁ : E
hx₁ : x₁ ∈ (convexHull 𝕜) s
x₂ : E
hx₂ : x₂ ∈ (convexHull 𝕜) s
hx : x ∈ openSegment 𝕜 x₁ x₂ ∧ (x₁ = x → x₂ ≠ x)
⊢ x₁ ∈ (convexHull 𝕜) (s \ {x}) ∧ x₂ ∈ (convexHull 𝕜) (s \ {x})

State before:
case refine'_2.intro.intro.intro.intro
𝕜 : Type u_1
E : Type u_2
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t : Set E
x✝ : E
hs : ∀ x ∈ s, x ∉ (convexHull 𝕜) (s \ {x})
x : E
hxs : x ∈ s
x₁ : E
hx₁ : x₁ ∈ (convexHull 𝕜) s
x₂ : E
hx₂ : x₂ ∈ (convexHull 𝕜) s
hx : x ∈ openSegment 𝕜 x₁ x₂ ∧ (x₁ = x → x₂ ≠ x)
⊢ x₁ ∈ (convexHull 𝕜) (s \ {x}) ∧ x₂ ∈ (convexHull 𝕜) (s \ {x})
Tactic:
have hx₁₂ : segment 𝕜 x₁ x₂ ⊆ convexHull 𝕜 s := (convex_convexHull 𝕜 _).segment_subset hx₁ hx₂
State after:
case refine'_2.intro.intro.intro.intro
𝕜 : Type u_1
E : Type u_2
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t : Set E
x✝ : E
hs : ∀ x ∈ s, x ∉ (convexHull 𝕜) (s \ {x})
x : E
hxs : x ∈ s
x₁ : E
hx₁ : x₁ ∈ (convexHull 𝕜) s
x₂ : E
hx₂ : x₂ ∈ (convexHull 𝕜) s
hx : x ∈ openSegment 𝕜 x₁ x₂ ∧ (x₁ = x → x₂ ≠ x)
hx₁₂ : segment 𝕜 x₁ x₂ ⊆ (convexHull 𝕜) s
⊢ x₁ ∈ (convexHull 𝕜) (s \ {x}) ∧ x₂ ∈ (convexHull 𝕜) (s \ {x})

State before:
case refine'_2.intro.intro.intro.intro
𝕜 : Type u_1
E : Type u_2
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t : Set E
x✝ : E
hs : ∀ x ∈ s, x ∉ (convexHull 𝕜) (s \ {x})
x : E
hxs : x ∈ s
x₁ : E
hx₁ : x₁ ∈ (convexHull 𝕜) s
x₂ : E
hx₂ : x₂ ∈ (convexHull 𝕜) s
hx : x ∈ openSegment 𝕜 x₁ x₂ ∧ (x₁ = x → x₂ ≠ x)
hx₁₂ : segment 𝕜 x₁ x₂ ⊆ (convexHull 𝕜) s
⊢ x₁ ∈ (convexHull 𝕜) (s \ {x}) ∧ x₂ ∈ (convexHull 𝕜) (s \ {x})
Tactic:
sorry
State after:
no goals

State before:
case refine'_1
𝕜 : Type u_1
E : Type u_2
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t : Set E
x : E
h : extremePoints 𝕜 ((convexHull 𝕜) s) = s
⊢ ConvexIndependent 𝕜 fun p => ↑p
Tactic:
exact (convex_convexHull 𝕜 _).convexIndependent_extremePoints
State after:
no goals

State before:
𝕜 : Type u_1
E : Type u_2
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t : Set E
x✝ : E
hs : ∀ x ∈ s, x ∉ (convexHull 𝕜) (s \ {x})
x : E
hxs : x ∈ s
x₁ : E
hx₁ : x₁ ∈ (convexHull 𝕜) s
x₂ : E
hx₂ : x₂ ∈ (convexHull 𝕜) s
hx : x ∈ openSegment 𝕜 x₁ x₂ ∧ (x₁ = x → x₂ ≠ x)
h : x₁ ∈ (convexHull 𝕜) (s \ {x}) ∧ x₂ ∈ (convexHull 𝕜) (s \ {x})
⊢ False
Tactic:
exact hs _ hxs (convex_iff_openSegment_subset.1 (convex_convexHull 𝕜 _) h.1 h.2 hx.1)
State after:
no goals