awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.Order.Basic (goal)
Goal:
α : Type u
β : Type v
inst : Preorder α
inst_1 : Preorder β
inst_2 : TopologicalSpace β
inst_3 : OrderTopology β
f : α → β
hf : ∀ {x y : α}, f x < f y ↔ x < y
x_1 : TopologicalSpace α := Preorder.topology α
this : OrderTopology α
x : α
⊢ 𝓝 x ≤ 𝓝 x
have simp : LE.le.{u} (α := Filter α)
  ((⨅ (i : β), ⨅ (_ : Membership.mem (γ := Set β) {x_2 : β | x_2 < f x} i), 𝓟 (f ⁻¹' {x : β | i < x})) ⊓
    ⨅ (i : β), ⨅ (_ : Membership.mem (γ := Set β) {x_2 : β | f x < x_2} i), 𝓟 (f ⁻¹' {x : β | x < i}))
  ((⨅ (b : α), ⨅ (_ : Membership.mem (γ := Set α) {x_2 : α | f x_2 < f x} b), 𝓟 {x : α | f b < f x}) ⊓
    ⨅ (b : α), ⨅ (_ : Membership.mem (γ := Set α) {x_2 : α | f x < f x_2} b), 𝓟 {x : α | f x < f b})
Tactic: simp only [nhds_eq_order, nhds_induced, comap_inf, comap_iInf, comap_principal, Ioi, Iio, ← hf]
-- Lean 4 proof step from Mathlib.Topology.Order.Basic (goal)
Goal:
α : Type u
β : Type v
inst : Preorder α
inst_1 : Preorder β
inst_2 : TopologicalSpace β
inst_3 : OrderTopology β
f : α → β
hf : ∀ {x y : α}, f x < f y ↔ x < y
x_1 : TopologicalSpace α := Preorder.topology α
this : OrderTopology α
x : α
⊢ LE.le.{u} (α := Filter α)
    ((⨅ (i : β), ⨅ (_ : Membership.mem (γ := Set β) {x_2 : β | x_2 < f x} i), 𝓟 (f ⁻¹' {x : β | i < x})) ⊓
      ⨅ (i : β), ⨅ (_ : Membership.mem (γ := Set β) {x_2 : β | f x < x_2} i), 𝓟 (f ⁻¹' {x : β | x < i}))
    ((⨅ (b : α), ⨅ (_ : Membership.mem (γ := Set α) {x_2 : α | f x_2 < f x} b), 𝓟 {x : α | f b < f x}) ⊓
      ⨅ (b : α), ⨅ (_ : Membership.mem (γ := Set α) {x_2 : α | f x < f x_2} b), 𝓟 {x : α | f x < f b})
have refine_1 : ∀ (a : α) (ha : Membership.mem (γ := Set α) {x_2 : α | f x_2 < f x} a),
  LE.le.{u} (α := Filter α)
    (⨅ (i : β), ⨅ (_ : Membership.mem (γ := Set β) {x_2 : β | x_2 < f x} i), 𝓟 (f ⁻¹' {x : β | i < x}))
    (𝓟 {x : α | f a < f x})
Tactic: refine inf_le_inf (le_iInf₂ fun a ha => ?_) (le_iInf₂ fun a ha => ?_)
-- Lean 4 proof step from Mathlib.Topology.Order.Basic (goal)
Goal:
α : Type u
β : Type v
inst : Preorder α
inst_1 : Preorder β
inst_2 : TopologicalSpace β
inst_3 : OrderTopology β
f : α → β
hf : ∀ {x y : α}, f x < f y ↔ x < y
x_1 : TopologicalSpace α := Preorder.topology α
this : OrderTopology α
x : α
refine_1 :
  ∀ (a : α) (ha : Membership.mem (γ := Set α) {x_2 : α | f x_2 < f x} a),
    LE.le.{u} (α := Filter α)
      (⨅ (i : β), ⨅ (_ : Membership.mem (γ := Set β) {x_2 : β | x_2 < f x} i), 𝓟 (f ⁻¹' {x : β | i < x}))
      (𝓟 {x : α | f a < f x})
⊢ LE.le.{u} (α := Filter α)
    ((⨅ (i : β), ⨅ (_ : Membership.mem (γ := Set β) {x_2 : β | x_2 < f x} i), 𝓟 (f ⁻¹' {x : β | i < x})) ⊓
      ⨅ (i : β), ⨅ (_ : Membership.mem (γ := Set β) {x_2 : β | f x < x_2} i), 𝓟 (f ⁻¹' {x : β | x < i}))
    ((⨅ (b : α), ⨅ (_ : Membership.mem (γ := Set α) {x_2 : α | f x_2 < f x} b), 𝓟 {x : α | f b < f x}) ⊓
      ⨅ (b : α), ⨅ (_ : Membership.mem (γ := Set α) {x_2 : α | f x < f x_2} b), 𝓟 {x : α | f x < f b})
have refine_2 : ∀ (a : α) (ha : Membership.mem (γ := Set α) {x_2 : α | f x < f x_2} a),
  LE.le.{u} (α := Filter α)
    (⨅ (i : β), ⨅ (_ : Membership.mem (γ := Set β) {x_2 : β | f x < x_2} i), 𝓟 (f ⁻¹' {x : β | x < i}))
    (𝓟 {x : α | f x < f a})
Tactic: refine inf_le_inf (le_iInf₂ fun a ha => ?_) (le_iInf₂ fun a ha => ?_)
-- Lean 4 proof step from Mathlib.Topology.Order.Basic (hypothesis)
Goal:
α : Type u
β : Type v
inst : Preorder α
inst_1 : Preorder β
inst_2 : TopologicalSpace β
inst_3 : OrderTopology β
f : α → β
hf : ∀ {x y : α}, f x < f y ↔ x < y
H₁ : ∀ {a : α} {b : β} {x : α}, b < f a → ¬b < f x → ∃ y < a, b ≤ f y
H₂ : ∀ {a : α} {b : β} {x : α}, f a < b → ¬f x < b → ∃ (y : α), a < y ∧ f y ≤ b
x : TopologicalSpace α := Preorder.topology α
⊢ induced f inst_2 = Preorder.topology α
have this : OrderTopology α
Tactic: have : OrderTopology α := ⟨rfl⟩
-- Lean 4 proof step from Mathlib.Topology.Order.Basic (goal)
Goal:
α : Type u
β : Type v
inst : Preorder α
inst_1 : Preorder β
inst_2 : TopologicalSpace β
inst_3 : OrderTopology β
f : α → β
hf : ∀ {x y : α}, f x < f y ↔ x < y
H₁ : ∀ {a : α} {b : β} {x : α}, b < f a → ¬b < f x → ∃ y < a, b ≤ f y
H₂ : ∀ {a : α} {b : β} {x : α}, f a < b → ¬f x < b → ∃ (y : α), a < y ∧ f y ≤ b
x : TopologicalSpace α := Preorder.topology α
this : OrderTopology α
⊢ induced f inst_2 = Preorder.topology α
have refine : Preorder.topology α ≤ induced f inst_2
Tactic: refine le_antisymm (induced_topology_le_preorder hf) ?_
-- Lean 4 proof step from Mathlib.Topology.Order.Basic (goal)
Goal:
α : Type u
β : Type v
inst : Preorder α
inst_1 : Preorder β
inst_2 : TopologicalSpace β
inst_3 : OrderTopology β
f : α → β
hf : ∀ {x y : α}, f x < f y ↔ x < y
H₁ : ∀ {a : α} {b : β} {x : α}, b < f a → ¬b < f x → ∃ y < a, b ≤ f y
H₂ : ∀ {a : α} {b : β} {x : α}, f a < b → ¬f x < b → ∃ (y : α), a < y ∧ f y ≤ b
x : TopologicalSpace α := Preorder.topology α
this : OrderTopology α
⊢ Preorder.topology α ≤ induced f inst_2
have refine : ∀ (a : α), 𝓝 a ≤ 𝓝 a
Tactic: refine le_of_nhds_le_nhds fun a => ?_
-- Lean 4 proof step from Mathlib.Topology.Order.Basic (goal)
Goal:
α : Type u
β : Type v
inst : Preorder α
inst_1 : Preorder β
inst_2 : TopologicalSpace β
inst_3 : OrderTopology β
f : α → β
hf : ∀ {x y : α}, f x < f y ↔ x < y
H₁ : ∀ {a : α} {b : β} {x : α}, b < f a → ¬b < f x → ∃ y < a, b ≤ f y
H₂ : ∀ {a : α} {b : β} {x : α}, f a < b → ¬f x < b → ∃ (y : α), a < y ∧ f y ≤ b
x : TopologicalSpace α := Preorder.topology α
this : OrderTopology α
a : α
⊢ 𝓝 a ≤ 𝓝 a
have simp : LE.le.{u} (α := Filter α) ((⨅ b ∈ Iio a, 𝓟 (Ioi b)) ⊓ ⨅ b ∈ Ioi a, 𝓟 (Iio b))
  ((⨅ i ∈ Iio (f a), 𝓟 (f ⁻¹' Ioi i)) ⊓ ⨅ i ∈ Ioi (f a), 𝓟 (f ⁻¹' Iio i))
Tactic: simp only [nhds_eq_order, nhds_induced, comap_inf, comap_iInf, comap_principal]
-- Lean 4 proof step from Mathlib.Topology.Order.Basic (goal)
Goal:
α : Type u
β : Type v
inst : Preorder α
inst_1 : Preorder β
inst_2 : TopologicalSpace β
inst_3 : OrderTopology β
f : α → β
hf : ∀ {x y : α}, f x < f y ↔ x < y
H₁ : ∀ {a : α} {b : β} {x : α}, b < f a → ¬b < f x → ∃ y < a, b ≤ f y
H₂ : ∀ {a : α} {b : β} {x : α}, f a < b → ¬f x < b → ∃ (y : α), a < y ∧ f y ≤ b
x : TopologicalSpace α := Preorder.topology α
this : OrderTopology α
a : α
⊢ LE.le.{u} (α := Filter α) ((⨅ b ∈ Iio a, 𝓟 (Ioi b)) ⊓ ⨅ b ∈ Ioi a, 𝓟 (Iio b))
    ((⨅ i ∈ Iio (f a), 𝓟 (f ⁻¹' Ioi i)) ⊓ ⨅ i ∈ Ioi (f a), 𝓟 (f ⁻¹' Iio i))
have refine_1 : ∀ (b : β) (hb : b ∈ Iio (f a)), ⨅ b ∈ Iio a, 𝓟 (Ioi b) ≤ 𝓟 (f ⁻¹' Ioi b)
Tactic: refine inf_le_inf (le_iInf₂ fun b hb => ?_) (le_iInf₂ fun b hb => ?_)
-- Lean 4 proof step from Mathlib.Topology.Order.Basic (goal)
Goal:
α : Type u
β : Type v
inst : Preorder α
inst_1 : Preorder β
inst_2 : TopologicalSpace β
inst_3 : OrderTopology β
f : α → β
hf : ∀ {x y : α}, f x < f y ↔ x < y
H₁ : ∀ {a : α} {b : β} {x : α}, b < f a → ¬b < f x → ∃ y < a, b ≤ f y
H₂ : ∀ {a : α} {b : β} {x : α}, f a < b → ¬f x < b → ∃ (y : α), a < y ∧ f y ≤ b
x : TopologicalSpace α := Preorder.topology α
this : OrderTopology α
a : α
refine_1 : ∀ (b : β) (hb : b ∈ Iio (f a)), ⨅ b ∈ Iio a, 𝓟 (Ioi b) ≤ 𝓟 (f ⁻¹' Ioi b)
⊢ LE.le.{u} (α := Filter α) ((⨅ b ∈ Iio a, 𝓟 (Ioi b)) ⊓ ⨅ b ∈ Ioi a, 𝓟 (Iio b))
    ((⨅ i ∈ Iio (f a), 𝓟 (f ⁻¹' Ioi i)) ⊓ ⨅ i ∈ Ioi (f a), 𝓟 (f ⁻¹' Iio i))
have refine_2 : ∀ (b : β) (hb : b ∈ Ioi (f a)), ⨅ b ∈ Ioi a, 𝓟 (Iio b) ≤ 𝓟 (f ⁻¹' Iio b)
Tactic: refine inf_le_inf (le_iInf₂ fun b hb => ?_) (le_iInf₂ fun b hb => ?_)
-- Lean 4 proof step from Mathlib.Topology.Order.Basic (goal)
Goal:
α : Type u
β : Type v
inst : Preorder α
inst_1 : Preorder β
inst_2 : TopologicalSpace β
inst_3 : OrderTopology β
f : α → β
hf : ∀ {x y : α}, f x < f y ↔ x < y
H₁ : ∀ {a : α} {b : β} {x : α}, b < f a → ¬b < f x → ∃ y < a, b ≤ f y
H₂ : ∀ {a : α} {b : β} {x : α}, f a < b → ¬f x < b → ∃ (y : α), a < y ∧ f y ≤ b
x : TopologicalSpace α := Preorder.topology α
this : OrderTopology α
a : α
b : β
hb : b ∈ Iio (f a)
⊢ ⨅ b ∈ Iio a, 𝓟 (Ioi b) ≤ 𝓟 (f ⁻¹' Ioi b)
have pos : ∀ (h : ∃ (x : α), ¬b < f x), ⨅ b ∈ Iio a, 𝓟 (Ioi b) ≤ 𝓟 (f ⁻¹' Ioi b)
Tactic: by_cases! h : ∃ x, ¬(b < f x)
-- Lean 4 proof step from Mathlib.Topology.Order.Basic (goal)
Goal:
α : Type u
β : Type v
inst : Preorder α
inst_1 : Preorder β
inst_2 : TopologicalSpace β
inst_3 : OrderTopology β
f : α → β
hf : ∀ {x y : α}, f x < f y ↔ x < y
H₁ : ∀ {a : α} {b : β} {x : α}, b < f a → ¬b < f x → ∃ y < a, b ≤ f y
H₂ : ∀ {a : α} {b : β} {x : α}, f a < b → ¬f x < b → ∃ (y : α), a < y ∧ f y ≤ b
x : TopologicalSpace α := Preorder.topology α
this : OrderTopology α
a : α
b : β
hb : b ∈ Iio (f a)
pos : ∀ (h : ∃ (x : α), ¬b < f x), ⨅ b ∈ Iio a, 𝓟 (Ioi b) ≤ 𝓟 (f ⁻¹' Ioi b)
⊢ ⨅ b ∈ Iio a, 𝓟 (Ioi b) ≤ 𝓟 (f ⁻¹' Ioi b)
have neg : ∀ (h : ∀ (x : α), b < f x), ⨅ b ∈ Iio a, 𝓟 (Ioi b) ≤ 𝓟 (f ⁻¹' Ioi b)
Tactic: by_cases! h : ∃ x, ¬(b < f x)
-- Lean 4 proof step from Mathlib.Topology.Order.Basic (goal)
Goal:
α : Type u
β : Type v
inst : Preorder α
inst_1 : Preorder β
inst_2 : TopologicalSpace β
inst_3 : OrderTopology β
f : α → β
hf : ∀ {x y : α}, f x < f y ↔ x < y
H₁ : ∀ {a : α} {b : β} {x : α}, b < f a → ¬b < f x → ∃ y < a, b ≤ f y
H₂ : ∀ {a : α} {b : β} {x : α}, f a < b → ¬f x < b → ∃ (y : α), a < y ∧ f y ≤ b
x : TopologicalSpace α := Preorder.topology α
this : OrderTopology α
a : α
b : β
hb : b ∈ Iio (f a)
h : ∃ (x : α), ¬b < f x
⊢ ⨅ b ∈ Iio a, 𝓟 (Ioi b) ≤ 𝓟 (f ⁻¹' Ioi b)
have pos : ∀ (x : α) (hx : ¬b < f x), ⨅ b ∈ Iio a, 𝓟 (Ioi b) ≤ 𝓟 (f ⁻¹' Ioi b)
Tactic: rcases h with ⟨x, hx⟩
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Topology.Order.Basic (goal)
Goal:
α : Type u
β : Type v
inst : Preorder α
inst_1 : Preorder β
inst_2 : TopologicalSpace β
inst_3 : OrderTopology β
f : α → β
hf : ∀ {x y : α}, f x < f y ↔ x < y
H₁ : ∀ {a : α} {b : β} {x : α}, b < f a → ¬b < f x → ∃ y < a, b ≤ f y
H₂ : ∀ {a : α} {b : β} {x : α}, f a < b → ¬f x < b → ∃ (y : α), a < y ∧ f y ≤ b
x_1 : TopologicalSpace α := Preorder.topology α
this : OrderTopology α
a : α
b : β
hb : b ∈ Iio (f a)
x : α
hx : ¬b < f x
⊢ ⨅ b ∈ Iio a, 𝓟 (Ioi b) ≤ 𝓟 (f ⁻¹' Ioi b)
have pos : ∀ (y : α) (hya : y < a) (hyb : b ≤ f y), ⨅ b ∈ Iio a, 𝓟 (Ioi b) ≤ 𝓟 (f ⁻¹' Ioi b)
Tactic: rcases H₁ hb hx with ⟨y, hya, hyb⟩
-- Lean 4 proof step from Mathlib.Topology.Order.Basic (goal)
Goal:
α : Type u
β : Type v
inst : Preorder α
inst_1 : Preorder β
inst_2 : TopologicalSpace β
inst_3 : OrderTopology β
f : α → β
hf : ∀ {x y : α}, f x < f y ↔ x < y
H₁ : ∀ {a : α} {b : β} {x : α}, b < f a → ¬b < f x → ∃ y < a, b ≤ f y
H₂ : ∀ {a : α} {b : β} {x : α}, f a < b → ¬f x < b → ∃ (y : α), a < y ∧ f y ≤ b
x : TopologicalSpace α := Preorder.topology α
this : OrderTopology α
a : α
b : β
hb : b ∈ Ioi (f a)
⊢ ⨅ b ∈ Ioi a, 𝓟 (Iio b) ≤ 𝓟 (f ⁻¹' Iio b)
have pos : ∀ (h : ∃ (x : α), ¬f x < b), ⨅ b ∈ Ioi a, 𝓟 (Iio b) ≤ 𝓟 (f ⁻¹' Iio b)
Tactic: by_cases! h : ∃ x, ¬(f x < b)
-- Lean 4 proof step from Mathlib.Topology.Order.Basic (goal)
Goal:
α : Type u
β : Type v
inst : Preorder α
inst_1 : Preorder β
inst_2 : TopologicalSpace β
inst_3 : OrderTopology β
f : α → β
hf : ∀ {x y : α}, f x < f y ↔ x < y
H₁ : ∀ {a : α} {b : β} {x : α}, b < f a → ¬b < f x → ∃ y < a, b ≤ f y
H₂ : ∀ {a : α} {b : β} {x : α}, f a < b → ¬f x < b → ∃ (y : α), a < y ∧ f y ≤ b
x : TopologicalSpace α := Preorder.topology α
this : OrderTopology α
a : α
b : β
hb : b ∈ Ioi (f a)
pos : ∀ (h : ∃ (x : α), ¬f x < b), ⨅ b ∈ Ioi a, 𝓟 (Iio b) ≤ 𝓟 (f ⁻¹' Iio b)
⊢ ⨅ b ∈ Ioi a, 𝓟 (Iio b) ≤ 𝓟 (f ⁻¹' Iio b)
have neg : ∀ (h : ∀ (x : α), f x < b), ⨅ b ∈ Ioi a, 𝓟 (Iio b) ≤ 𝓟 (f ⁻¹' Iio b)
Tactic: by_cases! h : ∃ x, ¬(f x < b)
-- Lean 4 proof step from Mathlib.Topology.Order.Basic (goal)
Goal:
α : Type u
β : Type v
inst : Preorder α
inst_1 : Preorder β
inst_2 : TopologicalSpace β
inst_3 : OrderTopology β
f : α → β
hf : ∀ {x y : α}, f x < f y ↔ x < y
H₁ : ∀ {a : α} {b : β} {x : α}, b < f a → ¬b < f x → ∃ y < a, b ≤ f y
H₂ : ∀ {a : α} {b : β} {x : α}, f a < b → ¬f x < b → ∃ (y : α), a < y ∧ f y ≤ b
x : TopologicalSpace α := Preorder.topology α
this : OrderTopology α
a : α
b : β
hb : b ∈ Ioi (f a)
h : ∃ (x : α), ¬f x < b
⊢ ⨅ b ∈ Ioi a, 𝓟 (Iio b) ≤ 𝓟 (f ⁻¹' Iio b)
have pos : ∀ (x : α) (hx : ¬f x < b), ⨅ b ∈ Ioi a, 𝓟 (Iio b) ≤ 𝓟 (f ⁻¹' Iio b)
Tactic: rcases h with ⟨x, hx⟩
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Topology.Order.Basic (goal)
Goal:
α : Type u
β : Type v
inst : Preorder α
inst_1 : Preorder β
inst_2 : TopologicalSpace β
inst_3 : OrderTopology β
f : α → β
hf : ∀ {x y : α}, f x < f y ↔ x < y
H₁ : ∀ {a : α} {b : β} {x : α}, b < f a → ¬b < f x → ∃ y < a, b ≤ f y
H₂ : ∀ {a : α} {b : β} {x : α}, f a < b → ¬f x < b → ∃ (y : α), a < y ∧ f y ≤ b
x_1 : TopologicalSpace α := Preorder.topology α
this : OrderTopology α
a : α
b : β
hb : b ∈ Ioi (f a)
x : α
hx : ¬f x < b
⊢ ⨅ b ∈ Ioi a, 𝓟 (Iio b) ≤ 𝓟 (f ⁻¹' Iio b)
have pos : ∀ (y : α) (hya : a < y) (hyb : f y ≤ b), ⨅ b ∈ Ioi a, 𝓟 (Iio b) ≤ 𝓟 (f ⁻¹' Iio b)
Tactic: rcases H₂ hb hx with ⟨y, hya, hyb⟩
-- Lean 4 proof step from Mathlib.Topology.Order.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : LinearOrder β
t : TopologicalSpace β
inst_2 : OrderTopology β
f : α → β
hf : StrictMono f
hc : (range f).OrdConnected
⊢ induced f t = Preorder.topology α
have refine_1 : ∀ {a : α} {b : β} {x : α} (h₁ : b < f a) (h₂ : ¬b < f x), ∃ y < a, b ≤ f y
Tactic: refine induced_topology_eq_preorder hf.lt_iff_lt (fun h₁ h₂ => ?_) fun h₁ h₂ => ?_
-- Lean 4 proof step from Mathlib.Topology.Order.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : LinearOrder β
t : TopologicalSpace β
inst_2 : OrderTopology β
f : α → β
hf : StrictMono f
hc : (range f).OrdConnected
refine_1 : ∀ {a : α} {b : β} {x : α} (h₁ : b < f a) (h₂ : ¬b < f x), ∃ y < a, b ≤ f y
⊢ induced f t = Preorder.topology α
have refine_2 : ∀ {a : α} {b : β} {x : α} (h₁ : f a < b) (h₂ : ¬f x < b), ∃ (y : α), a < y ∧ f y ≤ b
Tactic: refine induced_topology_eq_preorder hf.lt_iff_lt (fun h₁ h₂ => ?_) fun h₁ h₂ => ?_
-- Lean 4 proof step from Mathlib.Topology.Order.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : LinearOrder β
t : TopologicalSpace β
inst_2 : OrderTopology β
f : α → β
hf : StrictMono f
hc : (range f).OrdConnected
a : α
b : β
x : α
h₁ : b < f a
h₂ : ¬b < f x
⊢ ∃ y < a, b ≤ f y
have refine_1 : ∀ (y : α) (h₁ : f y < f a) (h₂ : ¬f y < f x), ∃ y_1 < a, f y ≤ f y_1
Tactic: rcases hc.out (mem_range_self _) (mem_range_self _) ⟨not_lt.1 h₂, h₁.le⟩ with ⟨y, rfl⟩
Cleared hypotheses: b, h₁, h₂
-- Lean 4 proof step from Mathlib.Topology.Order.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : LinearOrder β
t : TopologicalSpace β
inst_2 : OrderTopology β
f : α → β
hf : StrictMono f
hc : (range f).OrdConnected
a : α
b : β
x : α
h₁ : f a < b
h₂ : ¬f x < b
⊢ ∃ (y : α), a < y ∧ f y ≤ b
have refine_2 : ∀ (y : α) (h₁ : f a < f y) (h₂ : ¬f x < f y), ∃ (y_1 : α), a < y_1 ∧ f y_1 ≤ f y
Tactic: rcases hc.out (mem_range_self _) (mem_range_self _) ⟨h₁.le, not_lt.1 h₂⟩ with ⟨y, rfl⟩
Cleared hypotheses: b, h₁, h₂
-- Lean 4 proof step from Mathlib.Topology.Order.Basic (goal)
Goal:
α_1 : Type u
β : Type v
γ : Type w
α : Type u
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
t : Set α
ht : t.OrdConnected
⊢ OrdConnected.{u} (α := α) (range (ι := { x : α // x ∈ t }) (Subtype.val (p := fun (x : α) ↦ x ∈ t)))
have rwa : ∀ (ht : OrdConnected.{u} (α := α) (range (ι := { x : α // x ∈ t }) (Subtype.val (p := fun (x : α) ↦ x ∈ t)))),
  OrdConnected.{u} (α := α) (range (ι := { x : α // x ∈ t }) (Subtype.val (p := fun (x : α) ↦ x ∈ t)))
Tactic: rwa [← @Subtype.range_val _ t] at ht
Cleared hypotheses: ht
-- Lean 4 proof step from Mathlib.Topology.Order.Basic (goal)
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : Preorder α
inst_2 : OrderTopology α
a : α
⊢ 𝓝[≥] a = (⨅ (u : α), ⨅ (_ : a < u), 𝓟 (Iio u)) ⊓ 𝓟 (Ici a)
have rw : ((⨅ b ∈ Iio a, 𝓟 (Ioi b)) ⊓ ⨅ b ∈ Ioi a, 𝓟 (Iio b)) ⊓ 𝓟 (Ici a) = (⨅ (u : α), ⨅ (_ : a < u), 𝓟 (Iio u)) ⊓ 𝓟 (Ici a)
Tactic: rw [nhdsWithin, nhds_eq_order]
-- Lean 4 proof step from Mathlib.Topology.Order.Basic (goal)
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : Preorder α
inst_2 : OrderTopology α
a : α
⊢ ((⨅ b ∈ Iio a, 𝓟 (Ioi b)) ⊓ ⨅ b ∈ Ioi a, 𝓟 (Iio b)) ⊓ 𝓟 (Ici a) = (⨅ (u : α), ⨅ (_ : a < u), 𝓟 (Iio u)) ⊓ 𝓟 (Ici a)
have refine : (⨅ (u : α), ⨅ (_ : a < u), 𝓟 (Iio u)) ⊓ 𝓟 (Ici a) ≤ ⨅ b ∈ Iio a, 𝓟 (Ioi b)
Tactic: refine le_antisymm (inf_le_inf_right _ inf_le_right) (le_inf (le_inf ?_ inf_le_left) inf_le_right)
-- Lean 4 proof step from Mathlib.Topology.Order.Basic (hypothesis)
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTop α
inst_3 : OrderTopology α
inst_4 : Nontrivial α
⊢ HasBasis (α := α) (𝓝 ⊤) (fun (a : α) ↦ a < ⊤) fun (a : α) ↦ Ioi a
have this : ∃ (x : α), x < ⊤
Tactic: have : ∃ x : α, x < ⊤ := (exists_ne ⊤).imp fun x hx => hx.lt_top
-- Lean 4 proof step from Mathlib.Topology.Order.Basic (goal)
Goal:
α : Type u
β : Type v
inst : TopologicalSpace β
inst_1 : Preorder β
inst_2 : OrderTop β
inst_3 : OrderTopology β
l : Filter α
f g : α → β
hf : Tendsto f l (𝓝 ⊤)
hg : f ≤ᶠ[l] g
⊢ Tendsto g l (𝓝 ⊤)
have simp : ∀ (hf : ∀ (i : β) (i_1 : i < ⊤), ∀ᶠ (a : α) in l, f a ∈ Ioi i) (i : β) (i_1 : i < ⊤), ∀ᶠ (a : α) in l, g a ∈ Ioi i
Tactic: simp only [nhds_top_order, tendsto_iInf, tendsto_principal] at hf ⊢
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.Topology.Order.Basic (goal)
Goal:
α : Type u
β : Type v
inst : TopologicalSpace β
inst_1 : Preorder β
inst_2 : OrderTop β
inst_3 : OrderTopology β
l : Filter α
f g : α → β
hg : f ≤ᶠ[l] g
hf : ∀ (i : β) (i_1 : i < ⊤), ∀ᶠ (a : α) in l, f a ∈ Ioi i
x : β
hx : x < ⊤
⊢ ∀ᶠ (a : α) in l, g a ∈ Ioi x
have h : ∀ (a : α),
  Membership.mem (γ := Set α)
    {x_1 : α |
      Membership.mem (γ := Set α) {x_2 : α | (fun (a : α) ↦ f a ∈ Ioi x) x_2} x_1 →
        Membership.mem (γ := Set α)
          {x_2 : α |
            Membership.mem (γ := Set α) {x : α | (fun (x : α) ↦ f x ≤ g x) x} x_2 →
              Membership.mem (γ := Set α) {x_3 : α | (fun (a : α) ↦ g a ∈ Ioi x) x_3} x_2}
          x_1}
    a
Tactic: filter_upwards [hf x hx, hg] with _ using lt_of_lt_of_le
-- Lean 4 proof step from Mathlib.Topology.Order.Basic (goal)
Goal:
α : Type u
β : Type v
inst : TopologicalSpace β
inst_1 : Preorder β
inst_2 : OrderTop β
inst_3 : OrderTopology β
l : Filter α
f g : α → β
hg : f ≤ᶠ[l] g
hf : ∀ (i : β) (i_1 : i < ⊤), ∀ᶠ (a : α) in l, f a ∈ Ioi i
x : β
hx : x < ⊤
h :
  ∀ (a : α),
    Membership.mem (γ := Set α)
      {x_1 : α |
        Membership.mem (γ := Set α) {x_2 : α | (fun (a : α) ↦ f a ∈ Ioi x) x_2} x_1 →
          Membership.mem (γ := Set α)
            {x_2 : α |
              Membership.mem (γ := Set α) {x : α | (fun (x : α) ↦ f x ≤ g x) x} x_2 →
                Membership.mem (γ := Set α) {x_3 : α | (fun (a : α) ↦ g a ∈ Ioi x) x_3} x_2}
            x_1}
      a
⊢ ∀ᶠ (a : α) in l, g a ∈ Ioi x
have h₁ : ∀ (a : α), f a ∈ Ioi x → f a ≤ g a → g a ∈ Ioi x
Tactic: filter_upwards [hf x hx, hg] with _ using lt_of_lt_of_le
-- Lean 4 proof step from Mathlib.Topology.Order.Basic (goal)
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
a : α
s : Set α
hs : s ∈ 𝓝[≥] a
⊢ ∃ (b : α), a ≤ b ∧ Icc a b ∈ 𝓝[≥] a ∧ Icc a b ⊆ s
have inl : ∀ (ha : IsMax a), ∃ (b : α), a ≤ b ∧ Icc a b ∈ 𝓝[≥] a ∧ Icc a b ⊆ s
Tactic: rcases (em (IsMax a)).imp_right not_isMax_iff.mp with (ha | ha)
-- Lean 4 proof step from Mathlib.Topology.Order.Basic (goal)
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
a : α
s : Set α
hs : s ∈ 𝓝[≥] a
inl : ∀ (ha : IsMax a), ∃ (b : α), a ≤ b ∧ Icc a b ∈ 𝓝[≥] a ∧ Icc a b ⊆ s
⊢ ∃ (b : α), a ≤ b ∧ Icc a b ∈ 𝓝[≥] a ∧ Icc a b ⊆ s
have inr : ∀ (ha : ∃ (b : α), a < b), ∃ (b : α), a ≤ b ∧ Icc a b ∈ 𝓝[≥] a ∧ Icc a b ⊆ s
Tactic: rcases (em (IsMax a)).imp_right not_isMax_iff.mp with (ha | ha)
-- Lean 4 proof step from Mathlib.Topology.Order.Basic (goal)
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
a : α
s : Set α
hs : s ∈ 𝓝[≥] a
ha : IsMax a
⊢ ∃ (b : α), a ≤ b ∧ Icc a b ∈ 𝓝[≥] a ∧ Icc a b ⊆ s
have h : a ≤ a ∧ Icc a a ∈ 𝓝[≥] a ∧ Icc a a ⊆ s
Tactic: use a
-- Lean 4 proof step from Mathlib.Topology.Order.Basic (goal)
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
a : α
s : Set α
hs : s ∈ 𝓝[≥] a
ha : ∃ (b : α), a < b
⊢ ∃ (b : α), a ≤ b ∧ Icc a b ∈ 𝓝[≥] a ∧ Icc a b ⊆ s
have inr : ∀ (b : α) (hab : a < b) (hbs : Ico a b ⊆ s), ∃ (b : α), a ≤ b ∧ Icc a b ∈ 𝓝[≥] a ∧ Icc a b ⊆ s
Tactic: rcases (nhdsGE_basis_of_exists_gt ha).mem_iff.mp hs with ⟨b, hab, hbs⟩
-- Lean 4 proof step from Mathlib.Topology.Order.Basic (goal)
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
a : α
s : Set α
hs : s ∈ 𝓝[≥] a
ha : ∃ (b : α), a < b
b : α
hab : a < b
hbs : Ico a b ⊆ s
⊢ ∃ (b : α), a ≤ b ∧ Icc a b ∈ 𝓝[≥] a ∧ Icc a b ⊆ s
have inr : ∀ (H : Ioo a b = ∅), ∃ (b : α), a ≤ b ∧ Icc a b ∈ 𝓝[≥] a ∧ Icc a b ⊆ s
Tactic: rcases eq_empty_or_nonempty (Ioo a b) with (H | ⟨c, hc⟩)
-- Lean 4 proof step from Mathlib.Topology.Order.Basic (goal)
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
a : α
s : Set α
hs : s ∈ 𝓝[≥] a
ha : ∃ (b : α), a < b
b : α
hab : a < b
hbs : Ico a b ⊆ s
inr : ∀ (H : Ioo a b = ∅), ∃ (b : α), a ≤ b ∧ Icc a b ∈ 𝓝[≥] a ∧ Icc a b ⊆ s
⊢ ∃ (b : α), a ≤ b ∧ Icc a b ∈ 𝓝[≥] a ∧ Icc a b ⊆ s
have inr₁ : ∀ (c : α) (hc : c ∈ Ioo a b), ∃ (b : α), a ≤ b ∧ Icc a b ∈ 𝓝[≥] a ∧ Icc a b ⊆ s
Tactic: rcases eq_empty_or_nonempty (Ioo a b) with (H | ⟨c, hc⟩)
-- Lean 4 proof step from Mathlib.Topology.Order.Basic (goal)
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
a : α
s : Set α
hs : s ∈ 𝓝[≥] a
ha : ∃ (b : α), a < b
b : α
hab : a < b
hbs : Ico a b ⊆ s
H : Ioo a b = ∅
⊢ Ico a b = Icc a a
have rw : Icc a a ∪ Ioo a b = Icc a a
Tactic: rw [← Icc_union_Ioo_eq_Ico le_rfl hab, H, union_empty]
-- Lean 4 proof step from Mathlib.Topology.Order.Basic (goal)
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
a : α
s : Set α
hs : s ∈ 𝓝[≥] a
ha : ∃ (b : α), a < b
b : α
hab : a < b
hbs : Ico a b ⊆ s
H : Ioo a b = ∅
rw : Icc a a ∪ Ioo a b = Icc a a
⊢ Ico a b = Icc a a
have rw₁ : Icc a a ∪ ∅ = Icc a a
Tactic: rw [← Icc_union_Ioo_eq_Ico le_rfl hab, H, union_empty]
-- Lean 4 proof step from Mathlib.Topology.Order.Basic (goal)
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
a : α
s : Set α
hs : s ∈ 𝓝[≥] a
ha : ∃ (b : α), a < b
b : α
hab : a < b
hbs : Ico a b ⊆ s
H : Ioo a b = ∅
rw : Icc a a ∪ Ioo a b = Icc a a
rw₁ : Icc a a ∪ ∅ = Icc a a
⊢ Ico a b = Icc a a
have rw₂ : Icc a a = Icc a a
Tactic: rw [← Icc_union_Ioo_eq_Ico le_rfl hab, H, union_empty]
-- Lean 4 proof step from Mathlib.Topology.Order.Basic (hypothesis)
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
a : α
s : Set α
hs : s ∈ 𝓝[≥] a
ha : ∃ (b : α), a < b
b : α
hab : a < b
hbs : Ico a b ⊆ s
H : Ioo a b = ∅
⊢ ∃ (b : α), a ≤ b ∧ Icc a b ∈ 𝓝[≥] a ∧ Icc a b ⊆ s
have this : Ico a b = Icc a a
Tactic: have : Ico a b = Icc a a := by rw [← Icc_union_Ioo_eq_Ico le_rfl hab, H, union_empty]
-- Lean 4 proof step from Mathlib.Topology.Order.Basic (goal)
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
a : α
s : Set α
hs : s ∈ 𝓝 a
⊢ ∃ (b : α) (c : α), a ∈ Icc b c ∧ Icc b c ∈ 𝓝 a ∧ Icc b c ⊆ s
have rcases : ∀ (b : α) (hba : b ≤ a) (hb_nhds : Icc b a ∈ 𝓝[≤] a) (hbs : Icc b a ⊆ s),
  ∃ (b : α) (c : α), a ∈ Icc b c ∧ Icc b c ∈ 𝓝 a ∧ Icc b c ⊆ s
Tactic: rcases exists_Icc_mem_subset_of_mem_nhdsLE (nhdsWithin_le_nhds hs) with
    ⟨b, hba, hb_nhds, hbs⟩
-- Lean 4 proof step from Mathlib.Topology.Order.Basic (goal)
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
a : α
s : Set α
hs : s ∈ 𝓝 a
b : α
hba : b ≤ a
hb_nhds : Icc b a ∈ 𝓝[≤] a
hbs : Icc b a ⊆ s
⊢ ∃ (b : α) (c : α), a ∈ Icc b c ∧ Icc b c ∈ 𝓝 a ∧ Icc b c ⊆ s
have rcases : ∀ (c : α) (hac : a ≤ c) (hc_nhds : Icc a c ∈ 𝓝[≥] a) (hcs : Icc a c ⊆ s),
  ∃ (b : α) (c : α), a ∈ Icc b c ∧ Icc b c ∈ 𝓝 a ∧ Icc b c ⊆ s
Tactic: rcases exists_Icc_mem_subset_of_mem_nhdsGE (nhdsWithin_le_nhds hs) with
    ⟨c, hac, hc_nhds, hcs⟩