case h.mk
𝕜 : Type u_3
E : Type u_1
F : Type u_2
G : Type ?u.327345
ι : Type ?u.327348
π : ι → Type ?u.327353
inst✝⁴ : OrderedSemiring 𝕜
inst✝³ : AddCommMonoid E
inst✝² : AddCommMonoid F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
x : E
y₁ y₂ : F
x' : E
y' : F
⊢ (x', y') ∈ (fun y => (x, y)) '' [y₁-[𝕜]y₂] ↔ (x', y') ∈ [(x, y₁)-[𝕜](x, y₂)]
𝕜 : Type u_3
E : Type u_1
F : Type u_2
G : Type ?u.327345
ι : Type ?u.327348
π : ι → Type ?u.327353
inst✝⁴ : OrderedSemiring 𝕜
inst✝³ : AddCommMonoid E
inst✝² : AddCommMonoid F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
x : E
y₁ y₂ : F
⊢ (fun y => (x, y)) '' [y₁-[𝕜]y₂] = [(x, y₁)-[𝕜](x, y₂)]
ext ⟨x', y'⟩
case h.mk
𝕜 : Type u_3
E : Type u_1
F : Type u_2
G : Type ?u.327345
ι : Type ?u.327348
π : ι → Type ?u.327353
inst✝⁴ : OrderedSemiring 𝕜
inst✝³ : AddCommMonoid E
inst✝² : AddCommMonoid F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
x : E
y₁ y₂ : F
x' : E
y' : F
⊢ (∃ b b_1 h h h, x = x' ∧ b • y₁ + b_1 • y₂ = y') ↔ ∃ a b h h h, a • x + b • x = x' ∧ a • y₁ + b • y₂ = y'
case h.mk
𝕜 : Type u_3
E : Type u_1
F : Type u_2
G : Type ?u.327345
ι : Type ?u.327348
π : ι → Type ?u.327353
inst✝⁴ : OrderedSemiring 𝕜
inst✝³ : AddCommMonoid E
inst✝² : AddCommMonoid F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
x : E
y₁ y₂ : F
x' : E
y' : F
⊢ (x', y') ∈ (fun y => (x, y)) '' [y₁-[𝕜]y₂] ↔ (x', y') ∈ [(x, y₁)-[𝕜](x, y₂)]
simp_rw [Set.mem_image, segment, Set.mem_setOf, Prod.smul_mk, Prod.mk_add_mk, Prod.mk.inj_iff, ←
  exists_and_right, @exists_comm F, exists_eq_left']
case h.mk
𝕜 : Type u_3
E : Type u_1
F : Type u_2
G : Type ?u.327345
ι : Type ?u.327348
π : ι → Type ?u.327353
inst✝⁴ : OrderedSemiring 𝕜
inst✝³ : AddCommMonoid E
inst✝² : AddCommMonoid F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
x : E
y₁ y₂ : F
x' : E
y' : F
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ x = x' ∧ a • y₁ + b • y₂ = y' ↔ a • x + b • x = x' ∧ a • y₁ + b • y₂ = y'
case h.mk
𝕜 : Type u_3
E : Type u_1
F : Type u_2
G : Type ?u.327345
ι : Type ?u.327348
π : ι → Type ?u.327353
inst✝⁴ : OrderedSemiring 𝕜
inst✝³ : AddCommMonoid E
inst✝² : AddCommMonoid F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
x : E
y₁ y₂ : F
x' : E
y' : F
⊢ (∃ b b_1 h h h, x = x' ∧ b • y₁ + b_1 • y₂ = y') ↔ ∃ a b h h h, a • x + b • x = x' ∧ a • y₁ + b • y₂ = y'
refine' exists₅_congr fun a b ha hb hab => _
no goals
case h.mk
𝕜 : Type u_3
E : Type u_1
F : Type u_2
G : Type ?u.327345
ι : Type ?u.327348
π : ι → Type ?u.327353
inst✝⁴ : OrderedSemiring 𝕜
inst✝³ : AddCommMonoid E
inst✝² : AddCommMonoid F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
x : E
y₁ y₂ : F
x' : E
y' : F
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ x = x' ∧ a • y₁ + b • y₂ = y' ↔ a • x + b • x = x' ∧ a • y₁ + b • y₂ = y'
rw [Convex.combo_self hab]