awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Order.Basic
Goal:
α_1 : Type u
β : Type v
γ : Type w
ι : Type u_1
α : ι → Type u_2
inst : (i : ι) → Preorder (α i)
inst_1 : (i : ι) → TopologicalSpace (α i)
inst_2 : ∀ (i : ι), OrderTopology.{u_2} (α i)
f : (i : ι) → α i
i : ι
this : Tendsto (fun (g : (i : ι) → α i) ↦ g i) (𝓝 f) (𝓝 (f i))
⊢ Tendsto (image (eval (β := α) i) ∘ fun (p : ((i : ι) → α i) × ((i : ι) → α i)) ↦ Icc p.1 p.2) (𝓝 f ×ˢ 𝓝 f)
    (𝓝 (f i)).smallSets

Tactic:
(this.comp tendsto_fst).Icc (this.comp tendsto_snd) |>.smallSets_mono ?_

Premises used: Filter.Tendsto.Icc, Filter.Tendsto.smallSets_mono, Filter.Tendsto.comp, Filter.tendsto_snd, Filter.tendsto_fst
-- Module: Mathlib.Topology.Order.Basic
Goal:
α_1 : Type u
β : Type v
γ : Type w
ι : Type u_1
α : ι → Type u_2
inst : (i : ι) → Preorder (α i)
inst_1 : (i : ι) → TopologicalSpace (α i)
inst_2 : ∀ (i : ι), OrderTopology.{u_2} (α i)
f : (i : ι) → α i
i : ι
this : Tendsto (fun (g : (i : ι) → α i) ↦ g i) (𝓝 f) (𝓝 (f i))
tendsto_Ixx :
  ∀ᶠ (x : ((i : ι) → α i) × ((i : ι) → α i)) in 𝓝 f ×ˢ 𝓝 f,
    Subset.{u_2} (α := Set (α i))
      ((image (eval (β := α) i) ∘ fun (p : ((i : ι) → α i) × ((i : ι) → α i)) ↦ Icc p.1 p.2) x)
      (Icc (((fun (g : (i : ι) → α i) ↦ g i) ∘ Prod.fst) x) (((fun (g : (i : ι) → α i) ↦ g i) ∘ Prod.snd) x))
⊢ Tendsto (image (eval (β := α) i) ∘ fun (p : ((i : ι) → α i) × ((i : ι) → α i)) ↦ Icc p.1 p.2) (𝓝 f ×ˢ 𝓝 f)
    (𝓝 (f i)).smallSets

Tactic:
refine (this.comp tendsto_fst).Icc (this.comp tendsto_snd) |>.smallSets_mono ?_

Premises used: Filter.Tendsto.Icc, Filter.Tendsto.smallSets_mono, Filter.Tendsto.comp, Filter.tendsto_snd, Filter.tendsto_fst
-- Module: Mathlib.Topology.Order.Basic
Goal:
α_1 : Type u
β : Type v
γ : Type w
ι : Type u_1
α : ι → Type u_2
inst : (i : ι) → Preorder (α i)
inst_1 : (i : ι) → TopologicalSpace (α i)
inst_2 : ∀ (i : ι), OrderTopology.{u_2} (α i)
f : (i : ι) → α i
i : ι
this : Tendsto (fun (g : (i : ι) → α i) ↦ g i) (𝓝 f) (𝓝 (f i))
⊢ ∀ (a : ((i : ι) → α i) × ((i : ι) → α i)),
    Subset.{u_2} (α := Set (α i))
      ((image (eval (β := α) i) ∘ fun (p : ((i : ι) → α i) × ((i : ι) → α i)) ↦ Icc p.1 p.2) a)
      (Icc (((fun (g : (i : ι) → α i) ↦ g i) ∘ Prod.fst) a) (((fun (g : (i : ι) → α i) ↦ g i) ∘ Prod.snd) a))

Tactic:
fun ⟨f, g⟩ ↦ image_subset_iff.mpr fun p hp ↦ ⟨hp.1 i, hp.2 i⟩

Premises used: Iff.mpr, _private.0.tendstoIccClassNhdsPi.match_1, Function.comp, HasSubset.Subset, Function.eval, Prod.fst, Set.Icc, And.right, And.left, And.intro, Set.image, Set.image_subset_iff, Prod.snd
-- Module: Mathlib.Topology.Order.Basic
Goal:
α_1 : Type u
β : Type v
γ : Type w
ι : Type u_1
α : ι → Type u_2
inst : (i : ι) → Preorder (α i)
inst_1 : (i : ι) → TopologicalSpace (α i)
inst_2 : ∀ (i : ι), OrderTopology.{u_2} (α i)
f : (i : ι) → α i
i : ι
this : Tendsto (fun (g : (i : ι) → α i) ↦ g i) (𝓝 f) (𝓝 (f i))
tendsto_Ixx :
  ∀ (a : ((i : ι) → α i) × ((i : ι) → α i)),
    Membership.mem (γ := Set (((i : ι) → α i) × ((i : ι) → α i)))
      {x : ((i : ι) → α i) × ((i : ι) → α i) |
        (fun (x : ((i : ι) → α i) × ((i : ι) → α i)) ↦
            Subset.{u_2} (α := Set (α i))
              ((image (eval (β := α) i) ∘ fun (p : ((i : ι) → α i) × ((i : ι) → α i)) ↦ Icc p.1 p.2) x)
              (Icc (((fun (g : (i : ι) → α i) ↦ g i) ∘ Prod.fst) x) (((fun (g : (i : ι) → α i) ↦ g i) ∘ Prod.snd) x)))
          x}
      a
tendsto_Ixx₁ :
  ∀ (a : ((i : ι) → α i) × ((i : ι) → α i)),
    Subset.{u_2} (α := Set (α i))
      ((image (eval (β := α) i) ∘ fun (p : ((i : ι) → α i) × ((i : ι) → α i)) ↦ Icc p.1 p.2) a)
      (Icc (((fun (g : (i : ι) → α i) ↦ g i) ∘ Prod.fst) a) (((fun (g : (i : ι) → α i) ↦ g i) ∘ Prod.snd) a))
⊢ ∀ᶠ (x : ((i : ι) → α i) × ((i : ι) → α i)) in 𝓝 f ×ˢ 𝓝 f,
    Subset.{u_2} (α := Set (α i))
      ((image (eval (β := α) i) ∘ fun (p : ((i : ι) → α i) × ((i : ι) → α i)) ↦ Icc p.1 p.2) x)
      (Icc (((fun (g : (i : ι) → α i) ↦ g i) ∘ Prod.fst) x) (((fun (g : (i : ι) → α i) ↦ g i) ∘ Prod.snd) x))

Tactic:
filter_upwards [] using fun ⟨f, g⟩ ↦ image_subset_iff.mpr fun p hp ↦ ⟨hp.1 i, hp.2 i⟩
-- Module: Mathlib.Topology.Order.Basic
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 : TopologicalSpace α := Preorder.topology α
⊢ OrderTopology α

Tactic:
have : OrderTopology α := ⟨rfl⟩
-- Module: Mathlib.Topology.Order.Basic
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 : TopologicalSpace α := Preorder.topology α
this : OrderTopology α
⊢ induced f inst_2 ≤ Preorder.topology α

Tactic:
le_of_nhds_le_nhds fun x => ?_

Premises used: le_of_nhds_le_nhds
-- Module: Mathlib.Topology.Order.Basic
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 : TopologicalSpace α := Preorder.topology α
this : OrderTopology α
refine : ∀ (x : α), 𝓝 x ≤ 𝓝 x
⊢ induced f inst_2 ≤ Preorder.topology α

Tactic:
refine le_of_nhds_le_nhds fun x => ?_

Premises used: le_of_nhds_le_nhds
-- Module: Mathlib.Topology.Order.Basic
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 : α
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})
⊢ 𝓝 x ≤ 𝓝 x

Tactic:
simp only [nhds_eq_order, nhds_induced, comap_inf, comap_iInf, comap_principal, Ioi, Iio, ← hf]

Premises used: Set.Ioi, nhds_eq_order, Filter.comap_iInf, Filter.comap_inf, nhds_induced, Filter.comap_principal, Set.Iio
-- Module: Mathlib.Topology.Order.Basic
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})

Tactic:
inf_le_inf (le_iInf₂ fun a ha => ?_) (le_iInf₂ fun a ha => ?_)

Premises used: inf_le_inf, Set.Mem, le_iInf₂
-- Module: Mathlib.Topology.Order.Basic
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})
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})
⊢ 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:
refine inf_le_inf (le_iInf₂ fun a ha => ?_) (le_iInf₂ fun a ha => ?_)

Premises used: inf_le_inf
-- Module: Mathlib.Topology.Order.Basic
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 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:
iInf₂_le (f a) ha

Premises used: Set.Mem, iInf₂_le, setOf, Set.preimage
-- Module: Mathlib.Topology.Order.Basic
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 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:
iInf₂_le (f a) ha

Premises used: Set.Mem, iInf₂_le, setOf, Set.preimage
-- Module: Mathlib.Topology.Order.Basic
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 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:
exacts [iInf₂_le (f a) ha, iInf₂_le (f a) ha]

Premises used: iInf₂_le
-- Module: Mathlib.Topology.Order.Basic
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 α
⊢ OrderTopology α

Tactic:
have : OrderTopology α := ⟨rfl⟩
-- Module: Mathlib.Topology.Order.Basic
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 α

Tactic:
le_antisymm (induced_topology_le_preorder hf) ?_

Premises used: le_antisymm, induced_topology_le_preorder
-- Module: Mathlib.Topology.Order.Basic
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 α
refine : Preorder.topology α ≤ induced f inst_2
⊢ induced f inst_2 = Preorder.topology α

Tactic:
refine le_antisymm (induced_topology_le_preorder hf) ?_

Premises used: le_antisymm, induced_topology_le_preorder
-- Module: Mathlib.Topology.Order.Basic
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

Tactic:
le_of_nhds_le_nhds fun a => ?_

Premises used: le_of_nhds_le_nhds
-- Module: Mathlib.Topology.Order.Basic
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 α
refine : ∀ (a : α), 𝓝 a ≤ 𝓝 a
⊢ Preorder.topology α ≤ induced f inst_2

Tactic:
refine le_of_nhds_le_nhds fun a => ?_

Premises used: le_of_nhds_le_nhds
-- Module: Mathlib.Topology.Order.Basic
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 : α
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))
⊢ 𝓝 a ≤ 𝓝 a

Tactic:
simp only [nhds_eq_order, nhds_induced, comap_inf, comap_iInf, comap_principal]

Premises used: nhds_eq_order, Filter.comap_iInf, Filter.comap_inf, nhds_induced, Filter.comap_principal
-- Module: Mathlib.Topology.Order.Basic
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))

Tactic:
inf_le_inf (le_iInf₂ fun b hb => ?_) (le_iInf₂ fun b hb => ?_)

Premises used: inf_le_inf, Set.Mem, le_iInf₂
-- Module: Mathlib.Topology.Order.Basic
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)
refine_2 : ∀ (b : β) (hb : b ∈ Ioi (f a)), ⨅ b ∈ Ioi a, 𝓟 (Iio b) ≤ 𝓟 (f ⁻¹' Iio 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))

Tactic:
refine inf_le_inf (le_iInf₂ fun b hb => ?_) (le_iInf₂ fun b hb => ?_)

Premises used: inf_le_inf
-- Module: Mathlib.Topology.Order.Basic
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)
neg : ∀ (h : ∀ (x : α), b < f x), ⨅ b ∈ Iio a, 𝓟 (Ioi b) ≤ 𝓟 (f ⁻¹' Ioi b)
⊢ ⨅ b ∈ Iio a, 𝓟 (Ioi b) ≤ 𝓟 (f ⁻¹' Ioi b)

Tactic:
by_cases! h : ∃ x, ¬(b < f x)
-- Module: Mathlib.Topology.Order.Basic
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
pos : ∀ (x : α) (hx : ¬b < f x), ⨅ b ∈ Iio a, 𝓟 (Ioi b) ≤ 𝓟 (f ⁻¹' Ioi b)
⊢ ⨅ b ∈ Iio a, 𝓟 (Ioi b) ≤ 𝓟 (f ⁻¹' Ioi b)

Tactic:
rcases h with ⟨x, hx⟩
-- Module: Mathlib.Topology.Order.Basic
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
pos : ∀ (y : α) (hya : y < a) (hyb : b ≤ f y), ⨅ b ∈ Iio a, 𝓟 (Ioi b) ≤ 𝓟 (f ⁻¹' Ioi b)
⊢ ⨅ b ∈ Iio a, 𝓟 (Ioi b) ≤ 𝓟 (f ⁻¹' Ioi b)

Tactic:
rcases H₁ hb hx with ⟨y, hya, hyb⟩
-- Module: Mathlib.Topology.Order.Basic
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
y : α
hya : y < a
hyb : b ≤ f y
⊢ ⨅ b ∈ Iio a, 𝓟 (Ioi b) ≤ 𝓟 (f ⁻¹' Ioi b)

Tactic:
iInf₂_le_of_le y hya (principal_mono.2 fun z hz => hyb.trans_lt (hf.2 hz))

Premises used: Iff.mpr, Filter.principal_mono, Set.Mem, setOf, iInf₂_le_of_le, LE.le.trans_lt
-- Module: Mathlib.Topology.Order.Basic
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
y : α
hya : y < a
hyb : b ≤ f y
⊢ ⨅ b ∈ Iio a, 𝓟 (Ioi b) ≤ 𝓟 (f ⁻¹' Ioi b)

Tactic:
exact iInf₂_le_of_le y hya (principal_mono.2 fun z hz => hyb.trans_lt (hf.2 hz))

Premises used: iInf₂_le_of_le
-- Module: Mathlib.Topology.Order.Basic
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)

Tactic:
le_principal_iff.2 (univ_mem' h)

Premises used: Iff.mpr, Filter.le_principal_iff, Filter.univ_mem'
-- Module: Mathlib.Topology.Order.Basic
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)

Tactic:
exact le_principal_iff.2 (univ_mem' h)

Premises used: Iff.mpr, Filter.le_principal_iff, Filter.univ_mem'
-- Module: Mathlib.Topology.Order.Basic
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)
neg : ∀ (h : ∀ (x : α), f x < b), ⨅ b ∈ Ioi a, 𝓟 (Iio b) ≤ 𝓟 (f ⁻¹' Iio b)
⊢ ⨅ b ∈ Ioi a, 𝓟 (Iio b) ≤ 𝓟 (f ⁻¹' Iio b)

Tactic:
by_cases! h : ∃ x, ¬(f x < b)
-- Module: Mathlib.Topology.Order.Basic
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
pos : ∀ (x : α) (hx : ¬f x < b), ⨅ b ∈ Ioi a, 𝓟 (Iio b) ≤ 𝓟 (f ⁻¹' Iio b)
⊢ ⨅ b ∈ Ioi a, 𝓟 (Iio b) ≤ 𝓟 (f ⁻¹' Iio b)

Tactic:
rcases h with ⟨x, hx⟩
-- Module: Mathlib.Topology.Order.Basic
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
pos : ∀ (y : α) (hya : a < y) (hyb : f y ≤ b), ⨅ b ∈ Ioi a, 𝓟 (Iio b) ≤ 𝓟 (f ⁻¹' Iio b)
⊢ ⨅ b ∈ Ioi a, 𝓟 (Iio b) ≤ 𝓟 (f ⁻¹' Iio b)

Tactic:
rcases H₂ hb hx with ⟨y, hya, hyb⟩
-- Module: Mathlib.Topology.Order.Basic
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
y : α
hya : a < y
hyb : f y ≤ b
⊢ ⨅ b ∈ Ioi a, 𝓟 (Iio b) ≤ 𝓟 (f ⁻¹' Iio b)

Tactic:
iInf₂_le_of_le y hya (principal_mono.2 fun z hz => (hf.2 hz).trans_le hyb)

Premises used: Iff.mpr, Filter.principal_mono, Set.Mem, setOf, iInf₂_le_of_le, LT.lt.trans_le
-- Module: Mathlib.Topology.Order.Basic
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
y : α
hya : a < y
hyb : f y ≤ b
⊢ ⨅ b ∈ Ioi a, 𝓟 (Iio b) ≤ 𝓟 (f ⁻¹' Iio b)

Tactic:
exact iInf₂_le_of_le y hya (principal_mono.2 fun z hz => (hf.2 hz).trans_le hyb)

Premises used: iInf₂_le_of_le
-- Module: Mathlib.Topology.Order.Basic
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)

Tactic:
le_principal_iff.2 (univ_mem' h)

Premises used: Iff.mpr, Filter.le_principal_iff, Filter.univ_mem'