case h
𝕜 : Type u_3
E : Type ?u.385768
F : Type ?u.385771
G : Type ?u.385774
ι : Type u_1
π : ι → Type u_2
inst✝³ : OrderedSemiring 𝕜
inst✝² : (i : ι) → AddCommMonoid (π i)
inst✝¹ : (i : ι) → Module 𝕜 (π i)
s : Set ι
inst✝ : DecidableEq ι
i : ι
x₁ x₂ : π i
y z : (a : ι) → π a
⊢ z ∈ update y i '' [x₁-[𝕜]x₂] ↔ z ∈ [update y i x₁-[𝕜]update y i x₂]
𝕜 : Type u_3
E : Type ?u.385768
F : Type ?u.385771
G : Type ?u.385774
ι : Type u_1
π : ι → Type u_2
inst✝³ : OrderedSemiring 𝕜
inst✝² : (i : ι) → AddCommMonoid (π i)
inst✝¹ : (i : ι) → Module 𝕜 (π i)
s : Set ι
inst✝ : DecidableEq ι
i : ι
x₁ x₂ : π i
y : (i : ι) → π i
⊢ update y i '' [x₁-[𝕜]x₂] = [update y i x₁-[𝕜]update y i x₂]
ext z
case h
𝕜 : Type u_3
E : Type ?u.385768
F : Type ?u.385771
G : Type ?u.385774
ι : Type u_1
π : ι → Type u_2
inst✝³ : OrderedSemiring 𝕜
inst✝² : (i : ι) → AddCommMonoid (π i)
inst✝¹ : (i : ι) → Module 𝕜 (π i)
s : Set ι
inst✝ : DecidableEq ι
i : ι
x₁ x₂ : π i
y z : (a : ι) → π a
⊢ (∃ b b_1 h h h, b • x₁ + b_1 • x₂ = z i ∧ ∀ (x : ι), x ≠ i → y x = z x) ↔
    ∃ a b h h h, a • x₁ + b • x₂ = z i ∧ ∀ (x : ι), x ≠ i → (a • y + b • y) x = z x
case h
𝕜 : Type u_3
E : Type ?u.385768
F : Type ?u.385771
G : Type ?u.385774
ι : Type u_1
π : ι → Type u_2
inst✝³ : OrderedSemiring 𝕜
inst✝² : (i : ι) → AddCommMonoid (π i)
inst✝¹ : (i : ι) → Module 𝕜 (π i)
s : Set ι
inst✝ : DecidableEq ι
i : ι
x₁ x₂ : π i
y z : (a : ι) → π a
⊢ z ∈ update y i '' [x₁-[𝕜]x₂] ↔ z ∈ [update y i x₁-[𝕜]update y i x₂]
simp_rw [Set.mem_image, segment, Set.mem_setOf, ← update_smul, ← update_add, update_eq_iff, ←
  exists_and_right, @exists_comm (π i), exists_eq_left']
case h
𝕜 : Type u_3
E : Type ?u.385768
F : Type ?u.385771
G : Type ?u.385774
ι : Type u_1
π : ι → Type u_2
inst✝³ : OrderedSemiring 𝕜
inst✝² : (i : ι) → AddCommMonoid (π i)
inst✝¹ : (i : ι) → Module 𝕜 (π i)
s : Set ι
inst✝ : DecidableEq ι
i : ι
x₁ x₂ : π i
y z : (a : ι) → π a
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ (a • x₁ + b • x₂ = z i ∧ ∀ (x : ι), x ≠ i → y x = z x) ↔
    a • x₁ + b • x₂ = z i ∧ ∀ (x : ι), x ≠ i → (a • y + b • y) x = z x
case h
𝕜 : Type u_3
E : Type ?u.385768
F : Type ?u.385771
G : Type ?u.385774
ι : Type u_1
π : ι → Type u_2
inst✝³ : OrderedSemiring 𝕜
inst✝² : (i : ι) → AddCommMonoid (π i)
inst✝¹ : (i : ι) → Module 𝕜 (π i)
s : Set ι
inst✝ : DecidableEq ι
i : ι
x₁ x₂ : π i
y z : (a : ι) → π a
⊢ (∃ b b_1 h h h, b • x₁ + b_1 • x₂ = z i ∧ ∀ (x : ι), x ≠ i → y x = z x) ↔
    ∃ a b h h h, a • x₁ + b • x₂ = z i ∧ ∀ (x : ι), x ≠ i → (a • y + b • y) x = z x
refine' exists₅_congr fun a b ha hb hab => _
no goals
case h
𝕜 : Type u_3
E : Type ?u.385768
F : Type ?u.385771
G : Type ?u.385774
ι : Type u_1
π : ι → Type u_2
inst✝³ : OrderedSemiring 𝕜
inst✝² : (i : ι) → AddCommMonoid (π i)
inst✝¹ : (i : ι) → Module 𝕜 (π i)
s : Set ι
inst✝ : DecidableEq ι
i : ι
x₁ x₂ : π i
y z : (a : ι) → π a
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ (a • x₁ + b • x₂ = z i ∧ ∀ (x : ι), x ≠ i → y x = z x) ↔
    a • x₁ + b • x₂ = z i ∧ ∀ (x : ι), x ≠ i → (a • y + b • y) x = z x
rw [Convex.combo_self hab]