awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.Order.LeftRightLim (goal)
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : ConditionallyCompleteLinearOrder β
inst_2 : TopologicalSpace β
inst_3 : OrderTopology β
f : α → β
hf : Monotone f
x y : α
h : x < y
this_1 : TopologicalSpace α := Preorder.topology α
this : OrderTopology α
⊢ f x ≤ leftLim f y
have inl : ∀ (h' : 𝓝[<] y = ⊥), f x ≤ leftLim f y
Tactic: rcases eq_or_ne (𝓝[<] y) ⊥ with (h' | h')
-- Lean 4 proof step from Mathlib.Topology.Order.LeftRightLim (goal)
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : ConditionallyCompleteLinearOrder β
inst_2 : TopologicalSpace β
inst_3 : OrderTopology β
f : α → β
hf : Monotone f
x y : α
h : x < y
this_1 : TopologicalSpace α := Preorder.topology α
this : OrderTopology α
inl : ∀ (h' : 𝓝[<] y = ⊥), f x ≤ leftLim f y
⊢ f x ≤ leftLim f y
have inr : ∀ (h' : 𝓝[<] y ≠ ⊥), f x ≤ leftLim f y
Tactic: rcases eq_or_ne (𝓝[<] y) ⊥ with (h' | h')
-- Lean 4 proof step from Mathlib.Topology.Order.LeftRightLim (goal)
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : ConditionallyCompleteLinearOrder β
inst_2 : TopologicalSpace β
inst_3 : OrderTopology β
f : α → β
hf : Monotone f
x y : α
h : x < y
this_1 : TopologicalSpace α := Preorder.topology α
this : OrderTopology α
h' : 𝓝[<] y = ⊥
⊢ f x ≤ leftLim f y
have inl : f x ≤ f y
Tactic: rw [leftLim_eq_of_eq_bot _ h']
-- Lean 4 proof step from Mathlib.Topology.Order.LeftRightLim (goal)
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : ConditionallyCompleteLinearOrder β
inst_2 : TopologicalSpace β
inst_3 : OrderTopology β
f : α → β
hf : Monotone f
x y : α
h : x < y
this_1 : TopologicalSpace α := Preorder.topology α
this : OrderTopology α
h' : 𝓝[<] y ≠ ⊥
⊢ f x ≤ leftLim f y
have inr : f x ≤ sSup (f '' Iio y)
Tactic: rw [leftLim_eq_sSup hf h']
-- Lean 4 proof step from Mathlib.Topology.Order.LeftRightLim (goal)
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : ConditionallyCompleteLinearOrder β
inst_2 : TopologicalSpace β
inst_3 : OrderTopology β
f : α → β
hf : Monotone f
x y : α
h : x < y
this_1 : TopologicalSpace α := Preorder.topology α
this : OrderTopology α
h' : 𝓝[<] y ≠ ⊥
⊢ f x ≤ sSup (f '' Iio y)
have inr : f y ∈ upperBounds (f '' Iio y)
Tactic: refine le_csSup ⟨f y, ?_⟩ (mem_image_of_mem _ h)
-- Lean 4 proof step from Mathlib.Topology.Order.LeftRightLim (goal)
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : ConditionallyCompleteLinearOrder β
inst_2 : TopologicalSpace β
inst_3 : OrderTopology β
f : α → β
hf : Monotone f
x y : α
h : x < y
this_1 : TopologicalSpace α := Preorder.topology α
this : OrderTopology α
h' : 𝓝[<] y ≠ ⊥
⊢ f y ∈ upperBounds (f '' Iio y)
have inr : ∀ a < y, f a ≤ f y
Tactic: simp only [upperBounds, mem_image, mem_Iio, forall_exists_index, and_imp,
    forall_apply_eq_imp_iff₂, mem_setOf_eq]
-- Lean 4 proof step from Mathlib.Topology.Order.LeftRightLim (goal)
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : ConditionallyCompleteLinearOrder β
inst_2 : TopologicalSpace β
inst_3 : OrderTopology β
f : α → β
hf : Monotone f
x y : α
h : x ≤ y
⊢ leftLim f x ≤ leftLim f y
have inl : ∀ (h : x ≤ x), leftLim f x ≤ leftLim f x
Tactic: rcases eq_or_lt_of_le h with (rfl | hxy)
Cleared hypotheses: y, h
-- Lean 4 proof step from Mathlib.Topology.Order.LeftRightLim (goal)
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : ConditionallyCompleteLinearOrder β
inst_2 : TopologicalSpace β
inst_3 : OrderTopology β
f : α → β
hf : Monotone f
x y : α
h : x ≤ y
inl : ∀ (h : x ≤ x), leftLim f x ≤ leftLim f x
⊢ leftLim f x ≤ leftLim f y
have inr : ∀ (hxy : x < y), leftLim f x ≤ leftLim f y
Tactic: rcases eq_or_lt_of_le h with (rfl | hxy)
-- Lean 4 proof step from Mathlib.Topology.Order.LeftRightLim (hypothesis)
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : ConditionallyCompleteLinearOrder β
inst_2 : TopologicalSpace β
inst_3 : OrderTopology β
f : α → β
hf : Monotone f
x y : α
h : x < y
this : TopologicalSpace α := Preorder.topology α
⊢ rightLim f x ≤ leftLim f y
have this₁ : OrderTopology α
Tactic: haveI : OrderTopology α := ⟨rfl⟩
-- Lean 4 proof step from Mathlib.Topology.Order.LeftRightLim (goal)
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : ConditionallyCompleteLinearOrder β
inst_2 : TopologicalSpace β
inst_3 : OrderTopology β
f : α → β
hf : Monotone f
x y : α
h : x < y
this_1 : TopologicalSpace α := Preorder.topology α
this : OrderTopology α
⊢ rightLim f x ≤ leftLim f y
have inl : ∀ (h' : 𝓝[<] y = ⊥), rightLim f x ≤ leftLim f y
Tactic: rcases eq_or_neBot (𝓝[<] y) with (h' | h')
-- Lean 4 proof step from Mathlib.Topology.Order.LeftRightLim (goal)
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : ConditionallyCompleteLinearOrder β
inst_2 : TopologicalSpace β
inst_3 : OrderTopology β
f : α → β
hf : Monotone f
x y : α
h : x < y
this_1 : TopologicalSpace α := Preorder.topology α
this : OrderTopology α
inl : ∀ (h' : 𝓝[<] y = ⊥), rightLim f x ≤ leftLim f y
⊢ rightLim f x ≤ leftLim f y
have inr : ∀ (h' : (𝓝[<] y).NeBot), rightLim f x ≤ leftLim f y
Tactic: rcases eq_or_neBot (𝓝[<] y) with (h' | h')
-- Lean 4 proof step from Mathlib.Topology.Order.LeftRightLim (goal)
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : ConditionallyCompleteLinearOrder β
inst_2 : TopologicalSpace β
inst_3 : OrderTopology β
f : α → β
hf : Monotone f
x y : α
h : x < y
this_1 : TopologicalSpace α := Preorder.topology α
this : OrderTopology α
h' : (𝓝[<] y).NeBot
⊢ rightLim f x ≤ leftLim f y
have inr : ∀ (a : α) (xa : x < a) (ay : a < y), rightLim f x ≤ leftLim f y
Tactic: obtain ⟨a, ⟨xa, ay⟩⟩ : (Ioo x y).Nonempty := nonempty_of_mem (Ioo_mem_nhdsLT h)
-- Lean 4 proof step from Mathlib.Topology.Order.LeftRightLim (goal)
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : ConditionallyCompleteLinearOrder β
inst_2 : TopologicalSpace β
inst_3 : OrderTopology β
f : α → β
hf : Monotone f
inst_4 : TopologicalSpace α
inst_5 : OrderTopology α
x : α
⊢ Tendsto f (𝓝[<] x) (𝓝[≤] leftLim f x)
have apply : ∀ᶠ (x_1 : α) in 𝓝[<] x, f x_1 ∈ Iic (leftLim f x)
Tactic: apply tendsto_nhdsWithin_of_tendsto_nhds_of_eventually_within f (hf.tendsto_leftLim x)
-- Lean 4 proof step from Mathlib.Topology.Order.LeftRightLim (goal)
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : ConditionallyCompleteLinearOrder β
inst_2 : TopologicalSpace β
inst_3 : OrderTopology β
f : α → β
hf : Monotone f
inst_4 : TopologicalSpace α
inst_5 : OrderTopology α
x : α
⊢ ∀ᶠ (x_1 : α) in 𝓝[<] x, f x_1 ∈ Iic (leftLim f x)
have h : ∀ (a : α),
  Membership.mem (γ := Set α)
    {x_1 : α |
      x_1 ∈ Iio x → Membership.mem (γ := Set α) {x_2 : α | (fun (x_3 : α) ↦ f x_3 ∈ Iic (leftLim f x)) x_2} x_1}
    a
Tactic: filter_upwards [@self_mem_nhdsWithin _ _ x (Iio x)] with y hy using hf.le_leftLim hy
-- Lean 4 proof step from Mathlib.Topology.Order.LeftRightLim (goal)
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : ConditionallyCompleteLinearOrder β
inst_2 : TopologicalSpace β
inst_3 : OrderTopology β
f : α → β
hf : Monotone f
inst_4 : TopologicalSpace α
inst_5 : OrderTopology α
x : α
h :
  ∀ (a : α),
    Membership.mem (γ := Set α)
      {x_1 : α |
        x_1 ∈ Iio x → Membership.mem (γ := Set α) {x_2 : α | (fun (x_3 : α) ↦ f x_3 ∈ Iic (leftLim f x)) x_2} x_1}
      a
⊢ ∀ᶠ (x_1 : α) in 𝓝[<] x, f x_1 ∈ Iic (leftLim f x)
have h₁ : ∀ a ∈ Iio x, f a ∈ Iic (leftLim f x)
Tactic: filter_upwards [@self_mem_nhdsWithin _ _ x (Iio x)] with y hy using hf.le_leftLim hy
-- Lean 4 proof step from Mathlib.Topology.Order.LeftRightLim (goal)
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : ConditionallyCompleteLinearOrder β
inst_2 : TopologicalSpace β
inst_3 : OrderTopology β
f : α → β
hf : Monotone f
x : α
inst_4 : TopologicalSpace α
inst_5 : OrderTopology α
⊢ ContinuousWithinAt f (Iio x) x ↔ leftLim f x = f x
have inl : ∀ (h' : 𝓝[<] x = ⊥), ContinuousWithinAt f (Iio x) x ↔ leftLim f x = f x
Tactic: rcases eq_or_ne (𝓝[<] x) ⊥ with (h' | h')
-- Lean 4 proof step from Mathlib.Topology.Order.LeftRightLim (goal)
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : ConditionallyCompleteLinearOrder β
inst_2 : TopologicalSpace β
inst_3 : OrderTopology β
f : α → β
hf : Monotone f
x : α
inst_4 : TopologicalSpace α
inst_5 : OrderTopology α
inl : ∀ (h' : 𝓝[<] x = ⊥), ContinuousWithinAt f (Iio x) x ↔ leftLim f x = f x
⊢ ContinuousWithinAt f (Iio x) x ↔ leftLim f x = f x
have inr : ∀ (h' : 𝓝[<] x ≠ ⊥), ContinuousWithinAt f (Iio x) x ↔ leftLim f x = f x
Tactic: rcases eq_or_ne (𝓝[<] x) ⊥ with (h' | h')
-- Lean 4 proof step from Mathlib.Topology.Order.LeftRightLim (hypothesis)
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : ConditionallyCompleteLinearOrder β
inst_2 : TopologicalSpace β
inst_3 : OrderTopology β
f : α → β
hf : Monotone f
x : α
inst_4 : TopologicalSpace α
inst_5 : OrderTopology α
h' : 𝓝[<] x ≠ ⊥
⊢ ContinuousWithinAt f (Iio x) x ↔ leftLim f x = f x
have this : (𝓝[<] x).NeBot
Tactic: haveI : (𝓝[Iio x] x).NeBot := neBot_iff.2 h'
-- Lean 4 proof step from Mathlib.Topology.Order.LeftRightLim (goal)
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : ConditionallyCompleteLinearOrder β
inst_2 : TopologicalSpace β
inst_3 : OrderTopology β
f : α → β
hf : Monotone f
x : α
inst_4 : TopologicalSpace α
inst_5 : OrderTopology α
h' : 𝓝[<] x ≠ ⊥
this : (𝓝[<] x).NeBot
⊢ ContinuousWithinAt f (Iio x) x ↔ leftLim f x = f x
have inr : ∀ (h : leftLim f x = f x), ContinuousWithinAt f (Iio x) x
Tactic: refine ⟨fun h => tendsto_nhds_unique (hf.tendsto_leftLim x) h.tendsto, fun h => ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Order.LeftRightLim (hypothesis)
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : ConditionallyCompleteLinearOrder β
inst_2 : TopologicalSpace β
inst_3 : OrderTopology β
f : α → β
hf : Monotone f
x : α
inst_4 : TopologicalSpace α
inst_5 : OrderTopology α
h' : 𝓝[<] x ≠ ⊥
this : (𝓝[<] x).NeBot
h : leftLim f x = f x
⊢ ContinuousWithinAt f (Iio x) x
have this₁ : Tendsto f (𝓝[<] x) (𝓝 (leftLim f x))
Tactic: have := hf.tendsto_leftLim x
-- Lean 4 proof step from Mathlib.Topology.Order.LeftRightLim (goal)
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : ConditionallyCompleteLinearOrder β
inst_2 : TopologicalSpace β
inst_3 : OrderTopology β
f : α → β
hf : Monotone f
x : α
inst_4 : TopologicalSpace α
inst_5 : OrderTopology α
h' : 𝓝[<] x ≠ ⊥
this_1 : (𝓝[<] x).NeBot
h : leftLim f x = f x
this : Tendsto f (𝓝[<] x) (𝓝 (leftLim f x))
⊢ ContinuousWithinAt f (Iio x) x
have inr : ∀ (this : Tendsto f (𝓝[<] x) (𝓝 (f x))), ContinuousWithinAt f (Iio x) x
Tactic: rwa [h] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Topology.Order.LeftRightLim (goal)
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : ConditionallyCompleteLinearOrder β
inst_2 : TopologicalSpace β
inst_3 : OrderTopology β
f : α → β
hf : Monotone f
x : α
inst_4 : TopologicalSpace α
inst_5 : OrderTopology α
⊢ ContinuousAt f x ↔ leftLim f x = rightLim f x
have refine_1 : ∀ (h : ContinuousAt f x), leftLim f x = rightLim f x
Tactic: refine ⟨fun h => ?_, fun h => ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Order.LeftRightLim (goal)
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : ConditionallyCompleteLinearOrder β
inst_2 : TopologicalSpace β
inst_3 : OrderTopology β
f : α → β
hf : Monotone f
x : α
inst_4 : TopologicalSpace α
inst_5 : OrderTopology α
refine_1 : ∀ (h : ContinuousAt f x), leftLim f x = rightLim f x
⊢ ContinuousAt f x ↔ leftLim f x = rightLim f x
have refine_2 : ∀ (h : leftLim f x = rightLim f x), ContinuousAt f x
Tactic: refine ⟨fun h => ?_, fun h => ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Order.LeftRightLim (hypothesis)
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : ConditionallyCompleteLinearOrder β
inst_2 : TopologicalSpace β
inst_3 : OrderTopology β
f : α → β
hf : Monotone f
x : α
inst_4 : TopologicalSpace α
inst_5 : OrderTopology α
h : ContinuousAt f x
⊢ leftLim f x = rightLim f x
have A : leftLim f x = f x
Tactic: have A : leftLim f x = f x :=
      hf.continuousWithinAt_Iio_iff_leftLim_eq.1 h.continuousWithinAt
-- Lean 4 proof step from Mathlib.Topology.Order.LeftRightLim (hypothesis)
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : ConditionallyCompleteLinearOrder β
inst_2 : TopologicalSpace β
inst_3 : OrderTopology β
f : α → β
hf : Monotone f
x : α
inst_4 : TopologicalSpace α
inst_5 : OrderTopology α
h : ContinuousAt f x
A : leftLim f x = f x
⊢ leftLim f x = rightLim f x
have B : rightLim f x = f x
Tactic: have B : rightLim f x = f x :=
      hf.continuousWithinAt_Ioi_iff_rightLim_eq.1 h.continuousWithinAt
-- Lean 4 proof step from Mathlib.Topology.Order.LeftRightLim (goal)
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : ConditionallyCompleteLinearOrder β
inst_2 : TopologicalSpace β
inst_3 : OrderTopology β
f : α → β
hf : Monotone f
x : α
inst_4 : TopologicalSpace α
inst_5 : OrderTopology α
h : leftLim f x = rightLim f x
⊢ leftLim f x = f x
have apply : f x ≤ leftLim f x
Tactic: apply le_antisymm (leftLim_le hf (le_refl _))
-- Lean 4 proof step from Mathlib.Topology.Order.LeftRightLim (goal)
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : ConditionallyCompleteLinearOrder β
inst_2 : TopologicalSpace β
inst_3 : OrderTopology β
f : α → β
hf : Monotone f
x : α
inst_4 : TopologicalSpace α
inst_5 : OrderTopology α
h : leftLim f x = rightLim f x
⊢ f x ≤ leftLim f x
have rw : f x ≤ rightLim f x
Tactic: rw [h]
-- Lean 4 proof step from Mathlib.Topology.Order.LeftRightLim (hypothesis)
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : ConditionallyCompleteLinearOrder β
inst_2 : TopologicalSpace β
inst_3 : OrderTopology β
f : α → β
hf : Monotone f
x : α
inst_4 : TopologicalSpace α
inst_5 : OrderTopology α
h : leftLim f x = rightLim f x
⊢ ContinuousAt f x
have h' : leftLim f x = f x
Tactic: have h' : leftLim f x = f x := by
      apply le_antisymm (leftLim_le hf (le_refl _))
      rw [h]
      exact le_rightLim hf (le_refl _)
-- Lean 4 proof step from Mathlib.Topology.Order.LeftRightLim (goal)
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : ConditionallyCompleteLinearOrder β
inst_2 : TopologicalSpace β
inst_3 : OrderTopology β
f : α → β
hf : Monotone f
x : α
inst_4 : TopologicalSpace α
inst_5 : OrderTopology α
h : leftLim f x = rightLim f x
h' : leftLim f x = f x
⊢ ContinuousAt f x
have refine_2 : ContinuousWithinAt f (Iio x) x
Tactic: refine continuousAt_iff_continuous_left'_right'.2 ⟨?_, ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Order.LeftRightLim (goal)
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : ConditionallyCompleteLinearOrder β
inst_2 : TopologicalSpace β
inst_3 : OrderTopology β
f : α → β
hf : Monotone f
x : α
inst_4 : TopologicalSpace α
inst_5 : OrderTopology α
h : leftLim f x = rightLim f x
h' : leftLim f x = f x
refine_2 : ContinuousWithinAt f (Iio x) x
⊢ ContinuousAt f x
have refine_2₁ : ContinuousWithinAt f (Ioi x) x
Tactic: refine continuousAt_iff_continuous_left'_right'.2 ⟨?_, ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Order.LeftRightLim (hypothesis)
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : ConditionallyCompleteLinearOrder β
inst_2 : TopologicalSpace β
inst_3 : OrderTopology β
f : α → β
hf : Monotone f
x : α
inst_4 : TopologicalSpace α
inst_5 : OrderTopology α
h : leftLim f x = rightLim f x
h' : leftLim f x = f x
⊢ ContinuousWithinAt f (Ioi x) x
have h'₁ : rightLim f x = f x
Tactic: rw [h] at h'
Cleared hypotheses: h'
-- Lean 4 proof step from Mathlib.Topology.Order.LeftRightNhds (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
a b : α
hab : a < b
s : Set α
⊢ s ∈ 𝓝[>] a ↔ s ∈ 𝓝[Ioc a b] a
have rw : s ∈ 𝓝[>] a ↔ s ∈ 𝓝[>] a
Tactic: rw [nhdsWithin_Ioc_eq_nhdsGT hab]
-- Lean 4 proof step from Mathlib.Topology.Order.LeftRightNhds (hypothesis)
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
a b : α
hab : a < b
s : Set α
⊢ [s ∈ 𝓝[>] a, s ∈ 𝓝[Ioc a b] a, s ∈ 𝓝[Ioo a b] a, ∃ u ∈ Ioc a b, Ioo a u ⊆ s, ∃ u ∈ Ioi a, Ioo a u ⊆ s].TFAE
have tfae_1_iff_2 : s ∈ 𝓝[>] a ↔ s ∈ 𝓝[Ioc a b] a
Tactic: tfae_have 1 ↔ 2 := by
    rw [nhdsWithin_Ioc_eq_nhdsGT hab]
-- Lean 4 proof step from Mathlib.Topology.Order.LeftRightNhds (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
a b : α
hab : a < b
s : Set α
tfae_1_iff_2 : s ∈ 𝓝[>] a ↔ s ∈ 𝓝[Ioc a b] a
⊢ s ∈ 𝓝[>] a ↔ s ∈ 𝓝[Ioo a b] a
have rw : s ∈ 𝓝[>] a ↔ s ∈ 𝓝[>] a
Tactic: rw [nhdsWithin_Ioo_eq_nhdsGT hab]
-- Lean 4 proof step from Mathlib.Topology.Order.LeftRightNhds (hypothesis)
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
a b : α
hab : a < b
s : Set α
tfae_1_iff_2 : s ∈ 𝓝[>] a ↔ s ∈ 𝓝[Ioc a b] a
⊢ [s ∈ 𝓝[>] a, s ∈ 𝓝[Ioc a b] a, s ∈ 𝓝[Ioo a b] a, ∃ u ∈ Ioc a b, Ioo a u ⊆ s, ∃ u ∈ Ioi a, Ioo a u ⊆ s].TFAE
have tfae_1_iff_3 : s ∈ 𝓝[>] a ↔ s ∈ 𝓝[Ioo a b] a
Tactic: tfae_have 1 ↔ 3 := by
    rw [nhdsWithin_Ioo_eq_nhdsGT hab]
-- Lean 4 proof step from Mathlib.Topology.Order.LeftRightNhds (hypothesis)
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
a b : α
hab : a < b
s : Set α
tfae_1_iff_2 : s ∈ 𝓝[>] a ↔ s ∈ 𝓝[Ioc a b] a
tfae_1_iff_3 : s ∈ 𝓝[>] a ↔ s ∈ 𝓝[Ioo a b] a
⊢ [s ∈ 𝓝[>] a, s ∈ 𝓝[Ioc a b] a, s ∈ 𝓝[Ioo a b] a, ∃ u ∈ Ioc a b, Ioo a u ⊆ s, ∃ u ∈ Ioi a, Ioo a u ⊆ s].TFAE
have tfae_4_to_5 : ∀ (a_1 : ∃ u ∈ Ioc a b, Ioo a u ⊆ s), ∃ u ∈ Ioi a, Ioo a u ⊆ s
Tactic: tfae_have 4 → 5 := fun ⟨u, umem, hu⟩ => ⟨u, umem.1, hu⟩
-- Lean 4 proof step from Mathlib.Topology.Order.LeftRightNhds (hypothesis)
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
a b : α
hab : a < b
s : Set α
tfae_1_iff_2 : s ∈ 𝓝[>] a ↔ s ∈ 𝓝[Ioc a b] a
tfae_1_iff_3 : s ∈ 𝓝[>] a ↔ s ∈ 𝓝[Ioo a b] a
tfae_4_to_5 : ∀ (a_1 : ∃ u ∈ Ioc a b, Ioo a u ⊆ s), ∃ u ∈ Ioi a, Ioo a u ⊆ s
⊢ [s ∈ 𝓝[>] a, s ∈ 𝓝[Ioc a b] a, s ∈ 𝓝[Ioo a b] a, ∃ u ∈ Ioc a b, Ioo a u ⊆ s, ∃ u ∈ Ioi a, Ioo a u ⊆ s].TFAE
have tfae_5_to_1 : ∀ (a_1 : ∃ u ∈ Ioi a, Ioo a u ⊆ s), s ∈ 𝓝[>] a
Tactic: tfae_have 5 → 1
  | ⟨u, hau, hu⟩ => mem_of_superset (Ioo_mem_nhdsGT hau) hu
-- Lean 4 proof step from Mathlib.Topology.Order.LeftRightNhds (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
a b : α
hab : a < b
s : Set α
tfae_1_iff_2 : s ∈ 𝓝[>] a ↔ s ∈ 𝓝[Ioc a b] a
tfae_1_iff_3 : s ∈ 𝓝[>] a ↔ s ∈ 𝓝[Ioo a b] a
tfae_4_to_5 : ∀ (a_1 : ∃ u ∈ Ioc a b, Ioo a u ⊆ s), ∃ u ∈ Ioi a, Ioo a u ⊆ s
tfae_5_to_1 : ∀ (a_1 : ∃ u ∈ Ioi a, Ioo a u ⊆ s), s ∈ 𝓝[>] a
h_1 : s ∈ 𝓝[>] a
h : s ∈ 𝓝[>] a := h_1
⊢ ∃ u ∈ Ioc a b, Ioo a u ⊆ s
have rcases : ∀ (v : Set α) (va : v ∈ 𝓝 a) (hv : v ∩ Ioi a ⊆ s), ∃ u ∈ Ioc a b, Ioo a u ⊆ s
Tactic: rcases mem_nhdsWithin_iff_exists_mem_nhds_inter.1 h with ⟨v, va, hv⟩
-- Lean 4 proof step from Mathlib.Topology.Order.LeftRightNhds (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
a b : α
hab : a < b
s : Set α
tfae_1_iff_2 : s ∈ 𝓝[>] a ↔ s ∈ 𝓝[Ioc a b] a
tfae_1_iff_3 : s ∈ 𝓝[>] a ↔ s ∈ 𝓝[Ioo a b] a
tfae_4_to_5 : ∀ (a_1 : ∃ u ∈ Ioc a b, Ioo a u ⊆ s), ∃ u ∈ Ioi a, Ioo a u ⊆ s
tfae_5_to_1 : ∀ (a_1 : ∃ u ∈ Ioi a, Ioo a u ⊆ s), s ∈ 𝓝[>] a
h_1 : s ∈ 𝓝[>] a
h : s ∈ 𝓝[>] a := h_1
v : Set α
va : v ∈ 𝓝 a
hv : v ∩ Ioi a ⊆ s
⊢ ∃ u ∈ Ioc a b, Ioo a u ⊆ s
have rcases : ∀ (u : α) (au : u ∈ Ioc a b) (hu : Ico a u ⊆ v), ∃ u ∈ Ioc a b, Ioo a u ⊆ s
Tactic: rcases exists_Ico_subset_of_mem_nhds' va hab with ⟨u, au, hu⟩
-- Lean 4 proof step from Mathlib.Topology.Order.LeftRightNhds (hypothesis)
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
a b : α
hab : a < b
s : Set α
tfae_1_iff_2 : s ∈ 𝓝[>] a ↔ s ∈ 𝓝[Ioc a b] a
tfae_1_iff_3 : s ∈ 𝓝[>] a ↔ s ∈ 𝓝[Ioo a b] a
tfae_4_to_5 : ∀ (a_1 : ∃ u ∈ Ioc a b, Ioo a u ⊆ s), ∃ u ∈ Ioi a, Ioo a u ⊆ s
tfae_5_to_1 : ∀ (a_1 : ∃ u ∈ Ioi a, Ioo a u ⊆ s), s ∈ 𝓝[>] a
⊢ [s ∈ 𝓝[>] a, s ∈ 𝓝[Ioc a b] a, s ∈ 𝓝[Ioo a b] a, ∃ u ∈ Ioc a b, Ioo a u ⊆ s, ∃ u ∈ Ioi a, Ioo a u ⊆ s].TFAE
have tfae_1_to_4 : ∀ (a_1 : s ∈ 𝓝[>] a), ∃ u ∈ Ioc a b, Ioo a u ⊆ s
Tactic: tfae_have 1 → 4
  | h => by
    rcases mem_nhdsWithin_iff_exists_mem_nhds_inter.1 h with ⟨v, va, hv⟩
    rcases exists_Ico_subset_of_mem_nhds' va hab with ⟨u, au, hu⟩
    exact ⟨u, au, fun x hx => hv ⟨hu ⟨le_of_lt hx.1, hx.2⟩, hx.1⟩⟩
-- Lean 4 proof step from Mathlib.Topology.Order.LeftRightNhds (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
a : α
⊢ 𝓝[>] a = ⊥ ↔ IsTop a ∨ ∃ (b : α), a ⋖ b
have pos : ∀ (ha : IsTop a), 𝓝[>] a = ⊥ ↔ IsTop a ∨ ∃ (b : α), a ⋖ b
Tactic: by_cases ha : IsTop a
-- Lean 4 proof step from Mathlib.Topology.Order.LeftRightNhds (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
a : α
pos : ∀ (ha : IsTop a), 𝓝[>] a = ⊥ ↔ IsTop a ∨ ∃ (b : α), a ⋖ b
⊢ 𝓝[>] a = ⊥ ↔ IsTop a ∨ ∃ (b : α), a ⋖ b
have neg : ∀ (ha : ¬IsTop a), 𝓝[>] a = ⊥ ↔ IsTop a ∨ ∃ (b : α), a ⋖ b
Tactic: by_cases ha : IsTop a
-- Lean 4 proof step from Mathlib.Topology.Order.LeftRightNhds (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
a : α
ha : ¬IsTop a
⊢ 𝓝[>] a = ⊥ ↔ IsTop a ∨ ∃ (b : α), a ⋖ b
have neg : 𝓝[>] a = ⊥ ↔ ∃ (b : α), a ⋖ b
Tactic: simp only [ha, false_or]
-- Lean 4 proof step from Mathlib.Topology.Order.LeftRightNhds (hypothesis)
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
a : α
ha : ¬IsTop a
⊢ 𝓝[>] a = ⊥ ↔ ∃ (b : α), a ⋖ b
have ha₁ : ∃ (b : α), a < b
Tactic: rw [isTop_iff_isMax, not_isMax_iff] at ha
Cleared hypotheses: ha
-- Lean 4 proof step from Mathlib.Topology.Order.LeftRightNhds (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : SecondCountableTopology α
⊢ Set.Countable.{u_1} (α := α) {x : α | 𝓝[>] x = ⊥}
have simp : Set.Countable.{u_1} (α := α) ({a : α | IsTop a} ∪ {a : α | ∃ (b : α), a ⋖ b})
Tactic: simp only [nhdsGT_eq_bot_iff, setOf_or]
-- Lean 4 proof step from Mathlib.Topology.Order.LeftRightNhds (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : SecondCountableTopology α
s : Set α
t : Set α := {x : α | x ∈ s ∧ 𝓝[s ∩ Ioi x] x = ⊥ ∧ ¬IsTop x}
H : t.Countable
x : α
hx : Membership.mem (γ := Set α) {x : α | x ∈ s ∧ 𝓝[s ∩ Ioi x] x = ⊥} x
⊢ x ∈ t ∪ {x : α | IsTop x}
have pos : ∀ (h'x : IsTop x), x ∈ t ∪ {x : α | IsTop x}
Tactic: by_cases h'x : IsTop x
-- Lean 4 proof step from Mathlib.Topology.Order.LeftRightNhds (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : SecondCountableTopology α
s : Set α
t : Set α := {x : α | x ∈ s ∧ 𝓝[s ∩ Ioi x] x = ⊥ ∧ ¬IsTop x}
H : t.Countable
x : α
hx : Membership.mem (γ := Set α) {x : α | x ∈ s ∧ 𝓝[s ∩ Ioi x] x = ⊥} x
pos : ∀ (h'x : IsTop x), x ∈ t ∪ {x : α | IsTop x}
⊢ x ∈ t ∪ {x : α | IsTop x}
have neg : ∀ (h'x : ¬IsTop x), x ∈ t ∪ {x : α | IsTop x}
Tactic: by_cases h'x : IsTop x
-- Lean 4 proof step from Mathlib.Topology.Order.LeftRightNhds (hypothesis)
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : SecondCountableTopology α
s : Set α
t : Set α := {x : α | x ∈ s ∧ 𝓝[s ∩ Ioi x] x = ⊥ ∧ ¬IsTop x}
H : t.Countable
⊢ Set.Countable.{u_1} (α := α) {x : α | x ∈ s ∧ 𝓝[s ∩ Ioi x] x = ⊥}
have this : {x : α | x ∈ s ∧ 𝓝[s ∩ Ioi x] x = ⊥} ⊆ t ∪ {x : α | IsTop x}
Tactic: have : { x ∈ s | 𝓝[s ∩ Ioi x] x = ⊥ } ⊆ t ∪ {x | IsTop x} := by
      intro x hx
      by_cases h'x : IsTop x
      · simp [h'x]
      · simpa [-sep_and, t, h'x]
-- Lean 4 proof step from Mathlib.Topology.Order.LeftRightNhds (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : OrderTopology α
inst_3 : SecondCountableTopology α
s : Set α
t : Set α := {x : α | x ∈ s ∧ 𝓝[s ∩ Ioi x] x = ⊥ ∧ ¬IsTop x}
H : t.Countable
this : {x : α | x ∈ s ∧ 𝓝[s ∩ Ioi x] x = ⊥} ⊆ t ∪ {x : α | IsTop x}
⊢ Set.Countable.{u_1} (α := α) {x : α | x ∈ s ∧ 𝓝[s ∩ Ioi x] x = ⊥}
have apply : (t ∪ {x : α | IsTop x}).Countable
Tactic: apply Countable.mono this