-- Mathlib/Analysis/Convex/Extreme.lean
theorem mem_extremePoints_iff_forall_segment : x ∈ A.extremePoints 𝕜 ↔
    x ∈ A ∧ ∀ᵉ (x₁ ∈ A) (x₂ ∈ A), x ∈ segment 𝕜 x₁ x₂ → x₁ = x ∨ x₂ = x

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : LinearOrderedRing 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : DenselyOrdered 𝕜
inst✝ : NoZeroSMulDivisors 𝕜 E
A : 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

Tactic:
constructor

Result:
case mp
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : LinearOrderedRing 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : DenselyOrdered 𝕜
inst✝ : NoZeroSMulDivisors 𝕜 E
A : 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_1
E : Type u_2
inst✝⁴ : LinearOrderedRing 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : DenselyOrdered 𝕜
inst✝ : NoZeroSMulDivisors 𝕜 E
A : 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

Proof state:
case mp
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : LinearOrderedRing 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : DenselyOrdered 𝕜
inst✝ : NoZeroSMulDivisors 𝕜 E
A : 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

Tactic:
rintro H (rfl | rfl | hx)

Result:
case mp.inl
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : LinearOrderedRing 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : DenselyOrdered 𝕜
inst✝ : NoZeroSMulDivisors 𝕜 E
A : 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_1
E : Type u_2
inst✝⁴ : LinearOrderedRing 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : DenselyOrdered 𝕜
inst✝ : NoZeroSMulDivisors 𝕜 E
A : 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_1
E : Type u_2
inst✝⁴ : LinearOrderedRing 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : DenselyOrdered 𝕜
inst✝ : NoZeroSMulDivisors 𝕜 E
A : 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

Proof state:
case mpr
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : LinearOrderedRing 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : DenselyOrdered 𝕜
inst✝ : NoZeroSMulDivisors 𝕜 E
A : 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

Tactic:
rcases H (openSegment_subset_segment _ _ _ hx) with (rfl | rfl)

Result:
case mpr.inl
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : LinearOrderedRing 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : DenselyOrdered 𝕜
inst✝ : NoZeroSMulDivisors 𝕜 E
A : 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_1
E : Type u_2
inst✝⁴ : LinearOrderedRing 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : DenselyOrdered 𝕜
inst✝ : NoZeroSMulDivisors 𝕜 E
A : 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₂

Proof state:
case mpr.inl
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : LinearOrderedRing 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : DenselyOrdered 𝕜
inst✝ : NoZeroSMulDivisors 𝕜 E
A : 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_1
E : Type u_2
inst✝⁴ : LinearOrderedRing 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : DenselyOrdered 𝕜
inst✝ : NoZeroSMulDivisors 𝕜 E
A : 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₂

Tactic:
exacts [⟨rfl, (left_mem_openSegment_iff.1 hx).symm⟩, ⟨right_mem_openSegment_iff.1 hx, rfl⟩]

Result:
no goals

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : LinearOrderedRing 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : DenselyOrdered 𝕜
inst✝ : NoZeroSMulDivisors 𝕜 E
A : Set E
x : E
⊢ x ∈ extremePoints 𝕜 A ↔ x ∈ A ∧ ∀ x₁ ∈ A, ∀ x₂ ∈ A, x ∈ segment 𝕜 x₁ x₂ → x₁ = x ∨ x₂ = x

Tactic:
refine and_congr_right fun hxA ↦ forall₄_congr fun x₁ h₁ x₂ h₂ ↦ ?_

Result:
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : LinearOrderedRing 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : DenselyOrdered 𝕜
inst✝ : NoZeroSMulDivisors 𝕜 E
A : 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

Proof state:
case mp
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : LinearOrderedRing 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : DenselyOrdered 𝕜
inst✝ : NoZeroSMulDivisors 𝕜 E
A : 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

Tactic:
rw [← insert_endpoints_openSegment]

Result:
case mp
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : LinearOrderedRing 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : DenselyOrdered 𝕜
inst✝ : NoZeroSMulDivisors 𝕜 E
A : 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

Proof state:
case mpr
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : LinearOrderedRing 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : DenselyOrdered 𝕜
inst✝ : NoZeroSMulDivisors 𝕜 E
A : 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

Tactic:
intro H hx

Result:
case mpr
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : LinearOrderedRing 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : DenselyOrdered 𝕜
inst✝ : NoZeroSMulDivisors 𝕜 E
A : 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

Proof state:
case mp.inl
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : LinearOrderedRing 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : DenselyOrdered 𝕜
inst✝ : NoZeroSMulDivisors 𝕜 E
A : 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_1
E : Type u_2
inst✝⁴ : LinearOrderedRing 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : DenselyOrdered 𝕜
inst✝ : NoZeroSMulDivisors 𝕜 E
A : 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_1
E : Type u_2
inst✝⁴ : LinearOrderedRing 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : DenselyOrdered 𝕜
inst✝ : NoZeroSMulDivisors 𝕜 E
A : 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

Tactic:
exacts [Or.inl rfl, Or.inr rfl, Or.inl <| (H hx).1]

Result:
no goals