no goals
𝕜 : Type u_1
E : Type u_2
F : Type ?u.51012
ι : Type ?u.51015
π : ι → Type ?u.51020
inst✝⁴ : LinearOrderedRing 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : DenselyOrdered 𝕜
inst✝ : NoZeroSMulDivisors 𝕜 E
A B : Set E
x : E
hA : Convex 𝕜 A
⊢ x ∈ extremePoints 𝕜 A ↔ x ∈ A \ ↑(convexHull 𝕜).toOrderHom (A \ {x})
rw [hA.mem_extremePoints_iff_convex_diff, hA.convex_remove_iff_not_mem_convexHull_remove,
  mem_diff]