case h
𝕜 : Type u_3
E : Type ?u.408197
F : Type ?u.408200
G : Type ?u.408203
ι : 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 '' openSegment 𝕜 x₁ x₂ ↔ z ∈ openSegment 𝕜 (update y i x₁) (update y i x₂)
𝕜 : Type u_3
E : Type ?u.408197
F : Type ?u.408200
G : Type ?u.408203
ι : 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 '' openSegment 𝕜 x₁ x₂ = openSegment 𝕜 (update y i x₁) (update y i x₂)
ext z
case h
𝕜 : Type u_3
E : Type ?u.408197
F : Type ?u.408200
G : Type ?u.408203
ι : 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.408197
F : Type ?u.408200
G : Type ?u.408203
ι : 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 '' openSegment 𝕜 x₁ x₂ ↔ z ∈ openSegment 𝕜 (update y i x₁) (update y i x₂)
simp_rw [Set.mem_image, openSegment, 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.408197
F : Type ?u.408200
G : Type ?u.408203
ι : 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.408197
F : Type ?u.408200
G : Type ?u.408203
ι : 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.408197
F : Type ?u.408200
G : Type ?u.408203
ι : 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]