Theorem: Convex.isExtreme_iff_openSegment_subset_diff (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
hAconv : Convex 𝕜 s
⊢ IsExtreme 𝕜 s t ↔ t ⊆ s ∧ ∀ ⦃x y : E⦄, x ∈ s → y ∈ s \ t → openSegment 𝕜 x y ⊆ s \ t
Tactic:
refine' ⟨fun h => ⟨h.1, fun x y hx hy z hz =>
  ⟨hAconv.openSegment_subset hx hy.1 hz, fun hzB => hy.2 (h.2 hx hy.1 hzB hz).2⟩⟩,
    fun h => ⟨h.1, fun x hx y hy z hzB hz => ⟨_, _⟩⟩⟩
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
hAconv : Convex 𝕜 s
h : t ⊆ s ∧ ∀ ⦃x y : E⦄, x ∈ s → y ∈ s \ t → openSegment 𝕜 x y ⊆ s \ t
x : E
hx : x ∈ s
y : E
hy : y ∈ s
z : E
hzB : z ∈ t
hz : z ∈ openSegment 𝕜 x y
⊢ x ∈ t

case refine'_2
𝕜 : Type u_1
E : Type u_2
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t : Set E
x✝ : E
hAconv : Convex 𝕜 s
h : t ⊆ s ∧ ∀ ⦃x y : E⦄, x ∈ s → y ∈ s \ t → openSegment 𝕜 x y ⊆ s \ t
x : E
hx : x ∈ s
y : E
hy : y ∈ s
z : E
hzB : z ∈ t
hz : z ∈ openSegment 𝕜 x y
⊢ y ∈ t

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
hAconv : Convex 𝕜 s
h : t ⊆ s ∧ ∀ ⦃x y : E⦄, x ∈ s → y ∈ s \ t → openSegment 𝕜 x y ⊆ s \ t
x : E
hx : x ∈ s
y : E
hy : y ∈ s
z : E
hzB : z ∈ t
hz : z ∈ openSegment 𝕜 x y
⊢ x ∈ t
Tactic:
by_contra hxB
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
hAconv : Convex 𝕜 s
h : t ⊆ s ∧ ∀ ⦃x y : E⦄, x ∈ s → y ∈ s \ t → openSegment 𝕜 x y ⊆ s \ t
x : E
hx : x ∈ s
y : E
hy : y ∈ s
z : E
hzB : z ∈ t
hz : z ∈ openSegment 𝕜 x y
hxB : x ∉ t
⊢ False

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
hAconv : Convex 𝕜 s
h : t ⊆ s ∧ ∀ ⦃x y : E⦄, x ∈ s → y ∈ s \ t → openSegment 𝕜 x y ⊆ s \ t
x : E
hx : x ∈ s
y : E
hy : y ∈ s
z : E
hzB : z ∈ t
hz : z ∈ openSegment 𝕜 x y
hxB : x ∉ t
⊢ False
Tactic:
rw [openSegment_symm] at hz
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
hAconv : Convex 𝕜 s
h : t ⊆ s ∧ ∀ ⦃x y : E⦄, x ∈ s → y ∈ s \ t → openSegment 𝕜 x y ⊆ s \ t
x : E
hx : x ∈ s
y : E
hy : y ∈ s
z : E
hzB : z ∈ t
hz : z ∈ openSegment 𝕜 y x
hxB : x ∉ t
⊢ False

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
hAconv : Convex 𝕜 s
h : t ⊆ s ∧ ∀ ⦃x y : E⦄, x ∈ s → y ∈ s \ t → openSegment 𝕜 x y ⊆ s \ t
x : E
hx : x ∈ s
y : E
hy : y ∈ s
z : E
hzB : z ∈ t
hz : z ∈ openSegment 𝕜 y x
hxB : x ∉ t
⊢ False
Tactic:
exact (h.2 hy ⟨hx, hxB⟩ hz).2 hzB
State after:
no goals

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
hAconv : Convex 𝕜 s
h : t ⊆ s ∧ ∀ ⦃x y : E⦄, x ∈ s → y ∈ s \ t → openSegment 𝕜 x y ⊆ s \ t
x : E
hx : x ∈ s
y : E
hy : y ∈ s
z : E
hzB : z ∈ t
hz : z ∈ openSegment 𝕜 x y
⊢ y ∈ t
Tactic:
by_contra hyB
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
hAconv : Convex 𝕜 s
h : t ⊆ s ∧ ∀ ⦃x y : E⦄, x ∈ s → y ∈ s \ t → openSegment 𝕜 x y ⊆ s \ t
x : E
hx : x ∈ s
y : E
hy : y ∈ s
z : E
hzB : z ∈ t
hz : z ∈ openSegment 𝕜 x y
hyB : y ∉ t
⊢ 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
hAconv : Convex 𝕜 s
h : t ⊆ s ∧ ∀ ⦃x y : E⦄, x ∈ s → y ∈ s \ t → openSegment 𝕜 x y ⊆ s \ t
x : E
hx : x ∈ s
y : E
hy : y ∈ s
z : E
hzB : z ∈ t
hz : z ∈ openSegment 𝕜 x y
hyB : y ∉ t
⊢ False
Tactic:
exact (h.2 hx ⟨hy, hyB⟩ hz).2 hzB
State after:
no goals