-- Mathlib/Analysis/Convex/StoneSeparation.lean
theorem exists_convex_convex_compl_subset (hs : Convex 𝕜 s) (ht : Convex 𝕜 t) (hst : Disjoint s t) :
    ∃ C : Set E, Convex 𝕜 C ∧ Convex 𝕜 Cᶜ ∧ s ⊆ C ∧ t ⊆ Cᶜ

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t : Set E
hs : Convex 𝕜 s
ht : Convex 𝕜 t
hst : Disjoint s t
S : Set (Set E) := {C | Convex 𝕜 C ∧ Disjoint C t}
⊢ ∃ C, Convex 𝕜 C ∧ Convex 𝕜 Cᶜ ∧ s ⊆ C ∧ t ⊆ Cᶜ

Tactic:
obtain ⟨C, hsC, hmax⟩ :=
  zorn_subset_nonempty S
    (fun c hcS hc ⟨_, _⟩ =>
      ⟨⋃₀ c,
        ⟨hc.directedOn.convex_sUnion fun s hs => (hcS hs).1,
          disjoint_sUnion_left.2 fun c hc => (hcS hc).2⟩,
        fun s => subset_sUnion_of_mem⟩)
    s ⟨hs, hst⟩

Result:
case intro.intro
𝕜 : Type u_1
E : Type u_2
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t : Set E
hs : Convex 𝕜 s
ht : Convex 𝕜 t
hst : Disjoint s t
S : Set (Set E) := {C | Convex 𝕜 C ∧ Disjoint C t}
C : Set E
hsC : s ⊆ C
hmax : Maximal (fun x => x ∈ S) C
⊢ ∃ C, Convex 𝕜 C ∧ Convex 𝕜 Cᶜ ∧ s ⊆ C ∧ t ⊆ Cᶜ

Proof state:
case intro.intro.intro.intro.intro.intro.intro.intro
𝕜 : Type u_1
E : Type u_2
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t : Set E
hs : Convex 𝕜 s
ht : Convex 𝕜 t
hst : Disjoint s t
S : Set (Set E) := {C | Convex 𝕜 C ∧ Disjoint C t}
C : Set E
hsC : s ⊆ C
hmax : Maximal (fun x => x ∈ S) C
hC : Convex 𝕜 C ∧ Disjoint C t
x : E
hx : x ∈ Cᶜ
y : E
hy : y ∈ Cᶜ
z : E
hz : z ∈ segment 𝕜 x y
hzC : z ∈ C
h : ∀ c ∈ Cᶜ, ∃ a ∈ C, (segment 𝕜 c a ∩ t).Nonempty
p : E
hp : p ∈ C
u : E
hu : u ∈ segment 𝕜 x p
hut : u ∈ t
q : E
hq : q ∈ C
v : E
hv : v ∈ segment 𝕜 y q
hvt : v ∈ t
⊢ False

Tactic:
refine
  not_disjoint_segment_convexHull_triple hz hu hv
    (hC.2.symm.mono (ht.segment_subset hut hvt) <| convexHull_min ?_ hC.1)

Result:
case intro.intro.intro.intro.intro.intro.intro.intro
𝕜 : Type u_1
E : Type u_2
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t : Set E
hs : Convex 𝕜 s
ht : Convex 𝕜 t
hst : Disjoint s t
S : Set (Set E) := {C | Convex 𝕜 C ∧ Disjoint C t}
C : Set E
hsC : s ⊆ C
hmax : Maximal (fun x => x ∈ S) C
hC : Convex 𝕜 C ∧ Disjoint C t
x : E
hx : x ∈ Cᶜ
y : E
hy : y ∈ Cᶜ
z : E
hz : z ∈ segment 𝕜 x y
hzC : z ∈ C
h : ∀ c ∈ Cᶜ, ∃ a ∈ C, (segment 𝕜 c a ∩ t).Nonempty
p : E
hp : p ∈ C
u : E
hu : u ∈ segment 𝕜 x p
hut : u ∈ t
q : E
hq : q ∈ C
v : E
hv : v ∈ segment 𝕜 y q
hvt : v ∈ t
⊢ {p, q, z} ⊆ C

Proof state:
case intro.intro
𝕜 : Type u_1
E : Type u_2
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t : Set E
hs : Convex 𝕜 s
ht : Convex 𝕜 t
hst : Disjoint s t
S : Set (Set E) := {C | Convex 𝕜 C ∧ Disjoint C t}
C : Set E
hsC : s ⊆ C
hmax : Maximal (fun x => x ∈ S) C
hC : Convex 𝕜 C ∧ Disjoint C t
x : E
hx : x ∈ Cᶜ
y : E
hy : y ∈ Cᶜ
z : E
hz : z ∈ segment 𝕜 x y
hzC : z ∈ C
⊢ False

Tactic:
suffices h : ∀ c ∈ Cᶜ, ∃ a ∈ C, (segment 𝕜 c a ∩ t).Nonempty by
  obtain ⟨p, hp, u, hu, hut⟩ := h x hx
  obtain ⟨q, hq, v, hv, hvt⟩ := h y hy
  refine
    not_disjoint_segment_convexHull_triple hz hu hv
      (hC.2.symm.mono (ht.segment_subset hut hvt) <| convexHull_min ?_ hC.1)
  simp [insert_subset_iff, hp, hq, singleton_subset_iff.2 hzC]

Result:
case intro.intro
𝕜 : Type u_1
E : Type u_2
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t : Set E
hs : Convex 𝕜 s
ht : Convex 𝕜 t
hst : Disjoint s t
S : Set (Set E) := {C | Convex 𝕜 C ∧ Disjoint C t}
C : Set E
hsC : s ⊆ C
hmax : Maximal (fun x => x ∈ S) C
hC : Convex 𝕜 C ∧ Disjoint C t
x : E
hx : x ∈ Cᶜ
y : E
hy : y ∈ Cᶜ
z : E
hz : z ∈ segment 𝕜 x y
hzC : z ∈ C
⊢ ∀ c ∈ Cᶜ, ∃ a ∈ C, (segment 𝕜 c a ∩ t).Nonempty

Proof state:
case intro.intro.intro.intro
𝕜 : Type u_1
E : Type u_2
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t : Set E
hs : Convex 𝕜 s
ht : Convex 𝕜 t
hst : Disjoint s t
S : Set (Set E) := {C | Convex 𝕜 C ∧ Disjoint C t}
C : Set E
hsC : s ⊆ C
hmax : Maximal (fun x => x ∈ S) C
hC : Convex 𝕜 C ∧ Disjoint C t
x : E
hx : x ∈ Cᶜ
y : E
hy : y ∈ Cᶜ
z : E
hz : z ∈ segment 𝕜 x y
hzC : z ∈ C
h : ∀ c ∈ Cᶜ, ∃ a ∈ C, (segment 𝕜 c a ∩ t).Nonempty
p : E
hp : p ∈ C
u : E
hu : u ∈ segment 𝕜 x p
hut : u ∈ t
⊢ False

Tactic:
obtain ⟨q, hq, v, hv, hvt⟩ := h y hy

Result:
case intro.intro.intro.intro.intro.intro.intro.intro
𝕜 : Type u_1
E : Type u_2
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t : Set E
hs : Convex 𝕜 s
ht : Convex 𝕜 t
hst : Disjoint s t
S : Set (Set E) := {C | Convex 𝕜 C ∧ Disjoint C t}
C : Set E
hsC : s ⊆ C
hmax : Maximal (fun x => x ∈ S) C
hC : Convex 𝕜 C ∧ Disjoint C t
x : E
hx : x ∈ Cᶜ
y : E
hy : y ∈ Cᶜ
z : E
hz : z ∈ segment 𝕜 x y
hzC : z ∈ C
h : ∀ c ∈ Cᶜ, ∃ a ∈ C, (segment 𝕜 c a ∩ t).Nonempty
p : E
hp : p ∈ C
u : E
hu : u ∈ segment 𝕜 x p
hut : u ∈ t
q : E
hq : q ∈ C
v : E
hv : v ∈ segment 𝕜 y q
hvt : v ∈ t
⊢ False

Proof state:
case intro.intro
𝕜 : Type u_1
E : Type u_2
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t : Set E
hs : Convex 𝕜 s
ht : Convex 𝕜 t
hst : Disjoint s t
S : Set (Set E) := {C | Convex 𝕜 C ∧ Disjoint C t}
C : Set E
hsC : s ⊆ C
hmax : Maximal (fun x => x ∈ S) C
⊢ ∃ C, Convex 𝕜 C ∧ Convex 𝕜 Cᶜ ∧ s ⊆ C ∧ t ⊆ Cᶜ

Tactic:
obtain hC : _ ∧ _ := hmax.prop

Result:
case intro.intro
𝕜 : Type u_1
E : Type u_2
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t : Set E
hs : Convex 𝕜 s
ht : Convex 𝕜 t
hst : Disjoint s t
S : Set (Set E) := {C | Convex 𝕜 C ∧ Disjoint C t}
C : Set E
hsC : s ⊆ C
hmax : Maximal (fun x => x ∈ S) C
hC : Convex 𝕜 C ∧ Disjoint C t
⊢ ∃ C, Convex 𝕜 C ∧ Convex 𝕜 Cᶜ ∧ s ⊆ C ∧ t ⊆ Cᶜ

Proof state:
case intro.intro
𝕜 : Type u_1
E : Type u_2
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t : Set E
hs : Convex 𝕜 s
ht : Convex 𝕜 t
hst : Disjoint s t
S : Set (Set E) := {C | Convex 𝕜 C ∧ Disjoint C t}
C : Set E
hsC : s ⊆ C
hmax : Maximal (fun x => x ∈ S) C
hC : Convex 𝕜 C ∧ Disjoint C t
x : E
hx : x ∈ Cᶜ
y : E
hy : y ∈ Cᶜ
z : E
hz : z ∈ segment 𝕜 x y
hzC : z ∈ C
c : E
hc : c ∈ Cᶜ
h : ∀ a ∈ C, segment 𝕜 c a ∩ t = ∅
⊢ Disjoint ((convexHull 𝕜) (insert c C)) t

Tactic:
rw [convexHull_insert ⟨z, hzC⟩, convexJoin_singleton_left]

Result:
case intro.intro
𝕜 : Type u_1
E : Type u_2
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t : Set E
hs : Convex 𝕜 s
ht : Convex 𝕜 t
hst : Disjoint s t
S : Set (Set E) := {C | Convex 𝕜 C ∧ Disjoint C t}
C : Set E
hsC : s ⊆ C
hmax : Maximal (fun x => x ∈ S) C
hC : Convex 𝕜 C ∧ Disjoint C t
x : E
hx : x ∈ Cᶜ
y : E
hy : y ∈ Cᶜ
z : E
hz : z ∈ segment 𝕜 x y
hzC : z ∈ C
c : E
hc : c ∈ Cᶜ
h : ∀ a ∈ C, segment 𝕜 c a ∩ t = ∅
⊢ Disjoint (⋃ y ∈ (convexHull 𝕜) C, segment 𝕜 c y) t

Proof state:
case intro.intro
𝕜 : Type u_1
E : Type u_2
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t : Set E
hs : Convex 𝕜 s
ht : Convex 𝕜 t
hst : Disjoint s t
S : Set (Set E) := {C | Convex 𝕜 C ∧ Disjoint C t}
C : Set E
hsC : s ⊆ C
hmax : Maximal (fun x => x ∈ S) C
hC : Convex 𝕜 C ∧ Disjoint C t
x : E
hx : x ∈ Cᶜ
y : E
hy : y ∈ Cᶜ
z : E
hz : z ∈ segment 𝕜 x y
hzC : z ∈ C
c : E
hc : c ∈ Cᶜ
⊢ ∃ a ∈ C, (segment 𝕜 c a ∩ t).Nonempty

Tactic:
by_contra! h

Result:
case intro.intro
𝕜 : Type u_1
E : Type u_2
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t : Set E
hs : Convex 𝕜 s
ht : Convex 𝕜 t
hst : Disjoint s t
S : Set (Set E) := {C | Convex 𝕜 C ∧ Disjoint C t}
C : Set E
hsC : s ⊆ C
hmax : Maximal (fun x => x ∈ S) C
hC : Convex 𝕜 C ∧ Disjoint C t
x : E
hx : x ∈ Cᶜ
y : E
hy : y ∈ Cᶜ
z : E
hz : z ∈ segment 𝕜 x y
hzC : z ∈ C
c : E
hc : c ∈ Cᶜ
h : ∀ a ∈ C, segment 𝕜 c a ∩ t = ∅
⊢ False