case intro.intro.intro.intro.intro
𝕜 : Type u_3
E : Type ?u.380819
F : Type ?u.380822
G : Type ?u.380825
ι : Type u_1
π : ι → Type u_2
inst✝² : OrderedSemiring 𝕜
inst✝¹ : (i : ι) → AddCommMonoid (π i)
inst✝ : (i : ι) → Module 𝕜 (π i)
s : Set ι
x y z : (i : ι) → π i
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
hz : a • x + b • y = z
i : ι
⊢ z i ∈ (fun i => openSegment 𝕜 (x i) (y i)) i
𝕜 : Type u_3
E : Type ?u.380819
F : Type ?u.380822
G : Type ?u.380825
ι : Type u_1
π : ι → Type u_2
inst✝² : OrderedSemiring 𝕜
inst✝¹ : (i : ι) → AddCommMonoid (π i)
inst✝ : (i : ι) → Module 𝕜 (π i)
s : Set ι
x y : (i : ι) → π i
⊢ openSegment 𝕜 x y ⊆ pi s fun i => openSegment 𝕜 (x i) (y i)
rintro z ⟨a, b, ha, hb, hab, hz⟩ i -
no goals
case intro.intro.intro.intro.intro
𝕜 : Type u_3
E : Type ?u.380819
F : Type ?u.380822
G : Type ?u.380825
ι : Type u_1
π : ι → Type u_2
inst✝² : OrderedSemiring 𝕜
inst✝¹ : (i : ι) → AddCommMonoid (π i)
inst✝ : (i : ι) → Module 𝕜 (π i)
s : Set ι
x y z : (i : ι) → π i
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
hz : a • x + b • y = z
i : ι
⊢ z i ∈ (fun i => openSegment 𝕜 (x i) (y i)) i
exact ⟨a, b, ha, hb, hab, congr_fun hz i⟩