𝕜 : Type u_2
E : Type u_1
F : Type ?u.39769
ι : Type ?u.39772
π : ι → Type ?u.39777
inst✝⁴ : LinearOrderedRing 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : DenselyOrdered 𝕜
inst✝ : NoZeroSMulDivisors 𝕜 E
A B : Set E
x : E
hxA : x ∈ A
x₁ : E
h₁ : x₁ ∈ A
x₂ : E
h₂ : x₂ ∈ A
⊢ x ∈ openSegment 𝕜 x₁ x₂ → x₁ = x ∧ x₂ = x ↔ x ∈ segment 𝕜 x₁ x₂ → x₁ = x ∨ x₂ = x
𝕜 : Type u_2
E : Type u_1
F : Type ?u.39769
ι : Type ?u.39772
π : ι → Type ?u.39777
inst✝⁴ : LinearOrderedRing 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : DenselyOrdered 𝕜
inst✝ : NoZeroSMulDivisors 𝕜 E
A B : Set E
x : E
⊢ x ∈ extremePoints 𝕜 A ↔ x ∈ A ∧ ∀ (x₁ : E), x₁ ∈ A → ∀ (x₂ : E), x₂ ∈ A → x ∈ segment 𝕜 x₁ x₂ → x₁ = x ∨ x₂ = x
refine' and_congr_right fun hxA ↦ forall₄_congr fun x₁ h₁ x₂ h₂ ↦ _
case mp
𝕜 : Type u_2
E : Type u_1
F : Type ?u.39769
ι : Type ?u.39772
π : ι → Type ?u.39777
inst✝⁴ : LinearOrderedRing 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : DenselyOrdered 𝕜
inst✝ : NoZeroSMulDivisors 𝕜 E
A B : Set E
x : E
hxA : x ∈ A
x₁ : E
h₁ : x₁ ∈ A
x₂ : E
h₂ : x₂ ∈ A
⊢ (x ∈ openSegment 𝕜 x₁ x₂ → x₁ = x ∧ x₂ = x) → x ∈ segment 𝕜 x₁ x₂ → x₁ = x ∨ x₂ = x

case mpr
𝕜 : Type u_2
E : Type u_1
F : Type ?u.39769
ι : Type ?u.39772
π : ι → Type ?u.39777
inst✝⁴ : LinearOrderedRing 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : DenselyOrdered 𝕜
inst✝ : NoZeroSMulDivisors 𝕜 E
A B : Set E
x : E
hxA : x ∈ A
x₁ : E
h₁ : x₁ ∈ A
x₂ : E
h₂ : x₂ ∈ A
⊢ (x ∈ segment 𝕜 x₁ x₂ → x₁ = x ∨ x₂ = x) → x ∈ openSegment 𝕜 x₁ x₂ → x₁ = x ∧ x₂ = x
𝕜 : Type u_2
E : Type u_1
F : Type ?u.39769
ι : Type ?u.39772
π : ι → Type ?u.39777
inst✝⁴ : LinearOrderedRing 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : DenselyOrdered 𝕜
inst✝ : NoZeroSMulDivisors 𝕜 E
A B : Set E
x : E
hxA : x ∈ A
x₁ : E
h₁ : x₁ ∈ A
x₂ : E
h₂ : x₂ ∈ A
⊢ x ∈ openSegment 𝕜 x₁ x₂ → x₁ = x ∧ x₂ = x ↔ x ∈ segment 𝕜 x₁ x₂ → x₁ = x ∨ x₂ = x
constructor
case mp
𝕜 : Type u_2
E : Type u_1
F : Type ?u.39769
ι : Type ?u.39772
π : ι → Type ?u.39777
inst✝⁴ : LinearOrderedRing 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : DenselyOrdered 𝕜
inst✝ : NoZeroSMulDivisors 𝕜 E
A B : Set E
x : E
hxA : x ∈ A
x₁ : E
h₁ : x₁ ∈ A
x₂ : E
h₂ : x₂ ∈ A
⊢ (x ∈ openSegment 𝕜 x₁ x₂ → x₁ = x ∧ x₂ = x) → x ∈ insert x₁ (insert x₂ (openSegment 𝕜 x₁ x₂)) → x₁ = x ∨ x₂ = x
case mp
𝕜 : Type u_2
E : Type u_1
F : Type ?u.39769
ι : Type ?u.39772
π : ι → Type ?u.39777
inst✝⁴ : LinearOrderedRing 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : DenselyOrdered 𝕜
inst✝ : NoZeroSMulDivisors 𝕜 E
A B : Set E
x : E
hxA : x ∈ A
x₁ : E
h₁ : x₁ ∈ A
x₂ : E
h₂ : x₂ ∈ A
⊢ (x ∈ openSegment 𝕜 x₁ x₂ → x₁ = x ∧ x₂ = x) → x ∈ segment 𝕜 x₁ x₂ → x₁ = x ∨ x₂ = x
rw [← insert_endpoints_openSegment]
case mp.inl
𝕜 : Type u_2
E : Type u_1
F : Type ?u.39769
ι : Type ?u.39772
π : ι → Type ?u.39777
inst✝⁴ : LinearOrderedRing 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : DenselyOrdered 𝕜
inst✝ : NoZeroSMulDivisors 𝕜 E
A B : Set E
x : E
hxA : x ∈ A
x₂ : E
h₂ : x₂ ∈ A
h₁ : x ∈ A
H : x ∈ openSegment 𝕜 x x₂ → x = x ∧ x₂ = x
⊢ x = x ∨ x₂ = x

case mp.inr.inl
𝕜 : Type u_2
E : Type u_1
F : Type ?u.39769
ι : Type ?u.39772
π : ι → Type ?u.39777
inst✝⁴ : LinearOrderedRing 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : DenselyOrdered 𝕜
inst✝ : NoZeroSMulDivisors 𝕜 E
A B : Set E
x : E
hxA : x ∈ A
x₁ : E
h₁ : x₁ ∈ A
h₂ : x ∈ A
H : x ∈ openSegment 𝕜 x₁ x → x₁ = x ∧ x = x
⊢ x₁ = x ∨ x = x

case mp.inr.inr
𝕜 : Type u_2
E : Type u_1
F : Type ?u.39769
ι : Type ?u.39772
π : ι → Type ?u.39777
inst✝⁴ : LinearOrderedRing 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : DenselyOrdered 𝕜
inst✝ : NoZeroSMulDivisors 𝕜 E
A B : Set E
x : E
hxA : x ∈ A
x₁ : E
h₁ : x₁ ∈ A
x₂ : E
h₂ : x₂ ∈ A
H : x ∈ openSegment 𝕜 x₁ x₂ → x₁ = x ∧ x₂ = x
hx : x ∈ openSegment 𝕜 x₁ x₂
⊢ x₁ = x ∨ x₂ = x
case mp
𝕜 : Type u_2
E : Type u_1
F : Type ?u.39769
ι : Type ?u.39772
π : ι → Type ?u.39777
inst✝⁴ : LinearOrderedRing 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : DenselyOrdered 𝕜
inst✝ : NoZeroSMulDivisors 𝕜 E
A B : Set E
x : E
hxA : x ∈ A
x₁ : E
h₁ : x₁ ∈ A
x₂ : E
h₂ : x₂ ∈ A
⊢ (x ∈ openSegment 𝕜 x₁ x₂ → x₁ = x ∧ x₂ = x) → x ∈ insert x₁ (insert x₂ (openSegment 𝕜 x₁ x₂)) → x₁ = x ∨ x₂ = x
rintro H (rfl | rfl | hx)
no goals
case mp.inl
𝕜 : Type u_2
E : Type u_1
F : Type ?u.39769
ι : Type ?u.39772
π : ι → Type ?u.39777
inst✝⁴ : LinearOrderedRing 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : DenselyOrdered 𝕜
inst✝ : NoZeroSMulDivisors 𝕜 E
A B : Set E
x : E
hxA : x ∈ A
x₂ : E
h₂ : x₂ ∈ A
h₁ : x ∈ A
H : x ∈ openSegment 𝕜 x x₂ → x = x ∧ x₂ = x
⊢ x = x ∨ x₂ = x

case mp.inr.inl
𝕜 : Type u_2
E : Type u_1
F : Type ?u.39769
ι : Type ?u.39772
π : ι → Type ?u.39777
inst✝⁴ : LinearOrderedRing 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : DenselyOrdered 𝕜
inst✝ : NoZeroSMulDivisors 𝕜 E
A B : Set E
x : E
hxA : x ∈ A
x₁ : E
h₁ : x₁ ∈ A
h₂ : x ∈ A
H : x ∈ openSegment 𝕜 x₁ x → x₁ = x ∧ x = x
⊢ x₁ = x ∨ x = x

case mp.inr.inr
𝕜 : Type u_2
E : Type u_1
F : Type ?u.39769
ι : Type ?u.39772
π : ι → Type ?u.39777
inst✝⁴ : LinearOrderedRing 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : DenselyOrdered 𝕜
inst✝ : NoZeroSMulDivisors 𝕜 E
A B : Set E
x : E
hxA : x ∈ A
x₁ : E
h₁ : x₁ ∈ A
x₂ : E
h₂ : x₂ ∈ A
H : x ∈ openSegment 𝕜 x₁ x₂ → x₁ = x ∧ x₂ = x
hx : x ∈ openSegment 𝕜 x₁ x₂
⊢ x₁ = x ∨ x₂ = x
exacts [Or.inl rfl, Or.inr rfl, Or.inl <| (H hx).1]
case mpr
𝕜 : Type u_2
E : Type u_1
F : Type ?u.39769
ι : Type ?u.39772
π : ι → Type ?u.39777
inst✝⁴ : LinearOrderedRing 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : DenselyOrdered 𝕜
inst✝ : NoZeroSMulDivisors 𝕜 E
A B : Set E
x : E
hxA : x ∈ A
x₁ : E
h₁ : x₁ ∈ A
x₂ : E
h₂ : x₂ ∈ A
H : x ∈ segment 𝕜 x₁ x₂ → x₁ = x ∨ x₂ = x
hx : x ∈ openSegment 𝕜 x₁ x₂
⊢ x₁ = x ∧ x₂ = x
case mpr
𝕜 : Type u_2
E : Type u_1
F : Type ?u.39769
ι : Type ?u.39772
π : ι → Type ?u.39777
inst✝⁴ : LinearOrderedRing 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : DenselyOrdered 𝕜
inst✝ : NoZeroSMulDivisors 𝕜 E
A B : Set E
x : E
hxA : x ∈ A
x₁ : E
h₁ : x₁ ∈ A
x₂ : E
h₂ : x₂ ∈ A
⊢ (x ∈ segment 𝕜 x₁ x₂ → x₁ = x ∨ x₂ = x) → x ∈ openSegment 𝕜 x₁ x₂ → x₁ = x ∧ x₂ = x
intro H hx
case mpr.inl
𝕜 : Type u_2
E : Type u_1
F : Type ?u.39769
ι : Type ?u.39772
π : ι → Type ?u.39777
inst✝⁴ : LinearOrderedRing 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : DenselyOrdered 𝕜
inst✝ : NoZeroSMulDivisors 𝕜 E
A B : Set E
x₁ : E
h₁ : x₁ ∈ A
x₂ : E
h₂ : x₂ ∈ A
hxA : x₁ ∈ A
H : x₁ ∈ segment 𝕜 x₁ x₂ → x₁ = x₁ ∨ x₂ = x₁
hx : x₁ ∈ openSegment 𝕜 x₁ x₂
⊢ x₁ = x₁ ∧ x₂ = x₁

case mpr.inr
𝕜 : Type u_2
E : Type u_1
F : Type ?u.39769
ι : Type ?u.39772
π : ι → Type ?u.39777
inst✝⁴ : LinearOrderedRing 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : DenselyOrdered 𝕜
inst✝ : NoZeroSMulDivisors 𝕜 E
A B : Set E
x₁ : E
h₁ : x₁ ∈ A
x₂ : E
h₂ hxA : x₂ ∈ A
H : x₂ ∈ segment 𝕜 x₁ x₂ → x₁ = x₂ ∨ x₂ = x₂
hx : x₂ ∈ openSegment 𝕜 x₁ x₂
⊢ x₁ = x₂ ∧ x₂ = x₂
case mpr
𝕜 : Type u_2
E : Type u_1
F : Type ?u.39769
ι : Type ?u.39772
π : ι → Type ?u.39777
inst✝⁴ : LinearOrderedRing 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : DenselyOrdered 𝕜
inst✝ : NoZeroSMulDivisors 𝕜 E
A B : Set E
x : E
hxA : x ∈ A
x₁ : E
h₁ : x₁ ∈ A
x₂ : E
h₂ : x₂ ∈ A
H : x ∈ segment 𝕜 x₁ x₂ → x₁ = x ∨ x₂ = x
hx : x ∈ openSegment 𝕜 x₁ x₂
⊢ x₁ = x ∧ x₂ = x
rcases H (openSegment_subset_segment _ _ _ hx) with (rfl | rfl)
no goals
case mpr.inl
𝕜 : Type u_2
E : Type u_1
F : Type ?u.39769
ι : Type ?u.39772
π : ι → Type ?u.39777
inst✝⁴ : LinearOrderedRing 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : DenselyOrdered 𝕜
inst✝ : NoZeroSMulDivisors 𝕜 E
A B : Set E
x₁ : E
h₁ : x₁ ∈ A
x₂ : E
h₂ : x₂ ∈ A
hxA : x₁ ∈ A
H : x₁ ∈ segment 𝕜 x₁ x₂ → x₁ = x₁ ∨ x₂ = x₁
hx : x₁ ∈ openSegment 𝕜 x₁ x₂
⊢ x₁ = x₁ ∧ x₂ = x₁

case mpr.inr
𝕜 : Type u_2
E : Type u_1
F : Type ?u.39769
ι : Type ?u.39772
π : ι → Type ?u.39777
inst✝⁴ : LinearOrderedRing 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : DenselyOrdered 𝕜
inst✝ : NoZeroSMulDivisors 𝕜 E
A B : Set E
x₁ : E
h₁ : x₁ ∈ A
x₂ : E
h₂ hxA : x₂ ∈ A
H : x₂ ∈ segment 𝕜 x₁ x₂ → x₁ = x₂ ∨ x₂ = x₂
hx : x₂ ∈ openSegment 𝕜 x₁ x₂
⊢ x₁ = x₂ ∧ x₂ = x₂
exacts [⟨rfl, (left_mem_openSegment_iff.1 hx).symm⟩, ⟨right_mem_openSegment_iff.1 hx, rfl⟩]