awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.Order.LeftRightNhds (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : SecondCountableTopology α
s : Set α
t : Set α := {x : α | x ∈ s ∧ 𝓝[s ∩ Ioi x] x = ⊥ ∧ ¬IsTop x}
⊢ Set.Countable.{u_1} (α := α) {x : α | x ∈ s ∧ 𝓝[s ∩ Ioi x] x = ⊥}
have suffices : t.Countable
Tactic: suffices H : t.Countable by
    have : { x ∈ s | 𝓝[s ∩ Ioi x] x = ⊥ } ⊆ t ∪ {x | IsTop x} := by
      intro x hx
      by_cases h'x : IsTop x
      · simp [h'x]
      · simpa [-sep_and, t, h'x]
    apply Countable.mono this
    simp [H, (subsingleton_isTop α).countable]
-- Lean 4 proof step from Mathlib.Topology.Order.LeftRightNhds (hypothesis)
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : SecondCountableTopology α
s : Set α
t : Set α := {x : α | x ∈ s ∧ 𝓝[s ∩ Ioi x] x = ⊥ ∧ ¬IsTop x}
x : α
hx : x ∈ t
⊢ ∃ y > x, s ∩ Ioo x y = ∅
have hx₁ : x ∈ s ∧ (∃ u ∈ 𝓝 x, u ∩ (s ∩ Ioi x) = ∅) ∧ ∃ (x_1 : α), x < x_1
Tactic: simp only [← empty_mem_iff_bot, mem_nhdsWithin_iff_exists_mem_nhds_inter,
      subset_empty_iff, IsTop, not_forall, not_le, mem_setOf_eq, t] at hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Topology.Order.LeftRightNhds (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : SecondCountableTopology α
s : Set α
t : Set α := {x : α | x ∈ s ∧ 𝓝[s ∩ Ioi x] x = ⊥ ∧ ¬IsTop x}
x : α
hx : x ∈ s ∧ (∃ u ∈ 𝓝 x, u ∩ (s ∩ Ioi x) = ∅) ∧ ∃ (x_1 : α), x < x_1
⊢ ∃ y > x, s ∩ Ioo x y = ∅
have rcases : ∀ (u : Set α) (hu : u ∈ 𝓝 x) (h'u : u ∩ (s ∩ Ioi x) = ∅), ∃ y > x, s ∩ Ioo x y = ∅
Tactic: rcases hx.2.1 with ⟨u, hu, h'u⟩
-- Lean 4 proof step from Mathlib.Topology.Order.LeftRightNhds (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : SecondCountableTopology α
s : Set α
t : Set α := {x : α | x ∈ s ∧ 𝓝[s ∩ Ioi x] x = ⊥ ∧ ¬IsTop x}
x : α
hx : x ∈ s ∧ (∃ u ∈ 𝓝 x, u ∩ (s ∩ Ioi x) = ∅) ∧ ∃ (x_1 : α), x < x_1
u : Set α
hu : u ∈ 𝓝 x
h'u : u ∩ (s ∩ Ioi x) = ∅
⊢ ∃ y > x, s ∩ Ioo x y = ∅
have obtain : ∀ (y : α) (hxy : x < y) (hy : Ico x y ⊆ u), ∃ y > x, s ∩ Ioo x y = ∅
Tactic: obtain ⟨y, hxy, hy⟩ : ∃ y, x < y ∧ Ico x y ⊆ u := exists_Ico_subset_of_mem_nhds hu hx.2.2
-- Lean 4 proof step from Mathlib.Topology.Order.LeftRightNhds (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : SecondCountableTopology α
s : Set α
t : Set α := {x : α | x ∈ s ∧ 𝓝[s ∩ Ioi x] x = ⊥ ∧ ¬IsTop x}
x : α
hx : x ∈ s ∧ (∃ u ∈ 𝓝 x, u ∩ (s ∩ Ioi x) = ∅) ∧ ∃ (x_1 : α), x < x_1
u : Set α
hu : u ∈ 𝓝 x
h'u : u ∩ (s ∩ Ioi x) = ∅
y : α
hxy : x < y
hy : Ico x y ⊆ u
⊢ ∃ y > x, s ∩ Ioo x y = ∅
have refine : s ∩ Ioo x y = ∅
Tactic: refine ⟨y, hxy, ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Order.LeftRightNhds (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : SecondCountableTopology α
s : Set α
t : Set α := {x : α | x ∈ s ∧ 𝓝[s ∩ Ioi x] x = ⊥ ∧ ¬IsTop x}
x : α
hx : x ∈ s ∧ (∃ u ∈ 𝓝 x, u ∩ (s ∩ Ioi x) = ∅) ∧ ∃ (x_1 : α), x < x_1
u : Set α
hu : u ∈ 𝓝 x
h'u : u ∩ (s ∩ Ioi x) = ∅
y : α
hxy : x < y
hy : Ico x y ⊆ u
⊢ s ∩ Ioo x y = ∅
have contrapose! : ∀ (h'u : (s ∩ Ioo x y).Nonempty), (u ∩ (s ∩ Ioi x)).Nonempty
Tactic: contrapose! h'u
Cleared hypotheses: h'u
-- Lean 4 proof step from Mathlib.Topology.Order.LeftRightNhds (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : SecondCountableTopology α
s : Set α
t : Set α := {x : α | x ∈ s ∧ 𝓝[s ∩ Ioi x] x = ⊥ ∧ ¬IsTop x}
x : α
hx : x ∈ s ∧ (∃ u ∈ 𝓝 x, u ∩ (s ∩ Ioi x) = ∅) ∧ ∃ (x_1 : α), x < x_1
u : Set α
hu : u ∈ 𝓝 x
y : α
hxy : x < y
hy : Ico x y ⊆ u
h'u : (s ∩ Ioo x y).Nonempty
⊢ (u ∩ (s ∩ Ioi x)).Nonempty
have apply : s ∩ Ioo x y ⊆ u ∩ (s ∩ Ioi x)
Tactic: apply h'u.mono
-- Lean 4 proof step from Mathlib.Topology.Order.LeftRightNhds (hypothesis)
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : SecondCountableTopology α
s : Set α
t : Set α := {x : α | x ∈ s ∧ 𝓝[s ∩ Ioi x] x = ⊥ ∧ ¬IsTop x}
⊢ t.Countable
have this : ∀ (x : α) (hx : x ∈ t), ∃ y > x, s ∩ Ioo x y = ∅
Tactic: have (x) (hx : x ∈ t) : ∃ y > x, s ∩ Ioo x y = ∅ := by
    simp only [← empty_mem_iff_bot, mem_nhdsWithin_iff_exists_mem_nhds_inter,
      subset_empty_iff, IsTop, not_forall, not_le, mem_setOf_eq, t] at hx
    rcases hx.2.1 with ⟨u, hu, h'u⟩
    obtain ⟨y, hxy, hy⟩ : ∃ y, x < y ∧ Ico x y ⊆ u := exists_Ico_subset_of_mem_nhds hu hx.2.2
    refine ⟨y, hxy, ?_⟩
    contrapose! h'u
    apply h'u.mono
    intro z hz
    exact ⟨hy ⟨hz.2.1.le, hz.2.2⟩, hz.1, hz.2.1⟩
-- Lean 4 proof step from Mathlib.Topology.Order.LeftRightNhds (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : SecondCountableTopology α
s : Set α
t : Set α := {x : α | x ∈ s ∧ 𝓝[s ∩ Ioi x] x = ⊥ ∧ ¬IsTop x}
this : ∀ (x : α) (hx : x ∈ t), ∃ y > x, s ∩ Ioo x y = ∅
⊢ t.Countable
have choose! : ∀ (y : (x : α) → α) (hy : ∀ (x : α) (hx : x ∈ t), y x > x) (h'y : ∀ (x : α) (hx : x ∈ t), s ∩ Ioo x (y x) = ∅),
  t.Countable
Tactic: choose! y hy h'y using this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Topology.Order.LeftRightNhds (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : SecondCountableTopology α
s : Set α
t : Set α := {x : α | x ∈ s ∧ 𝓝[s ∩ Ioi x] x = ⊥ ∧ ¬IsTop x}
y : (x : α) → α
hy : ∀ (x : α) (hx : x ∈ t), y x > x
h'y : ∀ (x : α) (hx : x ∈ t), s ∩ Ioo x (y x) = ∅
⊢ t.Countable
have apply : t.PairwiseDisjoint (α := Set α) fun (x : α) ↦ Ioo x (y x)
Tactic: apply Set.PairwiseDisjoint.countable_of_Ioo (y := y) _ hy
-- Lean 4 proof step from Mathlib.Topology.Order.LeftRightNhds (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : SecondCountableTopology α
s : Set α
t : Set α := {x : α | x ∈ s ∧ 𝓝[s ∩ Ioi x] x = ⊥ ∧ ¬IsTop x}
y : (x : α) → α
hy : ∀ (x : α) (hx : x ∈ t), y x > x
h'y : ∀ (x : α) (hx : x ∈ t), s ∩ Ioo x (y x) = ∅
a : α
ha : a ∈ t
b : α
hb : b ∈ t
hab : a ≠ b
⊢ Disjoint (Ioo a (y a)) (Ioo b (y b))
have inr : ∀ (h : ∀ ⦃a : α⦄ (ha : a ∈ t) ⦃b : α⦄ (hb : b ∈ t) (hab : a ≠ b) (H : a < b), Disjoint (Ioo a (y a)) (Ioo b (y b)))
  (H : b ≤ a), Disjoint (Ioo a (y a)) (Ioo b (y b))
Tactic: wlog! H : a < b generalizing a b with h
-- Lean 4 proof step from Mathlib.Topology.Order.LeftRightNhds (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : SecondCountableTopology α
s : Set α
t : Set α := {x : α | x ∈ s ∧ 𝓝[s ∩ Ioi x] x = ⊥ ∧ ¬IsTop x}
y : (x : α) → α
hy : ∀ (x : α) (hx : x ∈ t), y x > x
h'y : ∀ (x : α) (hx : x ∈ t), s ∩ Ioo x (y x) = ∅
a : α
ha : a ∈ t
b : α
hb : b ∈ t
hab : a ≠ b
inr :
  ∀ (h : ∀ ⦃a : α⦄ (ha : a ∈ t) ⦃b : α⦄ (hb : b ∈ t) (hab : a ≠ b) (H : a < b), Disjoint (Ioo a (y a)) (Ioo b (y b)))
    (H : b ≤ a), Disjoint (Ioo a (y a)) (Ioo b (y b))
⊢ Disjoint (Ioo a (y a)) (Ioo b (y b))
have wlog! : ∀ ⦃a : α⦄ (ha : a ∈ t) ⦃b : α⦄ (hb : b ∈ t) (hab : a ≠ b) (H : a < b), Disjoint (Ioo a (y a)) (Ioo b (y b))
Tactic: wlog! H : a < b generalizing a b with h
Cleared hypotheses: a, ha, b, hb, hab
-- Lean 4 proof step from Mathlib.Topology.Order.LeftRightNhds (hypothesis)
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : SecondCountableTopology α
s : Set α
t : Set α := {x : α | x ∈ s ∧ 𝓝[s ∩ Ioi x] x = ⊥ ∧ ¬IsTop x}
y : (x : α) → α
hy : ∀ (x : α) (hx : x ∈ t), y x > x
h'y : ∀ (x : α) (hx : x ∈ t), s ∩ Ioo x (y x) = ∅
a : α
ha : a ∈ t
b : α
hb : b ∈ t
hab : a ≠ b
h : ∀ ⦃a : α⦄ (ha : a ∈ t) ⦃b : α⦄ (hb : b ∈ t) (hab : a ≠ b) (H : a < b), Disjoint (Ioo a (y a)) (Ioo b (y b))
H : b ≤ a
⊢ Disjoint (Ioo a (y a)) (Ioo b (y b))
have this : b < a
Tactic: have : b < a := lt_of_le_of_ne H hab.symm
-- Lean 4 proof step from Mathlib.Topology.Order.LeftRightNhds (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : SecondCountableTopology α
s : Set α
t : Set α := {x : α | x ∈ s ∧ 𝓝[s ∩ Ioi x] x = ⊥ ∧ ¬IsTop x}
y : (x : α) → α
hy : ∀ (x : α) (hx : x ∈ t), y x > x
h'y : ∀ (x : α) (hx : x ∈ t), s ∩ Ioo x (y x) = ∅
a : α
ha : a ∈ t
b : α
hb : b ∈ t
hab : a ≠ b
H : a < b
⊢ y a ≤ b
have by_contra! : ∀ (this : b < y a), False
Tactic: by_contra!
-- Lean 4 proof step from Mathlib.Topology.Order.LeftRightNhds (hypothesis)
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : SecondCountableTopology α
s : Set α
t : Set α := {x : α | x ∈ s ∧ 𝓝[s ∩ Ioi x] x = ⊥ ∧ ¬IsTop x}
y : (x : α) → α
hy : ∀ (x : α) (hx : x ∈ t), y x > x
h'y : ∀ (x : α) (hx : x ∈ t), s ∩ Ioo x (y x) = ∅
a : α
ha : a ∈ t
b : α
hb : b ∈ t
hab : a ≠ b
H : a < b
this : b < y a
⊢ False
have this₁ : b ∈ s ∩ Ioo a (y a)
Tactic: have : b ∈ s ∩ Ioo a (y a) := by simp [hb.1, H, this]
-- Lean 4 proof step from Mathlib.Topology.Order.LeftRightNhds (hypothesis)
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : SecondCountableTopology α
s : Set α
t : Set α := {x : α | x ∈ s ∧ 𝓝[s ∩ Ioi x] x = ⊥ ∧ ¬IsTop x}
y : (x : α) → α
hy : ∀ (x : α) (hx : x ∈ t), y x > x
h'y : ∀ (x : α) (hx : x ∈ t), s ∩ Ioo x (y x) = ∅
a : α
ha : a ∈ t
b : α
hb : b ∈ t
hab : a ≠ b
H : a < b
⊢ Disjoint (Ioo a (y a)) (Ioo b (y b))
have this : y a ≤ b
Tactic: have : y a ≤ b := by
    by_contra!
    have : b ∈ s ∩ Ioo a (y a) := by simp [hb.1, H, this]
    simp [h'y a ha] at this
-- Lean 4 proof step from Mathlib.Topology.Order.LeftRightNhds (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : SecondCountableTopology α
s : Set α
t : Set α := {x : α | x ∈ s ∧ 𝓝[s ∩ Ioi x] x = ⊥ ∧ ¬IsTop x}
y : (x : α) → α
hy : ∀ (x : α) (hx : x ∈ t), y x > x
h'y : ∀ (x : α) (hx : x ∈ t), s ∩ Ioo x (y x) = ∅
a : α
ha : a ∈ t
b : α
hb : b ∈ t
hab : a ≠ b
H : a < b
this : y a ≤ b
⊢ Disjoint (Ioo a (y a)) (Ioo b (y b))
have rw : ∀ ⦃a_1 : α⦄, a_1 ∈ Ioo a (y a) → ∀ ⦃b_1 : α⦄, b_1 ∈ Ioo b (y b) → a_1 ≠ b_1
Tactic: rw [disjoint_iff_forall_ne]
-- Lean 4 proof step from Mathlib.Topology.Order.LeftRightNhds (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : NoMaxOrder α
inst_4 : DenselyOrdered α
a : α
s : Set α
⊢ s ∈ 𝓝[>] a ↔ ∃ u ∈ Ioi a, Ioc a u ⊆ s
have rw : (∃ u ∈ Ioi a, Ioo a u ⊆ s) ↔ ∃ u ∈ Ioi a, Ioc a u ⊆ s
Tactic: rw [mem_nhdsGT_iff_exists_Ioo_subset]
-- Lean 4 proof step from Mathlib.Topology.Order.LeftRightNhds (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : NoMaxOrder α
inst_4 : DenselyOrdered α
a : α
s : Set α
⊢ (∃ u ∈ Ioi a, Ioo a u ⊆ s) ↔ ∃ u ∈ Ioi a, Ioc a u ⊆ s
have mp : (∃ u ∈ Ioi a, Ioo a u ⊆ s) → ∃ u ∈ Ioi a, Ioc a u ⊆ s
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.Order.LeftRightNhds (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : NoMaxOrder α
inst_4 : DenselyOrdered α
a : α
s : Set α
mp : (∃ u ∈ Ioi a, Ioo a u ⊆ s) → ∃ u ∈ Ioi a, Ioc a u ⊆ s
⊢ (∃ u ∈ Ioi a, Ioo a u ⊆ s) ↔ ∃ u ∈ Ioi a, Ioc a u ⊆ s
have mpr : (∃ u ∈ Ioi a, Ioc a u ⊆ s) → ∃ u ∈ Ioi a, Ioo a u ⊆ s
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.Order.LeftRightNhds (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : NoMaxOrder α
inst_4 : DenselyOrdered α
a : α
s : Set α
u : α
au : u ∈ Ioi a
as : Ioo a u ⊆ s
⊢ ∃ u ∈ Ioi a, Ioc a u ⊆ s
have mp : ∀ (v : α) (hv : a < v ∧ v < u), ∃ u ∈ Ioi a, Ioc a u ⊆ s
Tactic: rcases exists_between au with ⟨v, hv⟩
-- Lean 4 proof step from Mathlib.Topology.Order.LeftRightNhds (hypothesis)
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : NoMinOrder α
inst_4 : DenselyOrdered α
a : α
s : Set α
⊢ s ∈ 𝓝[<] a ↔ ∃ l ∈ Iio a, Ico l a ⊆ s
have this : Membership.mem (γ := Filter αᵒᵈ) (𝓝[>] (toDual : (a : α) → αᵒᵈ) a : Filter αᵒᵈ) ((⇑ofDual : (a : αᵒᵈ) → α) ⁻¹' s) ↔
  ∃ (u : αᵒᵈ),
    Membership.mem (γ := Set αᵒᵈ) (Ioi ((toDual : (a : α) → αᵒᵈ) a) : Set αᵒᵈ) u ∧
      Subset (α := Set αᵒᵈ) (Ioc ((toDual : (a : α) → αᵒᵈ) a) u : Set αᵒᵈ) ((⇑ofDual : (a : αᵒᵈ) → α) ⁻¹' s : Set αᵒᵈ)
Tactic: have : ofDual ⁻¹' s ∈ 𝓝[>] toDual a ↔ _ := mem_nhdsGT_iff_exists_Ioc_subset
-- Lean 4 proof step from Mathlib.Topology.Order.LeftRightNhds (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
a : α
⊢ 𝓝[<] a = ⊥ ↔ IsBot a ∨ ∃ (b : α), b ⋖ a
have h : α = αᵒᵈ → ∀ (x : α), x ⋖ a ↔ (toDual : (a : α) → αᵒᵈ) a ⋖ x
Tactic: convert! (config := { preTransparency := .default })
    nhdsGT_eq_bot_iff (a := OrderDual.toDual a) using 4
-- Lean 4 proof step from Mathlib.Topology.Order.LeftRightNhds (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
a b : α
hab : a < b
s : Set α
⊢ s ∈ 𝓝[≥] a ↔ s ∈ 𝓝[Icc a b] a
have rw : s ∈ 𝓝[≥] a ↔ s ∈ 𝓝[≥] a
Tactic: rw [nhdsWithin_Icc_eq_nhdsGE hab]
-- Lean 4 proof step from Mathlib.Topology.Order.LeftRightNhds (hypothesis)
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
a b : α
hab : a < b
s : Set α
⊢ [s ∈ 𝓝[≥] a, s ∈ 𝓝[Icc a b] a, s ∈ 𝓝[Ico a b] a, ∃ u ∈ Ioc a b, Ico a u ⊆ s, ∃ u ∈ Ioi a, Ico a u ⊆ s].TFAE
have tfae_1_iff_2 : s ∈ 𝓝[≥] a ↔ s ∈ 𝓝[Icc a b] a
Tactic: tfae_have 1 ↔ 2 := by
    rw [nhdsWithin_Icc_eq_nhdsGE hab]
-- Lean 4 proof step from Mathlib.Topology.Order.LeftRightNhds (goal)
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 ∈ 𝓝[Icc a b] a
⊢ s ∈ 𝓝[≥] a ↔ s ∈ 𝓝[Ico a b] a
have rw : s ∈ 𝓝[≥] a ↔ s ∈ 𝓝[≥] a
Tactic: rw [nhdsWithin_Ico_eq_nhdsGE hab]
-- Lean 4 proof step from Mathlib.Topology.Order.LeftRightNhds (hypothesis)
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 ∈ 𝓝[Icc a b] a
⊢ [s ∈ 𝓝[≥] a, s ∈ 𝓝[Icc a b] a, s ∈ 𝓝[Ico a b] a, ∃ u ∈ Ioc a b, Ico a u ⊆ s, ∃ u ∈ Ioi a, Ico a u ⊆ s].TFAE
have tfae_1_iff_3 : s ∈ 𝓝[≥] a ↔ s ∈ 𝓝[Ico a b] a
Tactic: tfae_have 1 ↔ 3 := by
    rw [nhdsWithin_Ico_eq_nhdsGE hab]
-- Lean 4 proof step from Mathlib.Topology.Order.LeftRightNhds (hypothesis)
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 ∈ 𝓝[Icc a b] a
tfae_1_iff_3 : s ∈ 𝓝[≥] a ↔ s ∈ 𝓝[Ico a b] a
⊢ [s ∈ 𝓝[≥] a, s ∈ 𝓝[Icc a b] a, s ∈ 𝓝[Ico a b] a, ∃ u ∈ Ioc a b, Ico a u ⊆ s, ∃ u ∈ Ioi a, Ico a u ⊆ s].TFAE
have tfae_1_iff_5 : s ∈ 𝓝[≥] a ↔ ∃ u ∈ Ioi a, Ico a u ⊆ s
Tactic: tfae_have 1 ↔ 5 := (nhdsGE_basis_of_exists_gt ⟨b, hab⟩).mem_iff
-- Lean 4 proof step from Mathlib.Topology.Order.LeftRightNhds (hypothesis)
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 ∈ 𝓝[Icc a b] a
tfae_1_iff_3 : s ∈ 𝓝[≥] a ↔ s ∈ 𝓝[Ico a b] a
tfae_1_iff_5 : s ∈ 𝓝[≥] a ↔ ∃ u ∈ Ioi a, Ico a u ⊆ s
⊢ [s ∈ 𝓝[≥] a, s ∈ 𝓝[Icc a b] a, s ∈ 𝓝[Ico a b] a, ∃ u ∈ Ioc a b, Ico a u ⊆ s, ∃ u ∈ Ioi a, Ico a u ⊆ s].TFAE
have tfae_4_to_5 : ∀ (a_1 : ∃ u ∈ Ioc a b, Ico a u ⊆ s), ∃ u ∈ Ioi a, Ico a u ⊆ s
Tactic: tfae_have 4 → 5 := fun ⟨u, umem, hu⟩ => ⟨u, umem.1, hu⟩
-- Lean 4 proof step from Mathlib.Topology.Order.LeftRightNhds (hypothesis)
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 ∈ 𝓝[Icc a b] a
tfae_1_iff_3 : s ∈ 𝓝[≥] a ↔ s ∈ 𝓝[Ico a b] a
tfae_1_iff_5 : s ∈ 𝓝[≥] a ↔ ∃ u ∈ Ioi a, Ico a u ⊆ s
tfae_4_to_5 : ∀ (a_1 : ∃ u ∈ Ioc a b, Ico a u ⊆ s), ∃ u ∈ Ioi a, Ico a u ⊆ s
⊢ [s ∈ 𝓝[≥] a, s ∈ 𝓝[Icc a b] a, s ∈ 𝓝[Ico a b] a, ∃ u ∈ Ioc a b, Ico a u ⊆ s, ∃ u ∈ Ioi a, Ico a u ⊆ s].TFAE
have tfae_5_to_4 : ∀ (a_1 : ∃ u ∈ Ioi a, Ico a u ⊆ s), ∃ u ∈ Ioc a b, Ico a u ⊆ s
Tactic: tfae_have 5 → 4
  | ⟨u, hua, hus⟩ => ⟨min u b, ⟨lt_min hua hab, min_le_right _ _⟩,
      (Ico_subset_Ico_right <| min_le_left _ _).trans hus⟩
-- Lean 4 proof step from Mathlib.Topology.Order.LeftRightNhds (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : CommGroup α
inst_2 : LinearOrder α
inst_3 : IsOrderedMonoid α
inst_4 : OrderTopology α
a : α
⊢ 𝓝 a = ⨅ (r : α), ⨅ (_ : r > 1), 𝓟 {b : α | |a / b|ₘ < r}
have simp : Eq.{u_1 + 1} (α := Filter α) ((⨅ b ∈ Iio a, 𝓟 (Ioi b)) ⊓ ⨅ b ∈ Ioi a, 𝓟 (Iio b))
  ((⨅ (x : α), ⨅ (_ : x > 1), 𝓟 {a_1 : α | x⁻¹ < a / a_1}) ⊓ ⨅ (x : α), ⨅ (_ : x > 1), 𝓟 {a_1 : α | a / a_1 < x})
Tactic: simp only [nhds_eq_order, mabs_lt, setOf_and, ← inf_principal, iInf_inf_eq]
-- Lean 4 proof step from Mathlib.Topology.Order.LeftRightNhds (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : CommGroup α
inst_2 : LinearOrder α
inst_3 : IsOrderedMonoid α
inst_4 : OrderTopology α
a : α
⊢ Eq.{u_1 + 1} (α := Filter α) ((⨅ b ∈ Iio a, 𝓟 (Ioi b)) ⊓ ⨅ b ∈ Ioi a, 𝓟 (Iio b))
    ((⨅ (x : α), ⨅ (_ : x > 1), 𝓟 {a_1 : α | x⁻¹ < a / a_1}) ⊓ ⨅ (x : α), ⨅ (_ : x > 1), 𝓟 {a_1 : α | a / a_1 < x})
have refine_1 : Eq.{u_1 + 1} (α := Filter α) (⨅ b ∈ Iio a, 𝓟 (Ioi b)) (⨅ (x : α), ⨅ (_ : x > 1), 𝓟 {a_1 : α | a / a_1 < x})
Tactic: refine (congr_arg₂ _ ?_ ?_).trans (inf_comm ..)
-- Lean 4 proof step from Mathlib.Topology.Order.LeftRightNhds (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : CommGroup α
inst_2 : LinearOrder α
inst_3 : IsOrderedMonoid α
inst_4 : OrderTopology α
a : α
refine_1 : Eq.{u_1 + 1} (α := Filter α) (⨅ b ∈ Iio a, 𝓟 (Ioi b)) (⨅ (x : α), ⨅ (_ : x > 1), 𝓟 {a_1 : α | a / a_1 < x})
⊢ Eq.{u_1 + 1} (α := Filter α) ((⨅ b ∈ Iio a, 𝓟 (Ioi b)) ⊓ ⨅ b ∈ Ioi a, 𝓟 (Iio b))
    ((⨅ (x : α), ⨅ (_ : x > 1), 𝓟 {a_1 : α | x⁻¹ < a / a_1}) ⊓ ⨅ (x : α), ⨅ (_ : x > 1), 𝓟 {a_1 : α | a / a_1 < x})
have refine_2 : Eq.{u_1 + 1} (α := Filter α) (⨅ b ∈ Ioi a, 𝓟 (Iio b)) (⨅ (x : α), ⨅ (_ : x > 1), 𝓟 {a_1 : α | x⁻¹ < a / a_1})
Tactic: refine (congr_arg₂ _ ?_ ?_).trans (inf_comm ..)
-- Lean 4 proof step from Mathlib.Topology.Order.LeftRightNhds (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : CommGroup α
inst_2 : LinearOrder α
inst_3 : IsOrderedMonoid α
inst_4 : OrderTopology α
a : α
⊢ Eq.{u_1 + 1} (α := Filter α) (⨅ b ∈ Iio a, 𝓟 (Ioi b)) (⨅ (x : α), ⨅ (_ : x > 1), 𝓟 {a_1 : α | a / a_1 < x})
have refine_1 : ∀ (x : α),
  Eq.{u_1 + 1} (α := Filter α)
    (⨅ (_ : GT.gt (α := α) ((Equiv.divLeft a : (a : α) → α) x : α) (1 : α)),
      𝓟 {a_1 : α | a / a_1 < (Equiv.divLeft a : (a : α) → α) x})
    (⨅ (_ : x ∈ Iio a), 𝓟 (Ioi x))
Tactic: refine (Equiv.divLeft a).iInf_congr fun x => ?_
-- Lean 4 proof step from Mathlib.Topology.Order.LeftRightNhds (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : CommGroup α
inst_2 : LinearOrder α
inst_3 : IsOrderedMonoid α
inst_4 : OrderTopology α
a : α
⊢ Eq.{u_1 + 1} (α := Filter α) (⨅ b ∈ Ioi a, 𝓟 (Iio b)) (⨅ (x : α), ⨅ (_ : x > 1), 𝓟 {a_1 : α | x⁻¹ < a / a_1})
have refine_2 : ∀ (x : α),
  Eq.{u_1 + 1} (α := Filter α)
    (⨅ (_ : GT.gt (α := α) ((Equiv.divRight a : (a : α) → α) x : α) (1 : α)),
      𝓟 {a_1 : α | ((Equiv.divRight a : (a : α) → α) x)⁻¹ < a / a_1})
    (⨅ (_ : x ∈ Ioi a), 𝓟 (Iio x))
Tactic: refine (Equiv.divRight a).iInf_congr fun x => ?_
-- Lean 4 proof step from Mathlib.Topology.Order.LeftRightNhds (goal)
Goal:
α : Type u_4
inst : TopologicalSpace α
inst_1 : CommGroup α
inst_2 : LinearOrder α
inst_3 : IsOrderedMonoid α
h_nhds : ∀ (a : α), 𝓝 a = ⨅ (r : α), ⨅ (_ : r > 1), 𝓟 {b : α | |a / b|ₘ < r}
⊢ OrderTopology α
have refine : ∀ (a : α), 𝓝 a = 𝓝 a
Tactic: refine ⟨TopologicalSpace.ext_nhds fun a => ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Order.LeftRightNhds (goal)
Goal:
α : Type u_4
inst : TopologicalSpace α
inst_1 : CommGroup α
inst_2 : LinearOrder α
inst_3 : IsOrderedMonoid α
h_nhds : ∀ (a : α), 𝓝 a = ⨅ (r : α), ⨅ (_ : r > 1), 𝓟 {b : α | |a / b|ₘ < r}
a : α
⊢ 𝓝 a = 𝓝 a
have rw : ⨅ (r : α), ⨅ (_ : r > 1), 𝓟 {b : α | |a / b|ₘ < r} = 𝓝 a
Tactic: rw [h_nhds]
-- Lean 4 proof step from Mathlib.Topology.Order.LeftRightNhds (hypothesis)
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : CommGroup α
inst_2 : LinearOrder α
inst_3 : IsOrderedMonoid α
inst_4 : OrderTopology α
l : Filter β
f g : β → α
C : α
hf : Tendsto f l (𝓝 C)
hg : Tendsto g l atTop
⊢ Tendsto.{u_2, u_1} (β := α) (fun (x : β) ↦ f x * g x) l atTop
have a : Nontrivial α
Tactic: nontriviality α
-- Lean 4 proof step from Mathlib.Topology.Order.LeftRightNhds (goal)
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : CommGroup α
inst_2 : LinearOrder α
inst_3 : IsOrderedMonoid α
inst_4 : OrderTopology α
l : Filter β
f g : β → α
C : α
hf : Tendsto f l (𝓝 C)
hg : Tendsto g l atTop
h : Nontrivial α
⊢ Tendsto.{u_2, u_1} (β := α) (fun (x : β) ↦ f x * g x) l atTop
have obtain : ∀ (C' : α) (hC' : C' < C), Tendsto.{u_2, u_1} (β := α) (fun (x : β) ↦ f x * g x) l atTop
Tactic: obtain ⟨C', hC'⟩ : ∃ C', C' < C := exists_lt C
-- Lean 4 proof step from Mathlib.Topology.Order.LeftRightNhds (goal)
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : CommGroup α
inst_2 : LinearOrder α
inst_3 : IsOrderedMonoid α
inst_4 : OrderTopology α
l : Filter β
f g : β → α
C : α
hf : Tendsto f l (𝓝 C)
hg : Tendsto g l atTop
h : Nontrivial α
C' : α
hC' : C' < C
⊢ Tendsto.{u_2, u_1} (β := α) (fun (x : β) ↦ f x * g x) l atTop
have refine : ∀ᶠ (x : β) in l, C' ≤ f x
Tactic: refine tendsto_atTop_mul_left_of_le' _ C' ?_ hg
-- Lean 4 proof step from Mathlib.Topology.Order.LeftRightNhds (goal)
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : CommGroup α
inst_2 : LinearOrder α
inst_3 : IsOrderedMonoid α
inst_4 : OrderTopology α
l : Filter β
f g : β → α
C : α
hf : Tendsto f l atTop
hg : Tendsto g l (𝓝 C)
x : β
| f x * g x
have rw : g x * f x
Tactic: rw [mul_comm]
-- Lean 4 proof step from Mathlib.Topology.Order.LeftRightNhds (goal)
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : CommGroup α
inst_2 : LinearOrder α
inst_3 : IsOrderedMonoid α
inst_4 : OrderTopology α
l : Filter β
f g : β → α
C : α
hf : Tendsto f l atTop
hg : Tendsto g l (𝓝 C)
⊢ Tendsto.{u_2, u_1} (β := α) (fun (x : β) ↦ f x * g x) l atTop
have conv : Tendsto.{u_2, u_1} (β := α) (fun (x : β) ↦ g x * f x) l atTop
Tactic: conv in _ * _ => rw [mul_comm]
-- Lean 4 proof step from Mathlib.Topology.Order.LeftRightNhds (goal)
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : CommGroup α
inst_2 : LinearOrder α
inst_3 : IsOrderedMonoid α
inst_4 : OrderTopology α
l : Filter β
f g : β → α
C : α
hf : Tendsto f l atBot
hg : Tendsto g l (𝓝 C)
x : β
| f x * g x
have rw : g x * f x
Tactic: rw [mul_comm]
-- Lean 4 proof step from Mathlib.Topology.Order.LeftRightNhds (goal)
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : CommGroup α
inst_2 : LinearOrder α
inst_3 : IsOrderedMonoid α
inst_4 : OrderTopology α
l : Filter β
f g : β → α
C : α
hf : Tendsto f l atBot
hg : Tendsto g l (𝓝 C)
⊢ Tendsto.{u_2, u_1} (β := α) (fun (x : β) ↦ f x * g x) l atBot
have conv : Tendsto.{u_2, u_1} (β := α) (fun (x : β) ↦ g x * f x) l atBot
Tactic: conv in _ * _ => rw [mul_comm]
-- Lean 4 proof step from Mathlib.Topology.Order.LeftRightNhds (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : CommGroup α
inst_2 : LinearOrder α
inst_3 : IsOrderedMonoid α
inst_4 : OrderTopology α
inst_5 : NoMaxOrder α
a : α
⊢ (𝓝 a).HasBasis (fun (ε : α) ↦ 1 < ε) fun (ε : α) ↦ {b : α | |b / a|ₘ < ε}
have simp : HasBasis (α := α) (⨅ (r : α), ⨅ (_ : r > 1), 𝓟 {b : α | |b / a|ₘ < r}) (fun (ε : α) ↦ 1 < ε) fun (ε : α) ↦
  {b : α | |b / a|ₘ < ε}
Tactic: simp only [nhds_eq_iInf_mabs_div, mabs_div_comm (a := a)]