case intro.intro.intro.intro.intro.intro.intro.intro
𝕜 : Type u_1
𝕝 : Type ?u.78535
E : Type u_2
F : Type ?u.78541
β : Type ?u.78544
inst✝⁷ : OrderedSemiring 𝕜
inst✝⁶ : TopologicalSpace E
inst✝⁵ : TopologicalSpace F
inst✝⁴ : AddCommGroup E
inst✝³ : AddCommGroup F
inst✝² : Module 𝕜 E
inst✝¹ : Module 𝕜 F
inst✝ : ContinuousAdd E
s t : Set E
hs : StrictConvex 𝕜 s
ht : StrictConvex 𝕜 t
v w : E
hv : v ∈ s
hw : w ∈ t
x y : E
hx : x ∈ s
hy : y ∈ t
h : (fun x x_1 => x + x_1) v w ≠ (fun x x_1 => x + x_1) x y
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
⊢ a • (fun x x_1 => x + x_1) v w + b • (fun x x_1 => x + x_1) x y ∈ interior (s + t)
𝕜 : Type u_1
𝕝 : Type ?u.78535
E : Type u_2
F : Type ?u.78541
β : Type ?u.78544
inst✝⁷ : OrderedSemiring 𝕜
inst✝⁶ : TopologicalSpace E
inst✝⁵ : TopologicalSpace F
inst✝⁴ : AddCommGroup E
inst✝³ : AddCommGroup F
inst✝² : Module 𝕜 E
inst✝¹ : Module 𝕜 F
inst✝ : ContinuousAdd E
s t : Set E
hs : StrictConvex 𝕜 s
ht : StrictConvex 𝕜 t
⊢ StrictConvex 𝕜 (s + t)
rintro _ ⟨v, w, hv, hw, rfl⟩ _ ⟨x, y, hx, hy, rfl⟩ h a b ha hb hab
case intro.intro.intro.intro.intro.intro.intro.intro
𝕜 : Type u_1
𝕝 : Type ?u.78535
E : Type u_2
F : Type ?u.78541
β : Type ?u.78544
inst✝⁷ : OrderedSemiring 𝕜
inst✝⁶ : TopologicalSpace E
inst✝⁵ : TopologicalSpace F
inst✝⁴ : AddCommGroup E
inst✝³ : AddCommGroup F
inst✝² : Module 𝕜 E
inst✝¹ : Module 𝕜 F
inst✝ : ContinuousAdd E
s t : Set E
hs : StrictConvex 𝕜 s
ht : StrictConvex 𝕜 t
v w : E
hv : v ∈ s
hw : w ∈ t
x y : E
hx : x ∈ s
hy : y ∈ t
h : (fun x x_1 => x + x_1) v w ≠ (fun x x_1 => x + x_1) x y
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
⊢ a • v + b • x + (a • w + b • y) ∈ interior (s + t)
case intro.intro.intro.intro.intro.intro.intro.intro
𝕜 : Type u_1
𝕝 : Type ?u.78535
E : Type u_2
F : Type ?u.78541
β : Type ?u.78544
inst✝⁷ : OrderedSemiring 𝕜
inst✝⁶ : TopologicalSpace E
inst✝⁵ : TopologicalSpace F
inst✝⁴ : AddCommGroup E
inst✝³ : AddCommGroup F
inst✝² : Module 𝕜 E
inst✝¹ : Module 𝕜 F
inst✝ : ContinuousAdd E
s t : Set E
hs : StrictConvex 𝕜 s
ht : StrictConvex 𝕜 t
v w : E
hv : v ∈ s
hw : w ∈ t
x y : E
hx : x ∈ s
hy : y ∈ t
h : (fun x x_1 => x + x_1) v w ≠ (fun x x_1 => x + x_1) x y
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
⊢ a • (fun x x_1 => x + x_1) v w + b • (fun x x_1 => x + x_1) x y ∈ interior (s + t)
rw [smul_add, smul_add, add_add_add_comm]
case intro.intro.intro.intro.intro.intro.intro.intro.inl
𝕜 : Type u_1
𝕝 : Type ?u.78535
E : Type u_2
F : Type ?u.78541
β : Type ?u.78544
inst✝⁷ : OrderedSemiring 𝕜
inst✝⁶ : TopologicalSpace E
inst✝⁵ : TopologicalSpace F
inst✝⁴ : AddCommGroup E
inst✝³ : AddCommGroup F
inst✝² : Module 𝕜 E
inst✝¹ : Module 𝕜 F
inst✝ : ContinuousAdd E
s t : Set E
hs : StrictConvex 𝕜 s
ht : StrictConvex 𝕜 t
v w : E
hv : v ∈ s
hw : w ∈ t
y : E
hy : y ∈ t
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
hx : v ∈ s
h : (fun x x_1 => x + x_1) v w ≠ (fun x x_1 => x + x_1) v y
⊢ a • v + b • v + (a • w + b • y) ∈ interior (s + t)

case intro.intro.intro.intro.intro.intro.intro.intro.inr
𝕜 : Type u_1
𝕝 : Type ?u.78535
E : Type u_2
F : Type ?u.78541
β : Type ?u.78544
inst✝⁷ : OrderedSemiring 𝕜
inst✝⁶ : TopologicalSpace E
inst✝⁵ : TopologicalSpace F
inst✝⁴ : AddCommGroup E
inst✝³ : AddCommGroup F
inst✝² : Module 𝕜 E
inst✝¹ : Module 𝕜 F
inst✝ : ContinuousAdd E
s t : Set E
hs : StrictConvex 𝕜 s
ht : StrictConvex 𝕜 t
v w : E
hv : v ∈ s
hw : w ∈ t
x y : E
hx : x ∈ s
hy : y ∈ t
h : (fun x x_1 => x + x_1) v w ≠ (fun x x_1 => x + x_1) x y
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
hvx : v ≠ x
⊢ a • v + b • x + (a • w + b • y) ∈ interior (s + t)
case intro.intro.intro.intro.intro.intro.intro.intro
𝕜 : Type u_1
𝕝 : Type ?u.78535
E : Type u_2
F : Type ?u.78541
β : Type ?u.78544
inst✝⁷ : OrderedSemiring 𝕜
inst✝⁶ : TopologicalSpace E
inst✝⁵ : TopologicalSpace F
inst✝⁴ : AddCommGroup E
inst✝³ : AddCommGroup F
inst✝² : Module 𝕜 E
inst✝¹ : Module 𝕜 F
inst✝ : ContinuousAdd E
s t : Set E
hs : StrictConvex 𝕜 s
ht : StrictConvex 𝕜 t
v w : E
hv : v ∈ s
hw : w ∈ t
x y : E
hx : x ∈ s
hy : y ∈ t
h : (fun x x_1 => x + x_1) v w ≠ (fun x x_1 => x + x_1) x y
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
⊢ a • v + b • x + (a • w + b • y) ∈ interior (s + t)
obtain rfl | hvx := eq_or_ne v x
no goals
case intro.intro.intro.intro.intro.intro.intro.intro.inr
𝕜 : Type u_1
𝕝 : Type ?u.78535
E : Type u_2
F : Type ?u.78541
β : Type ?u.78544
inst✝⁷ : OrderedSemiring 𝕜
inst✝⁶ : TopologicalSpace E
inst✝⁵ : TopologicalSpace F
inst✝⁴ : AddCommGroup E
inst✝³ : AddCommGroup F
inst✝² : Module 𝕜 E
inst✝¹ : Module 𝕜 F
inst✝ : ContinuousAdd E
s t : Set E
hs : StrictConvex 𝕜 s
ht : StrictConvex 𝕜 t
v w : E
hv : v ∈ s
hw : w ∈ t
x y : E
hx : x ∈ s
hy : y ∈ t
h : (fun x x_1 => x + x_1) v w ≠ (fun x x_1 => x + x_1) x y
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
hvx : v ≠ x
⊢ a • v + b • x + (a • w + b • y) ∈ interior (s + t)
exact
  subset_interior_add_left
    (add_mem_add (hs hv hx hvx ha hb hab) <| ht.convex hw hy ha.le hb.le hab)
case intro.intro.intro.intro.intro.intro.intro.intro.inl
𝕜 : Type u_1
𝕝 : Type ?u.78535
E : Type u_2
F : Type ?u.78541
β : Type ?u.78544
inst✝⁷ : OrderedSemiring 𝕜
inst✝⁶ : TopologicalSpace E
inst✝⁵ : TopologicalSpace F
inst✝⁴ : AddCommGroup E
inst✝³ : AddCommGroup F
inst✝² : Module 𝕜 E
inst✝¹ : Module 𝕜 F
inst✝ : ContinuousAdd E
s t : Set E
hs : StrictConvex 𝕜 s
ht : StrictConvex 𝕜 t
v w : E
hv : v ∈ s
hw : w ∈ t
y : E
hy : y ∈ t
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
hx : v ∈ s
h : (fun x x_1 => x + x_1) v w ≠ (fun x x_1 => x + x_1) v y
⊢ a • v + b • v + (a • w + b • y) ∈ interior ({v} + t)
case intro.intro.intro.intro.intro.intro.intro.intro.inl
𝕜 : Type u_1
𝕝 : Type ?u.78535
E : Type u_2
F : Type ?u.78541
β : Type ?u.78544
inst✝⁷ : OrderedSemiring 𝕜
inst✝⁶ : TopologicalSpace E
inst✝⁵ : TopologicalSpace F
inst✝⁴ : AddCommGroup E
inst✝³ : AddCommGroup F
inst✝² : Module 𝕜 E
inst✝¹ : Module 𝕜 F
inst✝ : ContinuousAdd E
s t : Set E
hs : StrictConvex 𝕜 s
ht : StrictConvex 𝕜 t
v w : E
hv : v ∈ s
hw : w ∈ t
y : E
hy : y ∈ t
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
hx : v ∈ s
h : (fun x x_1 => x + x_1) v w ≠ (fun x x_1 => x + x_1) v y
⊢ a • v + b • v + (a • w + b • y) ∈ interior (s + t)
refine' interior_mono (add_subset_add (singleton_subset_iff.2 hv) Subset.rfl) _
case intro.intro.intro.intro.intro.intro.intro.intro.inl
𝕜 : Type u_1
𝕝 : Type ?u.78535
E : Type u_2
F : Type ?u.78541
β : Type ?u.78544
inst✝⁷ : OrderedSemiring 𝕜
inst✝⁶ : TopologicalSpace E
inst✝⁵ : TopologicalSpace F
inst✝⁴ : AddCommGroup E
inst✝³ : AddCommGroup F
inst✝² : Module 𝕜 E
inst✝¹ : Module 𝕜 F
inst✝ : ContinuousAdd E
s t : Set E
hs : StrictConvex 𝕜 s
ht : StrictConvex 𝕜 t
v w : E
hv : v ∈ s
hw : w ∈ t
y : E
hy : y ∈ t
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
hx : v ∈ s
h : (fun x x_1 => x + x_1) v w ≠ (fun x x_1 => x + x_1) v y
⊢ v + (a • w + b • y) ∈ interior ((fun x x_1 => x + x_1) v '' t)
case intro.intro.intro.intro.intro.intro.intro.intro.inl
𝕜 : Type u_1
𝕝 : Type ?u.78535
E : Type u_2
F : Type ?u.78541
β : Type ?u.78544
inst✝⁷ : OrderedSemiring 𝕜
inst✝⁶ : TopologicalSpace E
inst✝⁵ : TopologicalSpace F
inst✝⁴ : AddCommGroup E
inst✝³ : AddCommGroup F
inst✝² : Module 𝕜 E
inst✝¹ : Module 𝕜 F
inst✝ : ContinuousAdd E
s t : Set E
hs : StrictConvex 𝕜 s
ht : StrictConvex 𝕜 t
v w : E
hv : v ∈ s
hw : w ∈ t
y : E
hy : y ∈ t
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
hx : v ∈ s
h : (fun x x_1 => x + x_1) v w ≠ (fun x x_1 => x + x_1) v y
⊢ a • v + b • v + (a • w + b • y) ∈ interior ({v} + t)
rw [Convex.combo_self hab, singleton_add]
no goals
case intro.intro.intro.intro.intro.intro.intro.intro.inl
𝕜 : Type u_1
𝕝 : Type ?u.78535
E : Type u_2
F : Type ?u.78541
β : Type ?u.78544
inst✝⁷ : OrderedSemiring 𝕜
inst✝⁶ : TopologicalSpace E
inst✝⁵ : TopologicalSpace F
inst✝⁴ : AddCommGroup E
inst✝³ : AddCommGroup F
inst✝² : Module 𝕜 E
inst✝¹ : Module 𝕜 F
inst✝ : ContinuousAdd E
s t : Set E
hs : StrictConvex 𝕜 s
ht : StrictConvex 𝕜 t
v w : E
hv : v ∈ s
hw : w ∈ t
y : E
hy : y ∈ t
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
hx : v ∈ s
h : (fun x x_1 => x + x_1) v w ≠ (fun x x_1 => x + x_1) v y
⊢ v + (a • w + b • y) ∈ interior ((fun x x_1 => x + x_1) v '' t)
exact
  (isOpenMap_add_left _).image_interior_subset _
    (mem_image_of_mem _ <| ht hw hy (ne_of_apply_ne _ h) ha hb hab)