case intro.intro.intro.intro.intro
𝕜 : Type u_3
E : Type u_1
F : Type u_2
G : Type ?u.305510
ι : Type ?u.305513
π : ι → Type ?u.305518
inst✝⁴ : OrderedSemiring 𝕜
inst✝³ : AddCommMonoid E
inst✝² : AddCommMonoid F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
x y z : E × F
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
hz : a • x + b • y = z
⊢ z ∈ openSegment 𝕜 x.fst y.fst ×ˢ openSegment 𝕜 x.snd y.snd
𝕜 : Type u_3
E : Type u_1
F : Type u_2
G : Type ?u.305510
ι : Type ?u.305513
π : ι → Type ?u.305518
inst✝⁴ : OrderedSemiring 𝕜
inst✝³ : AddCommMonoid E
inst✝² : AddCommMonoid F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
x y : E × F
⊢ openSegment 𝕜 x y ⊆ openSegment 𝕜 x.fst y.fst ×ˢ openSegment 𝕜 x.snd y.snd
rintro z ⟨a, b, ha, hb, hab, hz⟩
no goals
case intro.intro.intro.intro.intro
𝕜 : Type u_3
E : Type u_1
F : Type u_2
G : Type ?u.305510
ι : Type ?u.305513
π : ι → Type ?u.305518
inst✝⁴ : OrderedSemiring 𝕜
inst✝³ : AddCommMonoid E
inst✝² : AddCommMonoid F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
x y z : E × F
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
hz : a • x + b • y = z
⊢ z ∈ openSegment 𝕜 x.fst y.fst ×ˢ openSegment 𝕜 x.snd y.snd
exact ⟨⟨a, b, ha, hb, hab, congr_arg Prod.fst hz⟩, a, b, ha, hb, hab, congr_arg Prod.snd hz⟩