-- Mathlib/Analysis/Convex/Topology.lean
theorem Convex.interior_closure_eq_interior_of_nonempty_interior {s : Set E} (hs : Convex 𝕜 s)
    (hs' : (interior s).Nonempty) : interior (closure s) = interior s

Proof state:
𝕜 : Type u_2
E : Type u_3
inst✝⁷ : LinearOrderedField 𝕜
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module 𝕜 E
inst✝⁴ : TopologicalSpace E
inst✝³ : IsTopologicalAddGroup E
inst✝² : TopologicalSpace 𝕜
inst✝¹ : OrderTopology 𝕜
inst✝ : ContinuousSMul 𝕜 E
s : Set E
hs : Convex 𝕜 s
hs' : (interior s).Nonempty
⊢ interior (closure s) = interior s

Tactic:
refine subset_antisymm ?_ (interior_mono subset_closure)

Result:
𝕜 : Type u_2
E : Type u_3
inst✝⁷ : LinearOrderedField 𝕜
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module 𝕜 E
inst✝⁴ : TopologicalSpace E
inst✝³ : IsTopologicalAddGroup E
inst✝² : TopologicalSpace 𝕜
inst✝¹ : OrderTopology 𝕜
inst✝ : ContinuousSMul 𝕜 E
s : Set E
hs : Convex 𝕜 s
hs' : (interior s).Nonempty
⊢ interior (closure s) ⊆ interior s

Proof state:
𝕜 : Type u_2
E : Type u_3
inst✝⁷ : LinearOrderedField 𝕜
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module 𝕜 E
inst✝⁴ : TopologicalSpace E
inst✝³ : IsTopologicalAddGroup E
inst✝² : TopologicalSpace 𝕜
inst✝¹ : OrderTopology 𝕜
inst✝ : ContinuousSMul 𝕜 E
s : Set E
hs : Convex 𝕜 s
hs' : (interior s).Nonempty
⊢ interior (closure s) ⊆ interior s

Tactic:
intro y hy

Result:
𝕜 : Type u_2
E : Type u_3
inst✝⁷ : LinearOrderedField 𝕜
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module 𝕜 E
inst✝⁴ : TopologicalSpace E
inst✝³ : IsTopologicalAddGroup E
inst✝² : TopologicalSpace 𝕜
inst✝¹ : OrderTopology 𝕜
inst✝ : ContinuousSMul 𝕜 E
s : Set E
hs : Convex 𝕜 s
hs' : (interior s).Nonempty
y : E
hy : y ∈ interior (closure s)
⊢ y ∈ interior s

Proof state:
case intro.intro.intro.a
𝕜 : Type u_2
E : Type u_3
inst✝⁷ : LinearOrderedField 𝕜
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module 𝕜 E
inst✝⁴ : TopologicalSpace E
inst✝³ : IsTopologicalAddGroup E
inst✝² : TopologicalSpace 𝕜
inst✝¹ : OrderTopology 𝕜
inst✝ : ContinuousSMul 𝕜 E
s : Set E
hs : Convex 𝕜 s
y : E
hy : y ∈ interior (closure s)
x : E
hx : x ∈ interior s
h : (AffineMap.lineMap x y) 1 = y
t : 𝕜
ht1 : t > 1
ht : (AffineMap.lineMap x y) t ∈ closure s
⊢ y ∈ ⇑(AffineMap.lineMap x y) '' openSegment 𝕜 0 t

Tactic:
exact ⟨1, Ioo_subset_openSegment ⟨zero_lt_one, ht1⟩, h⟩

Result:
no goals

Proof state:
𝕜 : Type u_2
E : Type u_3
inst✝⁷ : LinearOrderedField 𝕜
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module 𝕜 E
inst✝⁴ : TopologicalSpace E
inst✝³ : IsTopologicalAddGroup E
inst✝² : TopologicalSpace 𝕜
inst✝¹ : OrderTopology 𝕜
inst✝ : ContinuousSMul 𝕜 E
s : Set E
hs : Convex 𝕜 s
hs' : (interior s).Nonempty
y : E
hy : y ∈ interior (closure s)
⊢ y ∈ interior s

Tactic:
rcases hs' with ⟨x, hx⟩

Result:
case intro
𝕜 : Type u_2
E : Type u_3
inst✝⁷ : LinearOrderedField 𝕜
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module 𝕜 E
inst✝⁴ : TopologicalSpace E
inst✝³ : IsTopologicalAddGroup E
inst✝² : TopologicalSpace 𝕜
inst✝¹ : OrderTopology 𝕜
inst✝ : ContinuousSMul 𝕜 E
s : Set E
hs : Convex 𝕜 s
y : E
hy : y ∈ interior (closure s)
x : E
hx : x ∈ interior s
⊢ y ∈ interior s

Proof state:
case intro
𝕜 : Type u_2
E : Type u_3
inst✝⁷ : LinearOrderedField 𝕜
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module 𝕜 E
inst✝⁴ : TopologicalSpace E
inst✝³ : IsTopologicalAddGroup E
inst✝² : TopologicalSpace 𝕜
inst✝¹ : OrderTopology 𝕜
inst✝ : ContinuousSMul 𝕜 E
s : Set E
hs : Convex 𝕜 s
y : E
hy : y ∈ interior (closure s)
x : E
hx : x ∈ interior s
h : (AffineMap.lineMap x y) 1 = y
⊢ y ∈ interior s

Tactic:
obtain ⟨t, ht1, ht⟩ := AffineMap.lineMap_continuous.tendsto' _ _ h |>.eventually_mem
  (mem_interior_iff_mem_nhds.1 hy) |>.exists_gt

Result:
case intro.intro.intro
𝕜 : Type u_2
E : Type u_3
inst✝⁷ : LinearOrderedField 𝕜
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module 𝕜 E
inst✝⁴ : TopologicalSpace E
inst✝³ : IsTopologicalAddGroup E
inst✝² : TopologicalSpace 𝕜
inst✝¹ : OrderTopology 𝕜
inst✝ : ContinuousSMul 𝕜 E
s : Set E
hs : Convex 𝕜 s
y : E
hy : y ∈ interior (closure s)
x : E
hx : x ∈ interior s
h : (AffineMap.lineMap x y) 1 = y
t : 𝕜
ht1 : t > 1
ht : (AffineMap.lineMap x y) t ∈ closure s
⊢ y ∈ interior s

Proof state:
case intro
𝕜 : Type u_2
E : Type u_3
inst✝⁷ : LinearOrderedField 𝕜
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module 𝕜 E
inst✝⁴ : TopologicalSpace E
inst✝³ : IsTopologicalAddGroup E
inst✝² : TopologicalSpace 𝕜
inst✝¹ : OrderTopology 𝕜
inst✝ : ContinuousSMul 𝕜 E
s : Set E
hs : Convex 𝕜 s
y : E
hy : y ∈ interior (closure s)
x : E
hx : x ∈ interior s
⊢ y ∈ interior s

Tactic:
have h := AffineMap.lineMap_apply_one (k := 𝕜) x y

Result:
case intro
𝕜 : Type u_2
E : Type u_3
inst✝⁷ : LinearOrderedField 𝕜
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module 𝕜 E
inst✝⁴ : TopologicalSpace E
inst✝³ : IsTopologicalAddGroup E
inst✝² : TopologicalSpace 𝕜
inst✝¹ : OrderTopology 𝕜
inst✝ : ContinuousSMul 𝕜 E
s : Set E
hs : Convex 𝕜 s
y : E
hy : y ∈ interior (closure s)
x : E
hx : x ∈ interior s
h : (AffineMap.lineMap x y) 1 = y
⊢ y ∈ interior s

Proof state:
case intro.intro.intro.a
𝕜 : Type u_2
E : Type u_3
inst✝⁷ : LinearOrderedField 𝕜
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module 𝕜 E
inst✝⁴ : TopologicalSpace E
inst✝³ : IsTopologicalAddGroup E
inst✝² : TopologicalSpace 𝕜
inst✝¹ : OrderTopology 𝕜
inst✝ : ContinuousSMul 𝕜 E
s : Set E
hs : Convex 𝕜 s
y : E
hy : y ∈ interior (closure s)
x : E
hx : x ∈ interior s
h : (AffineMap.lineMap x y) 1 = y
t : 𝕜
ht1 : t > 1
ht : (AffineMap.lineMap x y) t ∈ closure s
⊢ y ∈ openSegment 𝕜 x ((AffineMap.lineMap x y) t)

Tactic:
nth_rw 1 [← AffineMap.lineMap_apply_zero (k := 𝕜) x y, ← image_openSegment]

Result:
case intro.intro.intro.a
𝕜 : Type u_2
E : Type u_3
inst✝⁷ : LinearOrderedField 𝕜
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module 𝕜 E
inst✝⁴ : TopologicalSpace E
inst✝³ : IsTopologicalAddGroup E
inst✝² : TopologicalSpace 𝕜
inst✝¹ : OrderTopology 𝕜
inst✝ : ContinuousSMul 𝕜 E
s : Set E
hs : Convex 𝕜 s
y : E
hy : y ∈ interior (closure s)
x : E
hx : x ∈ interior s
h : (AffineMap.lineMap x y) 1 = y
t : 𝕜
ht1 : t > 1
ht : (AffineMap.lineMap x y) t ∈ closure s
⊢ y ∈ ⇑(AffineMap.lineMap x y) '' openSegment 𝕜 0 t

Proof state:
case intro.intro.intro
𝕜 : Type u_2
E : Type u_3
inst✝⁷ : LinearOrderedField 𝕜
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module 𝕜 E
inst✝⁴ : TopologicalSpace E
inst✝³ : IsTopologicalAddGroup E
inst✝² : TopologicalSpace 𝕜
inst✝¹ : OrderTopology 𝕜
inst✝ : ContinuousSMul 𝕜 E
s : Set E
hs : Convex 𝕜 s
y : E
hy : y ∈ interior (closure s)
x : E
hx : x ∈ interior s
h : (AffineMap.lineMap x y) 1 = y
t : 𝕜
ht1 : t > 1
ht : (AffineMap.lineMap x y) t ∈ closure s
⊢ y ∈ interior s

Tactic:
apply hs.openSegment_interior_closure_subset_interior hx ht

Result:
case intro.intro.intro.a
𝕜 : Type u_2
E : Type u_3
inst✝⁷ : LinearOrderedField 𝕜
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module 𝕜 E
inst✝⁴ : TopologicalSpace E
inst✝³ : IsTopologicalAddGroup E
inst✝² : TopologicalSpace 𝕜
inst✝¹ : OrderTopology 𝕜
inst✝ : ContinuousSMul 𝕜 E
s : Set E
hs : Convex 𝕜 s
y : E
hy : y ∈ interior (closure s)
x : E
hx : x ∈ interior s
h : (AffineMap.lineMap x y) 1 = y
t : 𝕜
ht1 : t > 1
ht : (AffineMap.lineMap x y) t ∈ closure s
⊢ y ∈ openSegment 𝕜 x ((AffineMap.lineMap x y) t)