case inl.intro
𝕜 : Type u_1
E : Type u_2
F : Type ?u.262136
β : Type ?u.262139
inst✝⁴ : LinearOrderedField 𝕜
inst✝³ : AddCommGroup E
inst✝² : AddCommGroup F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
s : Set E
h : Convex 𝕜 s
x y : E
hx : x ∈ s
hy : y ∈ s
hp hq : 0 ≤ 0
⊢ ∃ z, z ∈ s ∧ (0 + 0) • z = 0 • x + 0 • y

case inr
𝕜 : Type u_1
E : Type u_2
F : Type ?u.262136
β : Type ?u.262139
inst✝⁴ : LinearOrderedField 𝕜
inst✝³ : AddCommGroup E
inst✝² : AddCommGroup F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
s : Set E
h : Convex 𝕜 s
x y : E
p q : 𝕜
hx : x ∈ s
hy : y ∈ s
hp : 0 ≤ p
hq : 0 ≤ q
hpq : ¬(p = 0 ∧ q = 0)
⊢ ∃ z, z ∈ s ∧ (p + q) • z = p • x + q • y
𝕜 : Type u_1
E : Type u_2
F : Type ?u.262136
β : Type ?u.262139
inst✝⁴ : LinearOrderedField 𝕜
inst✝³ : AddCommGroup E
inst✝² : AddCommGroup F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
s : Set E
h : Convex 𝕜 s
x y : E
p q : 𝕜
hx : x ∈ s
hy : y ∈ s
hp : 0 ≤ p
hq : 0 ≤ q
⊢ ∃ z, z ∈ s ∧ (p + q) • z = p • x + q • y
rcases _root_.em (p = 0 ∧ q = 0) with (⟨rfl, rfl⟩ | hpq)
case inl.intro
𝕜 : Type u_1
E : Type u_2
F : Type ?u.262136
β : Type ?u.262139
inst✝⁴ : LinearOrderedField 𝕜
inst✝³ : AddCommGroup E
inst✝² : AddCommGroup F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
s : Set E
h : Convex 𝕜 s
x y : E
hx : x ∈ s
hy : y ∈ s
hp hq : 0 ≤ 0
⊢ (0 + 0) • x = 0 • x + 0 • y
case inl.intro
𝕜 : Type u_1
E : Type u_2
F : Type ?u.262136
β : Type ?u.262139
inst✝⁴ : LinearOrderedField 𝕜
inst✝³ : AddCommGroup E
inst✝² : AddCommGroup F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
s : Set E
h : Convex 𝕜 s
x y : E
hx : x ∈ s
hy : y ∈ s
hp hq : 0 ≤ 0
⊢ ∃ z, z ∈ s ∧ (0 + 0) • z = 0 • x + 0 • y
use x, hx
no goals
case inl.intro
𝕜 : Type u_1
E : Type u_2
F : Type ?u.262136
β : Type ?u.262139
inst✝⁴ : LinearOrderedField 𝕜
inst✝³ : AddCommGroup E
inst✝² : AddCommGroup F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
s : Set E
h : Convex 𝕜 s
x y : E
hx : x ∈ s
hy : y ∈ s
hp hq : 0 ≤ 0
⊢ (0 + 0) • x = 0 • x + 0 • y
simp
case inr
𝕜 : Type u_1
E : Type u_2
F : Type ?u.262136
β : Type ?u.262139
inst✝⁴ : LinearOrderedField 𝕜
inst✝³ : AddCommGroup E
inst✝² : AddCommGroup F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
s : Set E
h : Convex 𝕜 s
x y : E
p q : 𝕜
hx : x ∈ s
hy : y ∈ s
hp : 0 ≤ p
hq : 0 ≤ q
hpq : 0 < p + q
⊢ ∃ z, z ∈ s ∧ (p + q) • z = p • x + q • y
case inr
𝕜 : Type u_1
E : Type u_2
F : Type ?u.262136
β : Type ?u.262139
inst✝⁴ : LinearOrderedField 𝕜
inst✝³ : AddCommGroup E
inst✝² : AddCommGroup F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
s : Set E
h : Convex 𝕜 s
x y : E
p q : 𝕜
hx : x ∈ s
hy : y ∈ s
hp : 0 ≤ p
hq : 0 ≤ q
hpq : ¬(p = 0 ∧ q = 0)
⊢ ∃ z, z ∈ s ∧ (p + q) • z = p • x + q • y
replace hpq : 0 < p + q := (add_nonneg hp hq).lt_of_ne' (mt (add_eq_zero_iff' hp hq).1 hpq)
case inr
𝕜 : Type u_1
E : Type u_2
F : Type ?u.262136
β : Type ?u.262139
inst✝⁴ : LinearOrderedField 𝕜
inst✝³ : AddCommGroup E
inst✝² : AddCommGroup F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
s : Set E
h : Convex 𝕜 s
x y : E
p q : 𝕜
hx : x ∈ s
hy : y ∈ s
hp : 0 ≤ p
hq : 0 ≤ q
hpq : 0 < p + q
⊢ (p + q) • ((p / (p + q)) • x + (q / (p + q)) • y) = p • x + q • y
case inr
𝕜 : Type u_1
E : Type u_2
F : Type ?u.262136
β : Type ?u.262139
inst✝⁴ : LinearOrderedField 𝕜
inst✝³ : AddCommGroup E
inst✝² : AddCommGroup F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
s : Set E
h : Convex 𝕜 s
x y : E
p q : 𝕜
hx : x ∈ s
hy : y ∈ s
hp : 0 ≤ p
hq : 0 ≤ q
hpq : 0 < p + q
⊢ ∃ z, z ∈ s ∧ (p + q) • z = p • x + q • y
refine ⟨_, convex_iff_div.1 h hx hy hp hq hpq, ?_⟩
no goals
case inr
𝕜 : Type u_1
E : Type u_2
F : Type ?u.262136
β : Type ?u.262139
inst✝⁴ : LinearOrderedField 𝕜
inst✝³ : AddCommGroup E
inst✝² : AddCommGroup F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
s : Set E
h : Convex 𝕜 s
x y : E
p q : 𝕜
hx : x ∈ s
hy : y ∈ s
hp : 0 ≤ p
hq : 0 ≤ q
hpq : 0 < p + q
⊢ (p + q) • ((p / (p + q)) • x + (q / (p + q)) • y) = p • x + q • y
simp only [smul_add, smul_smul, mul_div_cancel' _ hpq.ne']