case mp
𝕜 : Type u_2
E : Type u_1
F : Type ?u.184015
G : Type ?u.184018
ι : Type ?u.184021
π : ι → Type ?u.184026
inst✝² : LinearOrderedSemifield 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
x y z : E
⊢ x ∈ [y-[𝕜]z] → ∃ a b, 0 ≤ a ∧ 0 ≤ b ∧ 0 < a + b ∧ (a / (a + b)) • y + (b / (a + b)) • z = x

case mpr
𝕜 : Type u_2
E : Type u_1
F : Type ?u.184015
G : Type ?u.184018
ι : Type ?u.184021
π : ι → Type ?u.184026
inst✝² : LinearOrderedSemifield 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
x y z : E
⊢ (∃ a b, 0 ≤ a ∧ 0 ≤ b ∧ 0 < a + b ∧ (a / (a + b)) • y + (b / (a + b)) • z = x) → x ∈ [y-[𝕜]z]
𝕜 : Type u_2
E : Type u_1
F : Type ?u.184015
G : Type ?u.184018
ι : Type ?u.184021
π : ι → Type ?u.184026
inst✝² : LinearOrderedSemifield 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
x y z : E
⊢ x ∈ [y-[𝕜]z] ↔ ∃ a b, 0 ≤ a ∧ 0 ≤ b ∧ 0 < a + 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.184015
G : Type ?u.184018
ι : Type ?u.184021
π : ι → Type ?u.184026
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 ∧ 0 < a_1 + 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.184015
G : Type ?u.184018
ι : Type ?u.184021
π : ι → Type ?u.184026
inst✝² : LinearOrderedSemifield 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
x y z : E
⊢ x ∈ [y-[𝕜]z] → ∃ a b, 0 ≤ a ∧ 0 ≤ b ∧ 0 < a + 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.184015
G : Type ?u.184018
ι : Type ?u.184021
π : ι → Type ?u.184026
inst✝² : LinearOrderedSemifield 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
y z : E
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ 0 < a + b ∧ (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.184015
G : Type ?u.184018
ι : Type ?u.184021
π : ι → Type ?u.184026
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 ∧ 0 < a_1 + 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.184015
G : Type ?u.184018
ι : Type ?u.184021
π : ι → Type ?u.184026
inst✝² : LinearOrderedSemifield 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
y z : E
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ 0 < a + b ∧ (a / (a + b)) • y + (b / (a + b)) • z = a • y + b • z
simp [*]
case mpr.intro.intro.intro.intro.intro
𝕜 : Type u_2
E : Type u_1
F : Type ?u.184015
G : Type ?u.184018
ι : Type ?u.184021
π : ι → Type ?u.184026
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 ∈ [y-[𝕜]z]
case mpr
𝕜 : Type u_2
E : Type u_1
F : Type ?u.184015
G : Type ?u.184018
ι : Type ?u.184021
π : ι → Type ?u.184026
inst✝² : LinearOrderedSemifield 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
x y z : E
⊢ (∃ a b, 0 ≤ a ∧ 0 ≤ b ∧ 0 < a + b ∧ (a / (a + b)) • y + (b / (a + b)) • z = x) → x ∈ [y-[𝕜]z]
rintro ⟨a, b, ha, hb, hab, rfl⟩
case mpr.intro.intro.intro.intro.intro
𝕜 : Type u_2
E : Type u_1
F : Type ?u.184015
G : Type ?u.184018
ι : Type ?u.184021
π : ι → Type ?u.184026
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.intro
𝕜 : Type u_2
E : Type u_1
F : Type ?u.184015
G : Type ?u.184018
ι : Type ?u.184021
π : ι → Type ?u.184026
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 ∈ [y-[𝕜]z]
refine' ⟨a / (a + b), b / (a + b), by positivity, by positivity, _, rfl⟩
no goals
case mpr.intro.intro.intro.intro.intro
𝕜 : Type u_2
E : Type u_1
F : Type ?u.184015
G : Type ?u.184018
ι : Type ?u.184021
π : ι → Type ?u.184026
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.184015
G : Type ?u.184018
ι : Type ?u.184021
π : ι → Type ?u.184026
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.184015
G : Type ?u.184018
ι : Type ?u.184021
π : ι → Type ?u.184026
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