[GOAL]
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t : Set E
p q u v x y z : E
hz : z ∈ segment 𝕜 x y
hu : u ∈ segment 𝕜 x p
hv : v ∈ segment 𝕜 y q
⊢ ¬Disjoint (segment 𝕜 u v) (↑(convexHull 𝕜) {p, q, z})
[PROOFSTEP]
rw [not_disjoint_iff]
[GOAL]
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t : Set E
p q u v x y z : E
hz : z ∈ segment 𝕜 x y
hu : u ∈ segment 𝕜 x p
hv : v ∈ segment 𝕜 y q
⊢ ∃ x, x ∈ segment 𝕜 u v ∧ x ∈ ↑(convexHull 𝕜) {p, q, z}
[PROOFSTEP]
obtain ⟨az, bz, haz, hbz, habz, rfl⟩ := hz
[GOAL]
case intro.intro.intro.intro.intro
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t : Set 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
⊢ ∃ x_1, x_1 ∈ segment 𝕜 u v ∧ x_1 ∈ ↑(convexHull 𝕜) {p, q, az • x + bz • y}
[PROOFSTEP]
obtain rfl | haz' := haz.eq_or_lt
[GOAL]
case intro.intro.intro.intro.intro.inl
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t : Set E
p q u v x y : E
hu : u ∈ segment 𝕜 x p
hv : v ∈ segment 𝕜 y q
bz : 𝕜
hbz : 0 ≤ bz
haz : 0 ≤ 0
habz : 0 + bz = 1
⊢ ∃ x_1, x_1 ∈ segment 𝕜 u v ∧ x_1 ∈ ↑(convexHull 𝕜) {p, q, 0 • x + bz • y}
[PROOFSTEP]
rw [zero_add] at habz 
[GOAL]
case intro.intro.intro.intro.intro.inl
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t : Set E
p q u v x y : E
hu : u ∈ segment 𝕜 x p
hv : v ∈ segment 𝕜 y q
bz : 𝕜
hbz : 0 ≤ bz
haz : 0 ≤ 0
habz : bz = 1
⊢ ∃ x_1, x_1 ∈ segment 𝕜 u v ∧ x_1 ∈ ↑(convexHull 𝕜) {p, q, 0 • x + bz • y}
[PROOFSTEP]
rw [zero_smul, zero_add, habz, one_smul]
[GOAL]
case intro.intro.intro.intro.intro.inl
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t : Set E
p q u v x y : E
hu : u ∈ segment 𝕜 x p
hv : v ∈ segment 𝕜 y q
bz : 𝕜
hbz : 0 ≤ bz
haz : 0 ≤ 0
habz : bz = 1
⊢ ∃ x, x ∈ segment 𝕜 u v ∧ x ∈ ↑(convexHull 𝕜) {p, q, y}
[PROOFSTEP]
refine' ⟨v, by apply right_mem_segment, segment_subset_convexHull _ _ hv⟩
[GOAL]
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t : Set E
p q u v x y : E
hu : u ∈ segment 𝕜 x p
hv : v ∈ segment 𝕜 y q
bz : 𝕜
hbz : 0 ≤ bz
haz : 0 ≤ 0
habz : bz = 1
⊢ v ∈ segment 𝕜 u v
[PROOFSTEP]
apply right_mem_segment
[GOAL]
case intro.intro.intro.intro.intro.inl.refine'_1
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t : Set E
p q u v x y : E
hu : u ∈ segment 𝕜 x p
hv : v ∈ segment 𝕜 y q
bz : 𝕜
hbz : 0 ≤ bz
haz : 0 ≤ 0
habz : bz = 1
⊢ y ∈ {p, q, y}
[PROOFSTEP]
simp
[GOAL]
case intro.intro.intro.intro.intro.inl.refine'_2
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t : Set E
p q u v x y : E
hu : u ∈ segment 𝕜 x p
hv : v ∈ segment 𝕜 y q
bz : 𝕜
hbz : 0 ≤ bz
haz : 0 ≤ 0
habz : bz = 1
⊢ q ∈ {p, q, y}
[PROOFSTEP]
simp
[GOAL]
case intro.intro.intro.intro.intro.inr
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t : Set 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, x_1 ∈ segment 𝕜 u v ∧ x_1 ∈ ↑(convexHull 𝕜) {p, q, az • x + bz • y}
[PROOFSTEP]
obtain ⟨av, bv, hav, hbv, habv, rfl⟩ := hv
[GOAL]
case intro.intro.intro.intro.intro.inr.intro.intro.intro.intro.intro
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t : Set 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, x_1 ∈ segment 𝕜 u (av • y + bv • q) ∧ x_1 ∈ ↑(convexHull 𝕜) {p, q, az • x + bz • y}
[PROOFSTEP]
obtain rfl | hav' := hav.eq_or_lt
[GOAL]
case intro.intro.intro.intro.intro.inr.intro.intro.intro.intro.intro.inl
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t : Set 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 : 0 ≤ 0
habv : 0 + bv = 1
⊢ ∃ x_1, x_1 ∈ segment 𝕜 u (0 • y + bv • q) ∧ x_1 ∈ ↑(convexHull 𝕜) {p, q, az • x + bz • y}
[PROOFSTEP]
rw [zero_add] at habv 
[GOAL]
case intro.intro.intro.intro.intro.inr.intro.intro.intro.intro.intro.inl
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t : Set 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 : 0 ≤ 0
habv : bv = 1
⊢ ∃ x_1, x_1 ∈ segment 𝕜 u (0 • y + bv • q) ∧ x_1 ∈ ↑(convexHull 𝕜) {p, q, az • x + bz • y}
[PROOFSTEP]
rw [zero_smul, zero_add, habv, one_smul]
[GOAL]
case intro.intro.intro.intro.intro.inr.intro.intro.intro.intro.intro.inl
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t : Set 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 : 0 ≤ 0
habv : bv = 1
⊢ ∃ x_1, x_1 ∈ segment 𝕜 u q ∧ x_1 ∈ ↑(convexHull 𝕜) {p, q, az • x + bz • y}
[PROOFSTEP]
exact ⟨q, right_mem_segment _ _ _, subset_convexHull _ _ <| by simp⟩
[GOAL]
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t : Set 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 : 0 ≤ 0
habv : bv = 1
⊢ q ∈ {p, q, az • x + bz • y}
[PROOFSTEP]
simp
[GOAL]
case intro.intro.intro.intro.intro.inr.intro.intro.intro.intro.intro.inr
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t : Set 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, x_1 ∈ segment 𝕜 u (av • y + bv • q) ∧ x_1 ∈ ↑(convexHull 𝕜) {p, q, az • x + bz • y}
[PROOFSTEP]
obtain ⟨au, bu, hau, hbu, habu, rfl⟩ := hu
[GOAL]
case intro.intro.intro.intro.intro.inr.intro.intro.intro.intro.intro.inr.intro.intro.intro.intro.intro
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t : Set 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, x_1 ∈ segment 𝕜 (au • x + bu • p) (av • y + bv • q) ∧ x_1 ∈ ↑(convexHull 𝕜) {p, q, az • x + bz • y}
[PROOFSTEP]
have hab : 0 < az * av + bz * au := add_pos_of_pos_of_nonneg (mul_pos haz' hav') (mul_nonneg hbz hau)
[GOAL]
case intro.intro.intro.intro.intro.inr.intro.intro.intro.intro.intro.inr.intro.intro.intro.intro.intro
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t : Set 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, x_1 ∈ segment 𝕜 (au • x + bu • p) (av • y + bv • q) ∧ x_1 ∈ ↑(convexHull 𝕜) {p, q, az • x + bz • y}
[PROOFSTEP]
refine'
  ⟨(az * av / (az * av + bz * au)) • (au • x + bu • p) + (bz * au / (az * av + bz * au)) • (av • y + bv • q),
    ⟨_, _, _, _, _, rfl⟩, _⟩
[GOAL]
case intro.intro.intro.intro.intro.inr.intro.intro.intro.intro.intro.inr.intro.intro.intro.intro.intro.refine'_1
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t : Set 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)
[PROOFSTEP]
exact div_nonneg (mul_nonneg haz hav) hab.le
[GOAL]
case intro.intro.intro.intro.intro.inr.intro.intro.intro.intro.intro.inr.intro.intro.intro.intro.intro.refine'_2
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t : Set 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)
[PROOFSTEP]
exact div_nonneg (mul_nonneg hbz hau) hab.le
[GOAL]
case intro.intro.intro.intro.intro.inr.intro.intro.intro.intro.intro.inr.intro.intro.intro.intro.intro.refine'_3
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t : Set 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
[PROOFSTEP]
rw [← add_div, div_self hab.ne']
[GOAL]
case intro.intro.intro.intro.intro.inr.intro.intro.intro.intro.intro.inr.intro.intro.intro.intro.intro.refine'_4
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t : Set 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)) • (au • x + bu • p) + (bz * au / (az * av + bz * au)) • (av • y + bv • q) ∈
    ↑(convexHull 𝕜) {p, q, az • x + bz • y}
[PROOFSTEP]
rw [smul_add, smul_add, add_add_add_comm, add_comm, ← mul_smul, ← mul_smul]
[GOAL]
case intro.intro.intro.intro.intro.inr.intro.intro.intro.intro.intro.inr.intro.intro.intro.intro.intro.refine'_4
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t : Set 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) * bu) • p + (bz * au / (az * av + bz * au) * bv) • q +
      ((az * av / (az * av + bz * au)) • au • x + (bz * au / (az * av + bz * au)) • av • y) ∈
    ↑(convexHull 𝕜) {p, q, az • x + bz • y}
[PROOFSTEP]
classical
let w : Fin 3 → 𝕜 := ![az * av * bu, bz * au * bv, au * av]
let z : Fin 3 → E := ![p, q, az • x + bz • y]
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
have hw : ∑ i, w i = az * av + bz * au :=
  by
  trans az * av * bu + (bz * au * bv + au * av)
  · simp [Fin.sum_univ_succ, Fin.sum_univ_zero]
  rw [← one_mul (au * av), ← habz, add_mul, ← add_assoc, add_add_add_comm, mul_assoc, ← mul_add, mul_assoc, ← mul_add,
    mul_comm av, ← add_mul, ← mul_add, add_comm bu, add_comm bv, habu, habv, one_mul, mul_one]
have hz : ∀ i, z i ∈ ({p, q, az • x + bz • y} : Set E) := fun i => by fin_cases i <;> simp
convert Finset.centerMass_mem_convexHull (Finset.univ : Finset (Fin 3)) (fun i _ => hw₀ i) (by rwa [hw]) fun i _ => hz i
rw [Finset.centerMass]
simp_rw [div_eq_inv_mul, hw, mul_assoc, mul_smul (az * av + bz * au)⁻¹, ← smul_add, add_assoc, ← mul_assoc]
congr 3
rw [← mul_smul, ← mul_rotate, mul_right_comm, mul_smul, ← mul_smul _ av, mul_rotate, mul_smul _ bz, ← smul_add]
simp only [smul_add, List.foldr, Matrix.cons_val_succ', Fin.mk_one, Matrix.cons_val_one, Matrix.head_cons, add_zero]
[GOAL]
case intro.intro.intro.intro.intro.inr.intro.intro.intro.intro.intro.inr.intro.intro.intro.intro.intro.refine'_4
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t : Set 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) * bu) • p + (bz * au / (az * av + bz * au) * bv) • q +
      ((az * av / (az * av + bz * au)) • au • x + (bz * au / (az * av + bz * au)) • av • y) ∈
    ↑(convexHull 𝕜) {p, q, az • x + bz • y}
[PROOFSTEP]
let w : Fin 3 → 𝕜 := ![az * av * bu, bz * au * bv, au * av]
[GOAL]
case intro.intro.intro.intro.intro.inr.intro.intro.intro.intro.intro.inr.intro.intro.intro.intro.intro.refine'_4
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t : Set 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]
⊢ (az * av / (az * av + bz * au) * bu) • p + (bz * au / (az * av + bz * au) * bv) • q +
      ((az * av / (az * av + bz * au)) • au • x + (bz * au / (az * av + bz * au)) • av • y) ∈
    ↑(convexHull 𝕜) {p, q, az • x + bz • y}
[PROOFSTEP]
let z : Fin 3 → E := ![p, q, az • x + bz • y]
[GOAL]
case intro.intro.intro.intro.intro.inr.intro.intro.intro.intro.intro.inr.intro.intro.intro.intro.intro.refine'_4
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t : Set 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]
⊢ (az * av / (az * av + bz * au) * bu) • p + (bz * au / (az * av + bz * au) * bv) • q +
      ((az * av / (az * av + bz * au)) • au • x + (bz * au / (az * av + bz * au)) • av • y) ∈
    ↑(convexHull 𝕜) {p, q, az • x + bz • y}
[PROOFSTEP]
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
[GOAL]
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t : Set 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
[PROOFSTEP]
rintro i
[GOAL]
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t : Set 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
[PROOFSTEP]
fin_cases i
[GOAL]
case head
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t : Set 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 { val := 0, isLt := (_ : 0 < 3) }
[PROOFSTEP]
exact mul_nonneg (mul_nonneg haz hav) hbu
[GOAL]
case tail.head
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t : Set 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 { val := 1, isLt := (_ : (fun a => a < 3) 1) }
[PROOFSTEP]
exact mul_nonneg (mul_nonneg hbz hau) hbv
[GOAL]
case tail.tail.head
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t : Set 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 { val := 2, isLt := (_ : (fun a => (fun a => a < 3) a) 2) }
[PROOFSTEP]
exact mul_nonneg hau hav
[GOAL]
case intro.intro.intro.intro.intro.inr.intro.intro.intro.intro.intro.inr.intro.intro.intro.intro.intro.refine'_4
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t : Set 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 / (az * av + bz * au) * bu) • p + (bz * au / (az * av + bz * au) * bv) • q +
      ((az * av / (az * av + bz * au)) • au • x + (bz * au / (az * av + bz * au)) • av • y) ∈
    ↑(convexHull 𝕜) {p, q, az • x + bz • y}
[PROOFSTEP]
have hw : ∑ i, w i = az * av + bz * au :=
  by
  trans az * av * bu + (bz * au * bv + au * av)
  · simp [Fin.sum_univ_succ, Fin.sum_univ_zero]
  rw [← one_mul (au * av), ← habz, add_mul, ← add_assoc, add_add_add_comm, mul_assoc, ← mul_add, mul_assoc, ← mul_add,
    mul_comm av, ← add_mul, ← mul_add, add_comm bu, add_comm bv, habu, habv, one_mul, mul_one]
[GOAL]
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t : Set 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
[PROOFSTEP]
trans az * av * bu + (bz * au * bv + au * av)
[GOAL]
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t : Set 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)
[PROOFSTEP]
simp [Fin.sum_univ_succ, Fin.sum_univ_zero]
[GOAL]
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t : Set 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
[PROOFSTEP]
rw [← one_mul (au * av), ← habz, add_mul, ← add_assoc, add_add_add_comm, mul_assoc, ← mul_add, mul_assoc, ← mul_add,
  mul_comm av, ← add_mul, ← mul_add, add_comm bu, add_comm bv, habu, habv, one_mul, mul_one]
[GOAL]
case intro.intro.intro.intro.intro.inr.intro.intro.intro.intro.intro.inr.intro.intro.intro.intro.intro.refine'_4
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t : Set 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
⊢ (az * av / (az * av + bz * au) * bu) • p + (bz * au / (az * av + bz * au) * bv) • q +
      ((az * av / (az * av + bz * au)) • au • x + (bz * au / (az * av + bz * au)) • av • y) ∈
    ↑(convexHull 𝕜) {p, q, az • x + bz • y}
[PROOFSTEP]
have hz : ∀ i, z i ∈ ({p, q, az • x + bz • y} : Set E) := fun i => by fin_cases i <;> simp
[GOAL]
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t : Set 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
⊢ z i ∈ {p, q, az • x + bz • y}
[PROOFSTEP]
fin_cases i
[GOAL]
case head
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t : Set 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
⊢ z { val := 0, isLt := (_ : 0 < 3) } ∈ {p, q, az • x + bz • y}
[PROOFSTEP]
simp
[GOAL]
case tail.head
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t : Set 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
⊢ z { val := 1, isLt := (_ : (fun a => a < 3) 1) } ∈ {p, q, az • x + bz • y}
[PROOFSTEP]
simp
[GOAL]
case tail.tail.head
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t : Set 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
⊢ z { val := 2, isLt := (_ : (fun a => (fun a => a < 3) a) 2) } ∈ {p, q, az • x + bz • y}
[PROOFSTEP]
simp
[GOAL]
case intro.intro.intro.intro.intro.inr.intro.intro.intro.intro.intro.inr.intro.intro.intro.intro.intro.refine'_4
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t : Set 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), z i ∈ {p, q, az • x + bz • y}
⊢ (az * av / (az * av + bz * au) * bu) • p + (bz * au / (az * av + bz * au) * bv) • q +
      ((az * av / (az * av + bz * au)) • au • x + (bz * au / (az * av + bz * au)) • av • y) ∈
    ↑(convexHull 𝕜) {p, q, az • x + bz • y}
[PROOFSTEP]
convert Finset.centerMass_mem_convexHull (Finset.univ : Finset (Fin 3)) (fun i _ => hw₀ i) (by rwa [hw]) fun i _ => hz i
[GOAL]
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t : Set 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), z i ∈ {p, q, az • x + bz • y}
⊢ 0 < ∑ i : Fin 3, w i
[PROOFSTEP]
rwa [hw]
[GOAL]
case h.e'_4
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t : Set 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), z i ∈ {p, q, az • x + bz • y}
⊢ (az * av / (az * av + bz * au) * bu) • p + (bz * au / (az * av + bz * au) * bv) • q +
      ((az * av / (az * av + bz * au)) • au • x + (bz * au / (az * av + bz * au)) • av • y) =
    Finset.centerMass Finset.univ (fun i => w i) fun i => z i
[PROOFSTEP]
rw [Finset.centerMass]
[GOAL]
case h.e'_4
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t : Set 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), z i ∈ {p, q, az • x + bz • y}
⊢ (az * av / (az * av + bz * au) * bu) • p + (bz * au / (az * av + bz * au) * bv) • q +
      ((az * av / (az * av + bz * au)) • au • x + (bz * au / (az * av + bz * au)) • av • y) =
    (∑ i : Fin 3, w i)⁻¹ • ∑ i : Fin 3, w i • z i
[PROOFSTEP]
simp_rw [div_eq_inv_mul, hw, mul_assoc, mul_smul (az * av + bz * au)⁻¹, ← smul_add, add_assoc, ← mul_assoc]
[GOAL]
case h.e'_4
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t : Set 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), z i ∈ {p, q, az • x + bz • y}
⊢ (az * av + bz * au)⁻¹ • ((az * av * bu) • p + ((bz * au * bv) • q + ((az * av) • au • x + (bz * au) • av • y))) =
    (az * av + bz * au)⁻¹ •
      ∑ x_1 : Fin 3,
        Matrix.vecCons (az * av * bu) ![bz * au * bv, au * av] x_1 • Matrix.vecCons p ![q, az • x + bz • y] x_1
[PROOFSTEP]
congr 3
[GOAL]
case h.e'_4.e_a.e_a.e_a
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t : Set 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), z i ∈ {p, q, az • x + bz • y}
⊢ (az * av) • au • x + (bz * au) • av • y =
    List.foldr (fun x x_1 => x + x_1) 0
      (List.map
        (fun x_1 =>
          Matrix.vecCons (az * av * bu) ![bz * au * bv, au * av] x_1 • Matrix.vecCons p ![q, az • x + bz • y] x_1)
        (List.pmap Fin.mk [2] (_ : ∀ (x : ℕ), x ∈ [2] → (fun a => a < 3) x)))
[PROOFSTEP]
rw [← mul_smul, ← mul_rotate, mul_right_comm, mul_smul, ← mul_smul _ av, mul_rotate, mul_smul _ bz, ← smul_add]
[GOAL]
case h.e'_4.e_a.e_a.e_a
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t : Set 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), z i ∈ {p, q, az • x + bz • y}
⊢ (au * av) • (az • x + bz • y) =
    List.foldr (fun x x_1 => x + x_1) 0
      (List.map
        (fun x_1 =>
          Matrix.vecCons (az * av * bu) ![bz * au * bv, au * av] x_1 • Matrix.vecCons p ![q, az • x + bz • y] x_1)
        (List.pmap Fin.mk [2] (_ : ∀ (x : ℕ), x ∈ [2] → (fun a => a < 3) x)))
[PROOFSTEP]
simp only [smul_add, List.foldr, Matrix.cons_val_succ', Fin.mk_one, Matrix.cons_val_one, Matrix.head_cons, add_zero]
[GOAL]
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
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ᶜ
[PROOFSTEP]
let S : Set (Set E) := {C | Convex 𝕜 C ∧ Disjoint C t}
[GOAL]
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
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ᶜ
[PROOFSTEP]
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⟩
[GOAL]
case intro.intro.intro
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
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ᶜ
[PROOFSTEP]
refine' ⟨C, hC.1, convex_iff_segment_subset.2 fun x hx y hy z hz hzC => _, hsC, hC.2.subset_compl_left⟩
[GOAL]
case intro.intro.intro
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
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
[PROOFSTEP]
suffices h : ∀ c ∈ Cᶜ, ∃ a ∈ C, (segment 𝕜 c a ∩ t).Nonempty
[GOAL]
case intro.intro.intro
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
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
[PROOFSTEP]
obtain ⟨p, hp, u, hu, hut⟩ := h x hx
[GOAL]
case intro.intro.intro.intro.intro.intro.intro
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
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
[PROOFSTEP]
obtain ⟨q, hq, v, hv, hvt⟩ := h y hy
[GOAL]
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
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
[PROOFSTEP]
refine'
  not_disjoint_segment_convexHull_triple hz hu hv (hC.2.symm.mono (ht.segment_subset hut hvt) <| convexHull_min _ hC.1)
[GOAL]
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
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
[PROOFSTEP]
simpa [insert_subset_iff, hp, hq, singleton_subset_iff.2 hzC]
[GOAL]
case h
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
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)
[PROOFSTEP]
rintro c hc
[GOAL]
case h
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
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)
[PROOFSTEP]
by_contra' h
[GOAL]
case h
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
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
[PROOFSTEP]
suffices h : Disjoint (convexHull 𝕜 (insert c C)) t
[GOAL]
case h
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
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 𝕜) (insert c C)) t
⊢ False
[PROOFSTEP]
rw [← hCmax _ ⟨convex_convexHull _ _, h⟩ ((subset_insert _ _).trans <| subset_convexHull _ _)] at hc 
[GOAL]
case h
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
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 𝕜) (insert c C))ᶜ
h✝ : ∀ (a : E), a ∈ C → ¬Set.Nonempty (segment 𝕜 c a ∩ t)
h : Disjoint (↑(convexHull 𝕜) (insert c C)) t
⊢ False
[PROOFSTEP]
exact hc (subset_convexHull _ _ <| mem_insert _ _)
[GOAL]
case h
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
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 𝕜) (insert c C)) t
[PROOFSTEP]
rw [convexHull_insert ⟨z, hzC⟩, convexJoin_singleton_left]
[GOAL]
case h
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
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 𝕜) C), segment 𝕜 c y) t
[PROOFSTEP]
refine' disjoint_iUnion₂_left.2 fun a ha => disjoint_iff_inf_le.mpr fun b hb => h a _ ⟨b, hb⟩
[GOAL]
case h
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
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 𝕜) C
b : E
hb : b ∈ segment 𝕜 c a ⊓ t
⊢ a ∈ C
[PROOFSTEP]
rwa [← hC.1.convexHull_eq]
