awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Order.Basic
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : LinearOrder β
inst_4 : SecondCountableTopology α
t : Set β
f : β → α
h : Nontrivial β
this : Nonempty α
s : Set β := {x : β | x ∈ t ∧ ∃ (z : α), f x < z ∧ ∀ y ∈ t, x < y → z ≤ f y}
z : (x : β) → α
hz : ∀ x ∈ s, f x < z x ∧ ∀ y ∈ t, x < y → z x ≤ f y
I : InjOn f s
fs_count : (f '' s).Countable
⊢ Set.Countable.{v} (α := β) {x : β | x ∈ t ∧ ∃ (z : α), f x < z ∧ ∀ y ∈ t, x < y → z ≤ f y}

Tactic:
MapsTo.countable_of_injOn (mapsTo_image f s) I fs_count

Premises used: Set.MapsTo.countable_of_injOn, Set.mapsTo_image
-- Module: Mathlib.Topology.Order.Basic
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : LinearOrder β
inst_4 : SecondCountableTopology α
t : Set β
f : β → α
h : Nontrivial β
this : Nonempty α
s : Set β := {x : β | x ∈ t ∧ ∃ (z : α), f x < z ∧ ∀ y ∈ t, x < y → z ≤ f y}
z : (x : β) → α
hz : ∀ x ∈ s, f x < z x ∧ ∀ y ∈ t, x < y → z x ≤ f y
I : InjOn f s
fs_count : (f '' s).Countable
⊢ Set.Countable.{v} (α := β) {x : β | x ∈ t ∧ ∃ (z : α), f x < z ∧ ∀ y ∈ t, x < y → z ≤ f y}

Tactic:
exact MapsTo.countable_of_injOn (mapsTo_image f s) I fs_count

Premises used: Set.MapsTo.countable_of_injOn, Set.mapsTo_image
-- Module: Mathlib.Topology.Order.Basic
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : LinearOrder β
f : β → α
inst_4 : SecondCountableTopology α
⊢ Set.Countable.{v} (α := β) {x : β | ∃ (z : α), f x < z ∧ ∀ (y : β), x < y → z ≤ f y}

Tactic:
simpa using countable_image_lt_image_Ioi_within univ f

Premises used: countable_image_lt_image_Ioi_within, Set.univ
-- Module: Mathlib.Topology.Order.Basic
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : LinearOrder β
inst_4 : SecondCountableTopology α
t : Set β
f : β → α
⊢ Set.Countable.{v} (α := β) {x : β | x ∈ t ∧ ∃ z < f x, ∀ y ∈ t, x < y → f y ≤ z}

Tactic:
countable_image_lt_image_Ioi_within (α := αᵒᵈ) t f

Premises used: countable_image_lt_image_Ioi_within, setOf, OrderDual
-- Module: Mathlib.Topology.Order.Basic
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : LinearOrder β
f : β → α
inst_4 : SecondCountableTopology α
⊢ Set.Countable.{v} (α := β) {x : β | ∃ z < f x, ∀ (y : β), x < y → f y ≤ z}

Tactic:
countable_image_lt_image_Ioi (α := αᵒᵈ) f

Premises used: setOf, countable_image_lt_image_Ioi, OrderDual
-- Module: Mathlib.Topology.Order.Basic
Goal:
α : Type u
β : Type v
γ : Type w
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : SeparableSpace α
inl : ∀ (h : Eq.{u + 1} (α := Set α) {x : α | IsTop x} ∅), IsCountablyGenerated.{u} (α := α) atTop
inr : ∀ (x : α) (hx : Membership.mem (γ := Set α) {x : α | IsTop x} x), IsCountablyGenerated.{u} (α := α) atTop
⊢ IsCountablyGenerated.{u} (α := α) atTop

Tactic:
obtain (h | ⟨x, hx⟩) := Set.eq_empty_or_nonempty {x : α | IsTop x}

Premises used: setOf, Set.eq_empty_or_nonempty, IsTop
-- Module: Mathlib.Topology.Order.Basic
Goal:
α : Type u
β : Type v
γ : Type w
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : SeparableSpace α
h : Eq.{u + 1} (α := Set α) {x : α | IsTop x} ∅
inl : ∀ (s : Set α) (s_count : s.Countable) (hs : Dense s), IsCountablyGenerated.{u} (α := α) atTop
⊢ IsCountablyGenerated.{u} (α := α) atTop

Tactic:
obtain ⟨s, s_count, hs⟩ := exists_countable_dense α

Premises used: TopologicalSpace.exists_countable_dense
-- Module: Mathlib.Topology.Order.Basic
Goal:
α : Type u
β : Type v
γ : Type w
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : SeparableSpace α
h : Eq.{u + 1} (α := Set α) {x : α | IsTop x} ∅
s : Set α
s_count : s.Countable
hs : Dense s
⊢ atTop = generate (Ici '' s)

Tactic:
atTop_eq_generate_of_not_bddAbove fun ⟨x, hx⟩ ↦ ?_

Premises used: False, _private.0.instIsCountablyGenerated_atTop.match_1, Filter.atTop_eq_generate_of_not_bddAbove
-- Module: Mathlib.Topology.Order.Basic
Goal:
α : Type u
β : Type v
γ : Type w
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : SeparableSpace α
h : Eq.{u + 1} (α := Set α) {x : α | IsTop x} ∅
s : Set α
s_count : s.Countable
hs : Dense s
refine : BddAbove s → ∀ (x : α) (hx : x ∈ upperBounds s), False
⊢ atTop = generate (Ici '' s)

Tactic:
refine atTop_eq_generate_of_not_bddAbove fun ⟨x, hx⟩ ↦ ?_

Premises used: Filter.atTop_eq_generate_of_not_bddAbove
-- Module: Mathlib.Topology.Order.Basic
Goal:
α : Type u
β : Type v
γ : Type w
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : SeparableSpace α
h : Eq.{u + 1} (α := Set α) {x : α | IsTop x} ∅
s : Set α
s_count : s.Countable
hs : Dense s
h_1 : BddAbove s
x : α
hx : x ∈ upperBounds s
⊢ ∀ (x : α), ∃ (x_1 : α), x < x_1

Tactic:
simp only [eq_empty_iff_forall_notMem, IsTop, mem_setOf_eq, not_forall, not_le] at h

Premises used: not_le, Set.mem_setOf_eq, Set.eq_empty_iff_forall_notMem, IsTop, Classical.not_forall
-- Module: Mathlib.Topology.Order.Basic
Goal:
α : Type u
β : Type v
γ : Type w
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : SeparableSpace α
s : Set α
s_count : s.Countable
hs : Dense s
h_1 : BddAbove s
x : α
hx : x ∈ upperBounds s
h : ∀ (x : α), ∃ (x_1 : α), x < x_1
obtain : ∀ (y : α) (hy : y ∈ s) (hxy : y ∈ Ioi x), False
⊢ False

Tactic:
obtain ⟨y, hy, hxy⟩ := hs.exists_mem_open isOpen_Ioi (h x)

Premises used: isOpen_Ioi, Dense.exists_mem_open
-- Module: Mathlib.Topology.Order.Basic
Goal:
α : Type u
β : Type v
γ : Type w
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : SeparableSpace α
s : Set α
s_count : s.Countable
hs : Dense s
h_1 : BddAbove s
x : α
hx : x ∈ upperBounds s
h : ∀ (x : α), ∃ (x_1 : α), x < x_1
y : α
hy : y ∈ s
hxy : y ∈ Ioi x
⊢ False

Tactic:
(hx hy).not_gt hxy

Premises used: LE.le.not_gt
-- Module: Mathlib.Topology.Order.Basic
Goal:
α : Type u
β : Type v
γ : Type w
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : SeparableSpace α
s : Set α
s_count : s.Countable
hs : Dense s
h_1 : BddAbove s
x : α
hx : x ∈ upperBounds s
h : ∀ (x : α), ∃ (x_1 : α), x < x_1
y : α
hy : y ∈ s
hxy : y ∈ Ioi x
⊢ False

Tactic:
exact (hx hy).not_gt hxy

Premises used: LE.le.not_gt
-- Module: Mathlib.Topology.Order.Basic
Goal:
α : Type u
β : Type v
γ : Type w
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : SeparableSpace α
h : Eq.{u + 1} (α := Set α) {x : α | IsTop x} ∅
s : Set α
s_count : s.Countable
hs : Dense s
⊢ atTop = generate (Ici '' s)

Tactic:
have : atTop = generate (Ici '' s) := by
      refine atTop_eq_generate_of_not_bddAbove fun ⟨x, hx⟩ ↦ ?_
      simp only [eq_empty_iff_forall_notMem, IsTop, mem_setOf_eq, not_forall, not_le] at h
      obtain ⟨y, hy, hxy⟩ := hs.exists_mem_open isOpen_Ioi (h x)
      exact (hx hy).not_gt hxy
-- Module: Mathlib.Topology.Order.Basic
Goal:
α : Type u
β : Type v
γ : Type w
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : SeparableSpace α
h : Eq.{u + 1} (α := Set α) {x : α | IsTop x} ∅
s : Set α
s_count : s.Countable
hs : Dense s
this : atTop = generate (Ici '' s)
inl : (generate (Ici '' s)).IsCountablyGenerated
⊢ IsCountablyGenerated.{u} (α := α) atTop

Tactic:
rw [this]
-- Module: Mathlib.Topology.Order.Basic
Goal:
α : Type u
β : Type v
γ : Type w
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : SeparableSpace α
h : Eq.{u + 1} (α := Set α) {x : α | IsTop x} ∅
s : Set α
s_count : s.Countable
hs : Dense s
this : atTop = generate (Ici '' s)
⊢ (generate (Ici '' s)).IsCountablyGenerated

Tactic:
⟨_, s_count.image _, rfl⟩

Premises used: Filter.IsCountablyGenerated.mk, Set.Countable.image, And.intro, Exists.intro, rfl
-- Module: Mathlib.Topology.Order.Basic
Goal:
α : Type u
β : Type v
γ : Type w
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : SeparableSpace α
h : Eq.{u + 1} (α := Set α) {x : α | IsTop x} ∅
s : Set α
s_count : s.Countable
hs : Dense s
this : atTop = generate (Ici '' s)
⊢ (generate (Ici '' s)).IsCountablyGenerated

Tactic:
exact ⟨_, s_count.image _, rfl⟩
-- Module: Mathlib.Topology.Order.Basic
Goal:
α : Type u
β : Type v
γ : Type w
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : SeparableSpace α
x : α
hx : Membership.mem (γ := Set α) {x : α | IsTop x} x
inr : IsCountablyGenerated (pure x)
⊢ IsCountablyGenerated.{u} (α := α) atTop

Tactic:
rw [atTop_eq_pure_of_isTop hx]

Premises used: Filter.atTop_eq_pure_of_isTop
-- Module: Mathlib.Topology.Order.Basic
Goal:
α : Type u
β : Type v
γ : Type w
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : SeparableSpace α
x : α
hx : Membership.mem (γ := Set α) {x : α | IsTop x} x
⊢ IsCountablyGenerated (pure x)

Tactic:
isCountablyGenerated_pure x

Premises used: Filter.isCountablyGenerated_pure
-- Module: Mathlib.Topology.Order.Basic
Goal:
α : Type u
β : Type v
γ : Type w
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : SeparableSpace α
x : α
hx : Membership.mem (γ := Set α) {x : α | IsTop x} x
⊢ IsCountablyGenerated (pure x)

Tactic:
exact isCountablyGenerated_pure x

Premises used: Filter.isCountablyGenerated_pure
-- Module: Mathlib.Topology.Order.Basic
Goal:
ι : Type u_1
X : ι → Type u_2
inst : Finite ι
inst_1 : (i : ι) → LinearOrder (X i)
inst_2 : (i : ι) → TopologicalSpace (X i)
inst_3 : ∀ (i : ι), OrderTopology.{u_2} (X i)
a x : (i : ι) → X i
ha : ∀ (i : ι), x i < a i
⊢ Iic a ∈ 𝓝 x

Tactic:
pi_univ_Iic a ▸ set_pi_mem_nhds (Set.toFinite _) fun _ _ => Iic_mem_nhds (ha _)

Premises used: set_pi_mem_nhds, Eq.rec, Set.pi_univ_Iic, Set.toFinite, Iic_mem_nhds
-- Module: Mathlib.Topology.Order.Basic
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
ι : Type u_1
inst_3 : Finite ι
a' x' : ι → α
ha : ∀ (i : ι), x' i < a' i
⊢ Iic a' ∈ 𝓝 x'

Tactic:
pi_Iic_mem_nhds ha

Premises used: Set.Mem, pi_Iic_mem_nhds
-- Module: Mathlib.Topology.Order.Basic
Goal:
ι : Type u_1
X : ι → Type u_2
inst : Finite ι
inst_1 : (i : ι) → LinearOrder (X i)
inst_2 : (i : ι) → TopologicalSpace (X i)
inst_3 : ∀ (i : ι), OrderTopology.{u_2} (X i)
a b x : (i : ι) → X i
ha : ∀ (i : ι), a i < x i
hb : ∀ (i : ι), x i < b i
⊢ Icc a b ∈ 𝓝 x

Tactic:
pi_univ_Icc a b ▸ set_pi_mem_nhds finite_univ fun _ _ => Icc_mem_nhds (ha _) (hb _)

Premises used: set_pi_mem_nhds, Eq.rec, Set.finite_univ, Icc_mem_nhds, Set.pi_univ_Icc
-- Module: Mathlib.Topology.Order.Basic
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
ι : Type u_1
inst_3 : Finite ι
a' b' x' : ι → α
ha : ∀ (i : ι), a' i < x' i
hb : ∀ (i : ι), x' i < b' i
⊢ Icc a' b' ∈ 𝓝 x'

Tactic:
pi_Icc_mem_nhds ha hb

Premises used: Set.Mem, pi_Icc_mem_nhds
-- Module: Mathlib.Topology.Order.Basic
Goal:
ι : Type u_1
X : ι → Type u_2
inst : Finite ι
inst_1 : (i : ι) → LinearOrder (X i)
inst_2 : (i : ι) → TopologicalSpace (X i)
inst_3 : ∀ (i : ι), OrderTopology.{u_2} (X i)
a x : (i : ι) → X i
inst_4 : Nonempty ι
ha : ∀ (i : ι), x i < a i
⊢ Iio a ∈ 𝓝 x

Tactic:
mem_of_superset
  (set_pi_mem_nhds finite_univ fun i _ ↦ Iio_mem_nhds (ha i)) (pi_univ_Iio_subset a)

Premises used: Iio_mem_nhds, set_pi_mem_nhds, Set.finite_univ, Set.pi_univ_Iio_subset, Filter.mem_of_superset
-- Module: Mathlib.Topology.Order.Basic
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
ι : Type u_1
inst_3 : Finite ι
a' x' : ι → α
inst_4 : Nonempty ι
ha : ∀ (i : ι), x' i < a' i
⊢ Iio a' ∈ 𝓝 x'

Tactic:
pi_Iio_mem_nhds ha

Premises used: pi_Iio_mem_nhds, Set.Mem
-- Module: Mathlib.Topology.Order.Basic
Goal:
ι : Type u_1
X : ι → Type u_2
inst : Finite ι
inst_1 : (i : ι) → LinearOrder (X i)
inst_2 : (i : ι) → TopologicalSpace (X i)
inst_3 : ∀ (i : ι), OrderTopology.{u_2} (X i)
a b x : (i : ι) → X i
inst_4 : Nonempty ι
ha : ∀ (i : ι), a i < x i
hb : ∀ (i : ι), x i < b i
⊢ Ioc a b ∈ 𝓝 x

Tactic:
mem_of_superset (set_pi_mem_nhds Set.finite_univ fun i _ => ?_) (pi_univ_Ioc_subset a b)

Premises used: set_pi_mem_nhds, Set.pi_univ_Ioc_subset, Set.finite_univ, Filter.mem_of_superset
-- Module: Mathlib.Topology.Order.Basic
Goal:
ι : Type u_1
X : ι → Type u_2
inst : Finite ι
inst_1 : (i : ι) → LinearOrder (X i)
inst_2 : (i : ι) → TopologicalSpace (X i)
inst_3 : ∀ (i : ι), OrderTopology.{u_2} (X i)
a b x : (i : ι) → X i
inst_4 : Nonempty ι
ha : ∀ (i : ι), a i < x i
hb : ∀ (i : ι), x i < b i
refine : ∀ (i : ι), Membership.mem (γ := Set ι) univ i → Ioc (a i) (b i) ∈ 𝓝 (x i)
⊢ Ioc a b ∈ 𝓝 x

Tactic:
refine mem_of_superset (set_pi_mem_nhds Set.finite_univ fun i _ => ?_) (pi_univ_Ioc_subset a b)

Premises used: set_pi_mem_nhds, Set.pi_univ_Ioc_subset, Set.finite_univ, Filter.mem_of_superset
-- Module: Mathlib.Topology.Order.Basic
Goal:
ι : Type u_1
X : ι → Type u_2
inst : Finite ι
inst_1 : (i : ι) → LinearOrder (X i)
inst_2 : (i : ι) → TopologicalSpace (X i)
inst_3 : ∀ (i : ι), OrderTopology.{u_2} (X i)
a b x : (i : ι) → X i
inst_4 : Nonempty ι
ha : ∀ (i : ι), a i < x i
hb : ∀ (i : ι), x i < b i
i : ι
h : Membership.mem (γ := Set ι) univ i
⊢ Ioc (a i) (b i) ∈ 𝓝 (x i)

Tactic:
Ioc_mem_nhds (ha i) (hb i)

Premises used: Ioc_mem_nhds
-- Module: Mathlib.Topology.Order.Basic
Goal:
ι : Type u_1
X : ι → Type u_2
inst : Finite ι
inst_1 : (i : ι) → LinearOrder (X i)
inst_2 : (i : ι) → TopologicalSpace (X i)
inst_3 : ∀ (i : ι), OrderTopology.{u_2} (X i)
a b x : (i : ι) → X i
inst_4 : Nonempty ι
ha : ∀ (i : ι), a i < x i
hb : ∀ (i : ι), x i < b i
i : ι
h : Membership.mem (γ := Set ι) univ i
⊢ Ioc (a i) (b i) ∈ 𝓝 (x i)

Tactic:
exact Ioc_mem_nhds (ha i) (hb i)

Premises used: Ioc_mem_nhds
-- Module: Mathlib.Topology.Order.Basic
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
ι : Type u_1
inst_3 : Finite ι
a' b' x' : ι → α
inst_4 : Nonempty ι
ha : ∀ (i : ι), a' i < x' i
hb : ∀ (i : ι), x' i < b' i
⊢ Ioc a' b' ∈ 𝓝 x'

Tactic:
pi_Ioc_mem_nhds ha hb

Premises used: Set.Mem, pi_Ioc_mem_nhds
-- Module: Mathlib.Topology.Order.Basic
Goal:
ι : Type u_1
X : ι → Type u_2
inst : Finite ι
inst_1 : (i : ι) → LinearOrder (X i)
inst_2 : (i : ι) → TopologicalSpace (X i)
inst_3 : ∀ (i : ι), OrderTopology.{u_2} (X i)
a b x : (i : ι) → X i
inst_4 : Nonempty ι
ha : ∀ (i : ι), a i < x i
hb : ∀ (i : ι), x i < b i
⊢ Ioo a b ∈ 𝓝 x

Tactic:
mem_of_superset (set_pi_mem_nhds Set.finite_univ fun i _ => ?_) (pi_univ_Ioo_subset a b)

Premises used: set_pi_mem_nhds, Set.pi_univ_Ioo_subset, Set.finite_univ, Filter.mem_of_superset
-- Module: Mathlib.Topology.Order.Basic
Goal:
ι : Type u_1
X : ι → Type u_2
inst : Finite ι
inst_1 : (i : ι) → LinearOrder (X i)
inst_2 : (i : ι) → TopologicalSpace (X i)
inst_3 : ∀ (i : ι), OrderTopology.{u_2} (X i)
a b x : (i : ι) → X i
inst_4 : Nonempty ι
ha : ∀ (i : ι), a i < x i
hb : ∀ (i : ι), x i < b i
refine : ∀ (i : ι), Membership.mem (γ := Set ι) univ i → Ioo (a i) (b i) ∈ 𝓝 (x i)
⊢ Ioo a b ∈ 𝓝 x

Tactic:
refine mem_of_superset (set_pi_mem_nhds Set.finite_univ fun i _ => ?_) (pi_univ_Ioo_subset a b)

Premises used: set_pi_mem_nhds, Set.pi_univ_Ioo_subset, Set.finite_univ, Filter.mem_of_superset
-- Module: Mathlib.Topology.Order.Basic
Goal:
ι : Type u_1
X : ι → Type u_2
inst : Finite ι
inst_1 : (i : ι) → LinearOrder (X i)
inst_2 : (i : ι) → TopologicalSpace (X i)
inst_3 : ∀ (i : ι), OrderTopology.{u_2} (X i)
a b x : (i : ι) → X i
inst_4 : Nonempty ι
ha : ∀ (i : ι), a i < x i
hb : ∀ (i : ι), x i < b i
i : ι
h : Membership.mem (γ := Set ι) univ i
⊢ Ioo (a i) (b i) ∈ 𝓝 (x i)

Tactic:
Ioo_mem_nhds (ha i) (hb i)

Premises used: Ioo_mem_nhds
-- Module: Mathlib.Topology.Order.Basic
Goal:
ι : Type u_1
X : ι → Type u_2
inst : Finite ι
inst_1 : (i : ι) → LinearOrder (X i)
inst_2 : (i : ι) → TopologicalSpace (X i)
inst_3 : ∀ (i : ι), OrderTopology.{u_2} (X i)
a b x : (i : ι) → X i
inst_4 : Nonempty ι
ha : ∀ (i : ι), a i < x i
hb : ∀ (i : ι), x i < b i
i : ι
h : Membership.mem (γ := Set ι) univ i
⊢ Ioo (a i) (b i) ∈ 𝓝 (x i)

Tactic:
exact Ioo_mem_nhds (ha i) (hb i)

Premises used: Ioo_mem_nhds
-- Module: Mathlib.Topology.Order.Basic
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
ι : Type u_1
inst_3 : Finite ι
a' b' x' : ι → α
inst_4 : Nonempty ι
ha : ∀ (i : ι), a' i < x' i
hb : ∀ (i : ι), x' i < b' i
⊢ Ioo a' b' ∈ 𝓝 x'

Tactic:
pi_Ioo_mem_nhds ha hb

Premises used: pi_Ioo_mem_nhds, Set.Mem
-- Module: Mathlib.Topology.Order.Basic
Goal:
X : Type u_1
inst : ConditionallyCompleteLinearOrder X
inst_1 : TopologicalSpace X
inst_2 : OrderTopology X
Y : Type u_2
inst_3 : ConditionallyCompleteLinearOrder Y
inst_4 : TopologicalSpace Y
inst_5 : OrderTopology Y
inst_6 : DenselyOrdered X
f : X → Y
x : X
hf : LeftOrdContinuous f
rw : Tendsto f (𝓝[≤] x) (𝓝 (f x))
⊢ ContinuousWithinAt f (Iic x) x

Tactic:
rw [ContinuousWithinAt, OrderTopology.topology_eq_generate_intervals (α := Y)]

Premises used: ContinuousWithinAt, OrderTopology.topology_eq_generate_intervals
-- Module: Mathlib.Topology.Order.Basic
Goal:
X : Type u_1
inst : ConditionallyCompleteLinearOrder X
inst_1 : TopologicalSpace X
inst_2 : OrderTopology X
Y : Type u_2
inst_3 : ConditionallyCompleteLinearOrder Y
inst_4 : TopologicalSpace Y
inst_5 : OrderTopology Y
inst_6 : DenselyOrdered X
f : X → Y
x : X
hf : LeftOrdContinuous f
simp_rw :
  ∀ (s : Set Y),
    Membership.mem (γ := Set (Set Y)) {s : Set Y | ∃ (a : Y), s = Ioi a ∨ s = Iio a} s →
      f x ∈ s → ∃ (u : Set X), IsOpen[inst_1] u ∧ x ∈ u ∧ u ∩ Iic x ⊆ f ⁻¹' s
⊢ Tendsto f (𝓝[≤] x) (𝓝 (f x))

Tactic:
simp_rw [TopologicalSpace.tendsto_nhds_generateFrom_iff, mem_nhdsWithin]

Premises used: TopologicalSpace.tendsto_nhds_generateFrom_iff, mem_nhdsWithin
-- Module: Mathlib.Topology.Order.Basic
Goal:
X : Type u_1
inst : ConditionallyCompleteLinearOrder X
inst_1 : TopologicalSpace X
inst_2 : OrderTopology X
Y : Type u_2
inst_3 : ConditionallyCompleteLinearOrder Y
inst_4 : TopologicalSpace Y
inst_5 : OrderTopology Y
inst_6 : DenselyOrdered X
f : X → Y
x : X
hf : LeftOrdContinuous f
z : Y
hxz : f x ∈ Ioi z
inl : ∀ (a : X) (hax : a ∈ Iio x) (hza : z < f a), ∃ (u : Set X), IsOpen[inst_1] u ∧ x ∈ u ∧ u ∩ Iic x ⊆ f ⁻¹' Ioi z
⊢ ∃ (u : Set X), IsOpen[inst_1] u ∧ x ∈ u ∧ u ∩ Iic x ⊆ f ⁻¹' Ioi z

Tactic:
obtain ⟨_, ⟨a, hax, rfl⟩, hza⟩ := (lt_isLUB_iff <| hf isLUB_Iio).mp hxz

Premises used: lt_isLUB_iff, isLUB_Iio, Iff.mp, rfl
-- Module: Mathlib.Topology.Order.Basic
Goal:
X : Type u_1
inst : ConditionallyCompleteLinearOrder X
inst_1 : TopologicalSpace X
inst_2 : OrderTopology X
Y : Type u_2
inst_3 : ConditionallyCompleteLinearOrder Y
inst_4 : TopologicalSpace Y
inst_5 : OrderTopology Y
inst_6 : DenselyOrdered X
f : X → Y
x : X
hf : LeftOrdContinuous f
z : Y
hxz : f x ∈ Ioi z
a : X
hax : a ∈ Iio x
hza : z < f a
⊢ ∃ (u : Set X), IsOpen[inst_1] u ∧ x ∈ u ∧ u ∩ Iic x ⊆ f ⁻¹' Ioi z

Tactic:
⟨Ioi a, isOpen_Ioi, hax, fun b hab ↦ hza.trans_le <| hf.mono hab.1.le⟩

Premises used: Set.Ioi, LT.lt.le, LeftOrdContinuous.mono, isOpen_Ioi, And.left, LT.lt.trans_le, And.intro, Exists.intro
-- Module: Mathlib.Topology.Order.Basic
Goal:
X : Type u_1
inst : ConditionallyCompleteLinearOrder X
inst_1 : TopologicalSpace X
inst_2 : OrderTopology X
Y : Type u_2
inst_3 : ConditionallyCompleteLinearOrder Y
inst_4 : TopologicalSpace Y
inst_5 : OrderTopology Y
inst_6 : DenselyOrdered X
f : X → Y
x : X
hf : LeftOrdContinuous f
z : Y
hxz : f x ∈ Ioi z
a : X
hax : a ∈ Iio x
hza : z < f a
⊢ ∃ (u : Set X), IsOpen[inst_1] u ∧ x ∈ u ∧ u ∩ Iic x ⊆ f ⁻¹' Ioi z

Tactic:
exact ⟨Ioi a, isOpen_Ioi, hax, fun b hab ↦ hza.trans_le <| hf.mono hab.1.le⟩
-- Module: Mathlib.Topology.Order.Basic
Goal:
X : Type u_1
inst : ConditionallyCompleteLinearOrder X
inst_1 : TopologicalSpace X
inst_2 : OrderTopology X
Y : Type u_2
inst_3 : ConditionallyCompleteLinearOrder Y
inst_4 : TopologicalSpace Y
inst_5 : OrderTopology Y
inst_6 : DenselyOrdered X
f : X → Y
x : X
hf : LeftOrdContinuous f
z : Y
hxz : f x ∈ Iio z
⊢ ∃ (u : Set X), IsOpen[inst_1] u ∧ x ∈ u ∧ u ∩ Iic x ⊆ f ⁻¹' Iio z

Tactic:
⟨univ, isOpen_univ, trivial, fun a ha ↦ (hf.mono ha.2).trans_lt hxz⟩

Premises used: trivial, Set.univ, LeftOrdContinuous.mono, isOpen_univ, And.right, And.intro, Exists.intro, LE.le.trans_lt
-- Module: Mathlib.Topology.Order.Basic
Goal:
X : Type u_1
inst : ConditionallyCompleteLinearOrder X
inst_1 : TopologicalSpace X
inst_2 : OrderTopology X
Y : Type u_2
inst_3 : ConditionallyCompleteLinearOrder Y
inst_4 : TopologicalSpace Y
inst_5 : OrderTopology Y
inst_6 : DenselyOrdered X
f : X → Y
x : X
hf : LeftOrdContinuous f
z : Y
hxz : f x ∈ Iio z
⊢ ∃ (u : Set X), IsOpen[inst_1] u ∧ x ∈ u ∧ u ∩ Iic x ⊆ f ⁻¹' Iio z

Tactic:
exact ⟨univ, isOpen_univ, trivial, fun a ha ↦ (hf.mono ha.2).trans_lt hxz⟩
-- Module: Mathlib.Topology.Order.Basic
Goal:
X : Type u_1
inst : ConditionallyCompleteLinearOrder X
inst_1 : TopologicalSpace X
inst_2 : OrderTopology X
Y : Type u_2
inst_3 : ConditionallyCompleteLinearOrder Y
inst_4 : TopologicalSpace Y
inst_5 : OrderTopology Y
inst_6 : DenselyOrdered X
f : X → Y
x : X
hf : RightOrdContinuous f
⊢ ContinuousWithinAt f (Ici x) x

Tactic:
hf.dual.continuousWithinAt_Iic

Premises used: Set.Ici, setOf, LeftOrdContinuous.continuousWithinAt_Iic, RightOrdContinuous.dual, OrderDual
-- Module: Mathlib.Topology.Order.Bornology
Goal:
α : Type u_1
s t : Set α
inst : Lattice α
inst_1 : Nonempty α
⊢ Membership.mem (γ := Set (Set α)) {s : Set α | BddBelow s ∧ BddAbove s} ∅

Tactic:
simp
-- Module: Mathlib.Topology.Order.Bornology
Goal:
α : Type u_1
s t : Set α
inst : Lattice α
inst_1 : Nonempty α
⊢ ∀ (x : α), Membership.mem (γ := Set (Set α)) {s : Set α | BddBelow s ∧ BddAbove s} {x}

Tactic:
simp
-- Module: Mathlib.Topology.Order.Bornology
Goal:
α : Type u_1
s : Set α
inst : Lattice α
inst_1 : Nonempty α
⊢ IsBounded s ↔ BddBelow s ∧ BddAbove s

Tactic:
simp [IsBounded, IsCobounded, -isCobounded_compl_iff]

Premises used: Bornology.IsBounded, Bornology.isCobounded_compl_iff, Bornology.IsCobounded
-- Module: Mathlib.Topology.Order.Bornology
Goal:
α : Type u_1
inst : Bornology α
inst_1 : Lattice α
inst_2 : Nonempty α
h : inst = orderBornology
s : Set α
rw : IsBounded s ↔ BddBelow s ∧ BddAbove s
rw₁ rw₂ : BddBelow s ∧ BddAbove s ↔ BddBelow s ∧ BddAbove s
⊢ IsBounded s ↔ BddBelow s ∧ BddAbove s

Tactic:
rw [h, orderBornology_isBounded]

Premises used: orderBornology_isBounded
-- Module: Mathlib.Topology.Order.Bornology
Goal:
α : Type u_1
inst : Bornology α
inst_1 : Lattice α
inst_2 : Nonempty α
refine : ∀ (h : IsOrderBornology α), inst = orderBornology
⊢ IsOrderBornology α ↔ inst = orderBornology

Tactic:
refine ⟨fun h ↦ ?_, fun h ↦ ⟨fun s ↦ by rw [h, orderBornology_isBounded]⟩⟩
-- Module: Mathlib.Topology.Order.Bornology
Goal:
α : Type u_1
inst : Bornology α
inst_1 : Lattice α
inst_2 : Nonempty α
h : IsOrderBornology α
h_cobounded : ∀ (s : Set α), s ∈ cobounded α ↔ s ∈ cobounded α
⊢ inst = orderBornology

Tactic:
ext s
-- Module: Mathlib.Topology.Order.Bornology
Goal:
α : Type u_1
inst : Bornology α
inst_1 : Lattice α
inst_2 : Nonempty α
h : IsOrderBornology α
s : Set α
⊢ s ∈ cobounded α ↔ s ∈ cobounded α

Tactic:
isBounded_compl_iff.symm.trans (h.1 _)

Premises used: Bornology.isBounded_compl_iff, IsOrderBornology.isBounded_iff_bddBelow_bddAbove, Iff.trans, Bornology.IsCobounded, Iff.symm
-- Module: Mathlib.Topology.Order.Bornology
Goal:
α : Type u_1
inst : Bornology α
inst_1 : Lattice α
inst_2 : Nonempty α
h : IsOrderBornology α
s : Set α
⊢ s ∈ cobounded α ↔ s ∈ cobounded α

Tactic:
exact isBounded_compl_iff.symm.trans (h.1 _)

Premises used: Bornology.isBounded_compl_iff, IsOrderBornology.isBounded_iff_bddBelow_bddAbove, Iff.trans, Iff.symm
-- Module: Mathlib.Topology.Order.Bornology
Goal:
α : Type u_1
s : Set α
inst : Bornology α
inst_1 : Preorder α
inst_2 : IsOrderBornology α
⊢ IsBounded s ↔ BddBelow s ∧ BddAbove s

Tactic:
IsOrderBornology.isBounded_iff_bddBelow_bddAbove _

Premises used: IsOrderBornology.isBounded_iff_bddBelow_bddAbove
-- Module: Mathlib.Topology.Order.Bornology
Goal:
α : Type u_1
s : Set α
inst : Bornology α
inst_1 : Preorder α
inst_2 : IsOrderBornology α
hs : IsBounded s
⊢ BddBelow s

Tactic:
(isBounded_iff_bddBelow_bddAbove.1 hs).1

Premises used: And.left, Iff.mp, isBounded_iff_bddBelow_bddAbove