awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Order.AtTopBotIxx
Goal:
X : Type u_1
inst : LinearOrder X
inst_1 : TopologicalSpace X
inst_2 : OrderTopology X
s : Set X
b : X
hsne : s.Nonempty
this : Nonempty.{u_1 + 1} (↑s : Type u_1)
hsub : s ⊆ Iio b
h : ∀ a < b, (s ∩ Ioo a b).Nonempty
a : X
hab : a < b
c : X
hcs : c ∈ s
hc : c ∈ Ioo a b
⊢ True ∧ Ici (Subtype.mk (p := fun (x : X) ↦ x ∈ s) c hcs) ⊆ Subtype.val (p := fun (x : X) ↦ x ∈ s) ⁻¹' Ioo a b

Tactic:
simp_all [subset_def, hc.1.trans_le]

Premises used: Set.subset_def, And.left, LT.lt.trans_le
-- Module: Mathlib.Topology.Order.AtTopBotIxx
Goal:
X : Type u_1
inst : LinearOrder X
inst_1 : TopologicalSpace X
inst_2 : OrderTopology X
s : Set X
b : X
hsne : s.Nonempty
this : Nonempty.{u_1 + 1} (↑s : Type u_1)
hsub : s ⊆ Iio b
h : ∀ a < b, (s ∩ Ioo a b).Nonempty
a : X
has : a ∈ s
right : Subtype.val (p := fun (x : X) ↦ x ∈ s) ⁻¹' Ioo a b ⊆ Ici (Subtype.mk (p := fun (x : X) ↦ x ∈ s) a has)
⊢ ∃ i < b, Subtype.val (p := fun (x : X) ↦ x ∈ s) ⁻¹' Ioo i b ⊆ Ici (Subtype.mk (p := fun (x : X) ↦ x ∈ s) a has)

Tactic:
use a, hsub has
-- Module: Mathlib.Topology.Order.AtTopBotIxx
Goal:
X : Type u_1
inst : LinearOrder X
inst_1 : TopologicalSpace X
inst_2 : OrderTopology X
s : Set X
b : X
hsne : s.Nonempty
this : Nonempty.{u_1 + 1} (↑s : Type u_1)
hsub : s ⊆ Iio b
h : ∀ a < b, (s ∩ Ioo a b).Nonempty
a : X
has : a ∈ s
⊢ Subtype.val (p := fun (x : X) ↦ x ∈ s) ⁻¹' Ioo a b ⊆ Ici (Subtype.mk (p := fun (x : X) ↦ x ∈ s) a has)

Tactic:
simp_all [subset_def, le_of_lt]

Premises used: Set.subset_def, le_of_lt
-- Module: Mathlib.Topology.Order.AtTopBotIxx
Goal:
X : Type u_1
inst : LinearOrder X
inst_1 : TopologicalSpace X
inst_2 : OrderTopology X
s : Set X
b : X
hsne : s.Nonempty
this_1 : Nonempty.{u_1 + 1} (↑s : Type u_1)
hsub : ¬s ⊆ Iio b
this : ¬Tendsto (α := (↑s : Type u_1)) (Subtype.val (p := fun (x : X) ↦ x ∈ s)) atTop (𝓝[<] b)
contrapose :
  ∀
    (this :
      ¬(Eq (α := Filter { x : X // x ∈ s }) (comap (Subtype.val (p := fun (x : X) ↦ x ∈ s)) (𝓝[<] b)) atTop ↔
          s ⊆ Iio b ∧ ∀ a < b, (s ∩ Ioo a b).Nonempty)),
    Tendsto (α := (↑s : Type u_1)) (Subtype.val (p := fun (x : X) ↦ x ∈ s)) atTop (𝓝[<] b)
⊢ Eq (α := Filter { x : X // x ∈ s }) (comap (Subtype.val (p := fun (x : X) ↦ x ∈ s)) (𝓝[<] b)) atTop ↔
    s ⊆ Iio b ∧ ∀ a < b, (s ∩ Ioo a b).Nonempty

Tactic:
contrapose this
-- Module: Mathlib.Topology.Order.AtTopBotIxx
Goal:
X : Type u_1
inst : LinearOrder X
inst_1 : TopologicalSpace X
inst_2 : OrderTopology X
s : Set X
b : X
hsne : s.Nonempty
this_1 : Nonempty.{u_1 + 1} (↑s : Type u_1)
hsub : ¬s ⊆ Iio b
this :
  ¬(Eq (α := Filter { x : X // x ∈ s }) (comap (Subtype.val (p := fun (x : X) ↦ x ∈ s)) (𝓝[<] b)) atTop ↔
      s ⊆ Iio b ∧ ∀ a < b, (s ∩ Ioo a b).Nonempty)
⊢ Tendsto (α := (↑s : Type u_1)) (Subtype.val (p := fun (x : X) ↦ x ∈ s)) atTop (𝓝[<] b)

Tactic:
simp_all [tendsto_iff_comap]

Premises used: Filter.tendsto_iff_comap
-- Module: Mathlib.Topology.Order.AtTopBotIxx
Goal:
X : Type u_1
inst : LinearOrder X
inst_1 : TopologicalSpace X
inst_2 : OrderTopology X
s : Set X
b : X
hsne : s.Nonempty
this : Nonempty.{u_1 + 1} (↑s : Type u_1)
hsub : ¬s ⊆ Iio b
neg : ¬Tendsto (α := (↑s : Type u_1)) (Subtype.val (p := fun (x : X) ↦ x ∈ s)) atTop (𝓝[<] b)
⊢ Eq (α := Filter { x : X // x ∈ s }) (comap (Subtype.val (p := fun (x : X) ↦ x ∈ s)) (𝓝[<] b)) atTop ↔
    s ⊆ Iio b ∧ ∀ a < b, (s ∩ Ioo a b).Nonempty

Tactic:
suffices ¬Tendsto (↑) (atTop : Filter s) (𝓝[<] b) by
      contrapose this
      simp_all [tendsto_iff_comap]
-- Module: Mathlib.Topology.Order.AtTopBotIxx
Goal:
X : Type u_1
inst : LinearOrder X
inst_1 : TopologicalSpace X
inst_2 : OrderTopology X
s : Set X
b : X
hsne : s.Nonempty
this : Nonempty.{u_1 + 1} (↑s : Type u_1)
hsub : ¬s ⊆ Iio b
h : Tendsto (α := (↑s : Type u_1)) (Subtype.val (p := fun (x : X) ↦ x ∈ s)) atTop (𝓝[<] b)
neg : ∀ (a : X) (has : a ∈ s) (ha : a ∉ Iio b), False
⊢ False

Tactic:
rcases not_subset_iff_exists_mem_notMem.mp hsub with ⟨a, has, ha⟩

Premises used: Set.not_subset_iff_exists_mem_notMem, Iff.mp
-- Module: Mathlib.Topology.Order.AtTopBotIxx
Goal:
X : Type u_1
inst : LinearOrder X
inst_1 : TopologicalSpace X
inst_2 : OrderTopology X
s : Set X
b : X
hsne : s.Nonempty
this : Nonempty.{u_1 + 1} (↑s : Type u_1)
hsub : ¬s ⊆ Iio b
h : Tendsto (α := (↑s : Type u_1)) (Subtype.val (p := fun (x : X) ↦ x ∈ s)) atTop (𝓝[<] b)
a : X
has : a ∈ s
ha : a ∉ Iio b
neg :
  ∀ (c : X) (hcs : c ∈ s) (hcb : (↑(Subtype.mk (p := fun (x : X) ↦ x ∈ s) c hcs) : X) ∈ Iio b)
    (hac : Subtype.mk (p := fun (x : X) ↦ x ∈ s) a has ≤ Subtype.mk (p := fun (x : X) ↦ x ∈ s) c hcs), False
⊢ False

Tactic:
rcases h.eventually eventually_mem_nhdsWithin |>.and (eventually_ge_atTop ⟨a, has⟩) |>.exists
      with ⟨⟨c, hcs⟩, hcb, hac⟩

Premises used: eventually_mem_nhdsWithin, Filter.Eventually.and, Filter.Eventually.exists, Filter.Tendsto.eventually, Filter.eventually_ge_atTop
-- Module: Mathlib.Topology.Order.AtTopBotIxx
Goal:
X : Type u_1
inst : LinearOrder X
inst_1 : TopologicalSpace X
inst_2 : OrderTopology X
s : Set X
b : X
hsne : s.Nonempty
this : Nonempty.{u_1 + 1} (↑s : Type u_1)
hsub : ¬s ⊆ Iio b
h : Tendsto (α := (↑s : Type u_1)) (Subtype.val (p := fun (x : X) ↦ x ∈ s)) atTop (𝓝[<] b)
a : X
has : a ∈ s
ha : a ∉ Iio b
c : X
hcs : c ∈ s
hcb : (↑(Subtype.mk (p := fun (x : X) ↦ x ∈ s) c hcs) : X) ∈ Iio b
hac : Subtype.mk (p := fun (x : X) ↦ x ∈ s) a has ≤ Subtype.mk (p := fun (x : X) ↦ x ∈ s) c hcs
neg : a < a
⊢ False

Tactic:
apply lt_irrefl a

Premises used: lt_irrefl
-- Module: Mathlib.Topology.Order.AtTopBotIxx
Goal:
X : Type u_1
inst : LinearOrder X
inst_1 : TopologicalSpace X
inst_2 : OrderTopology X
s : Set X
b : X
hsne : s.Nonempty
this : Nonempty.{u_1 + 1} (↑s : Type u_1)
hsub : ¬s ⊆ Iio b
h : Tendsto (α := (↑s : Type u_1)) (Subtype.val (p := fun (x : X) ↦ x ∈ s)) atTop (𝓝[<] b)
a : X
has : a ∈ s
ha : a ∉ Iio b
c : X
hcs : c ∈ s
hcb : (↑(Subtype.mk (p := fun (x : X) ↦ x ∈ s) c hcs) : X) ∈ Iio b
hac : Subtype.mk (p := fun (x : X) ↦ x ∈ s) a has ≤ Subtype.mk (p := fun (x : X) ↦ x ∈ s) c hcs
⊢ a ≤ c

Tactic:
simpa using hac
-- Module: Mathlib.Topology.Order.AtTopBotIxx
Goal:
X : Type u_1
inst : LinearOrder X
inst_1 : TopologicalSpace X
inst_2 : OrderTopology X
s : Set X
b : X
hsne : s.Nonempty
this : Nonempty.{u_1 + 1} (↑s : Type u_1)
hsub : ¬s ⊆ Iio b
h : Tendsto (α := (↑s : Type u_1)) (Subtype.val (p := fun (x : X) ↦ x ∈ s)) atTop (𝓝[<] b)
a : X
has : a ∈ s
ha : a ∉ Iio b
c : X
hcs : c ∈ s
hcb : (↑(Subtype.mk (p := fun (x : X) ↦ x ∈ s) c hcs) : X) ∈ Iio b
hac : Subtype.mk (p := fun (x : X) ↦ x ∈ s) a has ≤ Subtype.mk (p := fun (x : X) ↦ x ∈ s) c hcs
⊢ c < b

Tactic:
simpa using hcb
-- Module: Mathlib.Topology.Order.AtTopBotIxx
Goal:
X : Type u_1
inst : LinearOrder X
inst_1 : TopologicalSpace X
inst_2 : OrderTopology X
s : Set X
b : X
hsne : s.Nonempty
this : Nonempty.{u_1 + 1} (↑s : Type u_1)
hsub : ¬s ⊆ Iio b
h : Tendsto (α := (↑s : Type u_1)) (Subtype.val (p := fun (x : X) ↦ x ∈ s)) atTop (𝓝[<] b)
a : X
has : a ∈ s
ha : a ∉ Iio b
c : X
hcs : c ∈ s
hcb : (↑(Subtype.mk (p := fun (x : X) ↦ x ∈ s) c hcs) : X) ∈ Iio b
hac : Subtype.mk (p := fun (x : X) ↦ x ∈ s) a has ≤ Subtype.mk (p := fun (x : X) ↦ x ∈ s) c hcs
⊢ b ≤ a

Tactic:
simpa using ha
-- Module: Mathlib.Topology.Order.AtTopBotIxx
Goal:
X : Type u_1
inst : LinearOrder X
inst_1 : TopologicalSpace X
inst_2 : OrderTopology X
s : Set X
b : X
hsne : s.Nonempty
this : Nonempty.{u_1 + 1} (↑s : Type u_1)
hsub : ¬s ⊆ Iio b
h : Tendsto (α := (↑s : Type u_1)) (Subtype.val (p := fun (x : X) ↦ x ∈ s)) atTop (𝓝[<] b)
a : X
has : a ∈ s
ha : a ∉ Iio b
c : X
hcs : c ∈ s
hcb : (↑(Subtype.mk (p := fun (x : X) ↦ x ∈ s) c hcs) : X) ∈ Iio b
hac : Subtype.mk (p := fun (x : X) ↦ x ∈ s) a has ≤ Subtype.mk (p := fun (x : X) ↦ x ∈ s) c hcs
a₁ : a ≤ c
a₂ : c < b
a₃ : b ≤ a
⊢ a < a

Tactic:
calc
      a ≤ c := by simpa using hac
      _ < b := by simpa using hcb
      _ ≤ a := by simpa using ha
-- Module: Mathlib.Topology.Order.AtTopBotIxx
Goal:
X : Type u_1
inst : LinearOrder X
inst_1 : TopologicalSpace X
inst_2 : OrderTopology X
s : Set X
b : X
⊢ Eq (α := Filter { x : X // x ∈ s }) (comap (Subtype.val (p := fun (x : X) ↦ x ∈ s)) (𝓝[>] b)) atBot ↔
    s ⊆ Ioi b ∧ (s.Nonempty → ∀ a > b, (s ∩ Ioo b a).Nonempty)

Tactic:
comap_coe_nhdsLT_eq_atTop_iff (s := OrderDual.ofDual ⁻¹' s) (b := OrderDual.toDual b)
    |>.trans ?_

Premises used: Set.Ioi, Set.Mem, setOf, comap_coe_nhdsLT_eq_atTop_iff, Set.preimage, Iff.trans, Filter.atBot, Set.Iic, OrderDual
-- Module: Mathlib.Topology.Order.AtTopBotIxx
Goal:
X : Type u_1
inst : LinearOrder X
inst_1 : TopologicalSpace X
inst_2 : OrderTopology X
s : Set X
b : X
refine :
  Subset (α := Set Xᵒᵈ) ((⇑ofDual : (a : Xᵒᵈ) → X) ⁻¹' s : Set Xᵒᵈ) (Iio ((toDual : (a : X) → Xᵒᵈ) b) : Set Xᵒᵈ) ∧
      (Set.Nonempty (α := Xᵒᵈ) ((⇑ofDual : (a : Xᵒᵈ) → X) ⁻¹' s) →
        ∀ a < (toDual : (a : X) → Xᵒᵈ) b,
          ((⇑ofDual : (a : Xᵒᵈ) → X) ⁻¹' s ∩ Ioo a ((toDual : (a : X) → Xᵒᵈ) b)).Nonempty) ↔
    s ⊆ Ioi b ∧ (s.Nonempty → ∀ a > b, (s ∩ Ioo b a).Nonempty)
⊢ Eq (α := Filter { x : X // x ∈ s }) (comap (Subtype.val (p := fun (x : X) ↦ x ∈ s)) (𝓝[>] b)) atBot ↔
    s ⊆ Ioi b ∧ (s.Nonempty → ∀ a > b, (s ∩ Ioo b a).Nonempty)

Tactic:
refine comap_coe_nhdsLT_eq_atTop_iff (s := OrderDual.ofDual ⁻¹' s) (b := OrderDual.toDual b)
    |>.trans ?_

Premises used: comap_coe_nhdsLT_eq_atTop_iff, Iff.trans
-- Module: Mathlib.Topology.Order.AtTopBotIxx
Goal:
X : Type u_1
inst : LinearOrder X
inst_1 : TopologicalSpace X
inst_2 : OrderTopology X
s : Set X
b : X
⊢ Subset (α := Set Xᵒᵈ) ((⇑ofDual : (a : Xᵒᵈ) → X) ⁻¹' s : Set Xᵒᵈ) (Iio ((toDual : (a : X) → Xᵒᵈ) b) : Set Xᵒᵈ) ∧
      (Set.Nonempty (α := Xᵒᵈ) ((⇑ofDual : (a : Xᵒᵈ) → X) ⁻¹' s) →
        ∀ a < (toDual : (a : X) → Xᵒᵈ) b,
          ((⇑ofDual : (a : Xᵒᵈ) → X) ⁻¹' s ∩ Ioo a ((toDual : (a : X) → Xᵒᵈ) b)).Nonempty) ↔
    s ⊆ Ioi b ∧ (s.Nonempty → ∀ a > b, (s ∩ Ioo b a).Nonempty)

Tactic:
simp [← preimage_inter, ofDual.surjective]

Premises used: Set.preimage_inter, OrderDual.ofDual, Equiv.surjective
-- Module: Mathlib.Topology.Order.AtTopBotIxx
Goal:
X : Type u_1
inst : LinearOrder X
inst_1 : TopologicalSpace X
inst_2 : OrderTopology X
s : Set X
b : X
hsb : s ⊆ Iio b
hs : s.Nonempty → ∃ a < b, Ioo a b ⊆ s
hb : IsSuccPrelimit b
rw : s ⊆ Iio b ∧ (s.Nonempty → ∀ a < b, (s ∩ Ioo a b).Nonempty)
⊢ Eq (α := Filter { x : X // x ∈ s }) (comap (Subtype.val (p := fun (x : X) ↦ x ∈ s)) (𝓝[<] b)) atTop

Tactic:
rw [comap_coe_nhdsLT_eq_atTop_iff]

Premises used: comap_coe_nhdsLT_eq_atTop_iff
-- Module: Mathlib.Topology.Order.AtTopBotIxx
Goal:
X : Type u_1
inst : LinearOrder X
inst_1 : TopologicalSpace X
inst_2 : OrderTopology X
s : Set X
b : X
hsb : s ⊆ Iio b
hs : s.Nonempty → ∃ a < b, Ioo a b ⊆ s
hb : IsSuccPrelimit b
⊢ s ⊆ Iio b ∧ (s.Nonempty → ∀ a < b, (s ∩ Ioo a b).Nonempty)

Tactic:
⟨hsb, fun hsne a ha ↦ ?_⟩

Premises used: And.intro
-- Module: Mathlib.Topology.Order.AtTopBotIxx
Goal:
X : Type u_1
inst : LinearOrder X
inst_1 : TopologicalSpace X
inst_2 : OrderTopology X
s : Set X
b : X
hsb : s ⊆ Iio b
hs : s.Nonempty → ∃ a < b, Ioo a b ⊆ s
hb : IsSuccPrelimit b
refine : ∀ (hsne : s.Nonempty) (a : X) (ha : a < b), (s ∩ Ioo a b).Nonempty
⊢ s ⊆ Iio b ∧ (s.Nonempty → ∀ a < b, (s ∩ Ioo a b).Nonempty)

Tactic:
refine ⟨hsb, fun hsne a ha ↦ ?_⟩
-- Module: Mathlib.Topology.Order.AtTopBotIxx
Goal:
X : Type u_1
inst : LinearOrder X
inst_1 : TopologicalSpace X
inst_2 : OrderTopology X
s : Set X
b : X
hsb : s ⊆ Iio b
hs : s.Nonempty → ∃ a < b, Ioo a b ⊆ s
hb : IsSuccPrelimit b
hsne : s.Nonempty
a : X
ha : a < b
rcases : ∀ (c : X) (hcb : c < b) (hcs : Ioo c b ⊆ s), (s ∩ Ioo a b).Nonempty
⊢ (s ∩ Ioo a b).Nonempty

Tactic:
rcases hs hsne with ⟨c, hcb, hcs⟩
-- Module: Mathlib.Topology.Order.AtTopBotIxx
Goal:
X : Type u_1
inst : LinearOrder X
inst_1 : TopologicalSpace X
inst_2 : OrderTopology X
s : Set X
b : X
hsb : s ⊆ Iio b
hs : s.Nonempty → ∃ a < b, Ioo a b ⊆ s
hb : IsSuccPrelimit b
hsne : s.Nonempty
a : X
ha : a < b
c : X
hcb : c < b
hcs : Ioo c b ⊆ s
rcases : ∀ (x : X) (hxb : x < b) (hacx : max a c < x), (s ∩ Ioo a b).Nonempty
⊢ (s ∩ Ioo a b).Nonempty

Tactic:
rcases hb.lt_iff_exists_lt.mp (max_lt ha hcb) with ⟨x, hxb, hacx⟩

Premises used: max_lt, Order.IsSuccPrelimit.lt_iff_exists_lt, Iff.mp
-- Module: Mathlib.Topology.Order.AtTopBotIxx
Goal:
X : Type u_1
inst : LinearOrder X
inst_1 : TopologicalSpace X
inst_2 : OrderTopology X
s : Set X
b : X
hsb : s ⊆ Iio b
hs : s.Nonempty → ∃ a < b, Ioo a b ⊆ s
hb : IsSuccPrelimit b
hsne : s.Nonempty
a : X
ha : a < b
c : X
hcb : c < b
hcs : Ioo c b ⊆ s
x : X
hxb : x < b
hacx : max a c < x
⊢ a < x ∧ c < x

Tactic:
rw [max_lt_iff] at hacx

Premises used: max_lt_iff
-- Module: Mathlib.Topology.Order.AtTopBotIxx
Goal:
X : Type u_1
inst : LinearOrder X
inst_1 : TopologicalSpace X
inst_2 : OrderTopology X
s : Set X
b : X
hsb : s ⊆ Iio b
hs : s.Nonempty → ∃ a < b, Ioo a b ⊆ s
hb : IsSuccPrelimit b
hsne : s.Nonempty
a : X
ha : a < b
c : X
hcb : c < b
hcs : Ioo c b ⊆ s
x : X
hxb : x < b
hacx : a < x ∧ c < x
⊢ (s ∩ Ioo a b).Nonempty

Tactic:
⟨x, hcs ⟨hacx.2, hxb⟩, hacx.1, hxb⟩

Premises used: Set.Nonempty, And.right, And.left, And.intro, Exists.intro
-- Module: Mathlib.Topology.Order.AtTopBotIxx
Goal:
X : Type u_1
inst : LinearOrder X
inst_1 : TopologicalSpace X
inst_2 : OrderTopology X
s : Set X
b : X
hsb : s ⊆ Iio b
hs : s.Nonempty → ∃ a < b, Ioo a b ⊆ s
hb : IsSuccPrelimit b
hsne : s.Nonempty
a : X
ha : a < b
c : X
hcb : c < b
hcs : Ioo c b ⊆ s
x : X
hxb : x < b
hacx : a < x ∧ c < x
⊢ (s ∩ Ioo a b).Nonempty

Tactic:
exact ⟨x, hcs ⟨hacx.2, hxb⟩, hacx.1, hxb⟩
-- Module: Mathlib.Topology.Order.AtTopBotIxx
Goal:
X : Type u_1
inst : LinearOrder X
inst_1 : TopologicalSpace X
inst_2 : OrderTopology X
s : Set X
a : X
hsa : s ⊆ Ioi a
hs : s.Nonempty → ∃ b > a, Ioo a b ⊆ s
ha : IsPredPrelimit a
⊢ Eq (α := Filter { x : X // x ∈ s }) (comap (Subtype.val (p := fun (x : X) ↦ x ∈ s)) (𝓝[>] a)) atBot

Tactic:
comap_coe_nhdsLT_of_Ioo_subset (show ofDual ⁻¹' s ⊆ Iio (toDual a) from hsa) ?_ ha.dual

Premises used: Set.Ioi, comap_coe_nhdsLT_of_Ioo_subset, Set.Mem, setOf, Order.IsPredPrelimit.dual, Set.preimage, Filter.atBot, Set.Iic, OrderDual
-- Module: Mathlib.Topology.Order.AtTopBotIxx
Goal:
X : Type u_1
inst : LinearOrder X
inst_1 : TopologicalSpace X
inst_2 : OrderTopology X
s : Set X
a : X
hsa : s ⊆ Ioi a
hs : s.Nonempty → ∃ b > a, Ioo a b ⊆ s
ha : IsPredPrelimit a
refine :
  Set.Nonempty (α := Xᵒᵈ) ((⇑ofDual : (a : Xᵒᵈ) → X) ⁻¹' s) →
    ∃ a_2 < (toDual : (a : X) → Xᵒᵈ) a, Ioo a_2 ((toDual : (a : X) → Xᵒᵈ) a) ⊆ (⇑ofDual : (a : Xᵒᵈ) → X) ⁻¹' s
⊢ Eq (α := Filter { x : X // x ∈ s }) (comap (Subtype.val (p := fun (x : X) ↦ x ∈ s)) (𝓝[>] a)) atBot

Tactic:
refine comap_coe_nhdsLT_of_Ioo_subset (show ofDual ⁻¹' s ⊆ Iio (toDual a) from hsa) ?_ ha.dual

Premises used: comap_coe_nhdsLT_of_Ioo_subset, Order.IsPredPrelimit.dual
-- Module: Mathlib.Topology.Order.AtTopBotIxx
Goal:
X : Type u_1
inst : LinearOrder X
inst_1 : TopologicalSpace X
inst_2 : OrderTopology X
s : Set X
a : X
hsa : s ⊆ Ioi a
hs : s.Nonempty → ∃ b > a, Ioo a b ⊆ s
ha : IsPredPrelimit a
⊢ Set.Nonempty (α := Xᵒᵈ) ((⇑ofDual : (a : Xᵒᵈ) → X) ⁻¹' s) →
    ∃ a_2 < (toDual : (a : X) → Xᵒᵈ) a, Ioo a_2 ((toDual : (a : X) → Xᵒᵈ) a) ⊆ (⇑ofDual : (a : Xᵒᵈ) → X) ⁻¹' s

Tactic:
simpa only [OrderDual.exists, Ioo_toDual]

Premises used: Set.Ioo_toDual, OrderDual.exists
-- Module: Mathlib.Topology.Order.AtTopBotIxx
Goal:
X : Type u_1
inst : LinearOrder X
inst_1 : TopologicalSpace X
inst_2 : OrderTopology X
s : Set X
b : X
hsb : s ⊆ Iio b
hs : ∀ a' < b, ∃ a < b, Ioo a b ⊆ s
hb : IsSuccPrelimit b
inl : ∀ (hb' : Iio b = ∅), map (α := { x : X // x ∈ s }) (Subtype.val (p := fun (x : X) ↦ x ∈ s)) atTop = 𝓝[<] b
inr : ∀ (a : X) (ha : a ∈ Iio b), map (α := { x : X // x ∈ s }) (Subtype.val (p := fun (x : X) ↦ x ∈ s)) atTop = 𝓝[<] b
⊢ map (α := { x : X // x ∈ s }) (Subtype.val (p := fun (x : X) ↦ x ∈ s)) atTop = 𝓝[<] b

Tactic:
rcases eq_empty_or_nonempty (Iio b) with (hb' | ⟨a, ha⟩)

Premises used: Set.eq_empty_or_nonempty, Set.Iio
-- Module: Mathlib.Topology.Order.AtTopBotIxx
Goal:
X : Type u_1
inst : LinearOrder X
inst_1 : TopologicalSpace X
inst_2 : OrderTopology X
s : Set X
b : X
hsb : s ⊆ Iio b
hs : ∀ a' < b, ∃ a < b, Ioo a b ⊆ s
hb : IsSuccPrelimit b
hb' : Iio b = ∅
⊢ IsEmpty.{u_1 + 1} (↑s : Type u_1)

Tactic:
have : IsEmpty s := ⟨fun x => hb'.subset (hsb x.2)⟩
-- Module: Mathlib.Topology.Order.AtTopBotIxx
Goal:
X : Type u_1
inst : LinearOrder X
inst_1 : TopologicalSpace X
inst_2 : OrderTopology X
s : Set X
b : X
hsb : s ⊆ Iio b
hs : ∀ a' < b, ∃ a < b, Ioo a b ⊆ s
hb : IsSuccPrelimit b
hb' : Iio b = ∅
this : IsEmpty.{u_1 + 1} (↑s : Type u_1)
inl : map (α := { x : X // x ∈ s }) (Subtype.val (p := fun (x : X) ↦ x ∈ s)) ⊥ = 𝓝[<] b
inl₁ : ⊥ = 𝓝[<] b
inl₂ : ⊥ = 𝓝[∅] b
inl₃ inl₄ : Eq.{u_1 + 1} (α := Filter X) ⊥ ⊥
⊢ map (α := { x : X // x ∈ s }) (Subtype.val (p := fun (x : X) ↦ x ∈ s)) atTop = 𝓝[<] b

Tactic:
rw [filter_eq_bot_of_isEmpty atTop, Filter.map_bot, hb', nhdsWithin_empty]

Premises used: Filter.map_bot, Filter.atTop, nhdsWithin_empty, Filter.filter_eq_bot_of_isEmpty
-- Module: Mathlib.Topology.Order.AtTopBotIxx
Goal:
X : Type u_1
inst : LinearOrder X
inst_1 : TopologicalSpace X
inst_2 : OrderTopology X
s : Set X
b : X
hsb : s ⊆ Iio b
hs : ∀ a' < b, ∃ a < b, Ioo a b ⊆ s
hb : IsSuccPrelimit b
a : X
ha : a ∈ Iio b
inr : range (ι := { x : X // x ∈ s }) (Subtype.val (p := fun (x : X) ↦ x ∈ s)) ∈ 𝓝[<] b
⊢ map (α := { x : X // x ∈ s }) (Subtype.val (p := fun (x : X) ↦ x ∈ s)) atTop = 𝓝[<] b

Tactic:
rw [← comap_coe_nhdsLT_of_Ioo_subset hsb (fun _ => hs a ha) hb, map_comap_of_mem]

Premises used: comap_coe_nhdsLT_of_Ioo_subset, Filter.map_comap_of_mem
-- Module: Mathlib.Topology.Order.AtTopBotIxx
Goal:
X : Type u_1
inst : LinearOrder X
inst_1 : TopologicalSpace X
inst_2 : OrderTopology X
s : Set X
b : X
hsb : s ⊆ Iio b
hs : ∀ a' < b, ∃ a < b, Ioo a b ⊆ s
hb : IsSuccPrelimit b
a : X
ha : a ∈ Iio b
inr : s ∈ 𝓝[<] b
⊢ range (ι := { x : X // x ∈ s }) (Subtype.val (p := fun (x : X) ↦ x ∈ s)) ∈ 𝓝[<] b

Tactic:
rw [Subtype.range_val]

Premises used: Subtype.range_val
-- Module: Mathlib.Topology.Order.AtTopBotIxx
Goal:
X : Type u_1
inst : LinearOrder X
inst_1 : TopologicalSpace X
inst_2 : OrderTopology X
s : Set X
b : X
hsb : s ⊆ Iio b
hs : ∀ a' < b, ∃ a < b, Ioo a b ⊆ s
hb : IsSuccPrelimit b
a : X
ha : a ∈ Iio b
⊢ s ∈ 𝓝[<] b

Tactic:
(mem_nhdsLT_iff_exists_Ioo_subset' ha).2 (hs a ha)

Premises used: Iff.mpr, mem_nhdsLT_iff_exists_Ioo_subset'
-- Module: Mathlib.Topology.Order.AtTopBotIxx
Goal:
X : Type u_1
inst : LinearOrder X
inst_1 : TopologicalSpace X
inst_2 : OrderTopology X
s : Set X
b : X
hsb : s ⊆ Iio b
hs : ∀ a' < b, ∃ a < b, Ioo a b ⊆ s
hb : IsSuccPrelimit b
a : X
ha : a ∈ Iio b
⊢ s ∈ 𝓝[<] b

Tactic:
exact (mem_nhdsLT_iff_exists_Ioo_subset' ha).2 (hs a ha)

Premises used: Iff.mpr, mem_nhdsLT_iff_exists_Ioo_subset'
-- Module: Mathlib.Topology.Order.AtTopBotIxx
Goal:
X : Type u_1
inst : LinearOrder X
inst_1 : TopologicalSpace X
inst_2 : OrderTopology X
s : Set X
a : X
hsa : s ⊆ Ioi a
hs : ∀ b' > a, ∃ b > a, Ioo a b ⊆ s
ha : IsPredPrelimit a
⊢ map (α := { x : X // x ∈ s }) (Subtype.val (p := fun (x : X) ↦ x ∈ s)) atBot = 𝓝[>] a

Tactic:
map_coe_atTop_of_Ioo_subset (s := ofDual ⁻¹' s) (b := toDual a) hsa ?_ ha.dual

Premises used: Set.Ioi, Set.Mem, setOf, Order.IsPredPrelimit.dual, Set.preimage, Filter.atBot, Set.Iic, OrderDual, map_coe_atTop_of_Ioo_subset
-- Module: Mathlib.Topology.Order.AtTopBotIxx
Goal:
X : Type u_1
inst : LinearOrder X
inst_1 : TopologicalSpace X
inst_2 : OrderTopology X
s : Set X
a : X
hsa : s ⊆ Ioi a
hs : ∀ b' > a, ∃ b > a, Ioo a b ⊆ s
ha : IsPredPrelimit a
refine :
  ∀ a' < (toDual : (a : X) → Xᵒᵈ) a,
    ∃ a_2 < (toDual : (a : X) → Xᵒᵈ) a, Ioo a_2 ((toDual : (a : X) → Xᵒᵈ) a) ⊆ (⇑ofDual : (a : Xᵒᵈ) → X) ⁻¹' s
⊢ map (α := { x : X // x ∈ s }) (Subtype.val (p := fun (x : X) ↦ x ∈ s)) atBot = 𝓝[>] a

Tactic:
refine map_coe_atTop_of_Ioo_subset (s := ofDual ⁻¹' s) (b := toDual a) hsa ?_ ha.dual

Premises used: Order.IsPredPrelimit.dual, map_coe_atTop_of_Ioo_subset
-- Module: Mathlib.Topology.Order.AtTopBotIxx
Goal:
X : Type u_1
inst : LinearOrder X
inst_1 : TopologicalSpace X
inst_2 : OrderTopology X
s : Set X
a : X
hsa : s ⊆ Ioi a
hs : ∀ b' > a, ∃ b > a, Ioo a b ⊆ s
ha : IsPredPrelimit a
b' : Xᵒᵈ
hb' : b' < (toDual : (a : X) → Xᵒᵈ) a
⊢ ∃ a_1 < (toDual : (a : X) → Xᵒᵈ) a, Ioo a_1 ((toDual : (a : X) → Xᵒᵈ) a) ⊆ (⇑ofDual : (a : Xᵒᵈ) → X) ⁻¹' s

Tactic:
simpa [OrderDual.exists] using hs (ofDual b') hb'

Premises used: OrderDual.ofDual, OrderDual.exists, DFunLike.coe
-- Module: Mathlib.Topology.Order.AtTopBotIxx
Goal:
X : Type u_1
inst : LinearOrder X
inst_1 : TopologicalSpace X
inst_2 : OrderTopology X
a b : X
hb : IsSuccPrelimit b
⊢ Eq (α := Filter { x : X // x ∈ Ioo a b }) (comap (Subtype.val (p := fun (x : X) ↦ x ∈ Ioo a b)) (𝓝[<] b)) atTop

Tactic:
comap_coe_nhdsLT_of_Ioo_subset Ioo_subset_Iio_self
    (fun h => ⟨a, h.elim fun _x hx ↦ hx.1.trans hx.2, Subset.rfl⟩) hb

Premises used: comap_coe_nhdsLT_of_Ioo_subset, Set.Ioo_subset_Iio_self, Set.Subset.rfl, And.right, And.left, And.intro, Exists.intro, LT.lt.trans, Exists.elim
-- Module: Mathlib.Topology.Order.AtTopBotIxx
Goal:
X : Type u_1
inst : LinearOrder X
inst_1 : TopologicalSpace X
inst_2 : OrderTopology X
a b : X
ha : IsPredPrelimit a
⊢ Eq (α := Filter { x : X // x ∈ Ioo a b }) (comap (Subtype.val (p := fun (x : X) ↦ x ∈ Ioo a b)) (𝓝[>] a)) atBot

Tactic:
comap_coe_nhdsGT_of_Ioo_subset Ioo_subset_Ioi_self
    (fun h => ⟨b, h.elim fun _x hx ↦ hx.1.trans hx.2, Subset.rfl⟩) ha

Premises used: Set.Subset.rfl, And.right, And.left, And.intro, Exists.intro, LT.lt.trans, comap_coe_nhdsGT_of_Ioo_subset, Set.Ioo_subset_Ioi_self, Exists.elim
-- Module: Mathlib.Topology.Order.AtTopBotIxx
Goal:
X : Type u_1
inst : LinearOrder X
inst_1 : TopologicalSpace X
inst_2 : OrderTopology X
a : X
ha : IsPredPrelimit a
⊢ Eq (α := Filter { x : X // x ∈ Ioi a }) (comap (Subtype.val (p := fun (x : X) ↦ x ∈ Ioi a)) (𝓝[>] a)) atBot

Tactic:
comap_coe_nhdsGT_of_Ioo_subset Subset.rfl (fun ⟨x, hx⟩ => ⟨x, hx, Ioo_subset_Ioi_self⟩) ha

Premises used: Set.Ioi, Exists, _private.0.comap_coe_Ioi_nhdsGT.match_1, HasSubset.Subset, GT.gt, And, Set.Subset.rfl, And.intro, Exists.intro, comap_coe_nhdsGT_of_Ioo_subset, Set.Ioo_subset_Ioi_self, Set.Ioo
-- Module: Mathlib.Topology.Order.AtTopBotIxx
Goal:
X : Type u_1
inst : LinearOrder X
inst_1 : TopologicalSpace X
inst_2 : OrderTopology X
a : X
ha : IsSuccPrelimit a
⊢ Eq (α := Filter { x : X // x ∈ Iio a }) (comap (Subtype.val (p := fun (x : X) ↦ x ∈ Iio a)) (𝓝[<] a)) atTop

Tactic:
comap_coe_Ioi_nhdsGT (toDual a) ha.dual

Premises used: Order.IsSuccPrelimit.dual, OrderDual.toDual, comap_coe_Ioi_nhdsGT, Set.Ici, Set.Mem, setOf, Filter.atTop, OrderDual, Set.Iio, DFunLike.coe
-- Module: Mathlib.Topology.Order.AtTopBotIxx
Goal:
X : Type u_1
inst : LinearOrder X
inst_1 : TopologicalSpace X
inst_2 : OrderTopology X
a b : X
h : a < b
hb : IsSuccPrelimit b
⊢ map (α := { x : X // x ∈ Ioo a b }) (Subtype.val (p := fun (x : X) ↦ x ∈ Ioo a b)) atTop = 𝓝[<] b

Tactic:
map_coe_atTop_of_Ioo_subset Ioo_subset_Iio_self (fun _ _ => ⟨_, h, Subset.rfl⟩) hb

Premises used: Set.Ioo_subset_Iio_self, Set.Subset.rfl, And.intro, Exists.intro, map_coe_atTop_of_Ioo_subset
-- Module: Mathlib.Topology.Order.AtTopBotIxx
Goal:
X : Type u_1
inst : LinearOrder X
inst_1 : TopologicalSpace X
inst_2 : OrderTopology X
a b : X
h : a < b
ha : IsPredPrelimit a
⊢ map (α := { x : X // x ∈ Ioo a b }) (Subtype.val (p := fun (x : X) ↦ x ∈ Ioo a b)) atBot = 𝓝[>] a

Tactic:
map_coe_atBot_of_Ioo_subset Ioo_subset_Ioi_self (fun _ _ => ⟨_, h, Subset.rfl⟩) ha

Premises used: map_coe_atBot_of_Ioo_subset, Set.Subset.rfl, And.intro, Exists.intro, Set.Ioo_subset_Ioi_self
-- Module: Mathlib.Topology.Order.AtTopBotIxx
Goal:
X : Type u_1
inst : LinearOrder X
inst_1 : TopologicalSpace X
inst_2 : OrderTopology X
a : X
ha : IsPredPrelimit a
⊢ map (α := { x : X // x ∈ Ioi a }) (Subtype.val (p := fun (x : X) ↦ x ∈ Ioi a)) atBot = 𝓝[>] a

Tactic:
map_coe_atBot_of_Ioo_subset Subset.rfl (fun b hb => ⟨b, hb, Ioo_subset_Ioi_self⟩) ha

Premises used: map_coe_atBot_of_Ioo_subset, Set.Subset.rfl, And.intro, Exists.intro, Set.Ioo_subset_Ioi_self