awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.Order.Basic (goal)
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
x : α
xt : x ∈ t
x' : α
x't : x' ∈ t
hxx' : x ≠ x'
h' : x' < x
⊢ onFun (β := Set α) Disjoint (fun (x : α) ↦ Ioc (z x) x) x x'
have inr : ∀ (u : α) (ux : Membership.mem (γ := Set α) ((fun (x : α) ↦ Ioc (z x) x) x) u)
  (ux' : Membership.mem (γ := Set α) ((fun (x : α) ↦ Ioc (z x) x) x') u), y x' ∈ a
Tactic: refine disjoint_left.2 fun u ux ux' => x't.2.2.1 ?_
-- Lean 4 proof step from Mathlib.Topology.Order.Basic (goal)
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
x : α
xt : x ∈ t
x' : α
x't : x' ∈ t
hxx' : x ≠ x'
h' : x' < x
u : α
ux : Membership.mem (γ := Set α) ((fun (x : α) ↦ Ioc (z x) x) x) u
ux' : Membership.mem (γ := Set α) ((fun (x : α) ↦ Ioc (z x) x) x') u
⊢ y x' ∈ a
have inr : y x' ≤ x
Tactic: refine h'z x xt ⟨ux.1.trans_le (ux'.2.trans (hy x' x't.1).le), ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Order.Basic (goal)
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
x : α
xt : x ∈ t
x' : α
x't : x' ∈ t
hxx' : x ≠ x'
h' : x' < x
u : α
ux : Membership.mem (γ := Set α) ((fun (x : α) ↦ Ioc (z x) x) x) u
ux' : Membership.mem (γ := Set α) ((fun (x : α) ↦ Ioc (z x) x) x') u
⊢ y x' ≤ x
have inr : ∀ (H : x < y x'), False
Tactic: by_contra! H
-- Lean 4 proof step from Mathlib.Topology.Order.Basic (hypothesis)
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
⊢ Set.Countable.{u} (α := α) {x : α | x ∈ s ∧ x ∈ a ∧ y x ∉ a ∧ ¬IsBot x}
have this : 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')
-- Lean 4 proof step from Mathlib.Topology.Order.Basic (goal)
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}
have refine : ∀ (x : α) (hx : x ∈ t), IsOpen[inst] (Ioc (z x) x)
Tactic: refine this.countable_of_isOpen (fun x hx => ?_) fun x hx => ⟨x, hz x hx, le_rfl⟩
-- Lean 4 proof step from Mathlib.Topology.Order.Basic (goal)
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] (Ioc (z x) x)
have rw : IsOpen[inst] (Ioo (z x) (y x))
Tactic: rw [H]
-- Lean 4 proof step from Mathlib.Topology.Order.Basic (goal)
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
⊢ IsOpen[inst] (Ioc (z x) x)
have suffices : Ioc (z x) x = Ioo (z x) (y x)
Tactic: suffices H : Ioc (z x) x = Ioo (z x) (y x) by rw [H]; exact isOpen_Ioo
-- Lean 4 proof step from Mathlib.Topology.Order.Basic (goal)
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
⊢ Ioc (z x) x = Ioo (z x) (y x)
have apply : Ioo (z x) (y x) ⊆ Ioc (z x) x
Tactic: apply (Ioc_subset_Ioo_right (hy x hx.1).lt).antisymm
-- Lean 4 proof step from Mathlib.Topology.Order.Basic (hypothesis)
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : LinearOrder β
inst_4 : SecondCountableTopology α
t : Set β
f : β → α
⊢ Set.Countable.{v} (α := β) {x : β | x ∈ t ∧ ∃ (z : α), f x < z ∧ ∀ y ∈ t, x < y → z ≤ f y}
have a : Nontrivial β
Tactic: nontriviality β
-- Lean 4 proof step from Mathlib.Topology.Order.Basic (hypothesis)
Goal:
α : Type u
β : Type v
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : LinearOrder β
inst_4 : SecondCountableTopology α
t : Set β
f : β → α
h : Nontrivial β
⊢ Set.Countable.{v} (α := β) {x : β | x ∈ t ∧ ∃ (z : α), f x < z ∧ ∀ y ∈ t, x < y → z ≤ f y}
have this : Nonempty α
Tactic: have : Nonempty α := Nonempty.map f (by infer_instance)
-- Lean 4 proof step from Mathlib.Topology.Order.Basic (hypothesis)
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}
⊢ Set.Countable.{v} (α := β) {x : β | x ∈ t ∧ ∃ (z : α), f x < z ∧ ∀ y ∈ t, x < y → z ≤ f y}
have this₁ : ∀ 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
-- Lean 4 proof step from Mathlib.Topology.Order.Basic (goal)
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
⊢ Set.Countable.{v} (α := β) {x : β | x ∈ t ∧ ∃ (z : α), f x < z ∧ ∀ y ∈ t, x < y → z ≤ f y}
have 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}
Tactic: choose! z hz using this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Topology.Order.Basic (goal)
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
have hf : StrictMonoOn f s
Tactic: apply StrictMonoOn.injOn
-- Lean 4 proof step from Mathlib.Topology.Order.Basic (hypothesis)
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
⊢ Set.Countable.{v} (α := β) {x : β | x ∈ t ∧ ∃ (z : α), f x < z ∧ ∀ y ∈ t, x < y → z ≤ f y}
have I : 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
-- Lean 4 proof step from Mathlib.Topology.Order.Basic (goal)
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
⊢ onFun (β := Set α) Disjoint (fun (x : α) ↦ Ioo x (z (invFunOn f s x))) (f u) (f v)
have 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)
Tactic: wlog hle : u ≤ v generalizing u v
-- Lean 4 proof step from Mathlib.Topology.Order.Basic (goal)
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)
⊢ onFun (β := Set α) Disjoint (fun (x : α) ↦ Ioo x (z (invFunOn f s x))) (f u) (f v)
have 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)
Tactic: wlog hle : u ≤ v generalizing u v
Cleared hypotheses: u, us, v, vs, huv
-- Lean 4 proof step from Mathlib.Topology.Order.Basic (hypothesis)
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
⊢ onFun (β := Set α) Disjoint (fun (x : α) ↦ Ioo x (z (invFunOn f s x))) (f u) (f v)
have hlt : u < v
Tactic: have hlt : u < v := hle.lt_of_ne (ne_of_apply_ne _ huv)
-- Lean 4 proof step from Mathlib.Topology.Order.Basic (goal)
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
⊢ onFun (β := Set α) Disjoint (fun (x : α) ↦ Ioo x (z (invFunOn f s x))) (f u) (f v)
have 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
Tactic: apply disjoint_iff_forall_ne.2
-- Lean 4 proof step from Mathlib.Topology.Order.Basic (hypothesis)
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
⊢ False
have ha₁ : a ∈ Ioo (f u) (z u)
Tactic: simp only [I.leftInvOn_invFunOn us, I.leftInvOn_invFunOn vs] at ha hb
Cleared hypotheses: ha, hb
-- Lean 4 proof step from Mathlib.Topology.Order.Basic (hypothesis)
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)
⊢ False
have hb₁ : a ∈ Ioo (f v) (z v)
Tactic: simp only [I.leftInvOn_invFunOn us, I.leftInvOn_invFunOn vs] at ha hb
Cleared hypotheses: ha, hb
-- Lean 4 proof step from Mathlib.Topology.Order.Basic (hypothesis)
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
have A : (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)
-- Lean 4 proof step from Mathlib.Topology.Order.Basic (goal)
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))
⊢ (f '' s).Countable
have apply : ∀ x ∈ f '' s, x < z (invFunOn f s x)
Tactic: apply Set.PairwiseDisjoint.countable_of_Ioo A
-- Lean 4 proof step from Mathlib.Topology.Order.Basic (hypothesis)
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
⊢ Set.Countable.{v} (α := β) {x : β | x ∈ t ∧ ∃ (z : α), f x < z ∧ ∀ y ∈ t, x < y → z ≤ f y}
have fs_count : (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
-- Lean 4 proof step from Mathlib.Topology.Order.Basic (goal)
Goal:
α : Type u
β : Type v
γ : Type w
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : SeparableSpace α
⊢ IsCountablyGenerated.{u} (α := α) atTop
have inl : ∀ (h : Eq.{u + 1} (α := Set α) {x : α | IsTop x} ∅), IsCountablyGenerated.{u} (α := α) atTop
Tactic: obtain (h | ⟨x, hx⟩) := Set.eq_empty_or_nonempty {x : α | IsTop x}
-- Lean 4 proof step from Mathlib.Topology.Order.Basic (goal)
Goal:
α : Type u
β : Type v
γ : Type w
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : SeparableSpace α
inl : ∀ (h : Eq.{u + 1} (α := Set α) {x : α | IsTop x} ∅), IsCountablyGenerated.{u} (α := α) atTop
⊢ IsCountablyGenerated.{u} (α := α) atTop
have inr : ∀ (x : α) (hx : Membership.mem (γ := Set α) {x : α | IsTop x} x), IsCountablyGenerated.{u} (α := α) atTop
Tactic: obtain (h | ⟨x, hx⟩) := Set.eq_empty_or_nonempty {x : α | IsTop x}
-- Lean 4 proof step from Mathlib.Topology.Order.Basic (goal)
Goal:
α : Type u
β : Type v
γ : Type w
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : SeparableSpace α
h : Eq.{u + 1} (α := Set α) {x : α | IsTop x} ∅
⊢ IsCountablyGenerated.{u} (α := α) atTop
have inl : ∀ (s : Set α) (s_count : s.Countable) (hs : Dense s), IsCountablyGenerated.{u} (α := α) atTop
Tactic: obtain ⟨s, s_count, hs⟩ := exists_countable_dense α
-- Lean 4 proof step from Mathlib.Topology.Order.Basic (goal)
Goal:
α : Type u
β : Type v
γ : Type w
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : SeparableSpace α
h : Eq.{u + 1} (α := Set α) {x : α | IsTop x} ∅
s : Set α
s_count : s.Countable
hs : Dense s
⊢ atTop = generate (Ici '' s)
have refine : BddAbove s → ∀ (x : α) (hx : x ∈ upperBounds s), False
Tactic: refine atTop_eq_generate_of_not_bddAbove fun ⟨x, hx⟩ ↦ ?_
-- Lean 4 proof step from Mathlib.Topology.Order.Basic (hypothesis)
Goal:
α : Type u
β : Type v
γ : Type w
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : SeparableSpace α
h : Eq.{u + 1} (α := Set α) {x : α | IsTop x} ∅
s : Set α
s_count : s.Countable
hs : Dense s
h_1 : BddAbove s
x : α
hx : x ∈ upperBounds s
⊢ False
have h₁ : ∀ (x : α), ∃ (x_1 : α), x < x_1
Tactic: simp only [eq_empty_iff_forall_notMem, IsTop, mem_setOf_eq, not_forall, not_le] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Topology.Order.Basic (goal)
Goal:
α : Type u
β : Type v
γ : Type w
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : SeparableSpace α
s : Set α
s_count : s.Countable
hs : Dense s
h_1 : BddAbove s
x : α
hx : x ∈ upperBounds s
h : ∀ (x : α), ∃ (x_1 : α), x < x_1
⊢ False
have obtain : ∀ (y : α) (hy : y ∈ s) (hxy : y ∈ Ioi x), False
Tactic: obtain ⟨y, hy, hxy⟩ := hs.exists_mem_open isOpen_Ioi (h x)
-- Lean 4 proof step from Mathlib.Topology.Order.Basic (hypothesis)
Goal:
α : Type u
β : Type v
γ : Type w
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : SeparableSpace α
h : Eq.{u + 1} (α := Set α) {x : α | IsTop x} ∅
s : Set α
s_count : s.Countable
hs : Dense s
⊢ IsCountablyGenerated.{u} (α := α) atTop
have this : atTop = generate (Ici '' s)
Tactic: have : atTop = generate (Ici '' s) := by
      refine atTop_eq_generate_of_not_bddAbove fun ⟨x, hx⟩ ↦ ?_
      simp only [eq_empty_iff_forall_notMem, IsTop, mem_setOf_eq, not_forall, not_le] at h
      obtain ⟨y, hy, hxy⟩ := hs.exists_mem_open isOpen_Ioi (h x)
      exact (hx hy).not_gt hxy
-- Lean 4 proof step from Mathlib.Topology.Order.Basic (goal)
Goal:
α : Type u
β : Type v
γ : Type w
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : SeparableSpace α
h : Eq.{u + 1} (α := Set α) {x : α | IsTop x} ∅
s : Set α
s_count : s.Countable
hs : Dense s
this : atTop = generate (Ici '' s)
⊢ IsCountablyGenerated.{u} (α := α) atTop
have inl : (generate (Ici '' s)).IsCountablyGenerated
Tactic: rw [this]
-- Lean 4 proof step from Mathlib.Topology.Order.Basic (goal)
Goal:
α : Type u
β : Type v
γ : Type w
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : SeparableSpace α
x : α
hx : Membership.mem (γ := Set α) {x : α | IsTop x} x
⊢ IsCountablyGenerated.{u} (α := α) atTop
have inr : IsCountablyGenerated (pure x)
Tactic: rw [atTop_eq_pure_of_isTop hx]
-- Lean 4 proof step from Mathlib.Topology.Order.Basic (goal)
Goal:
ι : Type u_1
X : ι → Type u_2
inst : Finite ι
inst_1 : (i : ι) → LinearOrder (X i)
inst_2 : (i : ι) → TopologicalSpace (X i)
inst_3 : ∀ (i : ι), OrderTopology.{u_2} (X i)
a b x : (i : ι) → X i
inst_4 : Nonempty ι
ha : ∀ (i : ι), a i < x i
hb : ∀ (i : ι), x i < b i
⊢ Ioc a b ∈ 𝓝 x
have refine : ∀ (i : ι), Membership.mem (γ := Set ι) univ i → Ioc (a i) (b i) ∈ 𝓝 (x i)
Tactic: refine mem_of_superset (set_pi_mem_nhds Set.finite_univ fun i _ => ?_) (pi_univ_Ioc_subset a b)
-- Lean 4 proof step from Mathlib.Topology.Order.Basic (goal)
Goal:
ι : Type u_1
X : ι → Type u_2
inst : Finite ι
inst_1 : (i : ι) → LinearOrder (X i)
inst_2 : (i : ι) → TopologicalSpace (X i)
inst_3 : ∀ (i : ι), OrderTopology.{u_2} (X i)
a b x : (i : ι) → X i
inst_4 : Nonempty ι
ha : ∀ (i : ι), a i < x i
hb : ∀ (i : ι), x i < b i
⊢ Ioo a b ∈ 𝓝 x
have refine : ∀ (i : ι), Membership.mem (γ := Set ι) univ i → Ioo (a i) (b i) ∈ 𝓝 (x i)
Tactic: refine mem_of_superset (set_pi_mem_nhds Set.finite_univ fun i _ => ?_) (pi_univ_Ioo_subset a b)
-- Lean 4 proof step from Mathlib.Topology.Order.Basic (goal)
Goal:
X : Type u_1
inst : ConditionallyCompleteLinearOrder X
inst_1 : TopologicalSpace X
inst_2 : OrderTopology X
Y : Type u_2
inst_3 : ConditionallyCompleteLinearOrder Y
inst_4 : TopologicalSpace Y
inst_5 : OrderTopology Y
inst_6 : DenselyOrdered X
f : X → Y
x : X
hf : LeftOrdContinuous f
⊢ ContinuousWithinAt f (Iic x) x
have rw : Tendsto f (𝓝[≤] x) (𝓝 (f x))
Tactic: rw [ContinuousWithinAt, OrderTopology.topology_eq_generate_intervals (α := Y)]