awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Convex.StoneSeparation (goal)
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
⊢ ∃ 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
have 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
Tactic: obtain rfl | haz' := haz.eq_or_lt
-- Lean 4 proof step from Mathlib.Analysis.Convex.StoneSeparation (hypothesis)
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
⊢ ∃ 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
have habz₁ : bz = 1
Tactic: rw [zero_add] at habz
Cleared hypotheses: habz
-- Lean 4 proof step from Mathlib.Analysis.Convex.StoneSeparation (goal)
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
⊢ ∃ 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
have inl : ∃ x ∈ segment 𝕜 u v, Membership.mem (γ := Set E) ((convexHull 𝕜 : (a : Set E) → Set E) {p, q, y} : Set E) x
Tactic: rw [zero_smul, zero_add, habz, one_smul]
-- Lean 4 proof step from Mathlib.Analysis.Convex.StoneSeparation (goal)
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
⊢ ∃ x ∈ segment 𝕜 u v, Membership.mem (γ := Set E) ((convexHull 𝕜 : (a : Set E) → Set E) {p, q, y} : Set E) x
have inl : Membership.mem (γ := Set E) {p, q, y} y
Tactic: refine ⟨v, by apply right_mem_segment, segment_subset_convexHull ?_ ?_ hv⟩
-- Lean 4 proof step from Mathlib.Analysis.Convex.StoneSeparation (goal)
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
⊢ ∃ x ∈ segment 𝕜 u v, Membership.mem (γ := Set E) ((convexHull 𝕜 : (a : Set E) → Set E) {p, q, y} : Set E) x
have inl₁ : Membership.mem (γ := Set E) {p, q, y} q
Tactic: refine ⟨v, by apply right_mem_segment, segment_subset_convexHull ?_ ?_ hv⟩
-- Lean 4 proof step from Mathlib.Analysis.Convex.StoneSeparation (goal)
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
⊢ ∃ 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
have 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
Tactic: obtain ⟨av, bv, hav, hbv, habv, rfl⟩ := hv
Cleared hypotheses: v, hv
-- Lean 4 proof step from Mathlib.Analysis.Convex.StoneSeparation (goal)
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
⊢ ∃ 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
have 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
Tactic: obtain rfl | hav' := hav.eq_or_lt
Cleared hypotheses: av, hav, habv
-- Lean 4 proof step from Mathlib.Analysis.Convex.StoneSeparation (goal)
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
⊢ ∃ 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
have 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
Tactic: obtain rfl | hav' := hav.eq_or_lt
-- Lean 4 proof step from Mathlib.Analysis.Convex.StoneSeparation (hypothesis)
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
⊢ ∃ 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
have habv₁ : bv = 1
Tactic: rw [zero_add] at habv
Cleared hypotheses: habv
-- Lean 4 proof step from Mathlib.Analysis.Convex.StoneSeparation (goal)
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 (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
have 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
Tactic: rw [zero_smul, zero_add, habv, one_smul]
-- Lean 4 proof step from Mathlib.Analysis.Convex.StoneSeparation (goal)
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
⊢ ∃ 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
have 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
Tactic: obtain ⟨au, bu, hau, hbu, habu, rfl⟩ := hu
Cleared hypotheses: u, hu
-- Lean 4 proof step from Mathlib.Analysis.Convex.StoneSeparation (hypothesis)
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
⊢ ∃ 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
have hab : 0 < az * av + bz * au
Tactic: have hab : 0 < az * av + bz * au := by positivity
-- Lean 4 proof step from Mathlib.Analysis.Convex.StoneSeparation (goal)
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
have inr : 0 ≤ az * av / (az * av + bz * au)
Tactic: refine ⟨(az * av / (az * av + bz * au)) • (au • x + bu • p) +
    (bz * au / (az * av + bz * au)) • (av • y + bv • q), ⟨_, _, ?_, ?_, ?_, rfl⟩, ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.Convex.StoneSeparation (goal)
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)
⊢ ∃ 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
have inr₁ : 0 ≤ bz * au / (az * av + bz * au)
Tactic: refine ⟨(az * av / (az * av + bz * au)) • (au • x + bu • p) +
    (bz * au / (az * av + bz * au)) • (av • y + bv • q), ⟨_, _, ?_, ?_, ?_, rfl⟩, ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.Convex.StoneSeparation (goal)
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)
⊢ ∃ 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
have inr₂ : az * av / (az * av + bz * au) + bz * au / (az * av + bz * au) = 1
Tactic: refine ⟨(az * av / (az * av + bz * au)) • (au • x + bu • p) +
    (bz * au / (az * av + bz * au)) • (av • y + bv • q), ⟨_, _, ?_, ?_, ?_, rfl⟩, ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.Convex.StoneSeparation (goal)
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
⊢ ∃ 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
have 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))
Tactic: refine ⟨(az * av / (az * av + bz * au)) • (au • x + bu • p) +
    (bz * au / (az * av + bz * au)) • (av • y + bv • q), ⟨_, _, ?_, ?_, ?_, rfl⟩, ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.Convex.StoneSeparation (goal)
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 / (az * av + bz * au) + bz * au / (az * av + bz * au) = 1
have inr : az * av + bz * au ≠ 0
Tactic: rw [← add_div, div_self]
-- Lean 4 proof step from Mathlib.Analysis.Convex.StoneSeparation (goal)
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
have 0 : 0 ≤ w ((fun (i : Fin 3) ↦ i) (⟨0, sorry⟩ : Fin 3))
Tactic: fin_cases i
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.Analysis.Convex.StoneSeparation (goal)
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))
⊢ 0 ≤ w i
have 1 : 0 ≤ w ((fun (i : Fin 3) ↦ i) (⟨1, sorry⟩ : Fin 3))
Tactic: fin_cases i
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.Analysis.Convex.StoneSeparation (goal)
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))
⊢ 0 ≤ w i
have 2 : 0 ≤ w ((fun (i : Fin 3) ↦ i) (⟨2, sorry⟩ : Fin 3))
Tactic: fin_cases i
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.Analysis.Convex.StoneSeparation (hypothesis)
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]
⊢ 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))
have hw₀ : ∀ (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
-- Lean 4 proof step from Mathlib.Analysis.Convex.StoneSeparation (goal)
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
have trans : ∑ i : Fin 3, w i = az * av * bu + (bz * au * bv + au * av)
Tactic: trans az * av * bu + (bz * au * bv + au * av)
-- Lean 4 proof step from Mathlib.Analysis.Convex.StoneSeparation (goal)
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)
⊢ ∑ i : Fin 3, w i = az * av + bz * au
have trans₁ : az * av * bu + (bz * au * bv + au * av) = az * av + bz * au
Tactic: trans az * av * bu + (bz * au * bv + au * av)
-- Lean 4 proof step from Mathlib.Analysis.Convex.StoneSeparation (hypothesis)
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
⊢ 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))
have hw : ∑ 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
-- Lean 4 proof step from Mathlib.Analysis.Convex.StoneSeparation (goal)
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)
have 0 : Membership.mem (γ := Set E) {p, q, az • x + bz • y} (z ((fun (i : Fin 3) ↦ i) (⟨0, sorry⟩ : Fin 3)))
Tactic: fin_cases i
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.Analysis.Convex.StoneSeparation (goal)
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)))
⊢ Membership.mem (γ := Set E) {p, q, az • x + bz • y} (z i)
have 1 : Membership.mem (γ := Set E) {p, q, az • x + bz • y} (z ((fun (i : Fin 3) ↦ i) (⟨1, sorry⟩ : Fin 3)))
Tactic: fin_cases i
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.Analysis.Convex.StoneSeparation (goal)
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)))
⊢ Membership.mem (γ := Set E) {p, q, az • x + bz • y} (z i)
have 2 : Membership.mem (γ := Set E) {p, q, az • x + bz • y} (z ((fun (i : Fin 3) ↦ i) (⟨2, sorry⟩ : Fin 3)))
Tactic: fin_cases i
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.Analysis.Convex.StoneSeparation (hypothesis)
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) ((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))
have hz : ∀ (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]
-- Lean 4 proof step from Mathlib.Analysis.Convex.StoneSeparation (goal)
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)
⊢ 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))
have 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
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 ∈ _)