case intro.intro.intro.intro.intro
𝕜 : Type u_3
E : Type u_1
F : Type u_2
G : Type ?u.301724
ι : Type ?u.301727
π : ι → Type ?u.301732
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 ∈ [x.fst-[𝕜]y.fst] ×ˢ [x.snd-[𝕜]y.snd]
𝕜 : Type u_3
E : Type u_1
F : Type u_2
G : Type ?u.301724
ι : Type ?u.301727
π : ι → Type ?u.301732
inst✝⁴ : OrderedSemiring 𝕜
inst✝³ : AddCommMonoid E
inst✝² : AddCommMonoid F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
x y : E × F
⊢ [x-[𝕜]y] ⊆ [x.fst-[𝕜]y.fst] ×ˢ [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.301724
ι : Type ?u.301727
π : ι → Type ?u.301732
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 ∈ [x.fst-[𝕜]y.fst] ×ˢ [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⟩