awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Convex.Topology
Goal:
E : Type u_3
inst : AddCommGroup E
inst_1 : Module ℝ E
inst_2 : TopologicalSpace E
inst_3 : IsTopologicalAddGroup E
inst_4 : ContinuousSMul ℝ E
s : Set E
hs : Convex ℝ s
x : E
hx : x ∈ interior s
t : ℝ
ht : 1 < t
y : E
hy : y ∈ closure s
hne : t ≠ 0
rw :
  Membership.mem (α := E) (γ := Set E) ((fun (x_1 : ℝ) ↦ (lineMap x y : (a : ℝ) → E) x_1⁻¹) '' Ioi 1)
    ((lineMap x y : (a : ℝ) → E) t⁻¹ : E)
⊢ Membership.mem (α := E) (openSegment ℝ x y) ((homothety x t⁻¹ : (a : E) → E) y : E)

Tactic:
rw [openSegment_eq_image_lineMap, ← inv_one, ← inv_Ioi₀ (zero_lt_one' ℝ), ← image_inv_eq_inv,
    image_image, homothety_eq_lineMap]

Premises used: Set.image_image, Real, inv_one, zero_lt_one', openSegment_eq_image_lineMap, Set.inv_Ioi₀, Set.image_inv_eq_inv, AffineMap.homothety_eq_lineMap
-- Module: Mathlib.Analysis.Convex.Topology
Goal:
E : Type u_3
inst : AddCommGroup E
inst_1 : Module ℝ E
inst_2 : TopologicalSpace E
inst_3 : IsTopologicalAddGroup E
inst_4 : ContinuousSMul ℝ E
s : Set E
hs : Convex ℝ s
x : E
hx : x ∈ interior s
t : ℝ
ht : 1 < t
y : E
hy : y ∈ closure s
hne : t ≠ 0
⊢ Membership.mem (α := E) (γ := Set E) ((fun (x_1 : ℝ) ↦ (lineMap x y : (a : ℝ) → E) x_1⁻¹) '' Ioi 1)
    ((lineMap x y : (a : ℝ) → E) t⁻¹ : E)

Tactic:
mem_image_of_mem _ ht

Premises used: Set.Mem, Set.mem_image_of_mem
-- Module: Mathlib.Analysis.Convex.Topology
Goal:
E : Type u_3
inst : AddCommGroup E
inst_1 : Module ℝ E
inst_2 : TopologicalSpace E
inst_3 : IsTopologicalAddGroup E
inst_4 : ContinuousSMul ℝ E
s : Set E
hs : Convex ℝ s
x : E
hx : x ∈ interior s
t : ℝ
ht : 1 < t
y : E
hy : y ∈ closure s
hne : t ≠ 0
⊢ Membership.mem (α := E) (γ := Set E) ((fun (x_1 : ℝ) ↦ (lineMap x y : (a : ℝ) → E) x_1⁻¹) '' Ioi 1)
    ((lineMap x y : (a : ℝ) → E) t⁻¹ : E)

Tactic:
exact mem_image_of_mem _ ht

Premises used: Set.mem_image_of_mem
-- Module: Mathlib.Analysis.Convex.Topology
Goal:
E : Type u_3
inst : AddCommGroup E
inst_1 : Module ℝ E
inst_2 : TopologicalSpace E
inst_3 : IsTopologicalAddGroup E
inst_4 : ContinuousSMul ℝ E
s : Set E
hs : Convex ℝ s
x : E
hx : x ∈ interior s
t : ℝ
ht : 1 < t
⊢ closure s ⊆ interior ((⇑(homothety x t) : (a : E) → E) '' s)

Tactic:
(hs.closure_subset_image_homothety_interior_of_one_lt hx t ht).trans <|
    (homothety_isOpenMap x t (one_pos.trans ht).ne').image_interior_subset _

Premises used: IsOpenMap.image_interior_subset, HasSubset.Subset.trans, LT.lt.ne', AffineMap.homothety_isOpenMap, LT.lt.trans, Convex.closure_subset_image_homothety_interior_of_one_lt, one_pos
-- Module: Mathlib.Analysis.Convex.Topology
Goal:
E : Type u_3
inst : AddCommGroup E
inst_1 : Module ℝ E
inst_2 : TopologicalSpace E
inst_3 : IsTopologicalAddGroup E
inst_4 : ContinuousSMul ℝ E
s : Set E
hs : Convex ℝ s
x : E
hx : x ∈ interior s
t : ℝ
ht : 1 < t
⊢ s ⊆ interior ((⇑(homothety x t) : (a : E) → E) '' s)

Tactic:
subset_closure.trans <| hs.closure_subset_interior_image_homothety_of_one_lt hx t ht

Premises used: subset_closure, Convex.closure_subset_interior_image_homothety_of_one_lt, HasSubset.Subset.trans
-- Module: Mathlib.Analysis.Convex.Topology
Goal:
𝕜 : Type u_4
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : TopologicalSpace 𝕜
inst_4 : OrderTopology 𝕜
s : Set 𝕜
hs : Convex 𝕜 s
mp : s.Nontrivial → (interior s).Nonempty
mpr : (interior s).Nonempty → s.Nontrivial
⊢ s.Nontrivial ↔ (interior s).Nonempty

Tactic:
constructor
-- Module: Mathlib.Analysis.Convex.Topology
Goal:
𝕜 : Type u_4
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : TopologicalSpace 𝕜
inst_4 : OrderTopology 𝕜
s : Set 𝕜
hs : Convex 𝕜 s
x : 𝕜
hx : x ∈ s
y : 𝕜
hy : y ∈ s
h : x ≠ y
⊢ ∀ (hs : (interior [x -[𝕜] y]).Nonempty), (interior s).Nonempty

Tactic:
have hs' := Nonempty.mono <| interior_mono <| hs.segment_subset hx hy
-- Module: Mathlib.Analysis.Convex.Topology
Goal:
𝕜 : Type u_4
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : TopologicalSpace 𝕜
inst_4 : OrderTopology 𝕜
s : Set 𝕜
hs : Convex 𝕜 s
x : 𝕜
hx : x ∈ s
y : 𝕜
hy : y ∈ s
h : x ≠ y
hs' : ∀ (hs : (interior [x -[𝕜] y]).Nonempty), (interior s).Nonempty
⊢ ∀ (hs : x ≠ y), (interior s).Nonempty

Tactic:
rw [segment_eq_Icc', interior_Icc, nonempty_Ioo, inf_lt_sup] at hs'

Premises used: interior_Icc, segment_eq_Icc', Set.nonempty_Ioo, inf_lt_sup
-- Module: Mathlib.Analysis.Convex.Topology
Goal:
𝕜 : Type u_4
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : TopologicalSpace 𝕜
inst_4 : OrderTopology 𝕜
s : Set 𝕜
hs : Convex 𝕜 s
x : 𝕜
hx : x ∈ s
y : 𝕜
hy : y ∈ s
h : x ≠ y
hs' : ∀ (hs : x ≠ y), (interior s).Nonempty
⊢ (interior s).Nonempty

Tactic:
hs' h
-- Module: Mathlib.Analysis.Convex.Topology
Goal:
𝕜 : Type u_4
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : TopologicalSpace 𝕜
inst_4 : OrderTopology 𝕜
s : Set 𝕜
hs : Convex 𝕜 s
x : 𝕜
hx : x ∈ s
y : 𝕜
hy : y ∈ s
h : x ≠ y
hs' : ∀ (hs : x ≠ y), (interior s).Nonempty
⊢ (interior s).Nonempty

Tactic:
exact hs' h
-- Module: Mathlib.Analysis.Convex.Topology
Goal:
𝕜 : Type u_4
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : TopologicalSpace 𝕜
inst_4 : OrderTopology 𝕜
s : Set 𝕜
hs : Convex 𝕜 s
x : 𝕜
hx : x ∈ interior s
mpr : ∀ (hs : Convex 𝕜 (E := 𝕜) {x}) (hx : Membership.mem (γ := Set 𝕜) (interior {x}) x), Set.Nontrivial (α := 𝕜) {x}
mpr₁ : ∀ (h : s.Nontrivial), s.Nontrivial
⊢ s.Nontrivial

Tactic:
rcases eq_singleton_or_nontrivial (interior_subset hx) with rfl | h

Premises used: interior_subset, Set.eq_singleton_or_nontrivial, rfl
-- Module: Mathlib.Analysis.Convex.Topology
Goal:
𝕜 : Type u_4
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : TopologicalSpace 𝕜
inst_4 : OrderTopology 𝕜
x : 𝕜
hs : Convex 𝕜 (E := 𝕜) {x}
hx : Membership.mem (γ := Set 𝕜) (interior {x}) x
⊢ Membership.mem (γ := Set 𝕜) ∅ x

Tactic:
rw [interior_singleton] at hx

Premises used: interior_singleton
-- Module: Mathlib.Analysis.Convex.Topology
Goal:
𝕜 : Type u_4
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : TopologicalSpace 𝕜
inst_4 : OrderTopology 𝕜
x : 𝕜
hs : Convex 𝕜 (E := 𝕜) {x}
hx : Membership.mem (γ := Set 𝕜) ∅ x
⊢ Set.Nontrivial (α := 𝕜) {x}

Tactic:
hx.elim

Premises used: False.elim
-- Module: Mathlib.Analysis.Convex.Topology
Goal:
𝕜 : Type u_4
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : TopologicalSpace 𝕜
inst_4 : OrderTopology 𝕜
x : 𝕜
hs : Convex 𝕜 (E := 𝕜) {x}
hx : Membership.mem (γ := Set 𝕜) ∅ x
⊢ Set.Nontrivial (α := 𝕜) {x}

Tactic:
exact hx.elim

Premises used: False.elim
-- Module: Mathlib.Analysis.Convex.Topology
Goal:
𝕜 : Type u_4
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : TopologicalSpace 𝕜
inst_4 : OrderTopology 𝕜
s : Set 𝕜
hs : Convex 𝕜 s
x : 𝕜
hx : x ∈ interior s
h : s.Nontrivial
⊢ s.Nontrivial

Tactic:
h
-- Module: Mathlib.Analysis.Convex.Topology
Goal:
𝕜 : Type u_4
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : TopologicalSpace 𝕜
inst_4 : OrderTopology 𝕜
s : Set 𝕜
hs : Convex 𝕜 s
x : 𝕜
hx : x ∈ interior s
h : s.Nontrivial
⊢ s.Nontrivial

Tactic:
exact h
-- Module: Mathlib.Analysis.Convex.Topology
Goal:
𝕜 : Type u_4
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : TopologicalSpace 𝕜
inst_4 : OrderTopology 𝕜
s : Set 𝕜
hs : Convex 𝕜 s
a b : 𝕜
has : a ∈ closure[inst_3] s
hbs : b ∈ closure[inst_3] s
hs_sub : Subsingleton.{u_4 + 1} (↑s : Type u_4)
⊢ s.Subsingleton

Tactic:
simp only [subsingleton_coe] at hs_sub

Premises used: Set.subsingleton_coe
-- Module: Mathlib.Analysis.Convex.Topology
Goal:
𝕜 : Type u_4
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : TopologicalSpace 𝕜
inst_4 : OrderTopology 𝕜
s : Set 𝕜
hs : Convex 𝕜 s
a b : 𝕜
has : a ∈ closure[inst_3] s
hbs : b ∈ closure[inst_3] s
hs_sub : s.Subsingleton
⊢ Ioo a b ⊆ s

Tactic:
simp [hs_sub.closure has hbs]

Premises used: Set.Subsingleton.closure
-- Module: Mathlib.Analysis.Convex.Topology
Goal:
𝕜 : Type u_4
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : TopologicalSpace 𝕜
inst_4 : OrderTopology 𝕜
s : Set 𝕜
hs : Convex 𝕜 s
a b : 𝕜
has : a ∈ closure[inst_3] s
hbs : b ∈ closure[inst_3] s
h' : Nontrivial.{u_4} (↑s : Type u_4)
⊢ s.Nontrivial

Tactic:
simp only [nontrivial_coe_sort] at h'

Premises used: Set.nontrivial_coe_sort
-- Module: Mathlib.Analysis.Convex.Topology
Goal:
𝕜 : Type u_4
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : TopologicalSpace 𝕜
inst_4 : OrderTopology 𝕜
s : Set 𝕜
hs : Convex 𝕜 s
a b : 𝕜
has : a ∈ closure[inst_3] s
hbs : b ∈ closure[inst_3] s
h' : s.Nontrivial
⊢ Ioo a b = interior (Ioo a b)

Tactic:
interior_Ioo.symm

Premises used: interior_Ioo, Eq.symm
-- Module: Mathlib.Analysis.Convex.Topology
Goal:
𝕜 : Type u_4
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : TopologicalSpace 𝕜
inst_4 : OrderTopology 𝕜
s : Set 𝕜
hs : Convex 𝕜 s
a b : 𝕜
has : a ∈ closure[inst_3] s
hbs : b ∈ closure[inst_3] s
h' : s.Nontrivial
⊢ interior (Ioo a b) ⊆ interior (openSegment 𝕜 a b)

Tactic:
interior_mono <| Ioo_subset_openSegment

Premises used: interior_mono, Ioo_subset_openSegment
-- Module: Mathlib.Analysis.Convex.Topology
Goal:
𝕜 : Type u_4
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : TopologicalSpace 𝕜
inst_4 : OrderTopology 𝕜
s : Set 𝕜
hs : Convex 𝕜 s
a b : 𝕜
has : a ∈ closure[inst_3] s
hbs : b ∈ closure[inst_3] s
h' : s.Nontrivial
⊢ interior (openSegment 𝕜 a b) ⊆ interior (closure[inst_3] s)

Tactic:
interior_mono <| hs.closure.openSegment_subset has hbs

Premises used: interior_mono, Convex.openSegment_subset, Convex.closure
-- Module: Mathlib.Analysis.Convex.Topology
Goal:
𝕜 : Type u_4
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : TopologicalSpace 𝕜
inst_4 : OrderTopology 𝕜
s : Set 𝕜
hs : Convex 𝕜 s
a b : 𝕜
has : a ∈ closure[inst_3] s
hbs : b ∈ closure[inst_3] s
h' : s.Nontrivial
⊢ interior (closure[inst_3] s) = interior s

Tactic:
hs.interior_closure_eq_interior_of_nonempty_interior <|
      hs.nontrivial_iff_nonempty_interior.1 h'

Premises used: Convex.nontrivial_iff_nonempty_interior, Convex.interior_closure_eq_interior_of_nonempty_interior, Iff.mp
-- Module: Mathlib.Analysis.Convex.Topology
Goal:
𝕜 : Type u_4
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : TopologicalSpace 𝕜
inst_4 : OrderTopology 𝕜
s : Set 𝕜
hs : Convex 𝕜 s
a b : 𝕜
has : a ∈ closure[inst_3] s
hbs : b ∈ closure[inst_3] s
h' : s.Nontrivial
⊢ interior s ⊆ s

Tactic:
interior_subset

Premises used: interior_subset
-- Module: Mathlib.Analysis.Convex.Topology
Goal:
𝕜 : Type u_4
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : TopologicalSpace 𝕜
inst_4 : OrderTopology 𝕜
s : Set 𝕜
hs : Convex 𝕜 s
a b : 𝕜
has : a ∈ closure[inst_3] s
hbs : b ∈ closure[inst_3] s
h' : s.Nontrivial
⊢ Ioo a b ⊆ s

Tactic:
calc Ioo a b
    _ = interior (Ioo a b) := interior_Ioo.symm
    _ ⊆ interior (openSegment 𝕜 a b) := interior_mono <| Ioo_subset_openSegment
    _ ⊆ interior (closure s) := interior_mono <| hs.closure.openSegment_subset has hbs
    _ = interior s := hs.interior_closure_eq_interior_of_nonempty_interior <|
      hs.nontrivial_iff_nonempty_interior.1 h'
    _ ⊆ s := interior_subset

Premises used: Convex.nontrivial_iff_nonempty_interior, interior_subset, interior_mono, Convex.interior_closure_eq_interior_of_nonempty_interior, Convex.openSegment_subset, Convex.closure, Ioo_subset_openSegment, closure, interior, Iff.mp, openSegment, interior_Ioo, Eq.symm, Set.Ioo
-- Module: Mathlib.Analysis.Convex.Topology
Goal:
𝕜 : Type u_4
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : TopologicalSpace 𝕜
inst_4 : OrderTopology 𝕜
s : Set 𝕜
hs : Convex 𝕜 s
a b : 𝕜
has : a ∈ closure[inst_3] s
hbs : b ∈ closure[inst_3] s
⊢ Subsingleton.{u_4 + 1} (↑s : Type u_4) ∨ Nontrivial.{u_4} (↑s : Type u_4)

Tactic:
cases subsingleton_or_nontrivial s with
  | inl hs_sub =>
    simp only [subsingleton_coe] at hs_sub
    simp [hs_sub.closure has hbs]
  | inr h' =>
    simp only [nontrivial_coe_sort] at h'
    calc Ioo a b
    _ = interior (Ioo a b) := interior_Ioo.symm
    _ ⊆ interior (openSegment 𝕜 a b) := interior_mono <| Ioo_subset_openSegment
    _ ⊆ interior (closure s) := interior_mono <| hs.closure.openSegment_subset has hbs
    _ = interior s := hs.interior_closure_eq_interior_of_nonempty_interior <|
      hs.nontrivial_iff_nonempty_interior.1 h'
    _ ⊆ s := interior_subset

Premises used: interior_subset, interior_mono, Set.Elem, subsingleton_or_nontrivial, Convex.interior_closure_eq_interior_of_nonempty_interior, Convex.openSegment_subset, Convex.closure, Ioo_subset_openSegment, closure, interior, Set.subsingleton_coe, openSegment, interior_Ioo, Eq.symm, Set.Ioo, Set.nontrivial_coe_sort
-- Module: Mathlib.Analysis.Convex.Topology
Goal:
𝕜 : Type u_4
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : TopologicalSpace 𝕜
inst_4 : OrderTopology 𝕜
s : Set 𝕜
hs : Convex 𝕜 s
a : 𝕜
has : a ∈ closure[inst_3] s
h' : (s ∩ Iio a).Nonempty
obtain : ∀ (b : 𝕜) (hbs : b ∈ s) (hba : b ∈ Iio a), 𝓝[s ∩ Iio a] a = 𝓝[<] a
⊢ 𝓝[s ∩ Iio a] a = 𝓝[<] a

Tactic:
obtain ⟨b, hbs, hba⟩ := h'
-- Module: Mathlib.Analysis.Convex.Topology
Goal:
𝕜 : Type u_4
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : TopologicalSpace 𝕜
inst_4 : OrderTopology 𝕜
s : Set 𝕜
hs : Convex 𝕜 s
a : 𝕜
has : a ∈ closure[inst_3] s
b : 𝕜
hbs : b ∈ s
hba : b ∈ Iio a
⊢ 𝓝[s ∩ Iio a] a = 𝓝[<] a

Tactic:
nhdsWithin_inter_of_mem (mem_nhdsLT_iff_exists_Ioo_subset.2 ⟨b, hba, ?_⟩)

Premises used: Iff.mpr, nhdsWithin_inter_of_mem, mem_nhdsLT_iff_exists_Ioo_subset, And.intro, Exists.intro
-- Module: Mathlib.Analysis.Convex.Topology
Goal:
𝕜 : Type u_4
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : TopologicalSpace 𝕜
inst_4 : OrderTopology 𝕜
s : Set 𝕜
hs : Convex 𝕜 s
a : 𝕜
has : a ∈ closure[inst_3] s
b : 𝕜
hbs : b ∈ s
hba : b ∈ Iio a
refine : Ioo b a ⊆ s
⊢ 𝓝[s ∩ Iio a] a = 𝓝[<] a

Tactic:
refine nhdsWithin_inter_of_mem (mem_nhdsLT_iff_exists_Ioo_subset.2 ⟨b, hba, ?_⟩)

Premises used: Iff.mpr, nhdsWithin_inter_of_mem, mem_nhdsLT_iff_exists_Ioo_subset, And.intro, Exists.intro
-- Module: Mathlib.Analysis.Convex.Topology
Goal:
𝕜 : Type u_4
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : TopologicalSpace 𝕜
inst_4 : OrderTopology 𝕜
s : Set 𝕜
hs : Convex 𝕜 s
a : 𝕜
has : a ∈ closure[inst_3] s
b : 𝕜
hbs : b ∈ s
hba : b ∈ Iio a
⊢ Ioo b a ⊆ s

Tactic:
hs.Ioo_subset_of_mem_closure (subset_closure hbs) has

Premises used: Convex.Ioo_subset_of_mem_closure, subset_closure
-- Module: Mathlib.Analysis.Convex.Topology
Goal:
𝕜 : Type u_4
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : TopologicalSpace 𝕜
inst_4 : OrderTopology 𝕜
s : Set 𝕜
hs : Convex 𝕜 s
a : 𝕜
has : a ∈ closure[inst_3] s
b : 𝕜
hbs : b ∈ s
hba : b ∈ Iio a
⊢ Ioo b a ⊆ s

Tactic:
exact hs.Ioo_subset_of_mem_closure (subset_closure hbs) has

Premises used: Convex.Ioo_subset_of_mem_closure, subset_closure
-- Module: Mathlib.Analysis.Convex.Topology
Goal:
𝕜 : Type u_4
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : TopologicalSpace 𝕜
inst_4 : OrderTopology 𝕜
s : Set 𝕜
hs : Convex 𝕜 s
a : 𝕜
has : a ∈ closure[inst_3] s
h' : (s ∩ Ioi a).Nonempty
obtain : ∀ (b : 𝕜) (hbs : b ∈ s) (hba : b ∈ Ioi a), 𝓝[s ∩ Ioi a] a = 𝓝[>] a
⊢ 𝓝[s ∩ Ioi a] a = 𝓝[>] a

Tactic:
obtain ⟨b, hbs, hba⟩ := h'
-- Module: Mathlib.Analysis.Convex.Topology
Goal:
𝕜 : Type u_4
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : TopologicalSpace 𝕜
inst_4 : OrderTopology 𝕜
s : Set 𝕜
hs : Convex 𝕜 s
a : 𝕜
has : a ∈ closure[inst_3] s
b : 𝕜
hbs : b ∈ s
hba : b ∈ Ioi a
⊢ 𝓝[s ∩ Ioi a] a = 𝓝[>] a

Tactic:
nhdsWithin_inter_of_mem (mem_nhdsGT_iff_exists_Ioo_subset.2 ⟨b, hba, ?_⟩)

Premises used: Iff.mpr, nhdsWithin_inter_of_mem, And.intro, Exists.intro, mem_nhdsGT_iff_exists_Ioo_subset
-- Module: Mathlib.Analysis.Convex.Topology
Goal:
𝕜 : Type u_4
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : TopologicalSpace 𝕜
inst_4 : OrderTopology 𝕜
s : Set 𝕜
hs : Convex 𝕜 s
a : 𝕜
has : a ∈ closure[inst_3] s
b : 𝕜
hbs : b ∈ s
hba : b ∈ Ioi a
refine : Ioo a b ⊆ s
⊢ 𝓝[s ∩ Ioi a] a = 𝓝[>] a

Tactic:
refine nhdsWithin_inter_of_mem (mem_nhdsGT_iff_exists_Ioo_subset.2 ⟨b, hba, ?_⟩)

Premises used: Iff.mpr, nhdsWithin_inter_of_mem, And.intro, Exists.intro, mem_nhdsGT_iff_exists_Ioo_subset
-- Module: Mathlib.Analysis.Convex.Topology
Goal:
𝕜 : Type u_4
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : TopologicalSpace 𝕜
inst_4 : OrderTopology 𝕜
s : Set 𝕜
hs : Convex 𝕜 s
a : 𝕜
has : a ∈ closure[inst_3] s
b : 𝕜
hbs : b ∈ s
hba : b ∈ Ioi a
⊢ Ioo a b ⊆ s

Tactic:
hs.Ioo_subset_of_mem_closure has (subset_closure hbs)

Premises used: Convex.Ioo_subset_of_mem_closure, subset_closure
-- Module: Mathlib.Analysis.Convex.Topology
Goal:
𝕜 : Type u_4
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : TopologicalSpace 𝕜
inst_4 : OrderTopology 𝕜
s : Set 𝕜
hs : Convex 𝕜 s
a : 𝕜
has : a ∈ closure[inst_3] s
b : 𝕜
hbs : b ∈ s
hba : b ∈ Ioi a
⊢ Ioo a b ⊆ s

Tactic:
exact hs.Ioo_subset_of_mem_closure has (subset_closure hbs)

Premises used: Convex.Ioo_subset_of_mem_closure, subset_closure
-- Module: Mathlib.Analysis.Convex.Topology
Goal:
𝕜 : Type u_4
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : TopologicalSpace 𝕜
inst_4 : OrderTopology 𝕜
s : Set 𝕜
hs : Convex 𝕜 s
a : 𝕜
has : a ∈ closure[inst_3] s
h_Iio : (s ∩ Iio a).Nonempty
h_Ioi : (s ∩ Ioi a).Nonempty
rw : 𝓝[s ∩ Iio a] a ⊔ 𝓝[s ∩ Ioi a] a = 𝓝[<] a ⊔ 𝓝[>] a
⊢ 𝓝[s \ {a}] a = 𝓝[≠] a

Tactic:
rw [diff_eq, ← Iio_union_Ioi, inter_union_distrib_left, nhdsWithin_union, nhdsWithin_union]

Premises used: Set.diff_eq, Set.Iio_union_Ioi, nhdsWithin_union, Set.inter_union_distrib_left
-- Module: Mathlib.Analysis.Convex.Topology
Goal:
𝕜 : Type u_4
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : TopologicalSpace 𝕜
inst_4 : OrderTopology 𝕜
s : Set 𝕜
hs : Convex 𝕜 s
a : 𝕜
has : a ∈ closure[inst_3] s
h_Iio : (s ∩ Iio a).Nonempty
h_Ioi : (s ∩ Ioi a).Nonempty
⊢ 𝓝[s ∩ Iio a] a ⊔ 𝓝[s ∩ Ioi a] a = 𝓝[<] a ⊔ 𝓝[>] a

Tactic:
simp [hs.nhdsWithin_inter_Ioi_eq_nhdsGT has h_Ioi, hs.nhdsWithin_inter_Iio_eq_nhdsLT has h_Iio]

Premises used: Convex.nhdsWithin_inter_Iio_eq_nhdsLT, Convex.nhdsWithin_inter_Ioi_eq_nhdsGT
-- Module: Mathlib.Analysis.Convex.Topology
Goal:
𝕜 : Type u_4
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : TopologicalSpace 𝕜
inst_4 : OrderTopology 𝕜
s : Set 𝕜
hs : Convex 𝕜 s
a : 𝕜
has : a ∈ closure[inst_3] s
h_Iio : (s ∩ Iio a).Nonempty
h_Ioi : s ∩ Ioi a = ∅
rw : 𝓝[s ∩ Iio a] a ⊔ 𝓝[s ∩ Ioi a] a = 𝓝[<] a
⊢ 𝓝[s \ {a}] a = 𝓝[<] a

Tactic:
rw [diff_eq, ← Iio_union_Ioi, inter_union_distrib_left, nhdsWithin_union]

Premises used: Set.diff_eq, Set.Iio_union_Ioi, nhdsWithin_union, Set.inter_union_distrib_left
-- Module: Mathlib.Analysis.Convex.Topology
Goal:
𝕜 : Type u_4
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : TopologicalSpace 𝕜
inst_4 : OrderTopology 𝕜
s : Set 𝕜
hs : Convex 𝕜 s
a : 𝕜
has : a ∈ closure[inst_3] s
h_Iio : (s ∩ Iio a).Nonempty
h_Ioi : s ∩ Ioi a = ∅
⊢ 𝓝[s ∩ Iio a] a ⊔ 𝓝[s ∩ Ioi a] a = 𝓝[<] a

Tactic:
simp [h_Ioi, hs.nhdsWithin_inter_Iio_eq_nhdsLT has h_Iio]

Premises used: Convex.nhdsWithin_inter_Iio_eq_nhdsLT
-- Module: Mathlib.Analysis.Convex.Topology
Goal:
𝕜 : Type u_4
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : TopologicalSpace 𝕜
inst_4 : OrderTopology 𝕜
s : Set 𝕜
hs : Convex 𝕜 s
a : 𝕜
has : a ∈ closure[inst_3] s
h_Iio : s ∩ Iio a = ∅
h_Ioi : (s ∩ Ioi a).Nonempty
rw : 𝓝[s ∩ Iio a] a ⊔ 𝓝[s ∩ Ioi a] a = 𝓝[>] a
⊢ 𝓝[s \ {a}] a = 𝓝[>] a

Tactic:
rw [diff_eq, ← Iio_union_Ioi, inter_union_distrib_left, nhdsWithin_union]

Premises used: Set.diff_eq, Set.Iio_union_Ioi, nhdsWithin_union, Set.inter_union_distrib_left
-- Module: Mathlib.Analysis.Convex.Topology
Goal:
𝕜 : Type u_4
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : TopologicalSpace 𝕜
inst_4 : OrderTopology 𝕜
s : Set 𝕜
hs : Convex 𝕜 s
a : 𝕜
has : a ∈ closure[inst_3] s
h_Iio : s ∩ Iio a = ∅
h_Ioi : (s ∩ Ioi a).Nonempty
⊢ 𝓝[s ∩ Iio a] a ⊔ 𝓝[s ∩ Ioi a] a = 𝓝[>] a

Tactic:
simp [h_Iio, hs.nhdsWithin_inter_Ioi_eq_nhdsGT has h_Ioi]

Premises used: Convex.nhdsWithin_inter_Ioi_eq_nhdsGT
-- Module: Mathlib.Analysis.Convex.Topology
Goal:
𝕜 : Type u_4
inst : LinearOrder 𝕜
inst_1 : TopologicalSpace 𝕜
inst_2 : OrderTopology 𝕜
s : Set 𝕜
a : 𝕜
h : ∀ x ∈ closure[inst_1] s, Ioo x a ⊆ s
inl : ∀ (hs' : s ∩ Iio a = ∅), ∀ᶠ (x : 𝕜) in 𝓝[s ∩ Iio a] a, s \ {a} ∈ 𝓝 x
inr : ∀ (b : 𝕜) (hbs : b ∈ s) (hba : b ∈ Iio a), ∀ᶠ (x : 𝕜) in 𝓝[s ∩ Iio a] a, s \ {a} ∈ 𝓝 x
⊢ ∀ᶠ (x : 𝕜) in 𝓝[s ∩ Iio a] a, s \ {a} ∈ 𝓝 x

Tactic:
rcases eq_empty_or_nonempty (s ∩ Iio a) with hs' | ⟨b, hbs, hba⟩

Premises used: Inter.inter, Set.eq_empty_or_nonempty, Set.Iio
-- Module: Mathlib.Analysis.Convex.Topology
Goal:
𝕜 : Type u_4
inst : LinearOrder 𝕜
inst_1 : TopologicalSpace 𝕜
inst_2 : OrderTopology 𝕜
s : Set 𝕜
a : 𝕜
h : ∀ x ∈ closure[inst_1] s, Ioo x a ⊆ s
hs' : s ∩ Iio a = ∅
⊢ ∀ᶠ (x : 𝕜) in 𝓝[s ∩ Iio a] a, s \ {a} ∈ 𝓝 x

Tactic:
simp [hs']
-- Module: Mathlib.Analysis.Convex.Topology
Goal:
𝕜 : Type u_4
inst : LinearOrder 𝕜
inst_1 : TopologicalSpace 𝕜
inst_2 : OrderTopology 𝕜
s : Set 𝕜
a : 𝕜
h : ∀ x ∈ closure[inst_1] s, Ioo x a ⊆ s
b : 𝕜
hbs : b ∈ s
hba : b ∈ Iio a
⊢ Ioo b a ⊆ s

Tactic:
have : Ioo b a ⊆ s := h b (subset_closure hbs)
-- Module: Mathlib.Analysis.Convex.Topology
Goal:
𝕜 : Type u_4
inst : LinearOrder 𝕜
inst_1 : TopologicalSpace 𝕜
inst_2 : OrderTopology 𝕜
s : Set 𝕜
a : 𝕜
h : ∀ x ∈ closure[inst_1] s, Ioo x a ⊆ s
b : 𝕜
hbs : b ∈ s
hba : b ∈ Iio a
this : Ioo b a ⊆ s
apply : Ioo b a ∈ 𝓝[s ∩ Iio a] a
apply₁ : ∀ (x : 𝕜) (hx : x ∈ Ioo b a), s \ {a} ∈ 𝓝 x
⊢ ∀ᶠ (x : 𝕜) in 𝓝[s ∩ Iio a] a, s \ {a} ∈ 𝓝 x

Tactic:
apply eventually_of_mem (U := Ioo b a) ?_ fun x hx ↦ ?_

Premises used: Filter.eventually_of_mem
-- Module: Mathlib.Analysis.Convex.Topology
Goal:
𝕜 : Type u_4
inst : LinearOrder 𝕜
inst_1 : TopologicalSpace 𝕜
inst_2 : OrderTopology 𝕜
s : Set 𝕜
a : 𝕜
h : ∀ x ∈ closure[inst_1] s, Ioo x a ⊆ s
b : 𝕜
hbs : b ∈ s
hba : b ∈ Iio a
this : Ioo b a ⊆ s
⊢ Ioo b a ∈ 𝓝[s ∩ Iio a] a

Tactic:
mem_nhdsWithin.2 ⟨Ioi b, isOpen_Ioi, hba, fun _ ⟨h₁, _, h₂⟩ ↦ ⟨h₁, h₂⟩⟩

Premises used: Iff.mpr, Set.Ioi, Membership.mem, mem_nhdsWithin, isOpen_Ioi, And.intro, Exists.intro, _private.0.diff_singleton_eventually_mem_nhds_left.match_1, Set.Ioo
-- Module: Mathlib.Analysis.Convex.Topology
Goal:
𝕜 : Type u_4
inst : LinearOrder 𝕜
inst_1 : TopologicalSpace 𝕜
inst_2 : OrderTopology 𝕜
s : Set 𝕜
a : 𝕜
h : ∀ x ∈ closure[inst_1] s, Ioo x a ⊆ s
b : 𝕜
hbs : b ∈ s
hba : b ∈ Iio a
this : Ioo b a ⊆ s
⊢ Ioo b a ∈ 𝓝[s ∩ Iio a] a

Tactic:
exact mem_nhdsWithin.2 ⟨Ioi b, isOpen_Ioi, hba, fun _ ⟨h₁, _, h₂⟩ ↦ ⟨h₁, h₂⟩⟩
-- Module: Mathlib.Analysis.Convex.Topology
Goal:
𝕜 : Type u_4
inst : LinearOrder 𝕜
inst_1 : TopologicalSpace 𝕜
inst_2 : OrderTopology 𝕜
s : Set 𝕜
a : 𝕜
h : ∀ x ∈ closure[inst_1] s, Ioo x a ⊆ s
b : 𝕜
hbs : b ∈ s
hba : b ∈ Iio a
this : Ioo b a ⊆ s
x : 𝕜
hx : x ∈ Ioo b a
⊢ s \ {a} ∈ 𝓝 x

Tactic:
mem_nhds_iff.2 ⟨Ioo b a, subset_diff_singleton this right_notMem_Ioo, isOpen_Ioo, hx⟩

Premises used: Iff.mpr, mem_nhds_iff, isOpen_Ioo, Set.right_notMem_Ioo, Set.subset_diff_singleton, And.intro, Exists.intro, Set.Ioo
-- Module: Mathlib.Analysis.Convex.Topology
Goal:
𝕜 : Type u_4
inst : LinearOrder 𝕜
inst_1 : TopologicalSpace 𝕜
inst_2 : OrderTopology 𝕜
s : Set 𝕜
a : 𝕜
h : ∀ x ∈ closure[inst_1] s, Ioo x a ⊆ s
b : 𝕜
hbs : b ∈ s
hba : b ∈ Iio a
this : Ioo b a ⊆ s
x : 𝕜
hx : x ∈ Ioo b a
⊢ s \ {a} ∈ 𝓝 x

Tactic:
exact mem_nhds_iff.2 ⟨Ioo b a, subset_diff_singleton this right_notMem_Ioo, isOpen_Ioo, hx⟩

Premises used: Iff.mpr, mem_nhds_iff, isOpen_Ioo, Set.right_notMem_Ioo, Set.subset_diff_singleton, And.intro, Exists.intro, Set.Ioo