case mp
𝕜 : Type u_2
E : Type u_1
F : Type ?u.200437
G : Type ?u.200440
ι : Type ?u.200443
π : ι → Type ?u.200448
inst✝² : LinearOrderedSemifield 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
x y z : E
⊢ x ∈ openSegment 𝕜 y z → ∃ a b, 0 < a ∧ 0 < b ∧ (a / (a + b)) • y + (b / (a + b)) • z = x

case mpr
𝕜 : Type u_2
E : Type u_1
F : Type ?u.200437
G : Type ?u.200440
ι : Type ?u.200443
π : ι → Type ?u.200448
inst✝² : LinearOrderedSemifield 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
x y z : E
⊢ (∃ a b, 0 < a ∧ 0 < b ∧ (a / (a + b)) • y + (b / (a + b)) • z = x) → x ∈ openSegment 𝕜 y z
𝕜 : Type u_2
E : Type u_1
F : Type ?u.200437
G : Type ?u.200440
ι : Type ?u.200443
π : ι → Type ?u.200448
inst✝² : LinearOrderedSemifield 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
x y z : E
⊢ x ∈ openSegment 𝕜 y z ↔ ∃ a b, 0 < a ∧ 0 < b ∧ (a / (a + b)) • y + (b / (a + b)) • z = x
constructor
case mp.intro.intro.intro.intro.intro
𝕜 : Type u_2
E : Type u_1
F : Type ?u.200437
G : Type ?u.200440
ι : Type ?u.200443
π : ι → Type ?u.200448
inst✝² : LinearOrderedSemifield 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
y z : E
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
⊢ ∃ a_1 b_1, 0 < a_1 ∧ 0 < b_1 ∧ (a_1 / (a_1 + b_1)) • y + (b_1 / (a_1 + b_1)) • z = a • y + b • z
case mp
𝕜 : Type u_2
E : Type u_1
F : Type ?u.200437
G : Type ?u.200440
ι : Type ?u.200443
π : ι → Type ?u.200448
inst✝² : LinearOrderedSemifield 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
x y z : E
⊢ x ∈ openSegment 𝕜 y z → ∃ a b, 0 < a ∧ 0 < b ∧ (a / (a + b)) • y + (b / (a + b)) • z = x
rintro ⟨a, b, ha, hb, hab, rfl⟩
case mp.intro.intro.intro.intro.intro
𝕜 : Type u_2
E : Type u_1
F : Type ?u.200437
G : Type ?u.200440
ι : Type ?u.200443
π : ι → Type ?u.200448
inst✝² : LinearOrderedSemifield 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
y z : E
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
⊢ (a / (a + b)) • y + (b / (a + b)) • z = a • y + b • z
case mp.intro.intro.intro.intro.intro
𝕜 : Type u_2
E : Type u_1
F : Type ?u.200437
G : Type ?u.200440
ι : Type ?u.200443
π : ι → Type ?u.200448
inst✝² : LinearOrderedSemifield 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
y z : E
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
⊢ ∃ a_1 b_1, 0 < a_1 ∧ 0 < b_1 ∧ (a_1 / (a_1 + b_1)) • y + (b_1 / (a_1 + b_1)) • z = a • y + b • z
use a, b, ha, hb
no goals
case mp.intro.intro.intro.intro.intro
𝕜 : Type u_2
E : Type u_1
F : Type ?u.200437
G : Type ?u.200440
ι : Type ?u.200443
π : ι → Type ?u.200448
inst✝² : LinearOrderedSemifield 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
y z : E
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
⊢ (a / (a + b)) • y + (b / (a + b)) • z = a • y + b • z
rw [hab, div_one, div_one]
case mpr.intro.intro.intro.intro
𝕜 : Type u_2
E : Type u_1
F : Type ?u.200437
G : Type ?u.200440
ι : Type ?u.200443
π : ι → Type ?u.200448
inst✝² : LinearOrderedSemifield 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
y z : E
a b : 𝕜
ha : 0 < a
hb : 0 < b
⊢ (a / (a + b)) • y + (b / (a + b)) • z ∈ openSegment 𝕜 y z
case mpr
𝕜 : Type u_2
E : Type u_1
F : Type ?u.200437
G : Type ?u.200440
ι : Type ?u.200443
π : ι → Type ?u.200448
inst✝² : LinearOrderedSemifield 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
x y z : E
⊢ (∃ a b, 0 < a ∧ 0 < b ∧ (a / (a + b)) • y + (b / (a + b)) • z = x) → x ∈ openSegment 𝕜 y z
rintro ⟨a, b, ha, hb, rfl⟩
case mpr.intro.intro.intro.intro
𝕜 : Type u_2
E : Type u_1
F : Type ?u.200437
G : Type ?u.200440
ι : Type ?u.200443
π : ι → Type ?u.200448
inst✝² : LinearOrderedSemifield 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
y z : E
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : 0 < a + b
⊢ (a / (a + b)) • y + (b / (a + b)) • z ∈ openSegment 𝕜 y z
case mpr.intro.intro.intro.intro
𝕜 : Type u_2
E : Type u_1
F : Type ?u.200437
G : Type ?u.200440
ι : Type ?u.200443
π : ι → Type ?u.200448
inst✝² : LinearOrderedSemifield 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
y z : E
a b : 𝕜
ha : 0 < a
hb : 0 < b
⊢ (a / (a + b)) • y + (b / (a + b)) • z ∈ openSegment 𝕜 y z
have hab : 0 < a + b := by positivity
case mpr.intro.intro.intro.intro
𝕜 : Type u_2
E : Type u_1
F : Type ?u.200437
G : Type ?u.200440
ι : Type ?u.200443
π : ι → Type ?u.200448
inst✝² : LinearOrderedSemifield 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
y z : E
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : 0 < a + b
⊢ a / (a + b) + b / (a + b) = 1
case mpr.intro.intro.intro.intro
𝕜 : Type u_2
E : Type u_1
F : Type ?u.200437
G : Type ?u.200440
ι : Type ?u.200443
π : ι → Type ?u.200448
inst✝² : LinearOrderedSemifield 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
y z : E
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : 0 < a + b
⊢ (a / (a + b)) • y + (b / (a + b)) • z ∈ openSegment 𝕜 y z
refine' ⟨a / (a + b), b / (a + b), by positivity, by positivity, _, rfl⟩
no goals
case mpr.intro.intro.intro.intro
𝕜 : Type u_2
E : Type u_1
F : Type ?u.200437
G : Type ?u.200440
ι : Type ?u.200443
π : ι → Type ?u.200448
inst✝² : LinearOrderedSemifield 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
y z : E
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : 0 < a + b
⊢ a / (a + b) + b / (a + b) = 1
rw [← add_div, div_self hab.ne']
no goals
𝕜 : Type u_2
E : Type u_1
F : Type ?u.200437
G : Type ?u.200440
ι : Type ?u.200443
π : ι → Type ?u.200448
inst✝² : LinearOrderedSemifield 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
y z : E
a b : 𝕜
ha : 0 < a
hb : 0 < b
⊢ 0 < a + b
positivity
no goals
𝕜 : Type u_2
E : Type u_1
F : Type ?u.200437
G : Type ?u.200440
ι : Type ?u.200443
π : ι → Type ?u.200448
inst✝² : LinearOrderedSemifield 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
y z : E
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : 0 < a + b
⊢ 0 < a / (a + b)
positivity
no goals
𝕜 : Type u_2
E : Type u_1
F : Type ?u.200437
G : Type ?u.200440
ι : Type ?u.200443
π : ι → Type ?u.200448
inst✝² : LinearOrderedSemifield 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
y z : E
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : 0 < a + b
⊢ 0 < b / (a + b)
positivity