case intro.intro.intro.intro.intro
𝕜 : Type u_3
E : Type ?u.376048
F : Type ?u.376051
G : Type ?u.376054
ι : 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 => [x i-[𝕜]y i]) i
𝕜 : Type u_3
E : Type ?u.376048
F : Type ?u.376051
G : Type ?u.376054
ι : Type u_1
π : ι → Type u_2
inst✝² : OrderedSemiring 𝕜
inst✝¹ : (i : ι) → AddCommMonoid (π i)
inst✝ : (i : ι) → Module 𝕜 (π i)
s : Set ι
x y : (i : ι) → π i
⊢ [x-[𝕜]y] ⊆ pi s fun i => [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.376048
F : Type ?u.376051
G : Type ?u.376054
ι : 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 => [x i-[𝕜]y i]) i
exact ⟨a, b, ha, hb, hab, congr_fun hz i⟩