-- Mathlib/Analysis/Convex/Strict.lean
theorem StrictConvex.add (hs : StrictConvex 𝕜 s) (ht : StrictConvex 𝕜 t) :
    StrictConvex 𝕜 (s + t)

Proof state:
case intro.intro.intro.intro.intro.intro.intro.intro
𝕜 : Type u_1
E : Type u_3
inst✝⁴ : OrderedSemiring 𝕜
inst✝³ : TopologicalSpace E
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : ContinuousAdd E
s t : Set E
hs : StrictConvex 𝕜 s
ht : StrictConvex 𝕜 t
v : E
hv : v ∈ s
w : E
hw : w ∈ t
x : E
hx : x ∈ s
y : E
hy : y ∈ t
h : (fun x1 x2 => x1 + x2) v w ≠ (fun x1 x2 => x1 + x2) x y
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
⊢ a • (fun x1 x2 => x1 + x2) v w + b • (fun x1 x2 => x1 + x2) x y ∈ interior (s + t)

Tactic:
rw [smul_add, smul_add, add_add_add_comm]

Result:
case intro.intro.intro.intro.intro.intro.intro.intro
𝕜 : Type u_1
E : Type u_3
inst✝⁴ : OrderedSemiring 𝕜
inst✝³ : TopologicalSpace E
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : ContinuousAdd E
s t : Set E
hs : StrictConvex 𝕜 s
ht : StrictConvex 𝕜 t
v : E
hv : v ∈ s
w : E
hw : w ∈ t
x : E
hx : x ∈ s
y : E
hy : y ∈ t
h : (fun x1 x2 => x1 + x2) v w ≠ (fun x1 x2 => x1 + x2) 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)

Proof state:
case intro.intro.intro.intro.intro.intro.intro.intro.inl
𝕜 : Type u_1
E : Type u_3
inst✝⁴ : OrderedSemiring 𝕜
inst✝³ : TopologicalSpace E
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : ContinuousAdd E
s t : Set E
hs : StrictConvex 𝕜 s
ht : StrictConvex 𝕜 t
v : E
hv : v ∈ s
w : E
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 x1 x2 => x1 + x2) v w ≠ (fun x1 x2 => x1 + x2) v y
⊢ v + (a • w + b • y) ∈ interior ((fun x => v + x) '' t)

Tactic:
exact
  (isOpenMap_add_left _).image_interior_subset _
    (mem_image_of_mem _ <| ht hw hy (ne_of_apply_ne _ h) ha hb hab)

Result:
no goals

Proof state:
case intro.intro.intro.intro.intro.intro.intro.intro.inr
𝕜 : Type u_1
E : Type u_3
inst✝⁴ : OrderedSemiring 𝕜
inst✝³ : TopologicalSpace E
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : ContinuousAdd E
s t : Set E
hs : StrictConvex 𝕜 s
ht : StrictConvex 𝕜 t
v : E
hv : v ∈ s
w : E
hw : w ∈ t
x : E
hx : x ∈ s
y : E
hy : y ∈ t
h : (fun x1 x2 => x1 + x2) v w ≠ (fun x1 x2 => x1 + x2) 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)

Tactic:
exact
  subset_interior_add_left
    (add_mem_add (hs hv hx hvx ha hb hab) <| ht.convex hw hy ha.le hb.le hab)

Result:
no goals

Proof state:
case intro.intro.intro.intro.intro.intro.intro.intro.inl
𝕜 : Type u_1
E : Type u_3
inst✝⁴ : OrderedSemiring 𝕜
inst✝³ : TopologicalSpace E
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : ContinuousAdd E
s t : Set E
hs : StrictConvex 𝕜 s
ht : StrictConvex 𝕜 t
v : E
hv : v ∈ s
w : E
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 x1 x2 => x1 + x2) v w ≠ (fun x1 x2 => x1 + x2) v y
⊢ a • v + b • v + (a • w + b • y) ∈ interior ({v} + t)

Tactic:
rw [Convex.combo_self hab, singleton_add]

Result:
case intro.intro.intro.intro.intro.intro.intro.intro.inl
𝕜 : Type u_1
E : Type u_3
inst✝⁴ : OrderedSemiring 𝕜
inst✝³ : TopologicalSpace E
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : ContinuousAdd E
s t : Set E
hs : StrictConvex 𝕜 s
ht : StrictConvex 𝕜 t
v : E
hv : v ∈ s
w : E
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 x1 x2 => x1 + x2) v w ≠ (fun x1 x2 => x1 + x2) v y
⊢ v + (a • w + b • y) ∈ interior ((fun x => v + x) '' t)

Proof state:
case intro.intro.intro.intro.intro.intro.intro.intro
𝕜 : Type u_1
E : Type u_3
inst✝⁴ : OrderedSemiring 𝕜
inst✝³ : TopologicalSpace E
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : ContinuousAdd E
s t : Set E
hs : StrictConvex 𝕜 s
ht : StrictConvex 𝕜 t
v : E
hv : v ∈ s
w : E
hw : w ∈ t
x : E
hx : x ∈ s
y : E
hy : y ∈ t
h : (fun x1 x2 => x1 + x2) v w ≠ (fun x1 x2 => x1 + x2) 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)

Tactic:
obtain rfl | hvx := eq_or_ne v x

Result:
case intro.intro.intro.intro.intro.intro.intro.intro.inl
𝕜 : Type u_1
E : Type u_3
inst✝⁴ : OrderedSemiring 𝕜
inst✝³ : TopologicalSpace E
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : ContinuousAdd E
s t : Set E
hs : StrictConvex 𝕜 s
ht : StrictConvex 𝕜 t
v : E
hv : v ∈ s
w : E
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 x1 x2 => x1 + x2) v w ≠ (fun x1 x2 => x1 + x2) 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
E : Type u_3
inst✝⁴ : OrderedSemiring 𝕜
inst✝³ : TopologicalSpace E
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : ContinuousAdd E
s t : Set E
hs : StrictConvex 𝕜 s
ht : StrictConvex 𝕜 t
v : E
hv : v ∈ s
w : E
hw : w ∈ t
x : E
hx : x ∈ s
y : E
hy : y ∈ t
h : (fun x1 x2 => x1 + x2) v w ≠ (fun x1 x2 => x1 + x2) 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)

Proof state:
𝕜 : Type u_1
E : Type u_3
inst✝⁴ : OrderedSemiring 𝕜
inst✝³ : TopologicalSpace E
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : ContinuousAdd E
s t : Set E
hs : StrictConvex 𝕜 s
ht : StrictConvex 𝕜 t
⊢ StrictConvex 𝕜 (s + t)

Tactic:
rintro _ ⟨v, hv, w, hw, rfl⟩ _ ⟨x, hx, y, hy, rfl⟩ h a b ha hb hab

Result:
case intro.intro.intro.intro.intro.intro.intro.intro
𝕜 : Type u_1
E : Type u_3
inst✝⁴ : OrderedSemiring 𝕜
inst✝³ : TopologicalSpace E
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : ContinuousAdd E
s t : Set E
hs : StrictConvex 𝕜 s
ht : StrictConvex 𝕜 t
v : E
hv : v ∈ s
w : E
hw : w ∈ t
x : E
hx : x ∈ s
y : E
hy : y ∈ t
h : (fun x1 x2 => x1 + x2) v w ≠ (fun x1 x2 => x1 + x2) x y
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
⊢ a • (fun x1 x2 => x1 + x2) v w + b • (fun x1 x2 => x1 + x2) x y ∈ interior (s + t)

Proof state:
case intro.intro.intro.intro.intro.intro.intro.intro.inl
𝕜 : Type u_1
E : Type u_3
inst✝⁴ : OrderedSemiring 𝕜
inst✝³ : TopologicalSpace E
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : ContinuousAdd E
s t : Set E
hs : StrictConvex 𝕜 s
ht : StrictConvex 𝕜 t
v : E
hv : v ∈ s
w : E
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 x1 x2 => x1 + x2) v w ≠ (fun x1 x2 => x1 + x2) v y
⊢ a • v + b • v + (a • w + b • y) ∈ interior (s + t)

Tactic:
refine interior_mono (add_subset_add (singleton_subset_iff.2 hv) Subset.rfl) ?_

Result:
case intro.intro.intro.intro.intro.intro.intro.intro.inl
𝕜 : Type u_1
E : Type u_3
inst✝⁴ : OrderedSemiring 𝕜
inst✝³ : TopologicalSpace E
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : ContinuousAdd E
s t : Set E
hs : StrictConvex 𝕜 s
ht : StrictConvex 𝕜 t
v : E
hv : v ∈ s
w : E
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 x1 x2 => x1 + x2) v w ≠ (fun x1 x2 => x1 + x2) v y
⊢ a • v + b • v + (a • w + b • y) ∈ interior ({v} + t)