awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.Order.AtTopBotIxx (goal)
Goal:
X : Type u_1
inst : LinearOrder X
inst_1 : TopologicalSpace X
inst_2 : OrderTopology X
a b : X
α : Type u_2
l : Filter α
f : α → (↑(Ioo a b) : Type u_1)
hb : IsSuccPrelimit b
rw :
  Tendsto f l (comap (Subtype.val (p := fun (x : X) ↦ x ∈ Ioo a b)) (𝓝[<] b)) ↔
    Tendsto (fun (x : α) ↦ (↑(f x) : X)) l (𝓝[<] b)
⊢ Tendsto f l atTop ↔ Tendsto (fun (x : α) ↦ (↑(f x) : X)) l (𝓝[<] b)
have rw₁ : Tendsto (Subtype.val (p := fun (x : X) ↦ x ∈ Ioo a b) ∘ f) l (𝓝[<] b) ↔ Tendsto (fun (x : α) ↦ (↑(f x) : X)) l (𝓝[<] b)
Tactic: rw [← comap_coe_Ioo_nhdsLT a b hb, tendsto_comap_iff, Function.comp_def]
-- Lean 4 proof step from Mathlib.Topology.Order.AtTopBotIxx (goal)
Goal:
X : Type u_1
inst : LinearOrder X
inst_1 : TopologicalSpace X
inst_2 : OrderTopology X
a b : X
α : Type u_2
l : Filter α
f : α → (↑(Ioo a b) : Type u_1)
hb : IsSuccPrelimit b
rw :
  Tendsto f l (comap (Subtype.val (p := fun (x : X) ↦ x ∈ Ioo a b)) (𝓝[<] b)) ↔
    Tendsto (fun (x : α) ↦ (↑(f x) : X)) l (𝓝[<] b)
rw₁ :
  Tendsto (Subtype.val (p := fun (x : X) ↦ x ∈ Ioo a b) ∘ f) l (𝓝[<] b) ↔
    Tendsto (fun (x : α) ↦ (↑(f x) : X)) l (𝓝[<] b)
⊢ Tendsto f l atTop ↔ Tendsto (fun (x : α) ↦ (↑(f x) : X)) l (𝓝[<] b)
have rw₂ : Tendsto (fun (x : α) ↦ (↑(f x) : X)) l (𝓝[<] b) ↔ Tendsto (fun (x : α) ↦ (↑(f x) : X)) l (𝓝[<] b)
Tactic: rw [← comap_coe_Ioo_nhdsLT a b hb, tendsto_comap_iff, Function.comp_def]
-- Lean 4 proof step from Mathlib.Topology.Order.AtTopBotIxx (goal)
Goal:
X : Type u_1
inst : LinearOrder X
inst_1 : TopologicalSpace X
inst_2 : OrderTopology X
a b : X
α : Type u_2
l : Filter α
f : α → (↑(Ioo a b) : Type u_1)
ha : IsPredPrelimit a
⊢ Tendsto f l atBot ↔ Tendsto (fun (x : α) ↦ (↑(f x) : X)) l (𝓝[>] a)
have rw : Tendsto f l (comap (Subtype.val (p := fun (x : X) ↦ x ∈ Ioo a b)) (𝓝[>] a)) ↔
  Tendsto (fun (x : α) ↦ (↑(f x) : X)) l (𝓝[>] a)
Tactic: rw [← comap_coe_Ioo_nhdsGT a b ha, tendsto_comap_iff, Function.comp_def]
-- Lean 4 proof step from Mathlib.Topology.Order.AtTopBotIxx (goal)
Goal:
X : Type u_1
inst : LinearOrder X
inst_1 : TopologicalSpace X
inst_2 : OrderTopology X
a b : X
α : Type u_2
l : Filter α
f : α → (↑(Ioo a b) : Type u_1)
ha : IsPredPrelimit a
rw :
  Tendsto f l (comap (Subtype.val (p := fun (x : X) ↦ x ∈ Ioo a b)) (𝓝[>] a)) ↔
    Tendsto (fun (x : α) ↦ (↑(f x) : X)) l (𝓝[>] a)
⊢ Tendsto f l atBot ↔ Tendsto (fun (x : α) ↦ (↑(f x) : X)) l (𝓝[>] a)
have rw₁ : Tendsto (Subtype.val (p := fun (x : X) ↦ x ∈ Ioo a b) ∘ f) l (𝓝[>] a) ↔ Tendsto (fun (x : α) ↦ (↑(f x) : X)) l (𝓝[>] a)
Tactic: rw [← comap_coe_Ioo_nhdsGT a b ha, tendsto_comap_iff, Function.comp_def]
-- Lean 4 proof step from Mathlib.Topology.Order.AtTopBotIxx (goal)
Goal:
X : Type u_1
inst : LinearOrder X
inst_1 : TopologicalSpace X
inst_2 : OrderTopology X
a b : X
α : Type u_2
l : Filter α
f : α → (↑(Ioo a b) : Type u_1)
ha : IsPredPrelimit a
rw :
  Tendsto f l (comap (Subtype.val (p := fun (x : X) ↦ x ∈ Ioo a b)) (𝓝[>] a)) ↔
    Tendsto (fun (x : α) ↦ (↑(f x) : X)) l (𝓝[>] a)
rw₁ :
  Tendsto (Subtype.val (p := fun (x : X) ↦ x ∈ Ioo a b) ∘ f) l (𝓝[>] a) ↔
    Tendsto (fun (x : α) ↦ (↑(f x) : X)) l (𝓝[>] a)
⊢ Tendsto f l atBot ↔ Tendsto (fun (x : α) ↦ (↑(f x) : X)) l (𝓝[>] a)
have rw₂ : Tendsto (fun (x : α) ↦ (↑(f x) : X)) l (𝓝[>] a) ↔ Tendsto (fun (x : α) ↦ (↑(f x) : X)) l (𝓝[>] a)
Tactic: rw [← comap_coe_Ioo_nhdsGT a b ha, tendsto_comap_iff, Function.comp_def]
-- Lean 4 proof step from Mathlib.Topology.Order.AtTopBotIxx (goal)
Goal:
X : Type u_1
inst : LinearOrder X
inst_1 : TopologicalSpace X
inst_2 : OrderTopology X
a : X
α : Type u_2
l : Filter α
f : α → (↑(Ioi a) : Type u_1)
ha : IsPredPrelimit a
⊢ Tendsto f l atBot ↔ Tendsto (fun (x : α) ↦ (↑(f x) : X)) l (𝓝[>] a)
have rw : Tendsto f l (comap (Subtype.val (p := fun (x : X) ↦ x ∈ Ioi a)) (𝓝[>] a)) ↔
  Tendsto (fun (x : α) ↦ (↑(f x) : X)) l (𝓝[>] a)
Tactic: rw [← comap_coe_Ioi_nhdsGT a ha, tendsto_comap_iff, Function.comp_def]
-- Lean 4 proof step from Mathlib.Topology.Order.AtTopBotIxx (goal)
Goal:
X : Type u_1
inst : LinearOrder X
inst_1 : TopologicalSpace X
inst_2 : OrderTopology X
a : X
α : Type u_2
l : Filter α
f : α → (↑(Ioi a) : Type u_1)
ha : IsPredPrelimit a
rw :
  Tendsto f l (comap (Subtype.val (p := fun (x : X) ↦ x ∈ Ioi a)) (𝓝[>] a)) ↔
    Tendsto (fun (x : α) ↦ (↑(f x) : X)) l (𝓝[>] a)
⊢ Tendsto f l atBot ↔ Tendsto (fun (x : α) ↦ (↑(f x) : X)) l (𝓝[>] a)
have rw₁ : Tendsto (Subtype.val (p := fun (x : X) ↦ x ∈ Ioi a) ∘ f) l (𝓝[>] a) ↔ Tendsto (fun (x : α) ↦ (↑(f x) : X)) l (𝓝[>] a)
Tactic: rw [← comap_coe_Ioi_nhdsGT a ha, tendsto_comap_iff, Function.comp_def]
-- Lean 4 proof step from Mathlib.Topology.Order.AtTopBotIxx (goal)
Goal:
X : Type u_1
inst : LinearOrder X
inst_1 : TopologicalSpace X
inst_2 : OrderTopology X
a : X
α : Type u_2
l : Filter α
f : α → (↑(Ioi a) : Type u_1)
ha : IsPredPrelimit a
rw :
  Tendsto f l (comap (Subtype.val (p := fun (x : X) ↦ x ∈ Ioi a)) (𝓝[>] a)) ↔
    Tendsto (fun (x : α) ↦ (↑(f x) : X)) l (𝓝[>] a)
rw₁ :
  Tendsto (Subtype.val (p := fun (x : X) ↦ x ∈ Ioi a) ∘ f) l (𝓝[>] a) ↔ Tendsto (fun (x : α) ↦ (↑(f x) : X)) l (𝓝[>] a)
⊢ Tendsto f l atBot ↔ Tendsto (fun (x : α) ↦ (↑(f x) : X)) l (𝓝[>] a)
have rw₂ : Tendsto (fun (x : α) ↦ (↑(f x) : X)) l (𝓝[>] a) ↔ Tendsto (fun (x : α) ↦ (↑(f x) : X)) l (𝓝[>] a)
Tactic: rw [← comap_coe_Ioi_nhdsGT a ha, tendsto_comap_iff, Function.comp_def]
-- Lean 4 proof step from Mathlib.Topology.Order.AtTopBotIxx (goal)
Goal:
X : Type u_1
inst : LinearOrder X
inst_1 : TopologicalSpace X
inst_2 : OrderTopology X
a : X
α : Type u_2
l : Filter α
f : α → (↑(Iio a) : Type u_1)
ha : IsSuccPrelimit a
⊢ Tendsto f l atTop ↔ Tendsto (fun (x : α) ↦ (↑(f x) : X)) l (𝓝[<] a)
have rw : Tendsto f l (comap (Subtype.val (p := fun (x : X) ↦ x ∈ Iio a)) (𝓝[<] a)) ↔
  Tendsto (fun (x : α) ↦ (↑(f x) : X)) l (𝓝[<] a)
Tactic: rw [← comap_coe_Iio_nhdsLT a ha, tendsto_comap_iff, Function.comp_def]
-- Lean 4 proof step from Mathlib.Topology.Order.AtTopBotIxx (goal)
Goal:
X : Type u_1
inst : LinearOrder X
inst_1 : TopologicalSpace X
inst_2 : OrderTopology X
a : X
α : Type u_2
l : Filter α
f : α → (↑(Iio a) : Type u_1)
ha : IsSuccPrelimit a
rw :
  Tendsto f l (comap (Subtype.val (p := fun (x : X) ↦ x ∈ Iio a)) (𝓝[<] a)) ↔
    Tendsto (fun (x : α) ↦ (↑(f x) : X)) l (𝓝[<] a)
⊢ Tendsto f l atTop ↔ Tendsto (fun (x : α) ↦ (↑(f x) : X)) l (𝓝[<] a)
have rw₁ : Tendsto (Subtype.val (p := fun (x : X) ↦ x ∈ Iio a) ∘ f) l (𝓝[<] a) ↔ Tendsto (fun (x : α) ↦ (↑(f x) : X)) l (𝓝[<] a)
Tactic: rw [← comap_coe_Iio_nhdsLT a ha, tendsto_comap_iff, Function.comp_def]
-- Lean 4 proof step from Mathlib.Topology.Order.AtTopBotIxx (goal)
Goal:
X : Type u_1
inst : LinearOrder X
inst_1 : TopologicalSpace X
inst_2 : OrderTopology X
a : X
α : Type u_2
l : Filter α
f : α → (↑(Iio a) : Type u_1)
ha : IsSuccPrelimit a
rw :
  Tendsto f l (comap (Subtype.val (p := fun (x : X) ↦ x ∈ Iio a)) (𝓝[<] a)) ↔
    Tendsto (fun (x : α) ↦ (↑(f x) : X)) l (𝓝[<] a)
rw₁ :
  Tendsto (Subtype.val (p := fun (x : X) ↦ x ∈ Iio a) ∘ f) l (𝓝[<] a) ↔ Tendsto (fun (x : α) ↦ (↑(f x) : X)) l (𝓝[<] a)
⊢ Tendsto f l atTop ↔ Tendsto (fun (x : α) ↦ (↑(f x) : X)) l (𝓝[<] a)
have rw₂ : Tendsto (fun (x : α) ↦ (↑(f x) : X)) l (𝓝[<] a) ↔ Tendsto (fun (x : α) ↦ (↑(f x) : X)) l (𝓝[<] a)
Tactic: rw [← comap_coe_Iio_nhdsLT a ha, tendsto_comap_iff, Function.comp_def]
-- Lean 4 proof step from Mathlib.Topology.Order.AtTopBotIxx (goal)
Goal:
X : Type u_1
inst : LinearOrder X
inst_1 : TopologicalSpace X
inst_2 : OrderTopology X
α : Type u_2
inst_3 : LinearOrder α
inst_4 : LocallyFiniteOrder α
inst_5 : NoMaxOrder X
inst_6 : NoMinOrder X
f g : α → X
hl : Tendsto f atTop atTop
hu : Tendsto g atBot atBot
x : X
⊢ ∃ t ∈ 𝓝 x, Set.Finite.{u_2} (α := α) {i : α | ((fun (n : α) ↦ Icc (f n) (g n)) i ∩ t).Nonempty}
have inl : IsEmpty α → ∃ t ∈ 𝓝 x, Set.Finite.{u_2} (α := α) {i : α | ((fun (n : α) ↦ Icc (f n) (g n)) i ∩ t).Nonempty}
Tactic: cases isEmpty_or_nonempty α
-- Lean 4 proof step from Mathlib.Topology.Order.AtTopBotIxx (goal)
Goal:
X : Type u_1
inst : LinearOrder X
inst_1 : TopologicalSpace X
inst_2 : OrderTopology X
α : Type u_2
inst_3 : LinearOrder α
inst_4 : LocallyFiniteOrder α
inst_5 : NoMaxOrder X
inst_6 : NoMinOrder X
f g : α → X
hl : Tendsto f atTop atTop
hu : Tendsto g atBot atBot
x : X
inl : IsEmpty α → ∃ t ∈ 𝓝 x, Set.Finite.{u_2} (α := α) {i : α | ((fun (n : α) ↦ Icc (f n) (g n)) i ∩ t).Nonempty}
⊢ ∃ t ∈ 𝓝 x, Set.Finite.{u_2} (α := α) {i : α | ((fun (n : α) ↦ Icc (f n) (g n)) i ∩ t).Nonempty}
have inr : Nonempty α → ∃ t ∈ 𝓝 x, Set.Finite.{u_2} (α := α) {i : α | ((fun (n : α) ↦ Icc (f n) (g n)) i ∩ t).Nonempty}
Tactic: cases isEmpty_or_nonempty α
-- Lean 4 proof step from Mathlib.Topology.Order.AtTopBotIxx (goal)
Goal:
X : Type u_1
inst : LinearOrder X
inst_1 : TopologicalSpace X
inst_2 : OrderTopology X
α : Type u_2
inst_3 : LinearOrder α
inst_4 : LocallyFiniteOrder α
inst_5 : NoMaxOrder X
inst_6 : NoMinOrder X
f g : α → X
hl : Tendsto f atTop atTop
hu : Tendsto g atBot atBot
x : X
h : IsEmpty α
⊢ ∃ t ∈ 𝓝 x, Set.Finite.{u_2} (α := α) {i : α | ((fun (n : α) ↦ Icc (f n) (g n)) i ∩ t).Nonempty}
have h : univ ∈ 𝓝 x ∧ Set.Finite.{u_2} (α := α) {i : α | Set.Nonempty.{u_1} (α := X) ((fun (n : α) ↦ Icc (f n) (g n)) i ∩ univ)}
Tactic: use univ
-- Lean 4 proof step from Mathlib.Topology.Order.AtTopBotIxx (goal)
Goal:
X : Type u_1
inst : LinearOrder X
inst_1 : TopologicalSpace X
inst_2 : OrderTopology X
α : Type u_2
inst_3 : LinearOrder α
inst_4 : LocallyFiniteOrder α
inst_5 : NoMaxOrder X
inst_6 : NoMinOrder X
f g : α → X
hl : Tendsto f atTop atTop
hu : Tendsto g atBot atBot
x : X
h : Nonempty α
⊢ ∃ t ∈ 𝓝 x, Set.Finite.{u_2} (α := α) {i : α | ((fun (n : α) ↦ Icc (f n) (g n)) i ∩ t).Nonempty}
have inr : ∀ (x_L : X) (hx_L : x_L < x),
  ∃ t ∈ 𝓝 x, Set.Finite.{u_2} (α := α) {i : α | ((fun (n : α) ↦ Icc (f n) (g n)) i ∩ t).Nonempty}
Tactic: obtain ⟨x_L, hx_L⟩ := exists_lt x
-- Lean 4 proof step from Mathlib.Topology.Order.AtTopBotIxx (goal)
Goal:
X : Type u_1
inst : LinearOrder X
inst_1 : TopologicalSpace X
inst_2 : OrderTopology X
α : Type u_2
inst_3 : LinearOrder α
inst_4 : LocallyFiniteOrder α
inst_5 : NoMaxOrder X
inst_6 : NoMinOrder X
f g : α → X
hl : Tendsto f atTop atTop
hu : Tendsto g atBot atBot
x : X
h : Nonempty α
x_L : X
hx_L : x_L < x
⊢ ∃ t ∈ 𝓝 x, Set.Finite.{u_2} (α := α) {i : α | ((fun (n : α) ↦ Icc (f n) (g n)) i ∩ t).Nonempty}
have inr : ∀ (x_R : X) (hx_R : x < x_R),
  ∃ t ∈ 𝓝 x, Set.Finite.{u_2} (α := α) {i : α | ((fun (n : α) ↦ Icc (f n) (g n)) i ∩ t).Nonempty}
Tactic: obtain ⟨x_R, hx_R⟩ := exists_gt x
-- Lean 4 proof step from Mathlib.Topology.Order.AtTopBotIxx (goal)
Goal:
X : Type u_1
inst : LinearOrder X
inst_1 : TopologicalSpace X
inst_2 : OrderTopology X
α : Type u_2
inst_3 : LinearOrder α
inst_4 : LocallyFiniteOrder α
inst_5 : NoMaxOrder X
inst_6 : NoMinOrder X
f g : α → X
hl : Tendsto f atTop atTop
hu : Tendsto g atBot atBot
x : X
h : Nonempty α
x_L : X
hx_L : x_L < x
x_R : X
hx_R : x < x_R
⊢ ∃ t ∈ 𝓝 x, Set.Finite.{u_2} (α := α) {i : α | ((fun (n : α) ↦ Icc (f n) (g n)) i ∩ t).Nonempty}
have inr : ∀ (a_L : α) (ha_L : ∀ a ≤ a_L, g a ≤ x_L),
  ∃ t ∈ 𝓝 x, Set.Finite.{u_2} (α := α) {i : α | ((fun (n : α) ↦ Icc (f n) (g n)) i ∩ t).Nonempty}
Tactic: obtain ⟨a_L, ha_L : ∀ a ≤ a_L, g a ≤ x_L⟩ :=
    hu.eventually_le_atBot x_L |>.exists_forall_of_atBot
-- Lean 4 proof step from Mathlib.Topology.Order.AtTopBotIxx (goal)
Goal:
X : Type u_1
inst : LinearOrder X
inst_1 : TopologicalSpace X
inst_2 : OrderTopology X
α : Type u_2
inst_3 : LinearOrder α
inst_4 : LocallyFiniteOrder α
inst_5 : NoMaxOrder X
inst_6 : NoMinOrder X
f g : α → X
hl : Tendsto f atTop atTop
hu : Tendsto g atBot atBot
x : X
h : Nonempty α
x_L : X
hx_L : x_L < x
x_R : X
hx_R : x < x_R
a_L : α
ha_L : ∀ a ≤ a_L, g a ≤ x_L
⊢ ∃ t ∈ 𝓝 x, Set.Finite.{u_2} (α := α) {i : α | ((fun (n : α) ↦ Icc (f n) (g n)) i ∩ t).Nonempty}
have inr : ∀ (a_R : α) (ha_R : ∀ a ≥ a_R, x_R ≤ f a),
  ∃ t ∈ 𝓝 x, Set.Finite.{u_2} (α := α) {i : α | ((fun (n : α) ↦ Icc (f n) (g n)) i ∩ t).Nonempty}
Tactic: obtain ⟨a_R, ha_R : ∀ a ≥ a_R, x_R ≤ f a⟩ :=
    hl.eventually_ge_atTop x_R |>.exists_forall_of_atTop
-- Lean 4 proof step from Mathlib.Topology.Order.AtTopBotIxx (goal)
Goal:
X : Type u_1
inst : LinearOrder X
inst_1 : TopologicalSpace X
inst_2 : OrderTopology X
α : Type u_2
inst_3 : LinearOrder α
inst_4 : LocallyFiniteOrder α
inst_5 : NoMaxOrder X
inst_6 : NoMinOrder X
f g : α → X
hl : Tendsto f atTop atTop
hu : Tendsto g atBot atBot
x : X
h : Nonempty α
x_L : X
hx_L : x_L < x
x_R : X
hx_R : x < x_R
a_L : α
ha_L : ∀ a ≤ a_L, g a ≤ x_L
a_R : α
ha_R : ∀ a ≥ a_R, x_R ≤ f a
⊢ ∃ t ∈ 𝓝 x, Set.Finite.{u_2} (α := α) {i : α | ((fun (n : α) ↦ Icc (f n) (g n)) i ∩ t).Nonempty}
have inr : {i : α | ((fun (n : α) ↦ Icc (f n) (g n)) i ∩ Ioo x_L x_R).Nonempty} ⊆ Icc a_L a_R
Tactic: refine ⟨Ioo x_L x_R, Ioo_mem_nhds hx_L hx_R, (finite_Icc a_L a_R).subset ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Order.AtTopBotIxx (goal)
Goal:
X : Type u_1
inst : LinearOrder X
inst_1 : TopologicalSpace X
inst_2 : OrderTopology X
α : Type u_2
inst_3 : LinearOrder α
inst_4 : LocallyFiniteOrder α
inst_5 : NoMaxOrder X
inst_6 : NoMinOrder X
f g : α → X
hl : Tendsto f atTop atTop
hu : Tendsto g atBot atBot
x : X
h : Nonempty α
x_L : X
hx_L : x_L < x
x_R : X
hx_R : x < x_R
a_L : α
ha_L : ∀ a ≤ a_L, g a ≤ x_L
a_R : α
ha_R : ∀ a ≥ a_R, x_R ≤ f a
n : α
y : X
hf : f n ≤ y
hg : y ≤ g n
hxL : x_L < y
hxR : y < x_R
⊢ n ∈ Icc a_L a_R
have inr : a_L ≤ n
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.Order.AtTopBotIxx (goal)
Goal:
X : Type u_1
inst : LinearOrder X
inst_1 : TopologicalSpace X
inst_2 : OrderTopology X
α : Type u_2
inst_3 : LinearOrder α
inst_4 : LocallyFiniteOrder α
inst_5 : NoMaxOrder X
inst_6 : NoMinOrder X
f g : α → X
hl : Tendsto f atTop atTop
hu : Tendsto g atBot atBot
x : X
h : Nonempty α
x_L : X
hx_L : x_L < x
x_R : X
hx_R : x < x_R
a_L : α
ha_L : ∀ a ≤ a_L, g a ≤ x_L
a_R : α
ha_R : ∀ a ≥ a_R, x_R ≤ f a
n : α
y : X
hf : f n ≤ y
hg : y ≤ g n
hxL : x_L < y
hxR : y < x_R
inr : a_L ≤ n
⊢ n ∈ Icc a_L a_R
have inr₁ : n ≤ a_R
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.Order.AtTopBotIxx (goal)
Goal:
X : Type u_1
inst : LinearOrder X
inst_1 : TopologicalSpace X
inst_2 : OrderTopology X
α : Type u_2
inst_3 : LinearOrder α
inst_4 : LocallyFiniteOrder α
inst_5 : NoMaxOrder X
inst_6 : NoMinOrder X
f g : α → X
hl : Tendsto f atTop atTop
hu : Tendsto g atBot atBot
x : X
h : Nonempty α
x_L : X
hx_L : x_L < x
x_R : X
hx_R : x < x_R
a_L : α
ha_L : ∀ a ≤ a_L, g a ≤ x_L
a_R : α
ha_R : ∀ a ≥ a_R, x_R ≤ f a
n : α
y : X
hf : f n ≤ y
hg : y ≤ g n
hxL : x_L < y
hxR : y < x_R
⊢ a_L ≤ n
have inr : ∀ (hxL : n < a_L), y ≤ x_L
Tactic: contrapose! hxL
Cleared hypotheses: hxL
-- Lean 4 proof step from Mathlib.Topology.Order.AtTopBotIxx (goal)
Goal:
X : Type u_1
inst : LinearOrder X
inst_1 : TopologicalSpace X
inst_2 : OrderTopology X
α : Type u_2
inst_3 : LinearOrder α
inst_4 : LocallyFiniteOrder α
inst_5 : NoMaxOrder X
inst_6 : NoMinOrder X
f g : α → X
hl : Tendsto f atTop atTop
hu : Tendsto g atBot atBot
x : X
h : Nonempty α
x_L : X
hx_L : x_L < x
x_R : X
hx_R : x < x_R
a_L : α
ha_L : ∀ a ≤ a_L, g a ≤ x_L
a_R : α
ha_R : ∀ a ≥ a_R, x_R ≤ f a
n : α
y : X
hf : f n ≤ y
hg : y ≤ g n
hxL : x_L < y
hxR : y < x_R
⊢ n ≤ a_R
have inr : ∀ (hxR : a_R < n), x_R ≤ y
Tactic: contrapose! hxR
Cleared hypotheses: hxR
-- Lean 4 proof step from Mathlib.Topology.Order.Basic (goal)
Goal:
α : Type u
β : Type v
γ : Type w
ts : TopologicalSpace α
inst : Preorder α
inst_1 : OrderTopology α
inst_2 : Countable α
⊢ SecondCountableTopology α
have refine_1 : Set.Countable.{u} (α := Set α) {s : Set α | ∃ (a : α), s = Ioi a ∨ s = Iio a}
Tactic: refine ⟨{ s : Set α | ∃ a, s = Ioi a ∨ s = Iio a }, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Order.Basic (goal)
Goal:
α : Type u
β : Type v
γ : Type w
ts : TopologicalSpace α
inst : Preorder α
inst_1 : OrderTopology α
inst_2 : Countable α
refine_1 : Set.Countable.{u} (α := Set α) {s : Set α | ∃ (a : α), s = Ioi a ∨ s = Iio a}
⊢ SecondCountableTopology α
have refine_2 : ts = generateFrom {s : Set α | ∃ (a : α), s = Ioi a ∨ s = Iio a}
Tactic: refine ⟨{ s : Set α | ∃ a, s = Ioi a ∨ s = Iio a }, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Order.Basic (goal)
Goal:
α : Type u
β : Type v
γ : Type w
ts : TopologicalSpace α
inst : Preorder α
t : OrderTopology α
⊢ OrderTopology.{u} αᵒᵈ
have topology_eq_generate_intervals : Eq.{u + 1} (α := TopologicalSpace αᵒᵈ) OrderDual.instTopologicalSpace (Preorder.topology αᵒᵈ)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.Order.Basic (goal)
Goal:
α : Type u
β : Type v
γ : Type w
ts : TopologicalSpace α
inst : Preorder α
t : OrderTopology α
⊢ Eq.{u + 1} (α := TopologicalSpace αᵒᵈ) OrderDual.instTopologicalSpace (Preorder.topology αᵒᵈ)
have topology_eq_generate_intervals : ∀ [t : OrderTopology α], Eq.{u + 1} (α := TopologicalSpace αᵒᵈ) OrderDual.instTopologicalSpace (Preorder.topology αᵒᵈ)
Tactic: rcases t.topology_eq_generate_intervals with rfl
Cleared hypotheses: ts, t
-- Lean 4 proof step from Mathlib.Topology.Order.Basic (goal)
Goal:
α : Type u
β : Type v
γ : Type w
inst : Preorder α
t : OrderTopology α
⊢ Eq.{u + 1} (α := TopologicalSpace αᵒᵈ) OrderDual.instTopologicalSpace (Preorder.topology αᵒᵈ)
have topology_eq_generate_intervals : Eq.{u + 1} (α := TopologicalSpace αᵒᵈ) OrderDual.instTopologicalSpace
  (generateFrom {s : Set αᵒᵈ | ∃ (a : αᵒᵈ), s = Iio a ∨ s = Ioi a})
Tactic: simp_rw [Preorder.topology, or_comm]
-- Lean 4 proof step from Mathlib.Topology.Order.Basic (goal)
Goal:
α : Type u
β : Type v
ts : TopologicalSpace α
inst : Preorder α
inst_1 : OrderTopology α
inst_2 : TopologicalSpace β
f : β → α
⊢ Continuous[inst_2, ts] f ↔ ∀ (a : α), IsOpen[inst_2] (f ⁻¹' Ioi a) ∧ IsOpen[inst_2] (f ⁻¹' Iio a)
have simp_rw : (∀ (s : Set α),
    Membership.mem (γ := Set (Set α)) {s : Set α | ∃ (a : α), s = Ioi a ∨ s = Iio a} s → IsOpen[inst_2] (f ⁻¹' s)) ↔
  ∀ (a : α), IsOpen[inst_2] (f ⁻¹' Ioi a) ∧ IsOpen[inst_2] (f ⁻¹' Iio a)
Tactic: simp_rw +instances [OrderTopology.topology_eq_generate_intervals, continuous_generateFrom_iff]
-- Lean 4 proof step from Mathlib.Topology.Order.Basic (goal)
Goal:
α : Type u
ts : TopologicalSpace α
inst : Preorder α
t : OrderTopology α
s : Set α
⊢ IsOpen[ts] s ↔ GenerateOpen {s : Set α | ∃ (a : α), s = Ioi a ∨ s = Iio a} s
have rw : IsOpen[Preorder.topology α] s ↔ GenerateOpen {s : Set α | ∃ (a : α), s = Ioi a ∨ s = Iio a} s
Tactic: rw [t.topology_eq_generate_intervals]
-- Lean 4 proof step from Mathlib.Topology.Order.Basic (goal)
Goal:
α : Type u
ts : TopologicalSpace α
inst : Preorder α
inst_1 : OrderTopology α
a : α
⊢ 𝓝 a = (⨅ b ∈ Iio a, 𝓟 (Ioi b)) ⊓ ⨅ b ∈ Ioi a, 𝓟 (Iio b)
have rw : Eq.{u + 1} (α := Filter α)
  (⨅ (s : Set α),
    ⨅ (_ :
      Membership.mem (γ := Set (Set α))
        {s : Set α | a ∈ s ∧ Membership.mem (γ := Set (Set α)) {s : Set α | ∃ (a : α), s = Ioi a ∨ s = Iio a} s} s),
      𝓟 s)
  ((⨅ b ∈ Iio a, 𝓟 (Ioi b)) ⊓ ⨅ b ∈ Ioi a, 𝓟 (Iio b))
Tactic: rw [OrderTopology.topology_eq_generate_intervals (α := α), nhds_generateFrom]
-- Lean 4 proof step from Mathlib.Topology.Order.Basic (goal)
Goal:
α : Type u
ts : TopologicalSpace α
inst : Preorder α
inst_1 : OrderTopology α
a : α
⊢ Eq.{u + 1} (α := Filter α)
    (⨅ (s : Set α),
      ⨅ (_ :
        Membership.mem (γ := Set (Set α))
          {s : Set α | a ∈ s ∧ Membership.mem (γ := Set (Set α)) {s : Set α | ∃ (a : α), s = Ioi a ∨ s = Iio a} s} s),
        𝓟 s)
    ((⨅ b ∈ Iio a, 𝓟 (Ioi b)) ⊓ ⨅ b ∈ Ioi a, 𝓟 (Iio b))
have simp_rw : Eq.{u + 1} (α := Filter α) (⨅ (s : Set α), ⨅ (_ : a ∈ s ∧ ∃ (a : α), s = Ioi a ∨ s = Iio a), 𝓟 s)
  ((⨅ b ∈ Iio a, 𝓟 (Ioi b)) ⊓ ⨅ b ∈ Ioi a, 𝓟 (Iio b))
Tactic: simp_rw [mem_setOf_eq, @and_comm (a ∈ _), exists_or, or_and_right, iInf_or, iInf_and,
    iInf_exists, iInf_inf_eq, iInf_comm (ι := Set α), iInf_iInf_eq_left, mem_Ioi, mem_Iio]
-- Lean 4 proof step from Mathlib.Topology.Order.Basic (goal)
Goal:
α : Type u
ts : TopologicalSpace α
inst : Preorder α
inst_1 : OrderTopology α
a : α
simp_rw :
  Eq.{u + 1} (α := Filter α) (⨅ (s : Set α), ⨅ (_ : a ∈ s ∧ ∃ (a : α), s = Ioi a ∨ s = Iio a), 𝓟 s)
    ((⨅ b ∈ Iio a, 𝓟 (Ioi b)) ⊓ ⨅ b ∈ Ioi a, 𝓟 (Iio b))
⊢ Eq.{u + 1} (α := Filter α)
    (⨅ (s : Set α),
      ⨅ (_ :
        Membership.mem (γ := Set (Set α))
          {s : Set α | a ∈ s ∧ Membership.mem (γ := Set (Set α)) {s : Set α | ∃ (a : α), s = Ioi a ∨ s = Iio a} s} s),
        𝓟 s)
    ((⨅ b ∈ Iio a, 𝓟 (Ioi b)) ⊓ ⨅ b ∈ Ioi a, 𝓟 (Iio b))
have simp_rw₁ : Eq.{u + 1} (α := Filter α) (⨅ (s : Set α), ⨅ (_ : (∃ (a : α), s = Ioi a ∨ s = Iio a) ∧ a ∈ s), 𝓟 s)
  ((⨅ b ∈ Iio a, 𝓟 (Ioi b)) ⊓ ⨅ b ∈ Ioi a, 𝓟 (Iio b))
Tactic: simp_rw [mem_setOf_eq, @and_comm (a ∈ _), exists_or, or_and_right, iInf_or, iInf_and,
    iInf_exists, iInf_inf_eq, iInf_comm (ι := Set α), iInf_iInf_eq_left, mem_Ioi, mem_Iio]
-- Lean 4 proof step from Mathlib.Topology.Order.Basic (goal)
Goal:
α : Type u
ts : TopologicalSpace α
inst : Preorder α
inst_1 : OrderTopology α
a : α
simp_rw :
  Eq.{u + 1} (α := Filter α) (⨅ (s : Set α), ⨅ (_ : a ∈ s ∧ ∃ (a : α), s = Ioi a ∨ s = Iio a), 𝓟 s)
    ((⨅ b ∈ Iio a, 𝓟 (Ioi b)) ⊓ ⨅ b ∈ Ioi a, 𝓟 (Iio b))
simp_rw₁ :
  Eq.{u + 1} (α := Filter α) (⨅ (s : Set α), ⨅ (_ : (∃ (a : α), s = Ioi a ∨ s = Iio a) ∧ a ∈ s), 𝓟 s)
    ((⨅ b ∈ Iio a, 𝓟 (Ioi b)) ⊓ ⨅ b ∈ Ioi a, 𝓟 (Iio b))
⊢ Eq.{u + 1} (α := Filter α)
    (⨅ (s : Set α),
      ⨅ (_ :
        Membership.mem (γ := Set (Set α))
          {s : Set α | a ∈ s ∧ Membership.mem (γ := Set (Set α)) {s : Set α | ∃ (a : α), s = Ioi a ∨ s = Iio a} s} s),
        𝓟 s)
    ((⨅ b ∈ Iio a, 𝓟 (Ioi b)) ⊓ ⨅ b ∈ Ioi a, 𝓟 (Iio b))
have simp_rw₂ : Eq.{u + 1} (α := Filter α) (⨅ (s : Set α), ⨅ (_ : ((∃ (x : α), s = Ioi x) ∨ ∃ (x : α), s = Iio x) ∧ a ∈ s), 𝓟 s)
  ((⨅ b ∈ Iio a, 𝓟 (Ioi b)) ⊓ ⨅ b ∈ Ioi a, 𝓟 (Iio b))
Tactic: simp_rw [mem_setOf_eq, @and_comm (a ∈ _), exists_or, or_and_right, iInf_or, iInf_and,
    iInf_exists, iInf_inf_eq, iInf_comm (ι := Set α), iInf_iInf_eq_left, mem_Ioi, mem_Iio]
-- Lean 4 proof step from Mathlib.Topology.Order.Basic (goal)
Goal:
α : Type u
ts : TopologicalSpace α
inst : Preorder α
inst_1 : OrderTopology α
a : α
simp_rw :
  Eq.{u + 1} (α := Filter α) (⨅ (s : Set α), ⨅ (_ : a ∈ s ∧ ∃ (a : α), s = Ioi a ∨ s = Iio a), 𝓟 s)
    ((⨅ b ∈ Iio a, 𝓟 (Ioi b)) ⊓ ⨅ b ∈ Ioi a, 𝓟 (Iio b))
simp_rw₁ :
  Eq.{u + 1} (α := Filter α) (⨅ (s : Set α), ⨅ (_ : (∃ (a : α), s = Ioi a ∨ s = Iio a) ∧ a ∈ s), 𝓟 s)
    ((⨅ b ∈ Iio a, 𝓟 (Ioi b)) ⊓ ⨅ b ∈ Ioi a, 𝓟 (Iio b))
simp_rw₂ :
  Eq.{u + 1} (α := Filter α) (⨅ (s : Set α), ⨅ (_ : ((∃ (x : α), s = Ioi x) ∨ ∃ (x : α), s = Iio x) ∧ a ∈ s), 𝓟 s)
    ((⨅ b ∈ Iio a, 𝓟 (Ioi b)) ⊓ ⨅ b ∈ Ioi a, 𝓟 (Iio b))
⊢ Eq.{u + 1} (α := Filter α)
    (⨅ (s : Set α),
      ⨅ (_ :
        Membership.mem (γ := Set (Set α))
          {s : Set α | a ∈ s ∧ Membership.mem (γ := Set (Set α)) {s : Set α | ∃ (a : α), s = Ioi a ∨ s = Iio a} s} s),
        𝓟 s)
    ((⨅ b ∈ Iio a, 𝓟 (Ioi b)) ⊓ ⨅ b ∈ Ioi a, 𝓟 (Iio b))
have simp_rw₃ : Eq.{u + 1} (α := Filter α) (⨅ (s : Set α), ⨅ (_ : (∃ (x : α), s = Ioi x) ∧ a ∈ s ∨ (∃ (x : α), s = Iio x) ∧ a ∈ s), 𝓟 s)
  ((⨅ b ∈ Iio a, 𝓟 (Ioi b)) ⊓ ⨅ b ∈ Ioi a, 𝓟 (Iio b))
Tactic: simp_rw [mem_setOf_eq, @and_comm (a ∈ _), exists_or, or_and_right, iInf_or, iInf_and,
    iInf_exists, iInf_inf_eq, iInf_comm (ι := Set α), iInf_iInf_eq_left, mem_Ioi, mem_Iio]