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 u v x y : E
hu : u ∈ segment 𝕜 x p
hv : v ∈ segment 𝕜 y q
az bz : 𝕜
haz : 0 ≤ az
hbz : 0 ≤ bz
habz : az + bz = 1
inl :
  ∀ (haz : LE.le.{u_1} (α := 𝕜) 0 0) (habz : 0 + bz = 1),
    ∃ x_1 ∈ segment 𝕜 u v,
      Membership.mem (γ := Set E)
        ((convexHull 𝕜 : (a : Set E) → Set E) {p, q, HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) 0 x + bz • y} : Set E) x_1
inr :
  ∀ (haz' : 0 < az),
    ∃ x_1 ∈ segment 𝕜 u v,
      Membership.mem (γ := Set E) ((convexHull 𝕜 : (a : Set E) → Set E) {p, q, az • x + bz • y} : Set E) x_1
⊢ ∃ x_1 ∈ segment 𝕜 u v,
    Membership.mem (γ := Set E) ((convexHull 𝕜 : (a : Set E) → Set E) {p, q, az • x + bz • y} : Set E) x_1

Tactic:
obtain rfl | haz' := haz.eq_or_lt

Premises used: LE.le.eq_or_lt, rfl
-- 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 u v x y : E
hu : u ∈ segment 𝕜 x p
hv : v ∈ segment 𝕜 y q
bz : 𝕜
hbz : 0 ≤ bz
haz : LE.le.{u_1} (α := 𝕜) 0 0
habz : 0 + bz = 1
⊢ bz = 1

Tactic:
rw [zero_add] at habz

Premises used: zero_add
-- 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 u v x y : E
hu : u ∈ segment 𝕜 x p
hv : v ∈ segment 𝕜 y q
bz : 𝕜
hbz : 0 ≤ bz
haz : LE.le.{u_1} (α := 𝕜) 0 0
habz : bz = 1
inl : ∃ x ∈ segment 𝕜 u v, Membership.mem (γ := Set E) ((convexHull 𝕜 : (a : Set E) → Set E) {p, q, y} : Set E) x
⊢ ∃ x_1 ∈ segment 𝕜 u v,
    Membership.mem (γ := Set E)
      ((convexHull 𝕜 : (a : Set E) → Set E) {p, q, HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) 0 x + bz • y} : Set E) x_1

Tactic:
rw [zero_smul, zero_add, habz, one_smul]

Premises used: zero_add, one_smul, zero_smul
-- 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 u v x y : E
hu : u ∈ segment 𝕜 x p
hv : v ∈ segment 𝕜 y q
bz : 𝕜
hbz : 0 ≤ bz
haz : LE.le.{u_1} (α := 𝕜) 0 0
habz : bz = 1
⊢ v ∈ segment 𝕜 u v

Tactic:
apply right_mem_segment

Premises used: right_mem_segment
-- 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 u v x y : E
hu : u ∈ segment 𝕜 x p
hv : v ∈ segment 𝕜 y q
bz : 𝕜
hbz : 0 ≤ bz
haz : LE.le.{u_1} (α := 𝕜) 0 0
habz : bz = 1
inl : Membership.mem (γ := Set E) {p, q, y} y
inl₁ : Membership.mem (γ := Set E) {p, q, y} q
⊢ ∃ x ∈ segment 𝕜 u v, Membership.mem (γ := Set E) ((convexHull 𝕜 : (a : Set E) → Set E) {p, q, y} : Set E) x

Tactic:
refine ⟨v, by apply right_mem_segment, segment_subset_convexHull ?_ ?_ hv⟩
-- 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 u v x y : E
hu : u ∈ segment 𝕜 x p
hv : v ∈ segment 𝕜 y q
bz : 𝕜
hbz : 0 ≤ bz
haz : LE.le.{u_1} (α := 𝕜) 0 0
habz : bz = 1
⊢ Membership.mem (γ := Set E) {p, q, y} y

Tactic:
simp
-- 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 u v x y : E
hu : u ∈ segment 𝕜 x p
hv : v ∈ segment 𝕜 y q
bz : 𝕜
hbz : 0 ≤ bz
haz : LE.le.{u_1} (α := 𝕜) 0 0
habz : bz = 1
⊢ Membership.mem (γ := Set E) {p, q, y} q

Tactic:
simp
-- 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 u v x y : E
hu : u ∈ segment 𝕜 x p
hv : v ∈ segment 𝕜 y q
az bz : 𝕜
haz : 0 ≤ az
hbz : 0 ≤ bz
habz : az + bz = 1
haz' : 0 < az
inr :
  ∀ (av bv : 𝕜) (hav : 0 ≤ av) (hbv : 0 ≤ bv) (habv : av + bv = 1),
    ∃ x_1 ∈ segment 𝕜 u (av • y + bv • q),
      Membership.mem (γ := Set E) ((convexHull 𝕜 : (a : Set E) → Set E) {p, q, az • x + bz • y} : Set E) x_1
⊢ ∃ x_1 ∈ segment 𝕜 u v,
    Membership.mem (γ := Set E) ((convexHull 𝕜 : (a : Set E) → Set E) {p, q, az • x + bz • y} : Set E) x_1

Tactic:
obtain ⟨av, bv, hav, hbv, habv, rfl⟩ := hv

Premises used: rfl
-- 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 u x y : E
hu : u ∈ segment 𝕜 x p
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
inr :
  ∀ (hav : LE.le.{u_1} (α := 𝕜) 0 0) (habv : 0 + bv = 1),
    ∃ x_1 ∈ segment 𝕜 u (HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) 0 y + bv • q),
      Membership.mem (γ := Set E) ((convexHull 𝕜 : (a : Set E) → Set E) {p, q, az • x + bz • y} : Set E) x_1
inr₁ :
  ∀ (hav' : 0 < av),
    ∃ x_1 ∈ segment 𝕜 u (av • y + bv • q),
      Membership.mem (γ := Set E) ((convexHull 𝕜 : (a : Set E) → Set E) {p, q, az • x + bz • y} : Set E) x_1
⊢ ∃ x_1 ∈ segment 𝕜 u (av • y + bv • q),
    Membership.mem (γ := Set E) ((convexHull 𝕜 : (a : Set E) → Set E) {p, q, az • x + bz • y} : Set E) x_1

Tactic:
obtain rfl | hav' := hav.eq_or_lt

Premises used: LE.le.eq_or_lt, rfl
-- 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 u x y : E
hu : u ∈ segment 𝕜 x p
az bz : 𝕜
haz : 0 ≤ az
hbz : 0 ≤ bz
habz : az + bz = 1
haz' : 0 < az
bv : 𝕜
hbv : 0 ≤ bv
hav : LE.le.{u_1} (α := 𝕜) 0 0
habv : 0 + bv = 1
⊢ bv = 1

Tactic:
rw [zero_add] at habv

Premises used: zero_add
-- 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 u x y : E
hu : u ∈ segment 𝕜 x p
az bz : 𝕜
haz : 0 ≤ az
hbz : 0 ≤ bz
habz : az + bz = 1
haz' : 0 < az
bv : 𝕜
hbv : 0 ≤ bv
hav : LE.le.{u_1} (α := 𝕜) 0 0
habv : bv = 1
inr :
  ∃ x_1 ∈ segment 𝕜 u q,
    Membership.mem (γ := Set E) ((convexHull 𝕜 : (a : Set E) → Set E) {p, q, az • x + bz • y} : Set E) x_1
⊢ ∃ x_1 ∈ segment 𝕜 u (HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) 0 y + bv • q),
    Membership.mem (γ := Set E) ((convexHull 𝕜 : (a : Set E) → Set E) {p, q, az • x + bz • y} : Set E) x_1

Tactic:
rw [zero_smul, zero_add, habv, one_smul]

Premises used: zero_add, one_smul, zero_smul
-- 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 u x y : E
hu : u ∈ segment 𝕜 x p
az bz : 𝕜
haz : 0 ≤ az
hbz : 0 ≤ bz
habz : az + bz = 1
haz' : 0 < az
bv : 𝕜
hbv : 0 ≤ bv
hav : LE.le.{u_1} (α := 𝕜) 0 0
habv : bv = 1
⊢ Membership.mem (γ := Set E) {p, q, az • x + bz • y} q

Tactic:
simp
-- 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 u x y : E
hu : u ∈ segment 𝕜 x p
az bz : 𝕜
haz : 0 ≤ az
hbz : 0 ≤ bz
habz : az + bz = 1
haz' : 0 < az
bv : 𝕜
hbv : 0 ≤ bv
hav : LE.le.{u_1} (α := 𝕜) 0 0
habv : bv = 1
⊢ ∃ x_1 ∈ segment 𝕜 u q,
    Membership.mem (γ := Set E) ((convexHull 𝕜 : (a : Set E) → Set E) {p, q, az • x + bz • y} : Set E) x_1

Tactic:
exact ⟨q, right_mem_segment _ _ _, subset_convexHull _ _ <| by simp⟩
-- 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 u x y : E
hu : u ∈ segment 𝕜 x p
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
inr :
  ∀ (au bu : 𝕜) (hau : 0 ≤ au) (hbu : 0 ≤ bu) (habu : au + bu = 1),
    ∃ x_1 ∈ segment 𝕜 (au • x + bu • p) (av • y + bv • q),
      Membership.mem (γ := Set E) ((convexHull 𝕜 : (a : Set E) → Set E) {p, q, az • x + bz • y} : Set E) x_1
⊢ ∃ x_1 ∈ segment 𝕜 u (av • y + bv • q),
    Membership.mem (γ := Set E) ((convexHull 𝕜 : (a : Set E) → Set E) {p, q, az • x + bz • y} : Set E) x_1

Tactic:
obtain ⟨au, bu, hau, hbu, habu, rfl⟩ := hu

Premises used: rfl
-- 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
⊢ 0 < az * av + bz * au

Tactic:
positivity
-- 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
⊢ 0 < az * av + bz * au

Tactic:
have hab : 0 < az * av + bz * au := by positivity
-- 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
⊢ ∃ x_1 ∈ segment 𝕜 (au • x + bu • p) (av • y + bv • q),
    Membership.mem (γ := Set E) ((convexHull 𝕜 : (a : Set E) → Set E) {p, q, az • x + bz • y} : Set E) x_1

Tactic:
⟨(az * av / (az * av + bz * au)) • (au • x + bu • p) +
    (bz * au / (az * av + bz * au)) • (av • y + bv • q), ⟨_, _, ?_, ?_, ?_, rfl⟩, ?_⟩

Premises used: HMul.hMul, HDiv.hDiv, HAdd.hAdd, And.intro, Exists.intro, HSMul.hSMul, rfl
-- 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
inr : 0 ≤ az * av / (az * av + bz * au)
inr₁ : 0 ≤ bz * au / (az * av + bz * au)
inr₂ : az * av / (az * av + bz * au) + bz * au / (az * av + bz * au) = 1
inr₃ :
  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))
⊢ ∃ x_1 ∈ segment 𝕜 (au • x + bu • p) (av • y + bv • q),
    Membership.mem (γ := Set E) ((convexHull 𝕜 : (a : Set E) → Set E) {p, q, az • x + bz • y} : Set E) x_1

Tactic:
refine ⟨(az * av / (az * av + bz * au)) • (au • x + bu • p) +
    (bz * au / (az * av + bz * au)) • (av • y + bv • q), ⟨_, _, ?_, ?_, ?_, rfl⟩, ?_⟩
-- 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
⊢ 0 ≤ az * av / (az * av + bz * au)

Tactic:
positivity
-- 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
⊢ 0 ≤ bz * au / (az * av + bz * au)

Tactic:
positivity
-- 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
inr : az * av + bz * au ≠ 0
⊢ az * av / (az * av + bz * au) + bz * au / (az * av + bz * au) = 1

Tactic:
rw [← add_div, div_self]

Premises used: div_self, add_div
-- 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
⊢ az * av + bz * au ≠ 0

Tactic:
positivity
-- 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]
i : Fin 3
0 : 0 ≤ w ((fun (i : Fin 3) ↦ i) (⟨0, ⋯⟩ : Fin 3))
1 : 0 ≤ w ((fun (i : Fin 3) ↦ i) (⟨1, ⋯⟩ : Fin 3))
2 : 0 ≤ w ((fun (i : Fin 3) ↦ i) (⟨2, ⋯⟩ : Fin 3))
⊢ 0 ≤ w i

Tactic:
fin_cases i
-- 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]
⊢ 0 ≤ w ((fun (i : Fin 3) ↦ i) (⟨0, ⋯⟩ : Fin 3))

Tactic:
mul_nonneg (mul_nonneg haz hav) hbu

Premises used: Eq.mpr, mul_nonneg, Fin.cons, Fin.induction.go, Fin.induction, Fin.cases, Matrix.vecCons
-- 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]
⊢ 0 ≤ w ((fun (i : Fin 3) ↦ i) (⟨0, ⋯⟩ : Fin 3))

Tactic:
exact mul_nonneg (mul_nonneg haz hav) hbu

Premises used: mul_nonneg
-- 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]
⊢ 0 ≤ w ((fun (i : Fin 3) ↦ i) (⟨1, ⋯⟩ : Fin 3))

Tactic:
mul_nonneg (mul_nonneg hbz hau) hbv

Premises used: Eq.mpr, mul_nonneg, Fin.cons, Fin.induction.go, Fin.induction, Fin.cases, Matrix.vecCons
-- 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]
⊢ 0 ≤ w ((fun (i : Fin 3) ↦ i) (⟨1, ⋯⟩ : Fin 3))

Tactic:
exact mul_nonneg (mul_nonneg hbz hau) hbv

Premises used: mul_nonneg
-- 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]
⊢ 0 ≤ w ((fun (i : Fin 3) ↦ i) (⟨2, ⋯⟩ : Fin 3))

Tactic:
mul_nonneg hau hav

Premises used: Eq.mpr, mul_nonneg, Fin.cons, Fin.induction.go, Fin.induction, Fin.cases, Matrix.vecCons
-- 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]
⊢ 0 ≤ w ((fun (i : Fin 3) ↦ i) (⟨2, ⋯⟩ : Fin 3))

Tactic:
exact mul_nonneg hau hav

Premises used: mul_nonneg
-- 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]
⊢ ∀ (i : Fin 3), 0 ≤ w i

Tactic:
have hw₀ : ∀ i, 0 ≤ w i := by
      rintro i
      fin_cases i
      · exact mul_nonneg (mul_nonneg haz hav) hbu
      · exact mul_nonneg (mul_nonneg hbz hau) hbv
      · exact mul_nonneg hau hav
-- 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
trans : ∑ i : Fin 3, w i = az * av * bu + (bz * au * bv + au * av)
trans₁ : az * av * bu + (bz * au * bv + au * av) = az * av + bz * au
⊢ ∑ i : Fin 3, w i = az * av + bz * au

Tactic:
trans az * av * bu + (bz * au * bv + au * av)

Premises used: HMul.hMul, HAdd.hAdd
-- 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
⊢ ∑ i : Fin 3, w i = az * av * bu + (bz * au * bv + au * av)

Tactic:
simp [w, Fin.sum_univ_succ]

Premises used: Fin.sum_univ_succ
-- 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
⊢ az * av * bu + (bz * au * bv + au * av) = az * av + bz * au

Tactic:
linear_combination (au * bv - 1 * au) * habz + (-(1 * az * au) + au) * habv + az * av * habu

Premises used: HMul.hMul, HSub.hSub, HAdd.hAdd, OfNat.ofNat, Neg.neg
-- 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
⊢ ∑ i : Fin 3, w i = az * av + bz * au

Tactic:
have hw : ∑ i, w i = az * av + bz * au := by
      trans az * av * bu + (bz * au * bv + au * av)
      · simp [w, Fin.sum_univ_succ]
      linear_combination (au * bv - 1 * au) * habz + (-(1 * az * au) + au) * habv + az * av * habu
-- 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
0 : Membership.mem (γ := Set E) {p, q, az • x + bz • y} (z ((fun (i : Fin 3) ↦ i) (⟨0, ⋯⟩ : Fin 3)))
1 : Membership.mem (γ := Set E) {p, q, az • x + bz • y} (z ((fun (i : Fin 3) ↦ i) (⟨1, ⋯⟩ : Fin 3)))
2 : Membership.mem (γ := Set E) {p, q, az • x + bz • y} (z ((fun (i : Fin 3) ↦ i) (⟨2, ⋯⟩ : Fin 3)))
⊢ Membership.mem (γ := Set E) {p, q, az • x + bz • y} (z i)

Tactic:
fin_cases i
-- 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) (⟨0, ⋯⟩ : Fin 3)))

Tactic:
simp [z]