awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Order.Basic
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : SecondCountableTopology α
h : Nontrivial α
s : Set α := {x : α | ∃ (y : α), x ⋖ y}
y : (x : α) → α
hy : ∀ x ∈ s, x ⋖ y x
Hy : ∀ (x z : α), x ∈ s → z < y x → z ≤ x
a : Set α
ha : IsOpen[inst] a
t : Set α := {x : α | x ∈ s ∧ x ∈ a ∧ y x ∉ a ∧ ¬IsBot x}
z : (x : α) → α
hz : ∀ x ∈ t, z x < x
h'z : ∀ x ∈ t, Ioc (z x) x ⊆ a
⊢ t.PairwiseDisjoint (α := Set α) fun (x : α) ↦ Ioc (z x) x

Tactic:
have : PairwiseDisjoint t fun x => Ioc (z x) x := fun x xt x' x't hxx' => by
    rcases hxx'.lt_or_gt with (h' | h')
    · refine disjoint_left.2 fun u ux ux' => xt.2.2.1 ?_
      refine h'z x' x't ⟨ux'.1.trans_le (ux.2.trans (hy x xt.1).le), ?_⟩
      by_contra! H
      exact lt_irrefl _ ((Hy _ _ xt.1 H).trans_lt h')
    · refine disjoint_left.2 fun u ux ux' => x't.2.2.1 ?_
      refine h'z x xt ⟨ux.1.trans_le (ux'.2.trans (hy x' x't.1).le), ?_⟩
      by_contra! H
      exact lt_irrefl _ ((Hy _ _ x't.1 H).trans_lt h')
-- Module: Mathlib.Topology.Order.Basic
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : SecondCountableTopology α
h : Nontrivial α
s : Set α := {x : α | ∃ (y : α), x ⋖ y}
y : (x : α) → α
hy : ∀ x ∈ s, x ⋖ y x
Hy : ∀ (x z : α), x ∈ s → z < y x → z ≤ x
a : Set α
ha : IsOpen[inst] a
t : Set α := {x : α | x ∈ s ∧ x ∈ a ∧ y x ∉ a ∧ ¬IsBot x}
z : (x : α) → α
hz : ∀ x ∈ t, z x < x
h'z : ∀ x ∈ t, Ioc (z x) x ⊆ a
this : t.PairwiseDisjoint (α := Set α) fun (x : α) ↦ Ioc (z x) x
⊢ Set.Countable.{u} (α := α) {x : α | x ∈ s ∧ x ∈ a ∧ y x ∉ a ∧ ¬IsBot x}

Tactic:
this.countable_of_isOpen (fun x hx => ?_) fun x hx => ⟨x, hz x hx, le_rfl⟩

Premises used: le_rfl, Set.PairwiseDisjoint.countable_of_isOpen, setOf, And.intro, Exists.intro
-- Module: Mathlib.Topology.Order.Basic
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : SecondCountableTopology α
h : Nontrivial α
s : Set α := {x : α | ∃ (y : α), x ⋖ y}
y : (x : α) → α
hy : ∀ x ∈ s, x ⋖ y x
Hy : ∀ (x z : α), x ∈ s → z < y x → z ≤ x
a : Set α
ha : IsOpen[inst] a
t : Set α := {x : α | x ∈ s ∧ x ∈ a ∧ y x ∉ a ∧ ¬IsBot x}
z : (x : α) → α
hz : ∀ x ∈ t, z x < x
h'z : ∀ x ∈ t, Ioc (z x) x ⊆ a
this : t.PairwiseDisjoint (α := Set α) fun (x : α) ↦ Ioc (z x) x
refine : ∀ (x : α) (hx : x ∈ t), IsOpen[inst] (Ioc (z x) x)
⊢ Set.Countable.{u} (α := α) {x : α | x ∈ s ∧ x ∈ a ∧ y x ∉ a ∧ ¬IsBot x}

Tactic:
refine this.countable_of_isOpen (fun x hx => ?_) fun x hx => ⟨x, hz x hx, le_rfl⟩

Premises used: le_rfl, Set.PairwiseDisjoint.countable_of_isOpen, And.intro, Exists.intro
-- Module: Mathlib.Topology.Order.Basic
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : SecondCountableTopology α
h : Nontrivial α
s : Set α := {x : α | ∃ (y : α), x ⋖ y}
y : (x : α) → α
hy : ∀ x ∈ s, x ⋖ y x
Hy : ∀ (x z : α), x ∈ s → z < y x → z ≤ x
a : Set α
ha : IsOpen[inst] a
t : Set α := {x : α | x ∈ s ∧ x ∈ a ∧ y x ∉ a ∧ ¬IsBot x}
z : (x : α) → α
hz : ∀ x ∈ t, z x < x
h'z : ∀ x ∈ t, Ioc (z x) x ⊆ a
this : t.PairwiseDisjoint (α := Set α) fun (x : α) ↦ Ioc (z x) x
x : α
hx : x ∈ t
H : Ioc (z x) x = Ioo (z x) (y x)
rw : IsOpen[inst] (Ioo (z x) (y x))
⊢ IsOpen[inst] (Ioc (z x) x)

Tactic:
rw [H]
-- Module: Mathlib.Topology.Order.Basic
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : SecondCountableTopology α
h : Nontrivial α
s : Set α := {x : α | ∃ (y : α), x ⋖ y}
y : (x : α) → α
hy : ∀ x ∈ s, x ⋖ y x
Hy : ∀ (x z : α), x ∈ s → z < y x → z ≤ x
a : Set α
ha : IsOpen[inst] a
t : Set α := {x : α | x ∈ s ∧ x ∈ a ∧ y x ∉ a ∧ ¬IsBot x}
z : (x : α) → α
hz : ∀ x ∈ t, z x < x
h'z : ∀ x ∈ t, Ioc (z x) x ⊆ a
this : t.PairwiseDisjoint (α := Set α) fun (x : α) ↦ Ioc (z x) x
x : α
hx : x ∈ t
H : Ioc (z x) x = Ioo (z x) (y x)
⊢ IsOpen[inst] (Ioo (z x) (y x))

Tactic:
isOpen_Ioo

Premises used: isOpen_Ioo
-- Module: Mathlib.Topology.Order.Basic
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : SecondCountableTopology α
h : Nontrivial α
s : Set α := {x : α | ∃ (y : α), x ⋖ y}
y : (x : α) → α
hy : ∀ x ∈ s, x ⋖ y x
Hy : ∀ (x z : α), x ∈ s → z < y x → z ≤ x
a : Set α
ha : IsOpen[inst] a
t : Set α := {x : α | x ∈ s ∧ x ∈ a ∧ y x ∉ a ∧ ¬IsBot x}
z : (x : α) → α
hz : ∀ x ∈ t, z x < x
h'z : ∀ x ∈ t, Ioc (z x) x ⊆ a
this : t.PairwiseDisjoint (α := Set α) fun (x : α) ↦ Ioc (z x) x
x : α
hx : x ∈ t
H : Ioc (z x) x = Ioo (z x) (y x)
⊢ IsOpen[inst] (Ioo (z x) (y x))

Tactic:
exact isOpen_Ioo

Premises used: isOpen_Ioo
-- Module: Mathlib.Topology.Order.Basic
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : SecondCountableTopology α
h : Nontrivial α
s : Set α := {x : α | ∃ (y : α), x ⋖ y}
y : (x : α) → α
hy : ∀ x ∈ s, x ⋖ y x
Hy : ∀ (x z : α), x ∈ s → z < y x → z ≤ x
a : Set α
ha : IsOpen[inst] a
t : Set α := {x : α | x ∈ s ∧ x ∈ a ∧ y x ∉ a ∧ ¬IsBot x}
z : (x : α) → α
hz : ∀ x ∈ t, z x < x
h'z : ∀ x ∈ t, Ioc (z x) x ⊆ a
this : t.PairwiseDisjoint (α := Set α) fun (x : α) ↦ Ioc (z x) x
x : α
hx : x ∈ t
suffices : Ioc (z x) x = Ioo (z x) (y x)
⊢ IsOpen[inst] (Ioc (z x) x)

Tactic:
suffices H : Ioc (z x) x = Ioo (z x) (y x) by rw [H]; exact isOpen_Ioo
-- Module: Mathlib.Topology.Order.Basic
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : SecondCountableTopology α
h : Nontrivial α
s : Set α := {x : α | ∃ (y : α), x ⋖ y}
y : (x : α) → α
hy : ∀ x ∈ s, x ⋖ y x
Hy : ∀ (x z : α), x ∈ s → z < y x → z ≤ x
a : Set α
ha : IsOpen[inst] a
t : Set α := {x : α | x ∈ s ∧ x ∈ a ∧ y x ∉ a ∧ ¬IsBot x}
z : (x : α) → α
hz : ∀ x ∈ t, z x < x
h'z : ∀ x ∈ t, Ioc (z x) x ⊆ a
this : t.PairwiseDisjoint (α := Set α) fun (x : α) ↦ Ioc (z x) x
x : α
hx : x ∈ t
apply : Ioo (z x) (y x) ⊆ Ioc (z x) x
⊢ Ioc (z x) x = Ioo (z x) (y x)

Tactic:
apply (Ioc_subset_Ioo_right (hy x hx.1).lt).antisymm

Premises used: Set.Ioc_subset_Ioo_right, And.left, HasSubset.Subset.antisymm, CovBy.lt
-- Module: Mathlib.Topology.Order.Basic
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : SecondCountableTopology α
h : Nontrivial α
s : Set α := {x : α | ∃ (y : α), x ⋖ y}
y : (x : α) → α
hy : ∀ x ∈ s, x ⋖ y x
Hy : ∀ (x z : α), x ∈ s → z < y x → z ≤ x
a : Set α
ha : IsOpen[inst] a
t : Set α := {x : α | x ∈ s ∧ x ∈ a ∧ y x ∉ a ∧ ¬IsBot x}
z : (x : α) → α
hz : ∀ x ∈ t, z x < x
h'z : ∀ x ∈ t, Ioc (z x) x ⊆ a
this : t.PairwiseDisjoint (α := Set α) fun (x : α) ↦ Ioc (z x) x
x : α
hx : x ∈ t
⊢ ∀ (x_1 : α), z x < x_1 ∧ x_1 < y x → z x < x_1 ∧ x_1 ≤ x

Tactic:
fun u hu ↦ ⟨hu.1, Hy _ _ hx.1 hu.2⟩

Premises used: And.right, And.left, And.intro
-- Module: Mathlib.Topology.Order.Basic
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : SecondCountableTopology α
h : Nontrivial α
s : Set α := {x : α | ∃ (y : α), x ⋖ y}
y : (x : α) → α
hy : ∀ x ∈ s, x ⋖ y x
Hy : ∀ (x z : α), x ∈ s → z < y x → z ≤ x
a : Set α
ha : IsOpen[inst] a
t : Set α := {x : α | x ∈ s ∧ x ∈ a ∧ y x ∉ a ∧ ¬IsBot x}
z : (x : α) → α
hz : ∀ x ∈ t, z x < x
h'z : ∀ x ∈ t, Ioc (z x) x ⊆ a
this : t.PairwiseDisjoint (α := Set α) fun (x : α) ↦ Ioc (z x) x
x : α
hx : x ∈ t
⊢ ∀ (x_1 : α), z x < x_1 ∧ x_1 < y x → z x < x_1 ∧ x_1 ≤ x

Tactic:
exact fun u hu ↦ ⟨hu.1, Hy _ _ hx.1 hu.2⟩
-- Module: Mathlib.Topology.Order.Basic
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : SecondCountableTopology α
⊢ Set.Countable.{u} (α := α) {x : α | ∃ y < x, Ioo y x = ∅}

Tactic:
simpa only [← covBy_iff_Ioo_eq] using countable_setOf_covBy_left

Premises used: countable_setOf_covBy_left, covBy_iff_Ioo_eq
-- Module: Mathlib.Topology.Order.Basic
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : SecondCountableTopology α
y : α → α
s : Set α
h : s.PairwiseDisjoint (α := Set α) fun (x : α) ↦ Ioo x (y x)
h' : ∀ x ∈ s, x < y x
⊢ s.Countable

Tactic:
have : (s \ { x | ∃ y, x ⋖ y }).Countable :=
    (h.subset diff_subset).countable_of_isOpen (fun _ _ ↦ isOpen_Ioo) fun x hx ↦
      (not_covBy_iff_exists_mem_Ioo (h' _ hx.1)).1 <| mt (Exists.intro (y x)) hx.2
  this.of_diff countable_setOf_covBy_right

Premises used: Set.diff_subset, isOpen_Ioo, Set.PairwiseDisjoint.countable_of_isOpen, mt, Set.PairwiseDisjoint.subset, And.right, And.left, Set.Countable.of_diff, Exists.intro, Iff.mp, not_covBy_iff_exists_mem_Ioo, countable_setOf_covBy_right
-- Module: Mathlib.Topology.Order.Basic
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : LinearOrder β
inst_4 : SecondCountableTopology α
t : Set β
f : β → α
⊢ Nontrivial β

Tactic:
nontriviality β
-- Module: Mathlib.Topology.Order.Basic
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : LinearOrder β
inst_4 : SecondCountableTopology α
t : Set β
f : β → α
h : Nontrivial β
⊢ Nonempty β

Tactic:
infer_instance
-- Module: Mathlib.Topology.Order.Basic
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : LinearOrder β
inst_4 : SecondCountableTopology α
t : Set β
f : β → α
h : Nontrivial β
⊢ Nonempty α

Tactic:
have : Nonempty α := Nonempty.map f (by infer_instance)
-- Module: Mathlib.Topology.Order.Basic
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : LinearOrder β
inst_4 : SecondCountableTopology α
t : Set β
f : β → α
h : Nontrivial β
this : Nonempty α
s : Set β := {x : β | x ∈ t ∧ ∃ (z : α), f x < z ∧ ∀ y ∈ t, x < y → z ≤ f y}
⊢ ∀ x ∈ s, ∃ (z : α), f x < z ∧ ∀ y ∈ t, x < y → z ≤ f y

Tactic:
have : ∀ x, x ∈ s → ∃ z, f x < z ∧ ∀ y ∈ t, x < y → z ≤ f y := fun x hx ↦ hx.2
-- Module: Mathlib.Topology.Order.Basic
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : LinearOrder β
inst_4 : SecondCountableTopology α
t : Set β
f : β → α
h : Nontrivial β
this_1 : Nonempty α
s : Set β := {x : β | x ∈ t ∧ ∃ (z : α), f x < z ∧ ∀ y ∈ t, x < y → z ≤ f y}
this : ∀ x ∈ s, ∃ (z : α), f x < z ∧ ∀ y ∈ t, x < y → z ≤ f y
choose! :
  ∀ (z : (x : β) → α) (hz : ∀ x ∈ s, f x < z x ∧ ∀ y ∈ t, x < y → z x ≤ f y),
    Set.Countable.{v} (α := β) {x : β | x ∈ t ∧ ∃ (z : α), f x < z ∧ ∀ y ∈ t, x < y → z ≤ f y}
⊢ Set.Countable.{v} (α := β) {x : β | x ∈ t ∧ ∃ (z : α), f x < z ∧ ∀ y ∈ t, x < y → z ≤ f y}

Tactic:
choose! z hz using this
-- Module: Mathlib.Topology.Order.Basic
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : LinearOrder β
inst_4 : SecondCountableTopology α
t : Set β
f : β → α
h : Nontrivial β
this : Nonempty α
s : Set β := {x : β | x ∈ t ∧ ∃ (z : α), f x < z ∧ ∀ y ∈ t, x < y → z ≤ f y}
z : (x : β) → α
hz : ∀ x ∈ s, f x < z x ∧ ∀ y ∈ t, x < y → z x ≤ f y
hf : StrictMonoOn f s
⊢ InjOn f s

Tactic:
apply StrictMonoOn.injOn

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

Tactic:
(hz x hx).1

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

Tactic:
(hz x hx).2 y hy.1 hxy

Premises used: And.right, And.left
-- Module: Mathlib.Topology.Order.Basic
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : LinearOrder β
inst_4 : SecondCountableTopology α
t : Set β
f : β → α
h : Nontrivial β
this : Nonempty α
s : Set β := {x : β | x ∈ t ∧ ∃ (z : α), f x < z ∧ ∀ y ∈ t, x < y → z ≤ f y}
z : (x : β) → α
hz : ∀ x ∈ s, f x < z x ∧ ∀ y ∈ t, x < y → z x ≤ f y
x : β
hx : x ∈ s
y : β
hy : y ∈ s
hxy : x < y
⊢ f x < f y

Tactic:
calc
      f x < z x := (hz x hx).1
      _ ≤ f y := (hz x hx).2 y hy.1 hxy

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

Tactic:
have I : InjOn f s := by
    apply StrictMonoOn.injOn
    intro x hx y hy hxy
    calc
      f x < z x := (hz x hx).1
      _ ≤ f y := (hz x hx).2 y hy.1 hxy
-- Module: Mathlib.Topology.Order.Basic
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : LinearOrder β
inst_4 : SecondCountableTopology α
t : Set β
f : β → α
h : Nontrivial β
this : Nonempty α
s : Set β := {x : β | x ∈ t ∧ ∃ (z : α), f x < z ∧ ∀ y ∈ t, x < y → z ≤ f y}
z : (x : β) → α
hz : ∀ x ∈ s, f x < z x ∧ ∀ y ∈ t, x < y → z x ≤ f y
I : InjOn f s
u : β
us : u ∈ s
v : β
vs : v ∈ s
huv : f u ≠ f v
inr :
  ∀
    (this :
      ∀ (u : β) (us : u ∈ s) (v : β) (vs : v ∈ s) (huv : f u ≠ f v) (hle : u ≤ v),
        onFun (β := Set α) Disjoint (fun (x : α) ↦ Ioo x (z (invFunOn f s x))) (f u) (f v))
    (hle : ¬u ≤ v), onFun (β := Set α) Disjoint (fun (x : α) ↦ Ioo x (z (invFunOn f s x))) (f u) (f v)
wlog :
  ∀ (u : β) (us : u ∈ s) (v : β) (vs : v ∈ s) (huv : f u ≠ f v) (hle : u ≤ v),
    onFun (β := Set α) Disjoint (fun (x : α) ↦ Ioo x (z (invFunOn f s x))) (f u) (f v)
⊢ onFun (β := Set α) Disjoint (fun (x : α) ↦ Ioo x (z (invFunOn f s x))) (f u) (f v)

Tactic:
wlog hle : u ≤ v generalizing u v
-- Module: Mathlib.Topology.Order.Basic
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : LinearOrder β
inst_4 : SecondCountableTopology α
t : Set β
f : β → α
h : Nontrivial β
this_1 : Nonempty α
s : Set β := {x : β | x ∈ t ∧ ∃ (z : α), f x < z ∧ ∀ y ∈ t, x < y → z ≤ f y}
z : (x : β) → α
hz : ∀ x ∈ s, f x < z x ∧ ∀ y ∈ t, x < y → z x ≤ f y
I : InjOn f s
u : β
us : u ∈ s
v : β
vs : v ∈ s
huv : f u ≠ f v
this :
  ∀ (u : β) (us : u ∈ s) (v : β) (vs : v ∈ s) (huv : f u ≠ f v) (hle : u ≤ v),
    onFun (β := Set α) Disjoint (fun (x : α) ↦ Ioo x (z (invFunOn f s x))) (f u) (f v)
hle : ¬u ≤ v
⊢ onFun (β := Set α) Disjoint (fun (x : α) ↦ Ioo x (z (invFunOn f s x))) (f u) (f v)

Tactic:
(this v vs u us huv.symm (le_of_not_ge hle)).symm

Premises used: le_of_not_ge, Ne.symm, Disjoint.symm
-- Module: Mathlib.Topology.Order.Basic
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : LinearOrder β
inst_4 : SecondCountableTopology α
t : Set β
f : β → α
h : Nontrivial β
this_1 : Nonempty α
s : Set β := {x : β | x ∈ t ∧ ∃ (z : α), f x < z ∧ ∀ y ∈ t, x < y → z ≤ f y}
z : (x : β) → α
hz : ∀ x ∈ s, f x < z x ∧ ∀ y ∈ t, x < y → z x ≤ f y
I : InjOn f s
u : β
us : u ∈ s
v : β
vs : v ∈ s
huv : f u ≠ f v
this :
  ∀ (u : β) (us : u ∈ s) (v : β) (vs : v ∈ s) (huv : f u ≠ f v) (hle : u ≤ v),
    onFun (β := Set α) Disjoint (fun (x : α) ↦ Ioo x (z (invFunOn f s x))) (f u) (f v)
hle : ¬u ≤ v
⊢ onFun (β := Set α) Disjoint (fun (x : α) ↦ Ioo x (z (invFunOn f s x))) (f u) (f v)

Tactic:
exact (this v vs u us huv.symm (le_of_not_ge hle)).symm

Premises used: le_of_not_ge, Ne.symm, Disjoint.symm
-- Module: Mathlib.Topology.Order.Basic
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : LinearOrder β
inst_4 : SecondCountableTopology α
t : Set β
f : β → α
h : Nontrivial β
this : Nonempty α
s : Set β := {x : β | x ∈ t ∧ ∃ (z : α), f x < z ∧ ∀ y ∈ t, x < y → z ≤ f y}
z : (x : β) → α
hz : ∀ x ∈ s, f x < z x ∧ ∀ y ∈ t, x < y → z x ≤ f y
I : InjOn f s
u : β
us : u ∈ s
v : β
vs : v ∈ s
huv : f u ≠ f v
hle : u ≤ v
⊢ u < v

Tactic:
have hlt : u < v := hle.lt_of_ne (ne_of_apply_ne _ huv)
-- Module: Mathlib.Topology.Order.Basic
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : LinearOrder β
inst_4 : SecondCountableTopology α
t : Set β
f : β → α
h : Nontrivial β
this : Nonempty α
s : Set β := {x : β | x ∈ t ∧ ∃ (z : α), f x < z ∧ ∀ y ∈ t, x < y → z ≤ f y}
z : (x : β) → α
hz : ∀ x ∈ s, f x < z x ∧ ∀ y ∈ t, x < y → z x ≤ f y
I : InjOn f s
u : β
us : u ∈ s
v : β
vs : v ∈ s
huv : f u ≠ f v
hle : u ≤ v
hlt : u < v
apply :
  ∀ ⦃a : α⦄,
    Membership.mem (γ := Set α) ((fun (x : α) ↦ Ioo x (z (invFunOn f s x))) (f u)) a →
      ∀ ⦃b : α⦄, Membership.mem (γ := Set α) ((fun (x : α) ↦ Ioo x (z (invFunOn f s x))) (f v)) b → a ≠ b
⊢ onFun (β := Set α) Disjoint (fun (x : α) ↦ Ioo x (z (invFunOn f s x))) (f u) (f v)

Tactic:
apply disjoint_iff_forall_ne.2

Premises used: Iff.mpr, Set.disjoint_iff_forall_ne
-- Module: Mathlib.Topology.Order.Basic
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : LinearOrder β
inst_4 : SecondCountableTopology α
t : Set β
f : β → α
h : Nontrivial β
this : Nonempty α
s : Set β := {x : β | x ∈ t ∧ ∃ (z : α), f x < z ∧ ∀ y ∈ t, x < y → z ≤ f y}
z : (x : β) → α
hz : ∀ x ∈ s, f x < z x ∧ ∀ y ∈ t, x < y → z x ≤ f y
I : InjOn f s
u : β
us : u ∈ s
v : β
vs : v ∈ s
huv : f u ≠ f v
hle : u ≤ v
hlt : u < v
a : α
ha : Membership.mem (γ := Set α) ((fun (x : α) ↦ Ioo x (z (invFunOn f s x))) (f u)) a
hb : Membership.mem (γ := Set α) ((fun (x : α) ↦ Ioo x (z (invFunOn f s x))) (f v)) a
⊢ a ∈ Ioo (f u) (z u)

Tactic:
simp only [I.leftInvOn_invFunOn us, I.leftInvOn_invFunOn vs] at ha hb

Premises used: Set.InjOn.leftInvOn_invFunOn
-- Module: Mathlib.Topology.Order.Basic
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : LinearOrder β
inst_4 : SecondCountableTopology α
t : Set β
f : β → α
h : Nontrivial β
this : Nonempty α
s : Set β := {x : β | x ∈ t ∧ ∃ (z : α), f x < z ∧ ∀ y ∈ t, x < y → z ≤ f y}
z : (x : β) → α
hz : ∀ x ∈ s, f x < z x ∧ ∀ y ∈ t, x < y → z x ≤ f y
I : InjOn f s
u : β
us : u ∈ s
v : β
vs : v ∈ s
huv : f u ≠ f v
hle : u ≤ v
hlt : u < v
a : α
ha : Membership.mem (γ := Set α) ((fun (x : α) ↦ Ioo x (z (invFunOn f s x))) (f u)) a
hb : Membership.mem (γ := Set α) ((fun (x : α) ↦ Ioo x (z (invFunOn f s x))) (f v)) a
ha₁ : a ∈ Ioo (f u) (z u)
⊢ a ∈ Ioo (f v) (z v)

Tactic:
simp only [I.leftInvOn_invFunOn us, I.leftInvOn_invFunOn vs] at ha hb

Premises used: Set.InjOn.leftInvOn_invFunOn
-- Module: Mathlib.Topology.Order.Basic
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : LinearOrder β
inst_4 : SecondCountableTopology α
t : Set β
f : β → α
h : Nontrivial β
this : Nonempty α
s : Set β := {x : β | x ∈ t ∧ ∃ (z : α), f x < z ∧ ∀ y ∈ t, x < y → z ≤ f y}
z : (x : β) → α
hz : ∀ x ∈ s, f x < z x ∧ ∀ y ∈ t, x < y → z x ≤ f y
I : InjOn f s
u : β
us : u ∈ s
v : β
vs : v ∈ s
huv : f u ≠ f v
hle : u ≤ v
hlt : u < v
a : α
ha : a ∈ Ioo (f u) (z u)
hb : a ∈ Ioo (f v) (z v)
⊢ False

Tactic:
lt_irrefl _ ((ha.2.trans_le ((hz u us).2 v vs.1 hlt)).trans hb.1)

Premises used: lt_irrefl, And.right, And.left, LT.lt.trans_le, LT.lt.trans
-- Module: Mathlib.Topology.Order.Basic
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : LinearOrder β
inst_4 : SecondCountableTopology α
t : Set β
f : β → α
h : Nontrivial β
this : Nonempty α
s : Set β := {x : β | x ∈ t ∧ ∃ (z : α), f x < z ∧ ∀ y ∈ t, x < y → z ≤ f y}
z : (x : β) → α
hz : ∀ x ∈ s, f x < z x ∧ ∀ y ∈ t, x < y → z x ≤ f y
I : InjOn f s
u : β
us : u ∈ s
v : β
vs : v ∈ s
huv : f u ≠ f v
hle : u ≤ v
hlt : u < v
a : α
ha : a ∈ Ioo (f u) (z u)
hb : a ∈ Ioo (f v) (z v)
⊢ False

Tactic:
exact lt_irrefl _ ((ha.2.trans_le ((hz u us).2 v vs.1 hlt)).trans hb.1)

Premises used: lt_irrefl, And.right, And.left, LT.lt.trans_le, LT.lt.trans
-- Module: Mathlib.Topology.Order.Basic
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : LinearOrder β
inst_4 : SecondCountableTopology α
t : Set β
f : β → α
h : Nontrivial β
this : Nonempty α
s : Set β := {x : β | x ∈ t ∧ ∃ (z : α), f x < z ∧ ∀ y ∈ t, x < y → z ≤ f y}
z : (x : β) → α
hz : ∀ x ∈ s, f x < z x ∧ ∀ y ∈ t, x < y → z x ≤ f y
I : InjOn f s
⊢ (f '' s).PairwiseDisjoint (α := Set α) fun (x : α) ↦ Ioo x (z (invFunOn f s x))

Tactic:
have A : (f '' s).PairwiseDisjoint fun x => Ioo x (z (invFunOn f s x)) := by
      rintro _ ⟨u, us, rfl⟩ _ ⟨v, vs, rfl⟩ huv
      wlog hle : u ≤ v generalizing u v
      · exact (this v vs u us huv.symm (le_of_not_ge hle)).symm
      have hlt : u < v := hle.lt_of_ne (ne_of_apply_ne _ huv)
      apply disjoint_iff_forall_ne.2
      rintro a ha b hb rfl
      simp only [I.leftInvOn_invFunOn us, I.leftInvOn_invFunOn vs] at ha hb
      exact lt_irrefl _ ((ha.2.trans_le ((hz u us).2 v vs.1 hlt)).trans hb.1)
-- Module: Mathlib.Topology.Order.Basic
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : LinearOrder β
inst_4 : SecondCountableTopology α
t : Set β
f : β → α
h : Nontrivial β
this : Nonempty α
s : Set β := {x : β | x ∈ t ∧ ∃ (z : α), f x < z ∧ ∀ y ∈ t, x < y → z ≤ f y}
z : (x : β) → α
hz : ∀ x ∈ s, f x < z x ∧ ∀ y ∈ t, x < y → z x ≤ f y
I : InjOn f s
A : (f '' s).PairwiseDisjoint (α := Set α) fun (x : α) ↦ Ioo x (z (invFunOn f s x))
apply : ∀ x ∈ f '' s, x < z (invFunOn f s x)
⊢ (f '' s).Countable

Tactic:
apply Set.PairwiseDisjoint.countable_of_Ioo A

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

Tactic:
simpa only [I.leftInvOn_invFunOn ys] using (hz y ys).1

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

Tactic:
have fs_count : (f '' s).Countable := by
    have A : (f '' s).PairwiseDisjoint fun x => Ioo x (z (invFunOn f s x)) := by
      rintro _ ⟨u, us, rfl⟩ _ ⟨v, vs, rfl⟩ huv
      wlog hle : u ≤ v generalizing u v
      · exact (this v vs u us huv.symm (le_of_not_ge hle)).symm
      have hlt : u < v := hle.lt_of_ne (ne_of_apply_ne _ huv)
      apply disjoint_iff_forall_ne.2
      rintro a ha b hb rfl
      simp only [I.leftInvOn_invFunOn us, I.leftInvOn_invFunOn vs] at ha hb
      exact lt_irrefl _ ((ha.2.trans_le ((hz u us).2 v vs.1 hlt)).trans hb.1)
    apply Set.PairwiseDisjoint.countable_of_Ioo A
    rintro _ ⟨y, ys, rfl⟩
    simpa only [I.leftInvOn_invFunOn ys] using (hz y ys).1