-- Mathlib/Analysis/Convex/Strict.lean
theorem Directed.strictConvex_iUnion {ι : Sort*} {s : ι → Set E} (hdir : Directed (· ⊆ ·) s)
    (hs : ∀ ⦃i : ι⦄, StrictConvex 𝕜 (s i)) : StrictConvex 𝕜 (⋃ i, s i)

Proof state:
case intro
𝕜 : Type u_1
E : Type u_3
inst✝³ : OrderedSemiring 𝕜
inst✝² : TopologicalSpace E
inst✝¹ : AddCommMonoid E
inst✝ : SMul 𝕜 E
ι : Sort u_6
s : ι → Set E
hdir : Directed (fun x1 x2 => x1 ⊆ x2) s
hs : ∀ ⦃i : ι⦄, StrictConvex 𝕜 (s i)
x y : E
hy : ∃ i, y ∈ s i
hxy : x ≠ y
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
i : ι
hx : x ∈ s i
⊢ a • x + b • y ∈ interior (⋃ i, s i)

Tactic:
obtain ⟨j, hy⟩ := hy

Result:
case intro.intro
𝕜 : Type u_1
E : Type u_3
inst✝³ : OrderedSemiring 𝕜
inst✝² : TopologicalSpace E
inst✝¹ : AddCommMonoid E
inst✝ : SMul 𝕜 E
ι : Sort u_6
s : ι → Set E
hdir : Directed (fun x1 x2 => x1 ⊆ x2) s
hs : ∀ ⦃i : ι⦄, StrictConvex 𝕜 (s i)
x y : E
hxy : x ≠ y
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
i : ι
hx : x ∈ s i
j : ι
hy : y ∈ s j
⊢ a • x + b • y ∈ interior (⋃ i, s i)

Proof state:
case intro.intro.intro.intro
𝕜 : Type u_1
E : Type u_3
inst✝³ : OrderedSemiring 𝕜
inst✝² : TopologicalSpace E
inst✝¹ : AddCommMonoid E
inst✝ : SMul 𝕜 E
ι : Sort u_6
s : ι → Set E
hdir : Directed (fun x1 x2 => x1 ⊆ x2) s
hs : ∀ ⦃i : ι⦄, StrictConvex 𝕜 (s i)
x y : E
hxy : x ≠ y
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
i : ι
hx : x ∈ s i
j : ι
hy : y ∈ s j
k : ι
hik : s i ⊆ s k
hjk : s j ⊆ s k
⊢ a • x + b • y ∈ interior (⋃ i, s i)

Tactic:
exact interior_mono (subset_iUnion s k) (hs (hik hx) (hjk hy) hxy ha hb hab)

Result:
no goals

Proof state:
𝕜 : Type u_1
E : Type u_3
inst✝³ : OrderedSemiring 𝕜
inst✝² : TopologicalSpace E
inst✝¹ : AddCommMonoid E
inst✝ : SMul 𝕜 E
ι : Sort u_6
s : ι → Set E
hdir : Directed (fun x1 x2 => x1 ⊆ x2) s
hs : ∀ ⦃i : ι⦄, StrictConvex 𝕜 (s i)
x : E
hx : ∃ i, x ∈ s i
y : E
hy : ∃ i, y ∈ s i
hxy : x ≠ y
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
⊢ a • x + b • y ∈ interior (⋃ i, s i)

Tactic:
obtain ⟨i, hx⟩ := hx

Result:
case intro
𝕜 : Type u_1
E : Type u_3
inst✝³ : OrderedSemiring 𝕜
inst✝² : TopologicalSpace E
inst✝¹ : AddCommMonoid E
inst✝ : SMul 𝕜 E
ι : Sort u_6
s : ι → Set E
hdir : Directed (fun x1 x2 => x1 ⊆ x2) s
hs : ∀ ⦃i : ι⦄, StrictConvex 𝕜 (s i)
x y : E
hy : ∃ i, y ∈ s i
hxy : x ≠ y
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
i : ι
hx : x ∈ s i
⊢ a • x + b • y ∈ interior (⋃ i, s i)

Proof state:
𝕜 : Type u_1
E : Type u_3
inst✝³ : OrderedSemiring 𝕜
inst✝² : TopologicalSpace E
inst✝¹ : AddCommMonoid E
inst✝ : SMul 𝕜 E
ι : Sort u_6
s : ι → Set E
hdir : Directed (fun x1 x2 => x1 ⊆ x2) s
hs : ∀ ⦃i : ι⦄, StrictConvex 𝕜 (s i)
x : E
hx : x ∈ ⋃ i, s i
y : E
hy : y ∈ ⋃ i, s i
hxy : x ≠ y
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
⊢ a • x + b • y ∈ interior (⋃ i, s i)

Tactic:
rw [mem_iUnion] at hx hy

Result:
𝕜 : Type u_1
E : Type u_3
inst✝³ : OrderedSemiring 𝕜
inst✝² : TopologicalSpace E
inst✝¹ : AddCommMonoid E
inst✝ : SMul 𝕜 E
ι : Sort u_6
s : ι → Set E
hdir : Directed (fun x1 x2 => x1 ⊆ x2) s
hs : ∀ ⦃i : ι⦄, StrictConvex 𝕜 (s i)
x : E
hx : ∃ i, x ∈ s i
y : E
hy : ∃ i, y ∈ s i
hxy : x ≠ y
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
⊢ a • x + b • y ∈ interior (⋃ i, s i)

Proof state:
𝕜 : Type u_1
E : Type u_3
inst✝³ : OrderedSemiring 𝕜
inst✝² : TopologicalSpace E
inst✝¹ : AddCommMonoid E
inst✝ : SMul 𝕜 E
ι : Sort u_6
s : ι → Set E
hdir : Directed (fun x1 x2 => x1 ⊆ x2) s
hs : ∀ ⦃i : ι⦄, StrictConvex 𝕜 (s i)
⊢ StrictConvex 𝕜 (⋃ i, s i)

Tactic:
rintro x hx y hy hxy a b ha hb hab

Result:
𝕜 : Type u_1
E : Type u_3
inst✝³ : OrderedSemiring 𝕜
inst✝² : TopologicalSpace E
inst✝¹ : AddCommMonoid E
inst✝ : SMul 𝕜 E
ι : Sort u_6
s : ι → Set E
hdir : Directed (fun x1 x2 => x1 ⊆ x2) s
hs : ∀ ⦃i : ι⦄, StrictConvex 𝕜 (s i)
x : E
hx : x ∈ ⋃ i, s i
y : E
hy : y ∈ ⋃ i, s i
hxy : x ≠ y
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
⊢ a • x + b • y ∈ interior (⋃ i, s i)

Proof state:
case intro.intro
𝕜 : Type u_1
E : Type u_3
inst✝³ : OrderedSemiring 𝕜
inst✝² : TopologicalSpace E
inst✝¹ : AddCommMonoid E
inst✝ : SMul 𝕜 E
ι : Sort u_6
s : ι → Set E
hdir : Directed (fun x1 x2 => x1 ⊆ x2) s
hs : ∀ ⦃i : ι⦄, StrictConvex 𝕜 (s i)
x y : E
hxy : x ≠ y
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
i : ι
hx : x ∈ s i
j : ι
hy : y ∈ s j
⊢ a • x + b • y ∈ interior (⋃ i, s i)

Tactic:
obtain ⟨k, hik, hjk⟩ := hdir i j

Result:
case intro.intro.intro.intro
𝕜 : Type u_1
E : Type u_3
inst✝³ : OrderedSemiring 𝕜
inst✝² : TopologicalSpace E
inst✝¹ : AddCommMonoid E
inst✝ : SMul 𝕜 E
ι : Sort u_6
s : ι → Set E
hdir : Directed (fun x1 x2 => x1 ⊆ x2) s
hs : ∀ ⦃i : ι⦄, StrictConvex 𝕜 (s i)
x y : E
hxy : x ≠ y
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
i : ι
hx : x ∈ s i
j : ι
hy : y ∈ s j
k : ι
hik : s i ⊆ s k
hjk : s j ⊆ s k
⊢ a • x + b • y ∈ interior (⋃ i, s i)