awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Convex.StoneSeparation
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
p q x y : E
az bz : 𝕜
haz : 0 ≤ az
hbz : 0 ≤ bz
habz : az + bz = 1
haz' : 0 < az
av bv : 𝕜
hav : 0 ≤ av
hbv : 0 ≤ bv
habv : av + bv = 1
hav' : 0 < av
au bu : 𝕜
hau : 0 ≤ au
hbu : 0 ≤ bu
habu : au + bu = 1
hab : 0 < az * av + bz * au
w : Fin 3 → 𝕜 := ![az * av * bu, bz * au * bv, au * av]
z : Fin 3 → E := ![p, q, az • x + bz • y]
hw₀ : ∀ (i : Fin 3), 0 ≤ w i
hw : ∑ i : Fin 3, w i = az * av + bz * au
⊢ Membership.mem (γ := Set E) {p, q, az • x + bz • y} (z ((fun (i : Fin 3) ↦ i) (⟨1, ⋯⟩ : Fin 3)))

Tactic:
simp [z]
-- Module: Mathlib.Analysis.Convex.StoneSeparation
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
p q x y : E
az bz : 𝕜
haz : 0 ≤ az
hbz : 0 ≤ bz
habz : az + bz = 1
haz' : 0 < az
av bv : 𝕜
hav : 0 ≤ av
hbv : 0 ≤ bv
habv : av + bv = 1
hav' : 0 < av
au bu : 𝕜
hau : 0 ≤ au
hbu : 0 ≤ bu
habu : au + bu = 1
hab : 0 < az * av + bz * au
w : Fin 3 → 𝕜 := ![az * av * bu, bz * au * bv, au * av]
z : Fin 3 → E := ![p, q, az • x + bz • y]
hw₀ : ∀ (i : Fin 3), 0 ≤ w i
hw : ∑ i : Fin 3, w i = az * av + bz * au
⊢ Membership.mem (γ := Set E) {p, q, az • x + bz • y} (z ((fun (i : Fin 3) ↦ i) (⟨2, ⋯⟩ : Fin 3)))

Tactic:
simp [z]
-- Module: Mathlib.Analysis.Convex.StoneSeparation
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
p q x y : E
az bz : 𝕜
haz : 0 ≤ az
hbz : 0 ≤ bz
habz : az + bz = 1
haz' : 0 < az
av bv : 𝕜
hav : 0 ≤ av
hbv : 0 ≤ bv
habv : av + bv = 1
hav' : 0 < av
au bu : 𝕜
hau : 0 ≤ au
hbu : 0 ≤ bu
habu : au + bu = 1
hab : 0 < az * av + bz * au
w : Fin 3 → 𝕜 := ![az * av * bu, bz * au * bv, au * av]
z : Fin 3 → E := ![p, q, az • x + bz • y]
hw₀ : ∀ (i : Fin 3), 0 ≤ w i
hw : ∑ i : Fin 3, w i = az * av + bz * au
⊢ ∀ (i : Fin 3), Membership.mem (γ := Set E) {p, q, az • x + bz • y} (z i)

Tactic:
have hz : ∀ i, z i ∈ ({p, q, az • x + bz • y} : Set E) := fun i => by fin_cases i <;> simp [z]
-- Module: Mathlib.Analysis.Convex.StoneSeparation
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
p q x y : E
az bz : 𝕜
haz : 0 ≤ az
hbz : 0 ≤ bz
habz : az + bz = 1
haz' : 0 < az
av bv : 𝕜
hav : 0 ≤ av
hbv : 0 ≤ bv
habv : av + bv = 1
hav' : 0 < av
au bu : 𝕜
hau : 0 ≤ au
hbu : 0 ≤ bu
habu : au + bu = 1
hab : 0 < az * av + bz * au
w : Fin 3 → 𝕜 := ![az * av * bu, bz * au * bv, au * av]
z : Fin 3 → E := ![p, q, az • x + bz • y]
hw₀ : ∀ (i : Fin 3), 0 ≤ w i
hw : ∑ i : Fin 3, w i = az * av + bz * au
hz : ∀ (i : Fin 3), Membership.mem (γ := Set E) {p, q, az • x + bz • y} (z i)
rwa rwa₁ rwa₂ rwa₃ : 0 < az * av + bz * au
⊢ LT.lt.{u_1} (α := 𝕜) 0 (∑ i : Fin 3, w i)

Tactic:
rwa [hw]
-- Module: Mathlib.Analysis.Convex.StoneSeparation
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
p q x y : E
az bz : 𝕜
haz : 0 ≤ az
hbz : 0 ≤ bz
habz : az + bz = 1
haz' : 0 < az
av bv : 𝕜
hav : 0 ≤ av
hbv : 0 ≤ bv
habv : av + bv = 1
hav' : 0 < av
au bu : 𝕜
hau : 0 ≤ au
hbu : 0 ≤ bu
habu : au + bu = 1
hab : 0 < az * av + bz * au
w : Fin 3 → 𝕜 := ![az * av * bu, bz * au * bv, au * av]
z : Fin 3 → E := ![p, q, az • x + bz • y]
hw₀ : ∀ (i : Fin 3), 0 ≤ w i
hw : ∑ i : Fin 3, w i = az * av + bz * au
hz : ∀ (i : Fin 3), Membership.mem (γ := Set E) {p, q, az • x + bz • y} (z i)
h :
  (az * av / (az * av + bz * au)) • (au • x + bu • p) + (bz * au / (az * av + bz * au)) • (av • y + bv • q) =
    Finset.centerMass Finset.univ w z
⊢ Membership.mem (γ := Set E) ((convexHull 𝕜 : (a : Set E) → Set E) {p, q, az • x + bz • y} : Set E)
    ((az * av / (az * av + bz * au)) • (au • x + bu • p) + (bz * au / (az * av + bz * au)) • (av • y + bv • q))

Tactic:
convert!
      (Finset.centerMass_mem_convexHull (Finset.univ : Finset (Fin 3)) (fun i _ => hw₀ i)
          (by rwa [hw]) fun i _ => hz i :
        Finset.univ.centerMass w z ∈ _)

Premises used: Finset.univ, Finset.centerMass_mem_convexHull
-- Module: Mathlib.Analysis.Convex.StoneSeparation
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
p q x y : E
az bz : 𝕜
haz : 0 ≤ az
hbz : 0 ≤ bz
habz : az + bz = 1
haz' : 0 < az
av bv : 𝕜
hav : 0 ≤ av
hbv : 0 ≤ bv
habv : av + bv = 1
hav' : 0 < av
au bu : 𝕜
hau : 0 ≤ au
hbu : 0 ≤ bu
habu : au + bu = 1
hab : 0 < az * av + bz * au
w : Fin 3 → 𝕜 := ![az * av * bu, bz * au * bv, au * av]
z : Fin 3 → E := ![p, q, az • x + bz • y]
hw₀ : ∀ (i : Fin 3), 0 ≤ w i
hw : ∑ i : Fin 3, w i = az * av + bz * au
hz : ∀ (i : Fin 3), Membership.mem (γ := Set E) {p, q, az • x + bz • y} (z i)
h :
  (az * av / (az * av + bz * au)) • (au • x + bu • p) + (bz * au / (az * av + bz * au)) • (av • y + bv • q) =
    HSMul.hSMul (β := E) (az * av + bz * au)⁻¹ (∑ i : Fin 3, w i • z i)
⊢ (az * av / (az * av + bz * au)) • (au • x + bu • p) + (bz * au / (az * av + bz * au)) • (av • y + bv • q) =
    Finset.centerMass Finset.univ w z

Tactic:
rw [Finset.centerMass, hw]

Premises used: Finset.centerMass
-- Module: Mathlib.Analysis.Convex.StoneSeparation
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
p q x y : E
az bz : 𝕜
haz : 0 ≤ az
hbz : 0 ≤ bz
habz : az + bz = 1
haz' : 0 < az
av bv : 𝕜
hav : 0 ≤ av
hbv : 0 ≤ bv
habv : av + bv = 1
hav' : 0 < av
au bu : 𝕜
hau : 0 ≤ au
hbu : 0 ≤ bu
habu : au + bu = 1
hab : 0 < az * av + bz * au
w : Fin 3 → 𝕜 := ![az * av * bu, bz * au * bv, au * av]
z : Fin 3 → E := ![p, q, az • x + bz • y]
hw₀ : ∀ (i : Fin 3), 0 ≤ w i
hw : ∑ i : Fin 3, w i = az * av + bz * au
hz : ∀ (i : Fin 3), Membership.mem (γ := Set E) {p, q, az • x + bz • y} (z i)
trans :
  (az * av / (az * av + bz * au)) • (au • x + bu • p) + (bz * au / (az * av + bz * au)) • (av • y + bv • q) =
    (az * av + bz * au)⁻¹ • ((az * av * bu) • p + ((bz * au * bv) • q + (au * av) • (az • x + bz • y)))
trans₁ :
  (az * av + bz * au)⁻¹ • ((az * av * bu) • p + ((bz * au * bv) • q + (au * av) • (az • x + bz • y))) =
    HSMul.hSMul (β := E) (az * av + bz * au)⁻¹ (∑ i : Fin 3, w i • z i)
⊢ (az * av / (az * av + bz * au)) • (au • x + bu • p) + (bz * au / (az * av + bz * au)) • (av • y + bv • q) =
    HSMul.hSMul (β := E) (az * av + bz * au)⁻¹ (∑ i : Fin 3, w i • z i)

Tactic:
trans (az * av + bz * au)⁻¹ •
      ((az * av * bu) • p + ((bz * au * bv) • q + (au * av) • (az • x + bz • y)))

Premises used: HMul.hMul, HAdd.hAdd, HSMul.hSMul
-- Module: Mathlib.Analysis.Convex.StoneSeparation
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
p q x y : E
az bz : 𝕜
haz : 0 ≤ az
hbz : 0 ≤ bz
habz : az + bz = 1
haz' : 0 < az
av bv : 𝕜
hav : 0 ≤ av
hbv : 0 ≤ bv
habv : av + bv = 1
hav' : 0 < av
au bu : 𝕜
hau : 0 ≤ au
hbu : 0 ≤ bu
habu : au + bu = 1
hab : 0 < az * av + bz * au
w : Fin 3 → 𝕜 := ![az * av * bu, bz * au * bv, au * av]
z : Fin 3 → E := ![p, q, az • x + bz • y]
hw₀ : ∀ (i : Fin 3), 0 ≤ w i
hw : ∑ i : Fin 3, w i = az * av + bz * au
hz : ∀ (i : Fin 3), Membership.mem (γ := Set E) {p, q, az • x + bz • y} (z i)
⊢ (az * av / (az * av + bz * au)) • (au • x + bu • p) + (bz * au / (az * av + bz * au)) • (av • y + bv • q) =
    (az * av + bz * au)⁻¹ • ((az * av * bu) • p + ((bz * au * bv) • q + (au * av) • (az • x + bz • y)))

Tactic:
module
-- Module: Mathlib.Analysis.Convex.StoneSeparation
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
p q x y : E
az bz : 𝕜
haz : 0 ≤ az
hbz : 0 ≤ bz
habz : az + bz = 1
haz' : 0 < az
av bv : 𝕜
hav : 0 ≤ av
hbv : 0 ≤ bv
habv : av + bv = 1
hav' : 0 < av
au bu : 𝕜
hau : 0 ≤ au
hbu : 0 ≤ bu
habu : au + bu = 1
hab : 0 < az * av + bz * au
w : Fin 3 → 𝕜 := ![az * av * bu, bz * au * bv, au * av]
z : Fin 3 → E := ![p, q, az • x + bz • y]
hw₀ : ∀ (i : Fin 3), 0 ≤ w i
hw : ∑ i : Fin 3, w i = az * av + bz * au
hz : ∀ (i : Fin 3), Membership.mem (γ := Set E) {p, q, az • x + bz • y} (z i)
e_a :
  (au * av) • (az • x + bz • y) =
    List.foldr (fun (x1 x2 : E) ↦ x1 + x2) 0
      (List.map (fun (i : Fin 3) ↦ w i • z i)
        ((fun (x1 : Fin 3) (x2 : List (Fin 3)) ↦ (fun (i : Fin 3) ↦ i) x1 :: x2) ⟨2, ⋯⟩ []))
⊢ (az * av + bz * au)⁻¹ • ((az * av * bu) • p + ((bz * au * bv) • q + (au * av) • (az • x + bz • y))) =
    HSMul.hSMul (β := E) (az * av + bz * au)⁻¹ (∑ i : Fin 3, w i • z i)

Tactic:
congr 3
-- Module: Mathlib.Analysis.Convex.StoneSeparation
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
p q x y : E
az bz : 𝕜
haz : 0 ≤ az
hbz : 0 ≤ bz
habz : az + bz = 1
haz' : 0 < az
av bv : 𝕜
hav : 0 ≤ av
hbv : 0 ≤ bv
habv : av + bv = 1
hav' : 0 < av
au bu : 𝕜
hau : 0 ≤ au
hbu : 0 ≤ bu
habu : au + bu = 1
hab : 0 < az * av + bz * au
w : Fin 3 → 𝕜 := ![az * av * bu, bz * au * bv, au * av]
z : Fin 3 → E := ![p, q, az • x + bz • y]
hw₀ : ∀ (i : Fin 3), 0 ≤ w i
hw : ∑ i : Fin 3, w i = az * av + bz * au
hz : ∀ (i : Fin 3), Membership.mem (γ := Set E) {p, q, az • x + bz • y} (z i)
⊢ (au * av) • (az • x + bz • y) =
    List.foldr (fun (x1 x2 : E) ↦ x1 + x2) 0
      (List.map (fun (i : Fin 3) ↦ w i • z i)
        ((fun (x1 : Fin 3) (x2 : List (Fin 3)) ↦ (fun (i : Fin 3) ↦ i) x1 :: x2) ⟨2, ⋯⟩ []))

Tactic:
simp [w, z]
-- Module: Mathlib.Analysis.Convex.StoneSeparation
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
s t : Set E
hs : Convex 𝕜 s
ht : Convex 𝕜 t
hst : Disjoint s t
S : Set (Set E) := {C : Set E | Convex 𝕜 C ∧ Disjoint C t}
obtain :
  ∀ (C : Set E) (hsC : s ⊆ C) (hmax : Maximal (fun (x : Set E) ↦ x ∈ S) C),
    ∃ (C : Set E), Convex 𝕜 C ∧ Convex 𝕜 Cᶜ ∧ s ⊆ C ∧ t ⊆ Cᶜ
⊢ ∃ (C : Set E), 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⟩

Premises used: Iff.mpr, Set.sUnion, Membership.mem, Exists, Set.disjoint_sUnion_left, IsChain.directedOn, DirectedOn.convex_sUnion, And, And.right, And.left, zorn_subset_nonempty, And.intro, _private.0.exists_convex_convex_compl_subset.match_1, Exists.intro, Set.subset_sUnion_of_mem
-- Module: Mathlib.Analysis.Convex.StoneSeparation
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
s t : Set E
hs : Convex 𝕜 s
ht : Convex 𝕜 t
hst : Disjoint s t
S : Set (Set E) := {C : Set E | Convex 𝕜 C ∧ Disjoint C t}
C : Set E
hsC : s ⊆ C
hmax : Maximal (fun (x : Set E) ↦ x ∈ S) C
⊢ Convex 𝕜 C ∧ Disjoint C t

Tactic:
hmax.prop

Premises used: Set.Mem, setOf, Maximal.prop
-- Module: Mathlib.Analysis.Convex.StoneSeparation
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
s t : Set E
hs : Convex 𝕜 s
ht : Convex 𝕜 t
hst : Disjoint s t
S : Set (Set E) := {C : Set E | Convex 𝕜 C ∧ Disjoint C t}
C : Set E
hsC : s ⊆ C
hmax : Maximal (fun (x : Set E) ↦ x ∈ S) C
⊢ Convex 𝕜 C ∧ Disjoint C t

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

Premises used: Maximal.prop
-- Module: Mathlib.Analysis.Convex.StoneSeparation
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
s t : Set E
hs : Convex 𝕜 s
ht : Convex 𝕜 t
hst : Disjoint s t
S : Set (Set E) := {C : Set E | Convex 𝕜 C ∧ Disjoint C t}
C : Set E
hsC : s ⊆ C
hmax : Maximal (fun (x : Set E) ↦ x ∈ S) C
hC : Convex 𝕜 C ∧ Disjoint C t
⊢ ∃ (C : Set E), Convex 𝕜 C ∧ Convex 𝕜 Cᶜ ∧ s ⊆ C ∧ t ⊆ Cᶜ

Tactic:
⟨C, hC.1, convex_iff_segment_subset.2 fun x hx y hy z hz hzC => ?_, hsC, hC.2.subset_compl_left⟩

Premises used: Iff.mpr, And.right, And.left, Disjoint.subset_compl_left, And.intro, Exists.intro, convex_iff_segment_subset
-- Module: Mathlib.Analysis.Convex.StoneSeparation
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
s t : Set E
hs : Convex 𝕜 s
ht : Convex 𝕜 t
hst : Disjoint s t
S : Set (Set E) := {C : Set E | Convex 𝕜 C ∧ Disjoint C t}
C : Set E
hsC : s ⊆ C
hmax : Maximal (fun (x : Set E) ↦ x ∈ S) C
hC : Convex 𝕜 C ∧ Disjoint C t
fun : ∀ (x : E) (hx : x ∈ Cᶜ) (y : E) (hy : y ∈ Cᶜ) (z : E) (hz : z ∈ segment 𝕜 x y) (hzC : z ∈ C), False
⊢ ∃ (C : Set E), Convex 𝕜 C ∧ Convex 𝕜 Cᶜ ∧ s ⊆ C ∧ t ⊆ Cᶜ

Tactic:
refine
    ⟨C, hC.1, convex_iff_segment_subset.2 fun x hx y hy z hz hzC => ?_, hsC, hC.2.subset_compl_left⟩
-- Module: Mathlib.Analysis.Convex.StoneSeparation
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
s t : Set E
hs : Convex 𝕜 s
ht : Convex 𝕜 t
hst : Disjoint s t
S : Set (Set E) := {C : Set E | Convex 𝕜 C ∧ Disjoint C t}
C : Set E
hsC : s ⊆ C
hmax : Maximal (fun (x : Set E) ↦ 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
obtain : ∀ (p : E) (hp : p ∈ C) (u : E) (hu : u ∈ segment 𝕜 x p) (hut : u ∈ t), False
⊢ False

Tactic:
obtain ⟨p, hp, u, hu, hut⟩ := h x hx
-- Module: Mathlib.Analysis.Convex.StoneSeparation
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
s t : Set E
hs : Convex 𝕜 s
ht : Convex 𝕜 t
hst : Disjoint s t
S : Set (Set E) := {C : Set E | Convex 𝕜 C ∧ Disjoint C t}
C : Set E
hsC : s ⊆ C
hmax : Maximal (fun (x : Set E) ↦ 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
obtain : ∀ (q : E) (hq : q ∈ C) (v : E) (hv : v ∈ segment 𝕜 y q) (hvt : v ∈ t), False
⊢ False

Tactic:
obtain ⟨q, hq, v, hv, hvt⟩ := h y hy
-- Module: Mathlib.Analysis.Convex.StoneSeparation
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
s t : Set E
hs : Convex 𝕜 s
ht : Convex 𝕜 t
hst : Disjoint s t
S : Set (Set E) := {C : Set E | Convex 𝕜 C ∧ Disjoint C t}
C : Set E
hsC : s ⊆ C
hmax : Maximal (fun (x : Set E) ↦ 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:
not_disjoint_segment_convexHull_triple hz hu hv
        (hC.2.symm.mono (ht.segment_subset hut hvt) <| convexHull_min ?_ hC.1)

Premises used: not_disjoint_segment_convexHull_triple, Disjoint.symm, And.right, And.left, convexHull_min, Disjoint.mono, Convex.segment_subset
-- Module: Mathlib.Analysis.Convex.StoneSeparation
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
s t : Set E
hs : Convex 𝕜 s
ht : Convex 𝕜 t
hst : Disjoint s t
S : Set (Set E) := {C : Set E | Convex 𝕜 C ∧ Disjoint C t}
C : Set E
hsC : s ⊆ C
hmax : Maximal (fun (x : Set E) ↦ 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
not_disjoint_segment_convexHull_triple : {p, q, z} ⊆ C
⊢ False

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

Premises used: not_disjoint_segment_convexHull_triple, Disjoint.symm, And.right, And.left, convexHull_min, Disjoint.mono, Convex.segment_subset
-- Module: Mathlib.Analysis.Convex.StoneSeparation
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
s t : Set E
hs : Convex 𝕜 s
ht : Convex 𝕜 t
hst : Disjoint s t
S : Set (Set E) := {C : Set E | Convex 𝕜 C ∧ Disjoint C t}
C : Set E
hsC : s ⊆ C
hmax : Maximal (fun (x : Set E) ↦ 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

Tactic:
simp [insert_subset_iff, hp, hq, singleton_subset_iff.2 hzC]

Premises used: Iff.mpr, Set.singleton_subset_iff, Set.insert_subset_iff
-- Module: Mathlib.Analysis.Convex.StoneSeparation
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
s t : Set E
hs : Convex 𝕜 s
ht : Convex 𝕜 t
hst : Disjoint s t
S : Set (Set E) := {C : Set E | Convex 𝕜 C ∧ Disjoint C t}
C : Set E
hsC : s ⊆ C
hmax : Maximal (fun (x : Set E) ↦ 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
suffices : ∀ c ∈ Cᶜ, ∃ a ∈ C, (segment 𝕜 c a ∩ t).Nonempty
⊢ 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]
-- Module: Mathlib.Analysis.Convex.StoneSeparation
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
s t : Set E
hs : Convex 𝕜 s
ht : Convex 𝕜 t
hst : Disjoint s t
S : Set (Set E) := {C : Set E | Convex 𝕜 C ∧ Disjoint C t}
C : Set E
hsC : s ⊆ C
hmax : Maximal (fun (x : Set E) ↦ 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ᶜ
by_contra! : ∀ (h : ∀ (a : E) (_ : a ∈ C), segment 𝕜 c a ∩ t = ∅), False
⊢ ∃ a ∈ C, (segment 𝕜 c a ∩ t).Nonempty

Tactic:
by_contra! h
-- Module: Mathlib.Analysis.Convex.StoneSeparation
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
s t : Set E
hs : Convex 𝕜 s
ht : Convex 𝕜 t
hst : Disjoint s t
S : Set (Set E) := {C : Set E | Convex 𝕜 C ∧ Disjoint C t}
C : Set E
hsC : s ⊆ C
hmax : Maximal (fun (x : Set E) ↦ 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_1 : ∀ (a : E) (_ : a ∈ C), segment 𝕜 c a ∩ t = ∅
h : Disjoint ((convexHull 𝕜 : (a : Set E) → Set E) (insert c C)) t
⊢ Membership.mem (γ := Set E) (((convexHull 𝕜 : (a : Set E) → Set E) (insert c C))ᶜ : Set E) c

Tactic:
rw [hmax.eq_of_subset ⟨convex_convexHull _ _, h⟩ <|
      (subset_insert ..).trans <| subset_convexHull ..] at hc

Premises used: subset_convexHull, HasSubset.Subset.trans, convex_convexHull, Maximal.eq_of_subset, And.intro, Set.subset_insert
-- Module: Mathlib.Analysis.Convex.StoneSeparation
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
s t : Set E
hs : Convex 𝕜 s
ht : Convex 𝕜 t
hst : Disjoint s t
S : Set (Set E) := {C : Set E | Convex 𝕜 C ∧ Disjoint C t}
C : Set E
hsC : s ⊆ C
hmax : Maximal (fun (x : Set E) ↦ 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_1 : ∀ (a : E) (_ : a ∈ C), segment 𝕜 c a ∩ t = ∅
h : Disjoint ((convexHull 𝕜 : (a : Set E) → Set E) (insert c C)) t
hc₁ : Membership.mem (γ := Set E) (((convexHull 𝕜 : (a : Set E) → Set E) (insert c C))ᶜ : Set E) c
⊢ ∀ (a : E) (_ : a ∈ C), segment 𝕜 c a ∩ t = ∅

Tactic:
rw [hmax.eq_of_subset ⟨convex_convexHull _ _, h⟩ <|
      (subset_insert ..).trans <| subset_convexHull ..] at hc

Premises used: subset_convexHull, HasSubset.Subset.trans, convex_convexHull, Maximal.eq_of_subset, And.intro, Set.subset_insert
-- Module: Mathlib.Analysis.Convex.StoneSeparation
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
s t : Set E
hs : Convex 𝕜 s
ht : Convex 𝕜 t
hst : Disjoint s t
S : Set (Set E) := {C : Set E | Convex 𝕜 C ∧ Disjoint C t}
C : Set E
hsC : s ⊆ C
hmax : Maximal (fun (x : Set E) ↦ 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_1 : ∀ (a : E) (_ : a ∈ C), segment 𝕜 c a ∩ t = ∅
h : Disjoint ((convexHull 𝕜 : (a : Set E) → Set E) (insert c C)) t
hc₁ : Membership.mem (γ := Set E) (((convexHull 𝕜 : (a : Set E) → Set E) (insert c C))ᶜ : Set E) c
h₁ : ∀ (a : E) (_ : a ∈ C), segment 𝕜 c a ∩ t = ∅
⊢ Disjoint ((convexHull 𝕜 : (a : Set E) → Set E) (insert c C)) t

Tactic:
rw [hmax.eq_of_subset ⟨convex_convexHull _ _, h⟩ <|
      (subset_insert ..).trans <| subset_convexHull ..] at hc

Premises used: subset_convexHull, HasSubset.Subset.trans, convex_convexHull, Maximal.eq_of_subset, And.intro, Set.subset_insert
-- Module: Mathlib.Analysis.Convex.StoneSeparation
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
s t : Set E
hs : Convex 𝕜 s
ht : Convex 𝕜 t
hst : Disjoint s t
S : Set (Set E) := {C : Set E | Convex 𝕜 C ∧ Disjoint C t}
C : Set E
hsC : s ⊆ C
hmax : Maximal (fun (x : Set E) ↦ 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 : Membership.mem (γ := Set E) (((convexHull 𝕜 : (a : Set E) → Set E) (insert c C))ᶜ : Set E) c
h_1 : ∀ (a : E) (_ : a ∈ C), segment 𝕜 c a ∩ t = ∅
h : Disjoint ((convexHull 𝕜 : (a : Set E) → Set E) (insert c C)) t
⊢ False

Tactic:
hc (subset_convexHull _ _ <| mem_insert _ _)

Premises used: subset_convexHull, Set.mem_insert
-- Module: Mathlib.Analysis.Convex.StoneSeparation
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
s t : Set E
hs : Convex 𝕜 s
ht : Convex 𝕜 t
hst : Disjoint s t
S : Set (Set E) := {C : Set E | Convex 𝕜 C ∧ Disjoint C t}
C : Set E
hsC : s ⊆ C
hmax : Maximal (fun (x : Set E) ↦ 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 : Membership.mem (γ := Set E) (((convexHull 𝕜 : (a : Set E) → Set E) (insert c C))ᶜ : Set E) c
h_1 : ∀ (a : E) (_ : a ∈ C), segment 𝕜 c a ∩ t = ∅
h : Disjoint ((convexHull 𝕜 : (a : Set E) → Set E) (insert c C)) t
⊢ False

Tactic:
exact hc (subset_convexHull _ _ <| mem_insert _ _)

Premises used: subset_convexHull, Set.mem_insert