awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.Order.AtTopBotIxx (goal)
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)
⊢ 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
have 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)
Tactic: contrapose this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Topology.Order.AtTopBotIxx (goal)
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
⊢ 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
have neg : ¬Tendsto (α := (↑s : Type u_1)) (Subtype.val (p := fun (x : X) ↦ x ∈ s)) atTop (𝓝[<] b)
Tactic: suffices ¬Tendsto (↑) (atTop : Filter s) (𝓝[<] b) by
      contrapose this
      simp_all [tendsto_iff_comap]
-- Lean 4 proof step from Mathlib.Topology.Order.AtTopBotIxx (goal)
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)
⊢ False
have neg : ∀ (a : X) (has : a ∈ s) (ha : a ∉ Iio b), False
Tactic: rcases not_subset_iff_exists_mem_notMem.mp hsub with ⟨a, has, ha⟩
-- Lean 4 proof step from Mathlib.Topology.Order.AtTopBotIxx (goal)
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
⊢ False
have 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
Tactic: rcases h.eventually eventually_mem_nhdsWithin |>.and (eventually_ge_atTop ⟨a, has⟩) |>.exists
      with ⟨⟨c, hcs⟩, hcb, hac⟩
-- Lean 4 proof step from Mathlib.Topology.Order.AtTopBotIxx (goal)
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
⊢ False
have neg : a < a
Tactic: apply lt_irrefl a
-- Lean 4 proof step from Mathlib.Topology.Order.AtTopBotIxx (goal)
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
have a₁ : a ≤ c
Tactic: calc
      a ≤ c := by simpa using hac
      _ < b := by simpa using hcb
      _ ≤ a := by simpa using ha
-- Lean 4 proof step from Mathlib.Topology.Order.AtTopBotIxx (goal)
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 < a
have a₂ : c < b
Tactic: calc
      a ≤ c := by simpa using hac
      _ < b := by simpa using hcb
      _ ≤ a := by simpa using ha
-- Lean 4 proof step from Mathlib.Topology.Order.AtTopBotIxx (goal)
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 < a
have a₃ : b ≤ a
Tactic: calc
      a ≤ c := by simpa using hac
      _ < b := by simpa using hcb
      _ ≤ a := by simpa using ha
-- Lean 4 proof step from Mathlib.Topology.Order.AtTopBotIxx (goal)
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)
have 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)
Tactic: refine comap_coe_nhdsLT_eq_atTop_iff (s := OrderDual.ofDual ⁻¹' s) (b := OrderDual.toDual b)
    |>.trans ?_
-- Lean 4 proof step from Mathlib.Topology.Order.AtTopBotIxx (goal)
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
⊢ Eq (α := Filter { x : X // x ∈ s }) (comap (Subtype.val (p := fun (x : X) ↦ x ∈ s)) (𝓝[<] b)) atTop
have rw : s ⊆ Iio b ∧ (s.Nonempty → ∀ a < b, (s ∩ Ioo a b).Nonempty)
Tactic: rw [comap_coe_nhdsLT_eq_atTop_iff]
-- Lean 4 proof step from Mathlib.Topology.Order.AtTopBotIxx (goal)
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)
have refine : ∀ (hsne : s.Nonempty) (a : X) (ha : a < b), (s ∩ Ioo a b).Nonempty
Tactic: refine ⟨hsb, fun hsne a ha ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Order.AtTopBotIxx (goal)
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
⊢ (s ∩ Ioo a b).Nonempty
have rcases : ∀ (c : X) (hcb : c < b) (hcs : Ioo c b ⊆ s), (s ∩ Ioo a b).Nonempty
Tactic: rcases hs hsne with ⟨c, hcb, hcs⟩
-- Lean 4 proof step from Mathlib.Topology.Order.AtTopBotIxx (goal)
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
⊢ (s ∩ Ioo a b).Nonempty
have rcases : ∀ (x : X) (hxb : x < b) (hacx : max a c < x), (s ∩ Ioo a b).Nonempty
Tactic: rcases hb.lt_iff_exists_lt.mp (max_lt ha hcb) with ⟨x, hxb, hacx⟩
-- Lean 4 proof step from Mathlib.Topology.Order.AtTopBotIxx (hypothesis)
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
⊢ (s ∩ Ioo a b).Nonempty
have hacx₁ : a < x ∧ c < x
Tactic: rw [max_lt_iff] at hacx
Cleared hypotheses: hacx
-- Lean 4 proof step from Mathlib.Topology.Order.AtTopBotIxx (goal)
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
have 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
Tactic: refine comap_coe_nhdsLT_of_Ioo_subset (show ofDual ⁻¹' s ⊆ Iio (toDual a) from hsa) ?_ ha.dual
-- Lean 4 proof step from Mathlib.Topology.Order.AtTopBotIxx (goal)
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
⊢ map (α := { x : X // x ∈ s }) (Subtype.val (p := fun (x : X) ↦ x ∈ s)) atTop = 𝓝[<] b
have inl : ∀ (hb' : Iio 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⟩)
-- Lean 4 proof step from Mathlib.Topology.Order.AtTopBotIxx (goal)
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
⊢ map (α := { x : X // x ∈ s }) (Subtype.val (p := fun (x : X) ↦ x ∈ s)) atTop = 𝓝[<] b
have inr : ∀ (a : X) (ha : a ∈ Iio 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⟩)
-- Lean 4 proof step from Mathlib.Topology.Order.AtTopBotIxx (hypothesis)
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 = ∅
⊢ map (α := { x : X // x ∈ s }) (Subtype.val (p := fun (x : X) ↦ x ∈ s)) atTop = 𝓝[<] b
have this : IsEmpty.{u_1 + 1} (↑s : Type u_1)
Tactic: have : IsEmpty s := ⟨fun x => hb'.subset (hsb x.2)⟩
-- Lean 4 proof step from Mathlib.Topology.Order.AtTopBotIxx (goal)
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)
⊢ map (α := { x : X // x ∈ s }) (Subtype.val (p := fun (x : X) ↦ x ∈ s)) atTop = 𝓝[<] b
have inl : map (α := { x : X // x ∈ s }) (Subtype.val (p := fun (x : X) ↦ x ∈ s)) ⊥ = 𝓝[<] b
Tactic: rw [filter_eq_bot_of_isEmpty atTop, Filter.map_bot, hb', nhdsWithin_empty]
-- Lean 4 proof step from Mathlib.Topology.Order.AtTopBotIxx (goal)
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
⊢ map (α := { x : X // x ∈ s }) (Subtype.val (p := fun (x : X) ↦ x ∈ s)) atTop = 𝓝[<] b
have inl₁ : ⊥ = 𝓝[<] b
Tactic: rw [filter_eq_bot_of_isEmpty atTop, Filter.map_bot, hb', nhdsWithin_empty]
-- Lean 4 proof step from Mathlib.Topology.Order.AtTopBotIxx (goal)
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
⊢ map (α := { x : X // x ∈ s }) (Subtype.val (p := fun (x : X) ↦ x ∈ s)) atTop = 𝓝[<] b
have inl₂ : ⊥ = 𝓝[∅] b
Tactic: rw [filter_eq_bot_of_isEmpty atTop, Filter.map_bot, hb', nhdsWithin_empty]
-- Lean 4 proof step from Mathlib.Topology.Order.AtTopBotIxx (goal)
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
⊢ map (α := { x : X // x ∈ s }) (Subtype.val (p := fun (x : X) ↦ x ∈ s)) atTop = 𝓝[<] b
have inl₃ : Eq.{u_1 + 1} (α := Filter X) ⊥ ⊥
Tactic: rw [filter_eq_bot_of_isEmpty atTop, Filter.map_bot, hb', nhdsWithin_empty]
-- Lean 4 proof step from Mathlib.Topology.Order.AtTopBotIxx (goal)
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
⊢ map (α := { x : X // x ∈ s }) (Subtype.val (p := fun (x : X) ↦ x ∈ s)) atTop = 𝓝[<] b
have inr : range (ι := { x : X // x ∈ s }) (Subtype.val (p := fun (x : X) ↦ x ∈ s)) ∈ 𝓝[<] b
Tactic: rw [← comap_coe_nhdsLT_of_Ioo_subset hsb (fun _ => hs a ha) hb, map_comap_of_mem]
-- Lean 4 proof step from Mathlib.Topology.Order.AtTopBotIxx (goal)
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
⊢ range (ι := { x : X // x ∈ s }) (Subtype.val (p := fun (x : X) ↦ x ∈ s)) ∈ 𝓝[<] b
have inr : s ∈ 𝓝[<] b
Tactic: rw [Subtype.range_val]
-- Lean 4 proof step from Mathlib.Topology.Order.AtTopBotIxx (goal)
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
have 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
Tactic: refine map_coe_atTop_of_Ioo_subset (s := ofDual ⁻¹' s) (b := toDual a) hsa ?_ ha.dual
-- Lean 4 proof step from Mathlib.Topology.Order.AtTopBotIxx (goal)
Goal:
X : Type u_1
inst : LinearOrder X
inst_1 : TopologicalSpace X
inst_2 : OrderTopology X
a b : X
α : Type u_2
l : Filter α
f : X → α
h : a < b
hb : IsSuccPrelimit b
⊢ Tendsto (fun (x : (↑(Ioo a b) : Type u_1)) ↦ f (↑x : X)) atTop l ↔ Tendsto f (𝓝[<] b) l
have rw : Tendsto (fun (x : (↑(Ioo a b) : Type u_1)) ↦ f (↑x : X)) atTop l ↔
  Tendsto f (map (α := { x : X // x ∈ Ioo a b }) (Subtype.val (p := fun (x : X) ↦ x ∈ Ioo a b)) atTop) l
Tactic: rw [← map_coe_Ioo_atTop h hb, tendsto_map'_iff, Function.comp_def]
-- Lean 4 proof step from Mathlib.Topology.Order.AtTopBotIxx (goal)
Goal:
X : Type u_1
inst : LinearOrder X
inst_1 : TopologicalSpace X
inst_2 : OrderTopology X
a b : X
α : Type u_2
l : Filter α
f : X → α
h : a < b
hb : IsSuccPrelimit b
rw :
  Tendsto (fun (x : (↑(Ioo a b) : Type u_1)) ↦ f (↑x : X)) atTop l ↔
    Tendsto f (map (α := { x : X // x ∈ Ioo a b }) (Subtype.val (p := fun (x : X) ↦ x ∈ Ioo a b)) atTop) l
⊢ Tendsto (fun (x : (↑(Ioo a b) : Type u_1)) ↦ f (↑x : X)) atTop l ↔ Tendsto f (𝓝[<] b) l
have rw₁ : Tendsto (fun (x : (↑(Ioo a b) : Type u_1)) ↦ f (↑x : X)) atTop l ↔
  Tendsto (α := { x : X // x ∈ Ioo a b }) (f ∘ Subtype.val (p := fun (x : X) ↦ x ∈ Ioo a b)) atTop l
Tactic: rw [← map_coe_Ioo_atTop h hb, tendsto_map'_iff, Function.comp_def]
-- Lean 4 proof step from Mathlib.Topology.Order.AtTopBotIxx (goal)
Goal:
X : Type u_1
inst : LinearOrder X
inst_1 : TopologicalSpace X
inst_2 : OrderTopology X
a b : X
α : Type u_2
l : Filter α
f : X → α
h : a < b
hb : IsSuccPrelimit b
rw :
  Tendsto (fun (x : (↑(Ioo a b) : Type u_1)) ↦ f (↑x : X)) atTop l ↔
    Tendsto f (map (α := { x : X // x ∈ Ioo a b }) (Subtype.val (p := fun (x : X) ↦ x ∈ Ioo a b)) atTop) l
rw₁ :
  Tendsto (fun (x : (↑(Ioo a b) : Type u_1)) ↦ f (↑x : X)) atTop l ↔
    Tendsto (α := { x : X // x ∈ Ioo a b }) (f ∘ Subtype.val (p := fun (x : X) ↦ x ∈ Ioo a b)) atTop l
⊢ Tendsto (fun (x : (↑(Ioo a b) : Type u_1)) ↦ f (↑x : X)) atTop l ↔ Tendsto f (𝓝[<] b) l
have rw₂ : Tendsto (fun (x : (↑(Ioo a b) : Type u_1)) ↦ f (↑x : X)) atTop l ↔
  Tendsto (fun (x : { x : X // x ∈ Ioo a b }) ↦ f (↑x : X)) atTop l
Tactic: rw [← map_coe_Ioo_atTop h hb, tendsto_map'_iff, Function.comp_def]
-- Lean 4 proof step from Mathlib.Topology.Order.AtTopBotIxx (goal)
Goal:
X : Type u_1
inst : LinearOrder X
inst_1 : TopologicalSpace X
inst_2 : OrderTopology X
a b : X
α : Type u_2
l : Filter α
f : X → α
h : a < b
ha : IsPredPrelimit a
⊢ Tendsto (fun (x : (↑(Ioo a b) : Type u_1)) ↦ f (↑x : X)) atBot l ↔ Tendsto f (𝓝[>] a) l
have rw : Tendsto (fun (x : (↑(Ioo a b) : Type u_1)) ↦ f (↑x : X)) atBot l ↔
  Tendsto f (map (α := { x : X // x ∈ Ioo a b }) (Subtype.val (p := fun (x : X) ↦ x ∈ Ioo a b)) atBot) l
Tactic: rw [← map_coe_Ioo_atBot h ha, tendsto_map'_iff, Function.comp_def]
-- Lean 4 proof step from Mathlib.Topology.Order.AtTopBotIxx (goal)
Goal:
X : Type u_1
inst : LinearOrder X
inst_1 : TopologicalSpace X
inst_2 : OrderTopology X
a b : X
α : Type u_2
l : Filter α
f : X → α
h : a < b
ha : IsPredPrelimit a
rw :
  Tendsto (fun (x : (↑(Ioo a b) : Type u_1)) ↦ f (↑x : X)) atBot l ↔
    Tendsto f (map (α := { x : X // x ∈ Ioo a b }) (Subtype.val (p := fun (x : X) ↦ x ∈ Ioo a b)) atBot) l
⊢ Tendsto (fun (x : (↑(Ioo a b) : Type u_1)) ↦ f (↑x : X)) atBot l ↔ Tendsto f (𝓝[>] a) l
have rw₁ : Tendsto (fun (x : (↑(Ioo a b) : Type u_1)) ↦ f (↑x : X)) atBot l ↔
  Tendsto (α := { x : X // x ∈ Ioo a b }) (f ∘ Subtype.val (p := fun (x : X) ↦ x ∈ Ioo a b)) atBot l
Tactic: rw [← map_coe_Ioo_atBot h ha, tendsto_map'_iff, Function.comp_def]
-- Lean 4 proof step from Mathlib.Topology.Order.AtTopBotIxx (goal)
Goal:
X : Type u_1
inst : LinearOrder X
inst_1 : TopologicalSpace X
inst_2 : OrderTopology X
a b : X
α : Type u_2
l : Filter α
f : X → α
h : a < b
ha : IsPredPrelimit a
rw :
  Tendsto (fun (x : (↑(Ioo a b) : Type u_1)) ↦ f (↑x : X)) atBot l ↔
    Tendsto f (map (α := { x : X // x ∈ Ioo a b }) (Subtype.val (p := fun (x : X) ↦ x ∈ Ioo a b)) atBot) l
rw₁ :
  Tendsto (fun (x : (↑(Ioo a b) : Type u_1)) ↦ f (↑x : X)) atBot l ↔
    Tendsto (α := { x : X // x ∈ Ioo a b }) (f ∘ Subtype.val (p := fun (x : X) ↦ x ∈ Ioo a b)) atBot l
⊢ Tendsto (fun (x : (↑(Ioo a b) : Type u_1)) ↦ f (↑x : X)) atBot l ↔ Tendsto f (𝓝[>] a) l
have rw₂ : Tendsto (fun (x : (↑(Ioo a b) : Type u_1)) ↦ f (↑x : X)) atBot l ↔
  Tendsto (fun (x : { x : X // x ∈ Ioo a b }) ↦ f (↑x : X)) atBot l
Tactic: rw [← map_coe_Ioo_atBot h ha, tendsto_map'_iff, Function.comp_def]
-- Lean 4 proof step from Mathlib.Topology.Order.AtTopBotIxx (goal)
Goal:
X : Type u_1
inst : LinearOrder X
inst_1 : TopologicalSpace X
inst_2 : OrderTopology X
a : X
α : Type u_2
l : Filter α
f : X → α
ha : IsPredPrelimit a
⊢ Tendsto (fun (x : (↑(Ioi a) : Type u_1)) ↦ f (↑x : X)) atBot l ↔ Tendsto f (𝓝[>] a) l
have rw : Tendsto (fun (x : (↑(Ioi a) : Type u_1)) ↦ f (↑x : X)) atBot l ↔
  Tendsto f (map (α := { x : X // x ∈ Ioi a }) (Subtype.val (p := fun (x : X) ↦ x ∈ Ioi a)) atBot) l
Tactic: rw [← map_coe_Ioi_atBot a ha, tendsto_map'_iff, Function.comp_def]
-- Lean 4 proof step from Mathlib.Topology.Order.AtTopBotIxx (goal)
Goal:
X : Type u_1
inst : LinearOrder X
inst_1 : TopologicalSpace X
inst_2 : OrderTopology X
a : X
α : Type u_2
l : Filter α
f : X → α
ha : IsPredPrelimit a
rw :
  Tendsto (fun (x : (↑(Ioi a) : Type u_1)) ↦ f (↑x : X)) atBot l ↔
    Tendsto f (map (α := { x : X // x ∈ Ioi a }) (Subtype.val (p := fun (x : X) ↦ x ∈ Ioi a)) atBot) l
⊢ Tendsto (fun (x : (↑(Ioi a) : Type u_1)) ↦ f (↑x : X)) atBot l ↔ Tendsto f (𝓝[>] a) l
have rw₁ : Tendsto (fun (x : (↑(Ioi a) : Type u_1)) ↦ f (↑x : X)) atBot l ↔
  Tendsto (α := { x : X // x ∈ Ioi a }) (f ∘ Subtype.val (p := fun (x : X) ↦ x ∈ Ioi a)) atBot l
Tactic: rw [← map_coe_Ioi_atBot a ha, tendsto_map'_iff, Function.comp_def]
-- Lean 4 proof step from Mathlib.Topology.Order.AtTopBotIxx (goal)
Goal:
X : Type u_1
inst : LinearOrder X
inst_1 : TopologicalSpace X
inst_2 : OrderTopology X
a : X
α : Type u_2
l : Filter α
f : X → α
ha : IsPredPrelimit a
rw :
  Tendsto (fun (x : (↑(Ioi a) : Type u_1)) ↦ f (↑x : X)) atBot l ↔
    Tendsto f (map (α := { x : X // x ∈ Ioi a }) (Subtype.val (p := fun (x : X) ↦ x ∈ Ioi a)) atBot) l
rw₁ :
  Tendsto (fun (x : (↑(Ioi a) : Type u_1)) ↦ f (↑x : X)) atBot l ↔
    Tendsto (α := { x : X // x ∈ Ioi a }) (f ∘ Subtype.val (p := fun (x : X) ↦ x ∈ Ioi a)) atBot l
⊢ Tendsto (fun (x : (↑(Ioi a) : Type u_1)) ↦ f (↑x : X)) atBot l ↔ Tendsto f (𝓝[>] a) l
have rw₂ : Tendsto (fun (x : (↑(Ioi a) : Type u_1)) ↦ f (↑x : X)) atBot l ↔
  Tendsto (fun (x : { x : X // x ∈ Ioi a }) ↦ f (↑x : X)) atBot l
Tactic: rw [← map_coe_Ioi_atBot a ha, tendsto_map'_iff, Function.comp_def]
-- Lean 4 proof step from Mathlib.Topology.Order.AtTopBotIxx (goal)
Goal:
X : Type u_1
inst : LinearOrder X
inst_1 : TopologicalSpace X
inst_2 : OrderTopology X
a : X
α : Type u_2
l : Filter α
f : X → α
ha : IsSuccPrelimit a
⊢ Tendsto (fun (x : (↑(Iio a) : Type u_1)) ↦ f (↑x : X)) atTop l ↔ Tendsto f (𝓝[<] a) l
have rw : Tendsto (fun (x : (↑(Iio a) : Type u_1)) ↦ f (↑x : X)) atTop l ↔
  Tendsto f (map (α := { x : X // x ∈ Iio a }) (Subtype.val (p := fun (x : X) ↦ x ∈ Iio a)) atTop) l
Tactic: rw [← map_coe_Iio_atTop a ha, tendsto_map'_iff, Function.comp_def]
-- Lean 4 proof step from Mathlib.Topology.Order.AtTopBotIxx (goal)
Goal:
X : Type u_1
inst : LinearOrder X
inst_1 : TopologicalSpace X
inst_2 : OrderTopology X
a : X
α : Type u_2
l : Filter α
f : X → α
ha : IsSuccPrelimit a
rw :
  Tendsto (fun (x : (↑(Iio a) : Type u_1)) ↦ f (↑x : X)) atTop l ↔
    Tendsto f (map (α := { x : X // x ∈ Iio a }) (Subtype.val (p := fun (x : X) ↦ x ∈ Iio a)) atTop) l
⊢ Tendsto (fun (x : (↑(Iio a) : Type u_1)) ↦ f (↑x : X)) atTop l ↔ Tendsto f (𝓝[<] a) l
have rw₁ : Tendsto (fun (x : (↑(Iio a) : Type u_1)) ↦ f (↑x : X)) atTop l ↔
  Tendsto (α := { x : X // x ∈ Iio a }) (f ∘ Subtype.val (p := fun (x : X) ↦ x ∈ Iio a)) atTop l
Tactic: rw [← map_coe_Iio_atTop a ha, tendsto_map'_iff, Function.comp_def]
-- Lean 4 proof step from Mathlib.Topology.Order.AtTopBotIxx (goal)
Goal:
X : Type u_1
inst : LinearOrder X
inst_1 : TopologicalSpace X
inst_2 : OrderTopology X
a : X
α : Type u_2
l : Filter α
f : X → α
ha : IsSuccPrelimit a
rw :
  Tendsto (fun (x : (↑(Iio a) : Type u_1)) ↦ f (↑x : X)) atTop l ↔
    Tendsto f (map (α := { x : X // x ∈ Iio a }) (Subtype.val (p := fun (x : X) ↦ x ∈ Iio a)) atTop) l
rw₁ :
  Tendsto (fun (x : (↑(Iio a) : Type u_1)) ↦ f (↑x : X)) atTop l ↔
    Tendsto (α := { x : X // x ∈ Iio a }) (f ∘ Subtype.val (p := fun (x : X) ↦ x ∈ Iio a)) atTop l
⊢ Tendsto (fun (x : (↑(Iio a) : Type u_1)) ↦ f (↑x : X)) atTop l ↔ Tendsto f (𝓝[<] a) l
have rw₂ : Tendsto (fun (x : (↑(Iio a) : Type u_1)) ↦ f (↑x : X)) atTop l ↔
  Tendsto (fun (x : { x : X // x ∈ Iio a }) ↦ f (↑x : X)) atTop l
Tactic: rw [← map_coe_Iio_atTop a ha, tendsto_map'_iff, Function.comp_def]
-- Lean 4 proof step from Mathlib.Topology.Order.AtTopBotIxx (goal)
Goal:
X : Type u_1
inst : LinearOrder X
inst_1 : TopologicalSpace X
inst_2 : OrderTopology X
a b : X
α : Type u_2
l : Filter α
f : α → (↑(Ioo a b) : Type u_1)
hb : IsSuccPrelimit b
⊢ Tendsto f l atTop ↔ Tendsto (fun (x : α) ↦ (↑(f x) : X)) l (𝓝[<] b)
have rw : Tendsto f l (comap (Subtype.val (p := fun (x : X) ↦ x ∈ Ioo a b)) (𝓝[<] b)) ↔
  Tendsto (fun (x : α) ↦ (↑(f x) : X)) l (𝓝[<] b)
Tactic: rw [← comap_coe_Ioo_nhdsLT a b hb, tendsto_comap_iff, Function.comp_def]