awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Order.LeftRightLim
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : ConditionallyCompleteLinearOrder β
inst_2 : TopologicalSpace β
inst_3 : OrderTopology β
f : α → β
hf : Monotone f
x : α
inst_4 : TopologicalSpace α
inst_5 : OrderTopology α
h : leftLim f x = rightLim f x
h' : rightLim f x = f x
⊢ ContinuousWithinAt f (Ioi x) x

Tactic:
hf.continuousWithinAt_Ioi_iff_rightLim_eq.2 h'

Premises used: Iff.mpr, Monotone.continuousWithinAt_Ioi_iff_rightLim_eq
-- Module: Mathlib.Topology.Order.LeftRightLim
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : ConditionallyCompleteLinearOrder β
inst_2 : TopologicalSpace β
inst_3 : OrderTopology β
f : α → β
hf : Monotone f
x : α
inst_4 : TopologicalSpace α
inst_5 : OrderTopology α
h : leftLim f x = rightLim f x
h' : rightLim f x = f x
⊢ ContinuousWithinAt f (Ioi x) x

Tactic:
exact hf.continuousWithinAt_Ioi_iff_rightLim_eq.2 h'

Premises used: Iff.mpr, Monotone.continuousWithinAt_Ioi_iff_rightLim_eq
-- Module: Mathlib.Topology.Order.LeftRightLim
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : ConditionallyCompleteLinearOrder β
inst_2 : TopologicalSpace β
inst_3 : OrderTopology β
f : α → β
hf : Antitone f
x y : α
h : x ≤ y
⊢ f y ≤ leftLim f x

Tactic:
hf.dual_right.leftLim_le h

Premises used: Antitone.dual_right, Monotone.leftLim_le, OrderDual
-- Module: Mathlib.Topology.Order.LeftRightLim
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : ConditionallyCompleteLinearOrder β
inst_2 : TopologicalSpace β
inst_3 : OrderTopology β
f : α → β
hf : Antitone f
x y : α
h : x < y
⊢ leftLim f y ≤ f x

Tactic:
hf.dual_right.le_leftLim h

Premises used: Antitone.dual_right, OrderDual, Monotone.le_leftLim
-- Module: Mathlib.Topology.Order.LeftRightLim
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : ConditionallyCompleteLinearOrder β
inst_2 : TopologicalSpace β
inst_3 : OrderTopology β
f : α → β
hf : Antitone f
⊢ Antitone (leftLim f)

Tactic:
hf.dual_right.leftLim

Premises used: Monotone.leftLim, Antitone.dual_right, Antitone, OrderDual
-- Module: Mathlib.Topology.Order.LeftRightLim
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : ConditionallyCompleteLinearOrder β
inst_2 : TopologicalSpace β
inst_3 : OrderTopology β
f : α → β
hf : Antitone f
x y : α
h : x ≤ y
⊢ rightLim f y ≤ f x

Tactic:
hf.dual_right.le_rightLim h

Premises used: Antitone.dual_right, Monotone.le_rightLim, OrderDual
-- Module: Mathlib.Topology.Order.LeftRightLim
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : ConditionallyCompleteLinearOrder β
inst_2 : TopologicalSpace β
inst_3 : OrderTopology β
f : α → β
hf : Antitone f
x y : α
h : x < y
⊢ f y ≤ rightLim f x

Tactic:
hf.dual_right.rightLim_le h

Premises used: Antitone.dual_right, Monotone.rightLim_le, OrderDual
-- Module: Mathlib.Topology.Order.LeftRightLim
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : ConditionallyCompleteLinearOrder β
inst_2 : TopologicalSpace β
inst_3 : OrderTopology β
f : α → β
hf : Antitone f
⊢ Antitone (rightLim f)

Tactic:
hf.dual_right.rightLim

Premises used: Antitone.dual_right, Antitone, OrderDual, Monotone.rightLim
-- Module: Mathlib.Topology.Order.LeftRightLim
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : ConditionallyCompleteLinearOrder β
inst_2 : TopologicalSpace β
inst_3 : OrderTopology β
f : α → β
hf : Antitone f
x y : α
h : x ≤ y
⊢ rightLim f y ≤ leftLim f x

Tactic:
hf.dual_right.leftLim_le_rightLim h

Premises used: Antitone.dual_right, OrderDual, Monotone.leftLim_le_rightLim
-- Module: Mathlib.Topology.Order.LeftRightLim
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : ConditionallyCompleteLinearOrder β
inst_2 : TopologicalSpace β
inst_3 : OrderTopology β
f : α → β
hf : Antitone f
x y : α
h : x < y
⊢ leftLim f y ≤ rightLim f x

Tactic:
hf.dual_right.rightLim_le_leftLim h

Premises used: Antitone.dual_right, Monotone.rightLim_le_leftLim, OrderDual
-- Module: Mathlib.Topology.Order.LeftRightLim
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : ConditionallyCompleteLinearOrder β
inst_2 : TopologicalSpace β
inst_3 : OrderTopology β
f : α → β
hf : Antitone f
inst_4 : TopologicalSpace α
inst_5 : OrderTopology α
x : α
⊢ Tendsto f (𝓝[<] x) (𝓝 (leftLim f x))

Tactic:
hf.dual_right.tendsto_leftLim x

Premises used: Antitone.dual_right, OrderDual, Monotone.tendsto_leftLim
-- Module: Mathlib.Topology.Order.LeftRightLim
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : ConditionallyCompleteLinearOrder β
inst_2 : TopologicalSpace β
inst_3 : OrderTopology β
f : α → β
hf : Antitone f
inst_4 : TopologicalSpace α
inst_5 : OrderTopology α
x : α
⊢ Tendsto f (𝓝[<] x) (𝓝[≥] leftLim f x)

Tactic:
hf.dual_right.tendsto_leftLim_within x

Premises used: Set.Ici, Antitone.dual_right, setOf, Monotone.tendsto_leftLim_within, OrderDual
-- Module: Mathlib.Topology.Order.LeftRightLim
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : ConditionallyCompleteLinearOrder β
inst_2 : TopologicalSpace β
inst_3 : OrderTopology β
f : α → β
hf : Antitone f
inst_4 : TopologicalSpace α
inst_5 : OrderTopology α
x : α
⊢ Tendsto f (𝓝[>] x) (𝓝 (rightLim f x))

Tactic:
hf.dual_right.tendsto_rightLim x

Premises used: Antitone.dual_right, Monotone.tendsto_rightLim, OrderDual
-- Module: Mathlib.Topology.Order.LeftRightLim
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : ConditionallyCompleteLinearOrder β
inst_2 : TopologicalSpace β
inst_3 : OrderTopology β
f : α → β
hf : Antitone f
inst_4 : TopologicalSpace α
inst_5 : OrderTopology α
x : α
⊢ Tendsto f (𝓝[>] x) (𝓝[≤] rightLim f x)

Tactic:
hf.dual_right.tendsto_rightLim_within x

Premises used: Antitone.dual_right, setOf, Set.Iic, OrderDual, Monotone.tendsto_rightLim_within
-- Module: Mathlib.Topology.Order.LeftRightLim
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : ConditionallyCompleteLinearOrder β
inst_2 : TopologicalSpace β
inst_3 : OrderTopology β
f : α → β
hf : Antitone f
x : α
inst_4 : TopologicalSpace α
inst_5 : OrderTopology α
⊢ ContinuousWithinAt f (Iio x) x ↔ leftLim f x = f x

Tactic:
hf.dual_right.continuousWithinAt_Iio_iff_leftLim_eq

Premises used: Antitone.dual_right, Monotone.continuousWithinAt_Iio_iff_leftLim_eq, OrderDual
-- Module: Mathlib.Topology.Order.LeftRightLim
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : ConditionallyCompleteLinearOrder β
inst_2 : TopologicalSpace β
inst_3 : OrderTopology β
f : α → β
hf : Antitone f
x : α
inst_4 : TopologicalSpace α
inst_5 : OrderTopology α
⊢ ContinuousWithinAt f (Ioi x) x ↔ rightLim f x = f x

Tactic:
hf.dual_right.continuousWithinAt_Ioi_iff_rightLim_eq

Premises used: Antitone.dual_right, Monotone.continuousWithinAt_Ioi_iff_rightLim_eq, OrderDual
-- Module: Mathlib.Topology.Order.LeftRightLim
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : ConditionallyCompleteLinearOrder β
inst_2 : TopologicalSpace β
inst_3 : OrderTopology β
f : α → β
hf : Antitone f
x : α
inst_4 : TopologicalSpace α
inst_5 : OrderTopology α
⊢ ContinuousAt f x ↔ leftLim f x = rightLim f x

Tactic:
hf.dual_right.continuousAt_iff_leftLim_eq_rightLim

Premises used: Monotone.continuousAt_iff_leftLim_eq_rightLim, Antitone.dual_right, OrderDual
-- Module: Mathlib.Topology.Order.LeftRightNhds
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
a b : α
hab : a < b
s : Set α
⊢ s ∈ 𝓝[>] a

Tactic:
1

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.Topology.Order.LeftRightNhds
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
a b : α
hab : a < b
s : Set α
⊢ s ∈ 𝓝[Ioc a b] a

Tactic:
2

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.Topology.Order.LeftRightNhds
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
a b : α
hab : a < b
s : Set α
⊢ s ∈ 𝓝[>] a ↔ s ∈ 𝓝[Ioc a b] a

Tactic:
1 ↔ 2

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.Topology.Order.LeftRightNhds
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
a b : α
hab : a < b
s : Set α
rw rw₁ : s ∈ 𝓝[>] a ↔ s ∈ 𝓝[>] a
⊢ s ∈ 𝓝[>] a ↔ s ∈ 𝓝[Ioc a b] a

Tactic:
rw [nhdsWithin_Ioc_eq_nhdsGT hab]

Premises used: nhdsWithin_Ioc_eq_nhdsGT
-- Module: Mathlib.Topology.Order.LeftRightNhds
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
a b : α
hab : a < b
s : Set α
⊢ s ∈ 𝓝[>] a ↔ s ∈ 𝓝[Ioc a b] a

Tactic:
tfae_have 1 ↔ 2 := by
    rw [nhdsWithin_Ioc_eq_nhdsGT hab]
-- Module: Mathlib.Topology.Order.LeftRightNhds
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
a b : α
hab : a < b
s : Set α
tfae_1_iff_2 : s ∈ 𝓝[>] a ↔ s ∈ 𝓝[Ioc a b] a
⊢ s ∈ 𝓝[>] a

Tactic:
1

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.Topology.Order.LeftRightNhds
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
a b : α
hab : a < b
s : Set α
tfae_1_iff_2 : s ∈ 𝓝[>] a ↔ s ∈ 𝓝[Ioc a b] a
⊢ s ∈ 𝓝[Ioo a b] a

Tactic:
3

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.Topology.Order.LeftRightNhds
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
a b : α
hab : a < b
s : Set α
tfae_1_iff_2 : s ∈ 𝓝[>] a ↔ s ∈ 𝓝[Ioc a b] a
⊢ s ∈ 𝓝[>] a ↔ s ∈ 𝓝[Ioo a b] a

Tactic:
1 ↔ 3

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.Topology.Order.LeftRightNhds
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
a b : α
hab : a < b
s : Set α
tfae_1_iff_2 : s ∈ 𝓝[>] a ↔ s ∈ 𝓝[Ioc a b] a
rw rw₁ : s ∈ 𝓝[>] a ↔ s ∈ 𝓝[>] a
⊢ s ∈ 𝓝[>] a ↔ s ∈ 𝓝[Ioo a b] a

Tactic:
rw [nhdsWithin_Ioo_eq_nhdsGT hab]

Premises used: nhdsWithin_Ioo_eq_nhdsGT
-- Module: Mathlib.Topology.Order.LeftRightNhds
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
a b : α
hab : a < b
s : Set α
tfae_1_iff_2 : s ∈ 𝓝[>] a ↔ s ∈ 𝓝[Ioc a b] a
⊢ s ∈ 𝓝[>] a ↔ s ∈ 𝓝[Ioo a b] a

Tactic:
tfae_have 1 ↔ 3 := by
    rw [nhdsWithin_Ioo_eq_nhdsGT hab]
-- Module: Mathlib.Topology.Order.LeftRightNhds
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
a b : α
hab : a < b
s : Set α
tfae_1_iff_2 : s ∈ 𝓝[>] a ↔ s ∈ 𝓝[Ioc a b] a
tfae_1_iff_3 : s ∈ 𝓝[>] a ↔ s ∈ 𝓝[Ioo a b] a
⊢ ∃ u ∈ Ioc a b, Ioo a u ⊆ s

Tactic:
4

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.Topology.Order.LeftRightNhds
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
a b : α
hab : a < b
s : Set α
tfae_1_iff_2 : s ∈ 𝓝[>] a ↔ s ∈ 𝓝[Ioc a b] a
tfae_1_iff_3 : s ∈ 𝓝[>] a ↔ s ∈ 𝓝[Ioo a b] a
⊢ ∃ u ∈ Ioi a, Ioo a u ⊆ s

Tactic:
5

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.Topology.Order.LeftRightNhds
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
a b : α
hab : a < b
s : Set α
tfae_1_iff_2 : s ∈ 𝓝[>] a ↔ s ∈ 𝓝[Ioc a b] a
tfae_1_iff_3 : s ∈ 𝓝[>] a ↔ s ∈ 𝓝[Ioo a b] a
⊢ ∀ (a_1 : ∃ u ∈ Ioc a b, Ioo a u ⊆ s), ∃ u ∈ Ioi a, Ioo a u ⊆ s

Tactic:
4 → 5

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.Topology.Order.LeftRightNhds
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
a b : α
hab : a < b
s : Set α
tfae_1_iff_2 : s ∈ 𝓝[>] a ↔ s ∈ 𝓝[Ioc a b] a
tfae_1_iff_3 : s ∈ 𝓝[>] a ↔ s ∈ 𝓝[Ioo a b] a
⊢ ∀ (a_1 : ∃ u ∈ Ioc a b, Ioo a u ⊆ s), ∃ u ∈ Ioi a, Ioo a u ⊆ s

Tactic:
tfae_have 4 → 5 := fun ⟨u, umem, hu⟩ => ⟨u, umem.1, hu⟩
-- Module: Mathlib.Topology.Order.LeftRightNhds
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
a b : α
hab : a < b
s : Set α
tfae_1_iff_2 : s ∈ 𝓝[>] a ↔ s ∈ 𝓝[Ioc a b] a
tfae_1_iff_3 : s ∈ 𝓝[>] a ↔ s ∈ 𝓝[Ioo a b] a
tfae_4_to_5 : ∀ (a_1 : ∃ u ∈ Ioc a b, Ioo a u ⊆ s), ∃ u ∈ Ioi a, Ioo a u ⊆ s
⊢ ∃ u ∈ Ioi a, Ioo a u ⊆ s

Tactic:
5

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.Topology.Order.LeftRightNhds
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
a b : α
hab : a < b
s : Set α
tfae_1_iff_2 : s ∈ 𝓝[>] a ↔ s ∈ 𝓝[Ioc a b] a
tfae_1_iff_3 : s ∈ 𝓝[>] a ↔ s ∈ 𝓝[Ioo a b] a
tfae_4_to_5 : ∀ (a_1 : ∃ u ∈ Ioc a b, Ioo a u ⊆ s), ∃ u ∈ Ioi a, Ioo a u ⊆ s
⊢ s ∈ 𝓝[>] a

Tactic:
1

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.Topology.Order.LeftRightNhds
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
a b : α
hab : a < b
s : Set α
tfae_1_iff_2 : s ∈ 𝓝[>] a ↔ s ∈ 𝓝[Ioc a b] a
tfae_1_iff_3 : s ∈ 𝓝[>] a ↔ s ∈ 𝓝[Ioo a b] a
tfae_4_to_5 : ∀ (a_1 : ∃ u ∈ Ioc a b, Ioo a u ⊆ s), ∃ u ∈ Ioi a, Ioo a u ⊆ s
⊢ ∀ (a_1 : ∃ u ∈ Ioi a, Ioo a u ⊆ s), s ∈ 𝓝[>] a

Tactic:
5 → 1

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.Topology.Order.LeftRightNhds
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
a b : α
hab : a < b
s : Set α
tfae_1_iff_2 : s ∈ 𝓝[>] a ↔ s ∈ 𝓝[Ioc a b] a
tfae_1_iff_3 : s ∈ 𝓝[>] a ↔ s ∈ 𝓝[Ioo a b] a
tfae_4_to_5 : ∀ (a_1 : ∃ u ∈ Ioc a b, Ioo a u ⊆ s), ∃ u ∈ Ioi a, Ioo a u ⊆ s
⊢ ∀ (a_1 : ∃ u ∈ Ioi a, Ioo a u ⊆ s), s ∈ 𝓝[>] a

Tactic:
tfae_have 5 → 1
  | ⟨u, hau, hu⟩ => mem_of_superset (Ioo_mem_nhdsGT hau) hu
-- Module: Mathlib.Topology.Order.LeftRightNhds
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
a b : α
hab : a < b
s : Set α
tfae_1_iff_2 : s ∈ 𝓝[>] a ↔ s ∈ 𝓝[Ioc a b] a
tfae_1_iff_3 : s ∈ 𝓝[>] a ↔ s ∈ 𝓝[Ioo a b] a
tfae_4_to_5 : ∀ (a_1 : ∃ u ∈ Ioc a b, Ioo a u ⊆ s), ∃ u ∈ Ioi a, Ioo a u ⊆ s
tfae_5_to_1 : ∀ (a_1 : ∃ u ∈ Ioi a, Ioo a u ⊆ s), s ∈ 𝓝[>] a
⊢ s ∈ 𝓝[>] a

Tactic:
1

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.Topology.Order.LeftRightNhds
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
a b : α
hab : a < b
s : Set α
tfae_1_iff_2 : s ∈ 𝓝[>] a ↔ s ∈ 𝓝[Ioc a b] a
tfae_1_iff_3 : s ∈ 𝓝[>] a ↔ s ∈ 𝓝[Ioo a b] a
tfae_4_to_5 : ∀ (a_1 : ∃ u ∈ Ioc a b, Ioo a u ⊆ s), ∃ u ∈ Ioi a, Ioo a u ⊆ s
tfae_5_to_1 : ∀ (a_1 : ∃ u ∈ Ioi a, Ioo a u ⊆ s), s ∈ 𝓝[>] a
⊢ ∃ u ∈ Ioc a b, Ioo a u ⊆ s

Tactic:
4

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.Topology.Order.LeftRightNhds
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
a b : α
hab : a < b
s : Set α
tfae_1_iff_2 : s ∈ 𝓝[>] a ↔ s ∈ 𝓝[Ioc a b] a
tfae_1_iff_3 : s ∈ 𝓝[>] a ↔ s ∈ 𝓝[Ioo a b] a
tfae_4_to_5 : ∀ (a_1 : ∃ u ∈ Ioc a b, Ioo a u ⊆ s), ∃ u ∈ Ioi a, Ioo a u ⊆ s
tfae_5_to_1 : ∀ (a_1 : ∃ u ∈ Ioi a, Ioo a u ⊆ s), s ∈ 𝓝[>] a
⊢ ∀ (a_1 : s ∈ 𝓝[>] a), ∃ u ∈ Ioc a b, Ioo a u ⊆ s

Tactic:
1 → 4

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.Topology.Order.LeftRightNhds
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
a b : α
hab : a < b
s : Set α
tfae_1_iff_2 : s ∈ 𝓝[>] a ↔ s ∈ 𝓝[Ioc a b] a
tfae_1_iff_3 : s ∈ 𝓝[>] a ↔ s ∈ 𝓝[Ioo a b] a
tfae_4_to_5 : ∀ (a_1 : ∃ u ∈ Ioc a b, Ioo a u ⊆ s), ∃ u ∈ Ioi a, Ioo a u ⊆ s
tfae_5_to_1 : ∀ (a_1 : ∃ u ∈ Ioi a, Ioo a u ⊆ s), s ∈ 𝓝[>] a
h_1 : s ∈ 𝓝[>] a
h : s ∈ 𝓝[>] a := h_1
rcases : ∀ (v : Set α) (va : v ∈ 𝓝 a) (hv : v ∩ Ioi a ⊆ s), ∃ u ∈ Ioc a b, Ioo a u ⊆ s
⊢ ∃ u ∈ Ioc a b, Ioo a u ⊆ s

Tactic:
rcases mem_nhdsWithin_iff_exists_mem_nhds_inter.1 h with ⟨v, va, hv⟩

Premises used: Iff.mp, mem_nhdsWithin_iff_exists_mem_nhds_inter
-- Module: Mathlib.Topology.Order.LeftRightNhds
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
a b : α
hab : a < b
s : Set α
tfae_1_iff_2 : s ∈ 𝓝[>] a ↔ s ∈ 𝓝[Ioc a b] a
tfae_1_iff_3 : s ∈ 𝓝[>] a ↔ s ∈ 𝓝[Ioo a b] a
tfae_4_to_5 : ∀ (a_1 : ∃ u ∈ Ioc a b, Ioo a u ⊆ s), ∃ u ∈ Ioi a, Ioo a u ⊆ s
tfae_5_to_1 : ∀ (a_1 : ∃ u ∈ Ioi a, Ioo a u ⊆ s), s ∈ 𝓝[>] a
h_1 : s ∈ 𝓝[>] a
h : s ∈ 𝓝[>] a := h_1
v : Set α
va : v ∈ 𝓝 a
hv : v ∩ Ioi a ⊆ s
rcases : ∀ (u : α) (au : u ∈ Ioc a b) (hu : Ico a u ⊆ v), ∃ u ∈ Ioc a b, Ioo a u ⊆ s
⊢ ∃ u ∈ Ioc a b, Ioo a u ⊆ s

Tactic:
rcases exists_Ico_subset_of_mem_nhds' va hab with ⟨u, au, hu⟩

Premises used: exists_Ico_subset_of_mem_nhds'
-- Module: Mathlib.Topology.Order.LeftRightNhds
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
a b : α
hab : a < b
s : Set α
tfae_1_iff_2 : s ∈ 𝓝[>] a ↔ s ∈ 𝓝[Ioc a b] a
tfae_1_iff_3 : s ∈ 𝓝[>] a ↔ s ∈ 𝓝[Ioo a b] a
tfae_4_to_5 : ∀ (a_1 : ∃ u ∈ Ioc a b, Ioo a u ⊆ s), ∃ u ∈ Ioi a, Ioo a u ⊆ s
tfae_5_to_1 : ∀ (a_1 : ∃ u ∈ Ioi a, Ioo a u ⊆ s), s ∈ 𝓝[>] a
h_1 : s ∈ 𝓝[>] a
h : s ∈ 𝓝[>] a := h_1
v : Set α
va : v ∈ 𝓝 a
hv : v ∩ Ioi a ⊆ s
u : α
au : u ∈ Ioc a b
hu : Ico a u ⊆ v
⊢ ∃ u ∈ Ioc a b, Ioo a u ⊆ s

Tactic:
⟨u, au, fun x hx => hv ⟨hu ⟨le_of_lt hx.1, hx.2⟩, hx.1⟩⟩

Premises used: le_of_lt, And.right, And.left, And.intro, Exists.intro
-- Module: Mathlib.Topology.Order.LeftRightNhds
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
a b : α
hab : a < b
s : Set α
tfae_1_iff_2 : s ∈ 𝓝[>] a ↔ s ∈ 𝓝[Ioc a b] a
tfae_1_iff_3 : s ∈ 𝓝[>] a ↔ s ∈ 𝓝[Ioo a b] a
tfae_4_to_5 : ∀ (a_1 : ∃ u ∈ Ioc a b, Ioo a u ⊆ s), ∃ u ∈ Ioi a, Ioo a u ⊆ s
tfae_5_to_1 : ∀ (a_1 : ∃ u ∈ Ioi a, Ioo a u ⊆ s), s ∈ 𝓝[>] a
h_1 : s ∈ 𝓝[>] a
h : s ∈ 𝓝[>] a := h_1
v : Set α
va : v ∈ 𝓝 a
hv : v ∩ Ioi a ⊆ s
u : α
au : u ∈ Ioc a b
hu : Ico a u ⊆ v
⊢ ∃ u ∈ Ioc a b, Ioo a u ⊆ s

Tactic:
exact ⟨u, au, fun x hx => hv ⟨hu ⟨le_of_lt hx.1, hx.2⟩, hx.1⟩⟩
-- Module: Mathlib.Topology.Order.LeftRightNhds
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
a b : α
hab : a < b
s : Set α
tfae_1_iff_2 : s ∈ 𝓝[>] a ↔ s ∈ 𝓝[Ioc a b] a
tfae_1_iff_3 : s ∈ 𝓝[>] a ↔ s ∈ 𝓝[Ioo a b] a
tfae_4_to_5 : ∀ (a_1 : ∃ u ∈ Ioc a b, Ioo a u ⊆ s), ∃ u ∈ Ioi a, Ioo a u ⊆ s
tfae_5_to_1 : ∀ (a_1 : ∃ u ∈ Ioi a, Ioo a u ⊆ s), s ∈ 𝓝[>] a
⊢ ∀ (a_1 : s ∈ 𝓝[>] a), ∃ u ∈ Ioc a b, Ioo a u ⊆ s

Tactic:
tfae_have 1 → 4
  | h => by
    rcases mem_nhdsWithin_iff_exists_mem_nhds_inter.1 h with ⟨v, va, hv⟩
    rcases exists_Ico_subset_of_mem_nhds' va hab with ⟨u, au, hu⟩
    exact ⟨u, au, fun x hx => hv ⟨hu ⟨le_of_lt hx.1, hx.2⟩, hx.1⟩⟩
-- Module: Mathlib.Topology.Order.LeftRightNhds
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
a b : α
hab : a < b
s : Set α
tfae_1_iff_2 : s ∈ 𝓝[>] a ↔ s ∈ 𝓝[Ioc a b] a
tfae_1_iff_3 : s ∈ 𝓝[>] a ↔ s ∈ 𝓝[Ioo a b] a
tfae_4_to_5 : ∀ (a_1 : ∃ u ∈ Ioc a b, Ioo a u ⊆ s), ∃ u ∈ Ioi a, Ioo a u ⊆ s
tfae_5_to_1 : ∀ (a_1 : ∃ u ∈ Ioi a, Ioo a u ⊆ s), s ∈ 𝓝[>] a
tfae_1_to_4 : ∀ (a_1 : s ∈ 𝓝[>] a), ∃ u ∈ Ioc a b, Ioo a u ⊆ s
⊢ [s ∈ 𝓝[>] a, s ∈ 𝓝[Ioc a b] a, s ∈ 𝓝[Ioo a b] a, ∃ u ∈ Ioc a b, Ioo a u ⊆ s, ∃ u ∈ Ioi a, Ioo a u ⊆ s].TFAE

Tactic:
tfae_finish
-- Module: Mathlib.Topology.Order.LeftRightNhds
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
a u' : α
s : Set α
hu' : a < u'
⊢ s ∈ 𝓝[>] a ↔ ∃ u ∈ Ioc a u', Ioo a u ⊆ s

Tactic:
(TFAE_mem_nhdsGT hu' s).out 0 3

Premises used: TFAE_mem_nhdsGT, List.TFAE.out, OfNat.ofNat
-- Module: Mathlib.Topology.Order.LeftRightNhds
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
a u' : α
s : Set α
hu' : a < u'
⊢ s ∈ 𝓝[>] a ↔ ∃ u ∈ Ioi a, Ioo a u ⊆ s

Tactic:
(TFAE_mem_nhdsGT hu' s).out 0 4

Premises used: TFAE_mem_nhdsGT, List.TFAE.out, OfNat.ofNat
-- Module: Mathlib.Topology.Order.LeftRightNhds
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
a : α
h : ∃ (b : α), a < b
⊢ (𝓝[>] a).HasBasis (fun (x : α) ↦ a < x) (Ioo a)

Tactic:
let ⟨_, h⟩ := h
  ⟨fun _ => mem_nhdsGT_iff_exists_Ioo_subset' h⟩

Premises used: Set.Ioi, nhdsWithin, mem_nhdsGT_iff_exists_Ioo_subset', Filter.HasBasis, _private.0.nhdsGT_basis_of_exists_gt.match_1, Filter.HasBasis.mk, LT.lt, Set.Ioo
-- Module: Mathlib.Topology.Order.LeftRightNhds
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : NoMaxOrder α
a : α
⊢ (𝓝[>] a).HasBasis (fun (x : α) ↦ a < x) (Ioo a)

Tactic:
nhdsGT_basis_of_exists_gt <| exists_gt a

Premises used: nhdsGT_basis_of_exists_gt, NoMaxOrder.exists_gt
-- Module: Mathlib.Topology.Order.LeftRightNhds
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
a : α
pos : ∀ (ha : IsTop a), 𝓝[>] a = ⊥ ↔ IsTop a ∨ ∃ (b : α), a ⋖ b
neg : ∀ (ha : ¬IsTop a), 𝓝[>] a = ⊥ ↔ IsTop a ∨ ∃ (b : α), a ⋖ b
⊢ 𝓝[>] a = ⊥ ↔ IsTop a ∨ ∃ (b : α), a ⋖ b

Tactic:
by_cases ha : IsTop a

Premises used: IsTop
-- Module: Mathlib.Topology.Order.LeftRightNhds
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
a : α
ha : IsTop a
⊢ 𝓝[>] a = ⊥ ↔ IsTop a ∨ ∃ (b : α), a ⋖ b

Tactic:
simp [ha, ha.isMax.Ioi_eq]

Premises used: IsMax.Ioi_eq, IsTop.isMax
-- Module: Mathlib.Topology.Order.LeftRightNhds
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
a : α
ha : ¬IsTop a
neg : 𝓝[>] a = ⊥ ↔ ∃ (b : α), a ⋖ b
⊢ 𝓝[>] a = ⊥ ↔ IsTop a ∨ ∃ (b : α), a ⋖ b

Tactic:
simp only [ha, false_or]

Premises used: false_or
-- Module: Mathlib.Topology.Order.LeftRightNhds
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
a : α
ha : ¬IsTop a
⊢ ∃ (b : α), a < b

Tactic:
rw [isTop_iff_isMax, not_isMax_iff] at ha

Premises used: isTop_iff_isMax, not_isMax_iff
-- Module: Mathlib.Topology.Order.LeftRightNhds
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
a : α
ha : ∃ (b : α), a < b
⊢ 𝓝[>] a = ⊥ ↔ ∃ (b : α), a ⋖ b

Tactic:
simp only [(nhdsGT_basis_of_exists_gt ha).eq_bot_iff, covBy_iff_Ioo_eq]

Premises used: Filter.HasBasis.eq_bot_iff, nhdsGT_basis_of_exists_gt, covBy_iff_Ioo_eq
-- Module: Mathlib.Topology.Order.LeftRightNhds
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : NoMaxOrder α
a : α
s : Set α
⊢ s ∈ 𝓝[>] a ↔ ∃ u ∈ Ioi a, Ioo a u ⊆ s

Tactic:
let ⟨_u', hu'⟩ := exists_gt a
  mem_nhdsGT_iff_exists_Ioo_subset' hu'

Premises used: Set.Ioi, nhdsWithin, mem_nhdsGT_iff_exists_Ioo_subset', Membership.mem, Exists, HasSubset.Subset, NoMaxOrder.exists_gt, And, Iff, _private.0.nhdsGT_basis_of_exists_gt.match_1, Set.Ioo
-- Module: Mathlib.Topology.Order.LeftRightNhds
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : SecondCountableTopology α
simp : Set.Countable.{u_1} (α := α) ({a : α | IsTop a} ∪ {a : α | ∃ (b : α), a ⋖ b})
⊢ Set.Countable.{u_1} (α := α) {x : α | 𝓝[>] x = ⊥}

Tactic:
simp only [nhdsGT_eq_bot_iff, setOf_or]

Premises used: nhdsGT_eq_bot_iff, Set.setOf_or
-- Module: Mathlib.Topology.Order.LeftRightNhds
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : SecondCountableTopology α
⊢ Set.Countable.{u_1} (α := α) ({a : α | IsTop a} ∪ {a : α | ∃ (b : α), a ⋖ b})

Tactic:
(subsingleton_isTop α).countable.union countable_setOf_covBy_right

Premises used: Set.subsingleton_isTop, Set.Countable.union, countable_setOf_covBy_right, Set.Subsingleton.countable