𝕜 : Type u_1
E : Type u_2
ι : Type ?u.47333
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ᶜ
𝕜 : Type u_1
E : Type u_2
ι : Type ?u.47333
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t : Set E
hs : Convex 𝕜 s
ht : Convex 𝕜 t
hst : Disjoint s t
⊢ ∃ C, Convex 𝕜 C ∧ Convex 𝕜 (Cᶜ) ∧ s ⊆ C ∧ t ⊆ Cᶜ
let S : Set (Set E) := { C | Convex 𝕜 C ∧ Disjoint C t }
case intro.intro.intro
𝕜 : Type u_1
E : Type u_2
ι : Type ?u.47333
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
hC : C ∈ S
hsC : s ⊆ C
hCmax : ∀ (a : Set E), a ∈ S → C ⊆ a → a = C
⊢ ∃ C, Convex 𝕜 C ∧ Convex 𝕜 (Cᶜ) ∧ s ⊆ C ∧ t ⊆ Cᶜ
𝕜 : Type u_1
E : Type u_2
ι : Type ?u.47333
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ᶜ
obtain ⟨C, hC, hsC, hCmax⟩ :=
  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⟩
case intro.intro.intro
𝕜 : Type u_1
E : Type u_2
ι : Type ?u.47333
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
hC : C ∈ S
hsC : s ⊆ C
hCmax : ∀ (a : Set E), a ∈ S → C ⊆ a → a = C
x : E
hx : x ∈ Cᶜ
y : E
hy : y ∈ Cᶜ
z : E
hz : z ∈ segment 𝕜 x y
hzC : z ∈ C
⊢ False
case intro.intro.intro
𝕜 : Type u_1
E : Type u_2
ι : Type ?u.47333
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
hC : C ∈ S
hsC : s ⊆ C
hCmax : ∀ (a : Set E), a ∈ S → C ⊆ a → a = C
⊢ ∃ C, Convex 𝕜 C ∧ Convex 𝕜 (Cᶜ) ∧ s ⊆ C ∧ t ⊆ Cᶜ
refine'
  ⟨C, hC.1, convex_iff_segment_subset.2 fun x hx y hy z hz hzC => _, hsC, hC.2.subset_compl_left⟩
case intro.intro.intro
𝕜 : Type u_1
E : Type u_2
ι : Type ?u.47333
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
hC : C ∈ S
hsC : s ⊆ C
hCmax : ∀ (a : Set E), a ∈ S → C ⊆ a → a = C
x : E
hx : x ∈ Cᶜ
y : E
hy : y ∈ Cᶜ
z : E
hz : z ∈ segment 𝕜 x y
hzC : z ∈ C
h : ∀ (c : E), c ∈ Cᶜ → ∃ a, a ∈ C ∧ Set.Nonempty (segment 𝕜 c a ∩ t)
⊢ False

case h
𝕜 : Type u_1
E : Type u_2
ι : Type ?u.47333
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
hC : C ∈ S
hsC : s ⊆ C
hCmax : ∀ (a : Set E), a ∈ S → C ⊆ a → a = C
x : E
hx : x ∈ Cᶜ
y : E
hy : y ∈ Cᶜ
z : E
hz : z ∈ segment 𝕜 x y
hzC : z ∈ C
⊢ ∀ (c : E), c ∈ Cᶜ → ∃ a, a ∈ C ∧ Set.Nonempty (segment 𝕜 c a ∩ t)
case intro.intro.intro
𝕜 : Type u_1
E : Type u_2
ι : Type ?u.47333
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
hC : C ∈ S
hsC : s ⊆ C
hCmax : ∀ (a : Set E), a ∈ S → C ⊆ a → a = C
x : E
hx : x ∈ Cᶜ
y : E
hy : y ∈ Cᶜ
z : E
hz : z ∈ segment 𝕜 x y
hzC : z ∈ C
⊢ False
suffices h : ∀ c ∈ Cᶜ, ∃ a ∈ C, (segment 𝕜 c a ∩ t).Nonempty
case h
𝕜 : Type u_1
E : Type u_2
ι : Type ?u.47333
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
hC : C ∈ S
hsC : s ⊆ C
hCmax : ∀ (a : Set E), a ∈ S → C ⊆ a → a = C
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, a ∈ C ∧ Set.Nonempty (segment 𝕜 c a ∩ t)
case h
𝕜 : Type u_1
E : Type u_2
ι : Type ?u.47333
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
hC : C ∈ S
hsC : s ⊆ C
hCmax : ∀ (a : Set E), a ∈ S → C ⊆ a → a = C
x : E
hx : x ∈ Cᶜ
y : E
hy : y ∈ Cᶜ
z : E
hz : z ∈ segment 𝕜 x y
hzC : z ∈ C
⊢ ∀ (c : E), c ∈ Cᶜ → ∃ a, a ∈ C ∧ Set.Nonempty (segment 𝕜 c a ∩ t)
rintro c hc
case h
𝕜 : Type u_1
E : Type u_2
ι : Type ?u.47333
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
hC : C ∈ S
hsC : s ⊆ C
hCmax : ∀ (a : Set E), a ∈ S → C ⊆ a → a = C
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 : E), a ∈ C → ¬Set.Nonempty (segment 𝕜 c a ∩ t)
⊢ False
case h
𝕜 : Type u_1
E : Type u_2
ι : Type ?u.47333
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
hC : C ∈ S
hsC : s ⊆ C
hCmax : ∀ (a : Set E), a ∈ S → C ⊆ a → a = C
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, a ∈ C ∧ Set.Nonempty (segment 𝕜 c a ∩ t)
by_contra' h
case h
𝕜 : Type u_1
E : Type u_2
ι : Type ?u.47333
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
hC : C ∈ S
hsC : s ⊆ C
hCmax : ∀ (a : Set E), a ∈ S → C ⊆ a → a = C
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 : E), a ∈ C → ¬Set.Nonempty (segment 𝕜 c a ∩ t)
h : Disjoint (↑(convexHull 𝕜).toOrderHom (insert c C)) t
⊢ False

case h
𝕜 : Type u_1
E : Type u_2
ι : Type ?u.47333
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
hC : C ∈ S
hsC : s ⊆ C
hCmax : ∀ (a : Set E), a ∈ S → C ⊆ a → a = C
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 : E), a ∈ C → ¬Set.Nonempty (segment 𝕜 c a ∩ t)
⊢ Disjoint (↑(convexHull 𝕜).toOrderHom (insert c C)) t
case h
𝕜 : Type u_1
E : Type u_2
ι : Type ?u.47333
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
hC : C ∈ S
hsC : s ⊆ C
hCmax : ∀ (a : Set E), a ∈ S → C ⊆ a → a = C
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 : E), a ∈ C → ¬Set.Nonempty (segment 𝕜 c a ∩ t)
⊢ False
suffices h : Disjoint (convexHull 𝕜 (insert c C)) t
case h
𝕜 : Type u_1
E : Type u_2
ι : Type ?u.47333
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
hC : C ∈ S
hsC : s ⊆ C
hCmax : ∀ (a : Set E), a ∈ S → C ⊆ a → a = C
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 : E), a ∈ C → ¬Set.Nonempty (segment 𝕜 c a ∩ t)
⊢ Disjoint (⋃ (y : E) (_ : y ∈ ↑(convexHull 𝕜).toOrderHom C), segment 𝕜 c y) t
case h
𝕜 : Type u_1
E : Type u_2
ι : Type ?u.47333
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
hC : C ∈ S
hsC : s ⊆ C
hCmax : ∀ (a : Set E), a ∈ S → C ⊆ a → a = C
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 : E), a ∈ C → ¬Set.Nonempty (segment 𝕜 c a ∩ t)
⊢ Disjoint (↑(convexHull 𝕜).toOrderHom (insert c C)) t
rw [convexHull_insert ⟨z, hzC⟩, convexJoin_singleton_left]
case h
𝕜 : Type u_1
E : Type u_2
ι : Type ?u.47333
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
hC : C ∈ S
hsC : s ⊆ C
hCmax : ∀ (a : Set E), a ∈ S → C ⊆ a → a = C
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 : E), a ∈ C → ¬Set.Nonempty (segment 𝕜 c a ∩ t)
a : E
ha : a ∈ ↑(convexHull 𝕜).toOrderHom C
b : E
hb : b ∈ segment 𝕜 c a ⊓ t
⊢ a ∈ C
case h
𝕜 : Type u_1
E : Type u_2
ι : Type ?u.47333
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
hC : C ∈ S
hsC : s ⊆ C
hCmax : ∀ (a : Set E), a ∈ S → C ⊆ a → a = C
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 : E), a ∈ C → ¬Set.Nonempty (segment 𝕜 c a ∩ t)
⊢ Disjoint (⋃ (y : E) (_ : y ∈ ↑(convexHull 𝕜).toOrderHom C), segment 𝕜 c y) t
refine' disjoint_iUnion₂_left.2 fun a ha => disjoint_iff_inf_le.mpr fun b hb => h a _ ⟨b, hb⟩
no goals
case h
𝕜 : Type u_1
E : Type u_2
ι : Type ?u.47333
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
hC : C ∈ S
hsC : s ⊆ C
hCmax : ∀ (a : Set E), a ∈ S → C ⊆ a → a = C
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 : E), a ∈ C → ¬Set.Nonempty (segment 𝕜 c a ∩ t)
a : E
ha : a ∈ ↑(convexHull 𝕜).toOrderHom C
b : E
hb : b ∈ segment 𝕜 c a ⊓ t
⊢ a ∈ C
rwa [← hC.1.convexHull_eq]
case intro.intro.intro.intro.intro.intro.intro
𝕜 : Type u_1
E : Type u_2
ι : Type ?u.47333
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
hC : C ∈ S
hsC : s ⊆ C
hCmax : ∀ (a : Set E), a ∈ S → C ⊆ a → a = C
x : E
hx : x ∈ Cᶜ
y : E
hy : y ∈ Cᶜ
z : E
hz : z ∈ segment 𝕜 x y
hzC : z ∈ C
h : ∀ (c : E), c ∈ Cᶜ → ∃ a, a ∈ C ∧ Set.Nonempty (segment 𝕜 c a ∩ t)
p : E
hp : p ∈ C
u : E
hu : u ∈ segment 𝕜 x p
hut : u ∈ t
⊢ False
case intro.intro.intro
𝕜 : Type u_1
E : Type u_2
ι : Type ?u.47333
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
hC : C ∈ S
hsC : s ⊆ C
hCmax : ∀ (a : Set E), a ∈ S → C ⊆ a → a = C
x : E
hx : x ∈ Cᶜ
y : E
hy : y ∈ Cᶜ
z : E
hz : z ∈ segment 𝕜 x y
hzC : z ∈ C
h : ∀ (c : E), c ∈ Cᶜ → ∃ a, a ∈ C ∧ Set.Nonempty (segment 𝕜 c a ∩ t)
⊢ False
obtain ⟨p, hp, u, hu, hut⟩ := h x hx
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
𝕜 : Type u_1
E : Type u_2
ι : Type ?u.47333
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
hC : C ∈ S
hsC : s ⊆ C
hCmax : ∀ (a : Set E), a ∈ S → C ⊆ a → a = C
x : E
hx : x ∈ Cᶜ
y : E
hy : y ∈ Cᶜ
z : E
hz : z ∈ segment 𝕜 x y
hzC : z ∈ C
h : ∀ (c : E), c ∈ Cᶜ → ∃ a, a ∈ C ∧ Set.Nonempty (segment 𝕜 c a ∩ t)
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
case intro.intro.intro.intro.intro.intro.intro
𝕜 : Type u_1
E : Type u_2
ι : Type ?u.47333
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
hC : C ∈ S
hsC : s ⊆ C
hCmax : ∀ (a : Set E), a ∈ S → C ⊆ a → a = C
x : E
hx : x ∈ Cᶜ
y : E
hy : y ∈ Cᶜ
z : E
hz : z ∈ segment 𝕜 x y
hzC : z ∈ C
h : ∀ (c : E), c ∈ Cᶜ → ∃ a, a ∈ C ∧ Set.Nonempty (segment 𝕜 c a ∩ t)
p : E
hp : p ∈ C
u : E
hu : u ∈ segment 𝕜 x p
hut : u ∈ t
⊢ False
obtain ⟨q, hq, v, hv, hvt⟩ := h y hy
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
𝕜 : Type u_1
E : Type u_2
ι : Type ?u.47333
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
hC : C ∈ S
hsC : s ⊆ C
hCmax : ∀ (a : Set E), a ∈ S → C ⊆ a → a = C
x : E
hx : x ∈ Cᶜ
y : E
hy : y ∈ Cᶜ
z : E
hz : z ∈ segment 𝕜 x y
hzC : z ∈ C
h : ∀ (c : E), c ∈ Cᶜ → ∃ a, a ∈ C ∧ Set.Nonempty (segment 𝕜 c a ∩ t)
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
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
𝕜 : Type u_1
E : Type u_2
ι : Type ?u.47333
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
hC : C ∈ S
hsC : s ⊆ C
hCmax : ∀ (a : Set E), a ∈ S → C ⊆ a → a = C
x : E
hx : x ∈ Cᶜ
y : E
hy : y ∈ Cᶜ
z : E
hz : z ∈ segment 𝕜 x y
hzC : z ∈ C
h : ∀ (c : E), c ∈ Cᶜ → ∃ a, a ∈ C ∧ Set.Nonempty (segment 𝕜 c a ∩ t)
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
refine'
  not_disjoint_segment_convexHull_triple hz hu hv
    (hC.2.symm.mono (ht.segment_subset hut hvt) <| convexHull_min _ hC.1)
no goals
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
𝕜 : Type u_1
E : Type u_2
ι : Type ?u.47333
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
hC : C ∈ S
hsC : s ⊆ C
hCmax : ∀ (a : Set E), a ∈ S → C ⊆ a → a = C
x : E
hx : x ∈ Cᶜ
y : E
hy : y ∈ Cᶜ
z : E
hz : z ∈ segment 𝕜 x y
hzC : z ∈ C
h : ∀ (c : E), c ∈ Cᶜ → ∃ a, a ∈ C ∧ Set.Nonempty (segment 𝕜 c a ∩ t)
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
simpa [insert_subset, hp, hq, singleton_subset_iff.2 hzC]
case h
𝕜 : Type u_1
E : Type u_2
ι : Type ?u.47333
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
hC : C ∈ S
hsC : s ⊆ C
hCmax : ∀ (a : Set E), a ∈ S → C ⊆ a → a = C
x : E
hx : x ∈ Cᶜ
y : E
hy : y ∈ Cᶜ
z : E
hz : z ∈ segment 𝕜 x y
hzC : z ∈ C
c : E
hc : c ∈ ↑(convexHull 𝕜).toOrderHom (insert c C)ᶜ
h✝ : ∀ (a : E), a ∈ C → ¬Set.Nonempty (segment 𝕜 c a ∩ t)
h : Disjoint (↑(convexHull 𝕜).toOrderHom (insert c C)) t
⊢ False
case h
𝕜 : Type u_1
E : Type u_2
ι : Type ?u.47333
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
hC : C ∈ S
hsC : s ⊆ C
hCmax : ∀ (a : Set E), a ∈ S → C ⊆ a → a = C
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 : E), a ∈ C → ¬Set.Nonempty (segment 𝕜 c a ∩ t)
h : Disjoint (↑(convexHull 𝕜).toOrderHom (insert c C)) t
⊢ False
rw [←
  hCmax _ ⟨convex_convexHull _ _, h⟩ ((subset_insert _ _).trans <| subset_convexHull _ _)] at hc
no goals
case h
𝕜 : Type u_1
E : Type u_2
ι : Type ?u.47333
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
hC : C ∈ S
hsC : s ⊆ C
hCmax : ∀ (a : Set E), a ∈ S → C ⊆ a → a = C
x : E
hx : x ∈ Cᶜ
y : E
hy : y ∈ Cᶜ
z : E
hz : z ∈ segment 𝕜 x y
hzC : z ∈ C
c : E
hc : c ∈ ↑(convexHull 𝕜).toOrderHom (insert c C)ᶜ
h✝ : ∀ (a : E), a ∈ C → ¬Set.Nonempty (segment 𝕜 c a ∩ t)
h : Disjoint (↑(convexHull 𝕜).toOrderHom (insert c C)) t
⊢ False
exact hc (subset_convexHull _ _ <| mem_insert _ _)