awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.Order.MonotoneConvergence (goal)
Goal:
α : Type u_1
ι : Type u_3
inst : Preorder ι
inst_1 : TopologicalSpace α
inst_2 : ConditionallyCompletePartialOrderSup α
inst_3 : SupConvergenceClass α
f : ι → α
h_mono : Monotone f
hbdd : BddAbove (range f)
inl : ∀ (h : Eq.{u_3 + 1} (α := Filter ι) atTop ⊥), Tendsto f atTop (𝓝 (⨆ (i : ι), f i))
⊢ Tendsto f atTop (𝓝 (⨆ (i : ι), f i))
have inr : ∀ (h : Ne.{u_3 + 1} (α := Filter ι) atTop ⊥), Tendsto f atTop (𝓝 (⨆ (i : ι), f i))
Tactic: obtain (h | h) := eq_or_ne atTop (⊥ : Filter ι)
-- Lean 4 proof step from Mathlib.Topology.Order.MonotoneConvergence (hypothesis)
Goal:
α : Type u_1
ι : Type u_3
inst : Preorder ι
inst_1 : TopologicalSpace α
inst_2 : ConditionallyCompletePartialOrderSup α
inst_3 : SupConvergenceClass α
f : ι → α
h_mono : Monotone f
hbdd : BddAbove (range f)
h : Ne.{u_3 + 1} (α := Filter ι) atTop ⊥
⊢ Tendsto f atTop (𝓝 (⨆ (i : ι), f i))
have h₁ : Nonempty ι
Tactic: obtain ⟨h₁, h₂⟩ := Filter.atTop_neBot_iff.mp ⟨h⟩
-- Lean 4 proof step from Mathlib.Topology.Order.MonotoneConvergence (hypothesis)
Goal:
α : Type u_1
ι : Type u_3
inst : Preorder ι
inst_1 : TopologicalSpace α
inst_2 : ConditionallyCompletePartialOrderSup α
inst_3 : SupConvergenceClass α
f : ι → α
h_mono : Monotone f
hbdd : BddAbove (range f)
h : Ne.{u_3 + 1} (α := Filter ι) atTop ⊥
h₁ : Nonempty ι
⊢ Tendsto f atTop (𝓝 (⨆ (i : ι), f i))
have h₂ : IsDirectedOrder ι
Tactic: obtain ⟨h₁, h₂⟩ := Filter.atTop_neBot_iff.mp ⟨h⟩
-- Lean 4 proof step from Mathlib.Topology.Order.MonotoneConvergence (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
inst_2 : TopologicalSpace α
inst_3 : TopologicalSpace β
inst_4 : SupConvergenceClass α
inst_5 : SupConvergenceClass β
⊢ SupConvergenceClass (α × β)
have tendsto_coe_atTop_isLUB : ∀ (a : α × β) (s : Set (α × β)),
  IsLUB s a → Tendsto (α := { x : α × β // x ∈ s }) (Subtype.val (p := fun (x : α × β) ↦ x ∈ s)) atTop (𝓝 a)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.Order.MonotoneConvergence (hypothesis)
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
inst_2 : TopologicalSpace α
inst_3 : TopologicalSpace β
inst_4 : SupConvergenceClass α
inst_5 : SupConvergenceClass β
a : α
b : β
s : Set (α × β)
h : IsLUB s (a, b)
⊢ Tendsto (α := { x : α × β // x ∈ s }) (Subtype.val (p := fun (x : α × β) ↦ x ∈ s)) atTop (𝓝 (a, b))
have h₁ : IsLUB (range (s.restrict (π := fun (a : α × β) ↦ α) fst)) (a, b).1 ∧
  IsLUB (range (s.restrict (π := fun (a : α × β) ↦ β) snd)) (a, b).2
Tactic: rw [isLUB_prod, ← range_restrict, ← range_restrict] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Topology.Order.MonotoneConvergence (hypothesis)
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
inst_2 : TopologicalSpace α
inst_3 : TopologicalSpace β
inst_4 : SupConvergenceClass α
inst_5 : SupConvergenceClass β
a : α
b : β
s : Set (α × β)
h :
  IsLUB (range (s.restrict (π := fun (a : α × β) ↦ α) fst)) (a, b).1 ∧
    IsLUB (range (s.restrict (π := fun (a : α × β) ↦ β) snd)) (a, b).2
⊢ Tendsto (α := { x : α × β // x ∈ s }) (Subtype.val (p := fun (x : α × β) ↦ x ∈ s)) atTop (𝓝 (a, b))
have A : Tendsto (fun (x : (↑s : Type (max u_1 u_2))) ↦ (↑x : α × β).1) atTop (𝓝 a)
Tactic: have A : Tendsto (fun x : s => (x : α × β).1) atTop (𝓝 a) :=
    tendsto_atTop_isLUB (monotone_fst.restrict s) h.1
-- Lean 4 proof step from Mathlib.Topology.Order.MonotoneConvergence (hypothesis)
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
inst_2 : TopologicalSpace α
inst_3 : TopologicalSpace β
inst_4 : SupConvergenceClass α
inst_5 : SupConvergenceClass β
a : α
b : β
s : Set (α × β)
h :
  IsLUB (range (s.restrict (π := fun (a : α × β) ↦ α) fst)) (a, b).1 ∧
    IsLUB (range (s.restrict (π := fun (a : α × β) ↦ β) snd)) (a, b).2
A : Tendsto (fun (x : (↑s : Type (max u_1 u_2))) ↦ (↑x : α × β).1) atTop (𝓝 a)
⊢ Tendsto (α := { x : α × β // x ∈ s }) (Subtype.val (p := fun (x : α × β) ↦ x ∈ s)) atTop (𝓝 (a, b))
have B : Tendsto (fun (x : (↑s : Type (max u_1 u_2))) ↦ (↑x : α × β).2) atTop (𝓝 b)
Tactic: have B : Tendsto (fun x : s => (x : α × β).2) atTop (𝓝 b) :=
    tendsto_atTop_isLUB (monotone_snd.restrict s) h.2
-- Lean 4 proof step from Mathlib.Topology.Order.MonotoneConvergence (goal)
Goal:
α_1 : Type u_1
β : Type u_2
ι : Type u_3
α : ι → Type u_4
inst : (i : ι) → Preorder (α i)
inst_1 : (i : ι) → TopologicalSpace (α i)
inst_2 : ∀ (i : ι), SupConvergenceClass.{u_4} (α i)
⊢ SupConvergenceClass ((i : ι) → α i)
have refine : ∀ (f : (i : ι) → α i) (s : Set ((i : ι) → α i)) (h : IsLUB s f),
  Tendsto (α := { x : (i : ι) → α i // x ∈ s }) (Subtype.val (p := fun (x : (i : ι) → α i) ↦ x ∈ s)) atTop (𝓝 f)
Tactic: refine ⟨fun f s h => ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Order.MonotoneConvergence (hypothesis)
Goal:
α_1 : Type u_1
β : Type u_2
ι : Type u_3
α : ι → Type u_4
inst : (i : ι) → Preorder (α i)
inst_1 : (i : ι) → TopologicalSpace (α i)
inst_2 : ∀ (i : ι), SupConvergenceClass.{u_4} (α i)
f : (i : ι) → α i
s : Set ((i : ι) → α i)
h : IsLUB s f
⊢ Tendsto (α := { x : (i : ι) → α i // x ∈ s }) (Subtype.val (p := fun (x : (i : ι) → α i) ↦ x ∈ s)) atTop (𝓝 f)
have h₁ : ∀ (a : ι), IsLUB (range (s.restrict (π := fun (a_1 : (x : ι) → α x) ↦ α a) (eval (β := α) a))) (f a)
Tactic: simp only [isLUB_pi, ← range_restrict] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Topology.Order.MonotoneConvergence (goal)
Goal:
ι₁ : Type u_3
ι₂ : Type u_4
α : Type u_5
inst : SemilatticeSup ι₁
inst_1 : Preorder ι₂
inst_2 : Nonempty ι₁
inst_3 : TopologicalSpace α
inst_4 : ConditionallyCompleteLinearOrder α
inst_5 : OrderTopology α
inst_6 : NoMaxOrder α
f : ι₂ → α
φ : ι₁ → ι₂
l : α
hf : Monotone f
hg : Tendsto φ atTop atTop
⊢ Tendsto f atTop (𝓝 l) ↔ Tendsto (f ∘ φ) atTop (𝓝 l)
have mp : Tendsto f atTop (𝓝 l) → Tendsto (f ∘ φ) atTop (𝓝 l)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.Order.MonotoneConvergence (goal)
Goal:
ι₁ : Type u_3
ι₂ : Type u_4
α : Type u_5
inst : SemilatticeSup ι₁
inst_1 : Preorder ι₂
inst_2 : Nonempty ι₁
inst_3 : TopologicalSpace α
inst_4 : ConditionallyCompleteLinearOrder α
inst_5 : OrderTopology α
inst_6 : NoMaxOrder α
f : ι₂ → α
φ : ι₁ → ι₂
l : α
hf : Monotone f
hg : Tendsto φ atTop atTop
mp : Tendsto f atTop (𝓝 l) → Tendsto (f ∘ φ) atTop (𝓝 l)
⊢ Tendsto f atTop (𝓝 l) ↔ Tendsto (f ∘ φ) atTop (𝓝 l)
have mpr : Tendsto (f ∘ φ) atTop (𝓝 l) → Tendsto f atTop (𝓝 l)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.Order.MonotoneConvergence (goal)
Goal:
ι₁ : Type u_3
ι₂ : Type u_4
α : Type u_5
inst : SemilatticeSup ι₁
inst_1 : Preorder ι₂
inst_2 : Nonempty ι₁
inst_3 : TopologicalSpace α
inst_4 : ConditionallyCompleteLinearOrder α
inst_5 : OrderTopology α
inst_6 : NoMaxOrder α
f : ι₂ → α
φ : ι₁ → ι₂
l : α
hf : Monotone f
hg : Tendsto φ atTop atTop
h : Tendsto (f ∘ φ) atTop (𝓝 l)
⊢ Tendsto f atTop (𝓝 l)
have mpr : ∀ (h' : Tendsto f atTop atTop), Tendsto f atTop (𝓝 l)
Tactic: rcases tendsto_atTop_of_monotone hf with (h' | ⟨l', hl'⟩)
-- Lean 4 proof step from Mathlib.Topology.Order.MonotoneConvergence (goal)
Goal:
ι₁ : Type u_3
ι₂ : Type u_4
α : Type u_5
inst : SemilatticeSup ι₁
inst_1 : Preorder ι₂
inst_2 : Nonempty ι₁
inst_3 : TopologicalSpace α
inst_4 : ConditionallyCompleteLinearOrder α
inst_5 : OrderTopology α
inst_6 : NoMaxOrder α
f : ι₂ → α
φ : ι₁ → ι₂
l : α
hf : Monotone f
hg : Tendsto φ atTop atTop
h : Tendsto (f ∘ φ) atTop (𝓝 l)
mpr : ∀ (h' : Tendsto f atTop atTop), Tendsto f atTop (𝓝 l)
⊢ Tendsto f atTop (𝓝 l)
have mpr₁ : ∀ (l' : α) (hl' : Tendsto f atTop (𝓝 l')), Tendsto f atTop (𝓝 l)
Tactic: rcases tendsto_atTop_of_monotone hf with (h' | ⟨l', hl'⟩)
-- Lean 4 proof step from Mathlib.Topology.Order.MonotoneConvergence (goal)
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : Preorder α
inst_2 : OrderClosedTopology α
inst_3 : Preorder β
inst_4 : IsDirectedOrder β
inst_5 : Nonempty β
f : β → α
a : α
hf : Monotone f
ha : Tendsto f atTop (𝓝 a)
⊢ IsLUB (range f) a
have left : a ∈ upperBounds (range f)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.Order.MonotoneConvergence (goal)
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : Preorder α
inst_2 : OrderClosedTopology α
inst_3 : Preorder β
inst_4 : IsDirectedOrder β
inst_5 : Nonempty β
f : β → α
a : α
hf : Monotone f
ha : Tendsto f atTop (𝓝 a)
left : a ∈ upperBounds (range f)
⊢ IsLUB (range f) a
have right : a ∈ lowerBounds (upperBounds (range f))
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.Order.NhdsSet (goal)
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderClosedTopology α
a : α
⊢ 𝓝ˢ (Ici a) = 𝓝 a ⊔ 𝓟 (Ioi a)
have rw : 𝓝ˢ (insert a (Ioi a)) = 𝓝 a ⊔ 𝓟 (Ioi a)
Tactic: rw [← Ioi_insert, nhdsSet_insert, nhdsSet_Ioi]
-- Lean 4 proof step from Mathlib.Topology.Order.NhdsSet (goal)
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderClosedTopology α
a : α
rw : 𝓝ˢ (insert a (Ioi a)) = 𝓝 a ⊔ 𝓟 (Ioi a)
⊢ 𝓝ˢ (Ici a) = 𝓝 a ⊔ 𝓟 (Ioi a)
have rw₁ : 𝓝 a ⊔ 𝓝ˢ (Ioi a) = 𝓝 a ⊔ 𝓟 (Ioi a)
Tactic: rw [← Ioi_insert, nhdsSet_insert, nhdsSet_Ioi]
-- Lean 4 proof step from Mathlib.Topology.Order.NhdsSet (goal)
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderClosedTopology α
a : α
rw : 𝓝ˢ (insert a (Ioi a)) = 𝓝 a ⊔ 𝓟 (Ioi a)
rw₁ : 𝓝 a ⊔ 𝓝ˢ (Ioi a) = 𝓝 a ⊔ 𝓟 (Ioi a)
⊢ 𝓝ˢ (Ici a) = 𝓝 a ⊔ 𝓟 (Ioi a)
have rw₂ : 𝓝 a ⊔ 𝓟 (Ioi a) = 𝓝 a ⊔ 𝓟 (Ioi a)
Tactic: rw [← Ioi_insert, nhdsSet_insert, nhdsSet_Ioi]
-- Lean 4 proof step from Mathlib.Topology.Order.NhdsSet (goal)
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderClosedTopology α
a b : α
h : a < b
⊢ 𝓝ˢ (Ico a b) = 𝓝 a ⊔ 𝓟 (Ioo a b)
have rw : 𝓝ˢ (insert a (Ioo a b)) = 𝓝 a ⊔ 𝓟 (Ioo a b)
Tactic: rw [← Ioo_insert_left h, nhdsSet_insert, nhdsSet_Ioo]
-- Lean 4 proof step from Mathlib.Topology.Order.NhdsSet (goal)
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderClosedTopology α
a b : α
h : a < b
rw : 𝓝ˢ (insert a (Ioo a b)) = 𝓝 a ⊔ 𝓟 (Ioo a b)
⊢ 𝓝ˢ (Ico a b) = 𝓝 a ⊔ 𝓟 (Ioo a b)
have rw₁ : 𝓝 a ⊔ 𝓝ˢ (Ioo a b) = 𝓝 a ⊔ 𝓟 (Ioo a b)
Tactic: rw [← Ioo_insert_left h, nhdsSet_insert, nhdsSet_Ioo]
-- Lean 4 proof step from Mathlib.Topology.Order.NhdsSet (goal)
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderClosedTopology α
a b : α
h : a < b
rw : 𝓝ˢ (insert a (Ioo a b)) = 𝓝 a ⊔ 𝓟 (Ioo a b)
rw₁ : 𝓝 a ⊔ 𝓝ˢ (Ioo a b) = 𝓝 a ⊔ 𝓟 (Ioo a b)
⊢ 𝓝ˢ (Ico a b) = 𝓝 a ⊔ 𝓟 (Ioo a b)
have rw₂ : 𝓝 a ⊔ 𝓟 (Ioo a b) = 𝓝 a ⊔ 𝓟 (Ioo a b)
Tactic: rw [← Ioo_insert_left h, nhdsSet_insert, nhdsSet_Ioo]
-- Lean 4 proof step from Mathlib.Topology.Order.NhdsSet (goal)
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderClosedTopology α
a b : α
h : a < b
⊢ 𝓝ˢ (Ioc a b) = 𝓝 b ⊔ 𝓟 (Ioo a b)
have rw : 𝓝ˢ (insert b (Ioo a b)) = 𝓝 b ⊔ 𝓟 (Ioo a b)
Tactic: rw [← Ioo_insert_right h, nhdsSet_insert, nhdsSet_Ioo]
-- Lean 4 proof step from Mathlib.Topology.Order.NhdsSet (goal)
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderClosedTopology α
a b : α
h : a < b
rw : 𝓝ˢ (insert b (Ioo a b)) = 𝓝 b ⊔ 𝓟 (Ioo a b)
⊢ 𝓝ˢ (Ioc a b) = 𝓝 b ⊔ 𝓟 (Ioo a b)
have rw₁ : 𝓝 b ⊔ 𝓝ˢ (Ioo a b) = 𝓝 b ⊔ 𝓟 (Ioo a b)
Tactic: rw [← Ioo_insert_right h, nhdsSet_insert, nhdsSet_Ioo]
-- Lean 4 proof step from Mathlib.Topology.Order.NhdsSet (goal)
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderClosedTopology α
a b : α
h : a < b
rw : 𝓝ˢ (insert b (Ioo a b)) = 𝓝 b ⊔ 𝓟 (Ioo a b)
rw₁ : 𝓝 b ⊔ 𝓝ˢ (Ioo a b) = 𝓝 b ⊔ 𝓟 (Ioo a b)
⊢ 𝓝ˢ (Ioc a b) = 𝓝 b ⊔ 𝓟 (Ioo a b)
have rw₂ : 𝓝 b ⊔ 𝓟 (Ioo a b) = 𝓝 b ⊔ 𝓟 (Ioo a b)
Tactic: rw [← Ioo_insert_right h, nhdsSet_insert, nhdsSet_Ioo]
-- Lean 4 proof step from Mathlib.Topology.Order.NhdsSet (goal)
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderClosedTopology α
a b : α
h : a ≤ b
⊢ 𝓝ˢ (Icc a b) = 𝓝 a ⊔ 𝓝 b ⊔ 𝓟 (Ioo a b)
have inl : ∀ (h : a ≤ a), 𝓝ˢ (Icc a a) = 𝓝 a ⊔ 𝓝 a ⊔ 𝓟 (Ioo a a)
Tactic: rcases h.eq_or_lt with rfl | hlt
Cleared hypotheses: b, h
-- Lean 4 proof step from Mathlib.Topology.Order.NhdsSet (goal)
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderClosedTopology α
a b : α
h : a ≤ b
inl : ∀ (h : a ≤ a), 𝓝ˢ (Icc a a) = 𝓝 a ⊔ 𝓝 a ⊔ 𝓟 (Ioo a a)
⊢ 𝓝ˢ (Icc a b) = 𝓝 a ⊔ 𝓝 b ⊔ 𝓟 (Ioo a b)
have inr : ∀ (hlt : a < b), 𝓝ˢ (Icc a b) = 𝓝 a ⊔ 𝓝 b ⊔ 𝓟 (Ioo a b)
Tactic: rcases h.eq_or_lt with rfl | hlt
-- Lean 4 proof step from Mathlib.Topology.Order.NhdsSet (goal)
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderClosedTopology α
a b : α
h : a ≤ b
hlt : a < b
⊢ 𝓝ˢ (Icc a b) = 𝓝 a ⊔ 𝓝 b ⊔ 𝓟 (Ioo a b)
have inr : 𝓝ˢ (insert a (Ioc a b)) = 𝓝 a ⊔ 𝓝 b ⊔ 𝓟 (Ioo a b)
Tactic: rw [← Ioc_insert_left h, nhdsSet_insert, nhdsSet_Ioc hlt, sup_assoc]
-- Lean 4 proof step from Mathlib.Topology.Order.NhdsSet (goal)
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderClosedTopology α
a b : α
h : a ≤ b
hlt : a < b
inr : 𝓝ˢ (insert a (Ioc a b)) = 𝓝 a ⊔ 𝓝 b ⊔ 𝓟 (Ioo a b)
⊢ 𝓝ˢ (Icc a b) = 𝓝 a ⊔ 𝓝 b ⊔ 𝓟 (Ioo a b)
have inr₁ : 𝓝 a ⊔ 𝓝ˢ (Ioc a b) = 𝓝 a ⊔ 𝓝 b ⊔ 𝓟 (Ioo a b)
Tactic: rw [← Ioc_insert_left h, nhdsSet_insert, nhdsSet_Ioc hlt, sup_assoc]
-- Lean 4 proof step from Mathlib.Topology.Order.NhdsSet (goal)
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderClosedTopology α
a b : α
h : a ≤ b
hlt : a < b
inr : 𝓝ˢ (insert a (Ioc a b)) = 𝓝 a ⊔ 𝓝 b ⊔ 𝓟 (Ioo a b)
inr₁ : 𝓝 a ⊔ 𝓝ˢ (Ioc a b) = 𝓝 a ⊔ 𝓝 b ⊔ 𝓟 (Ioo a b)
⊢ 𝓝ˢ (Icc a b) = 𝓝 a ⊔ 𝓝 b ⊔ 𝓟 (Ioo a b)
have inr₂ : 𝓝 a ⊔ (𝓝 b ⊔ 𝓟 (Ioo a b)) = 𝓝 a ⊔ 𝓝 b ⊔ 𝓟 (Ioo a b)
Tactic: rw [← Ioc_insert_left h, nhdsSet_insert, nhdsSet_Ioc hlt, sup_assoc]
-- Lean 4 proof step from Mathlib.Topology.Order.NhdsSet (goal)
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderClosedTopology α
a b : α
h : a ≤ b
hlt : a < b
inr : 𝓝ˢ (insert a (Ioc a b)) = 𝓝 a ⊔ 𝓝 b ⊔ 𝓟 (Ioo a b)
inr₁ : 𝓝 a ⊔ 𝓝ˢ (Ioc a b) = 𝓝 a ⊔ 𝓝 b ⊔ 𝓟 (Ioo a b)
inr₂ : 𝓝 a ⊔ (𝓝 b ⊔ 𝓟 (Ioo a b)) = 𝓝 a ⊔ 𝓝 b ⊔ 𝓟 (Ioo a b)
⊢ 𝓝ˢ (Icc a b) = 𝓝 a ⊔ 𝓝 b ⊔ 𝓟 (Ioo a b)
have inr₃ : 𝓝 a ⊔ (𝓝 b ⊔ 𝓟 (Ioo a b)) = 𝓝 a ⊔ (𝓝 b ⊔ 𝓟 (Ioo a b))
Tactic: rw [← Ioc_insert_left h, nhdsSet_insert, nhdsSet_Ioc hlt, sup_assoc]
-- Lean 4 proof step from Mathlib.Topology.Order.NhdsSet (goal)
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderClosedTopology α
a b : α
⊢ Ioi a ∈ 𝓝ˢ (Ici b) ↔ a < b
have rw : Ici b ⊆ Ioi a ↔ a < b
Tactic: rw [isOpen_Ioi.mem_nhdsSet, Ici_subset_Ioi]
-- Lean 4 proof step from Mathlib.Topology.Order.NhdsSet (goal)
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderClosedTopology α
a b : α
rw : Ici b ⊆ Ioi a ↔ a < b
⊢ Ioi a ∈ 𝓝ˢ (Ici b) ↔ a < b
have rw₁ : a < b ↔ a < b
Tactic: rw [isOpen_Ioi.mem_nhdsSet, Ici_subset_Ioi]
-- Lean 4 proof step from Mathlib.Topology.Order.NhdsSet (goal)
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
a : α
h : Nonempty.{u_1 + 1} (↑(Ioi a) : Type u_1)
⊢ (𝓝ˢ (Iic a)).HasBasis (fun (x : α) ↦ a < x) Iio
have refine : ∀ (s : Set α) (hs : s ∈ 𝓝ˢ (Iic a)), ∃ (i : α), a < i ∧ Iio i ⊆ s
Tactic: refine ⟨fun s ↦ ⟨fun hs ↦ ?_, fun ⟨b, hab, hb⟩ ↦ mem_of_superset (Iio_mem_nhdsSet_Iic hab) hb⟩⟩
-- Lean 4 proof step from Mathlib.Topology.Order.NhdsSet (hypothesis)
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
a : α
h : Nonempty.{u_1 + 1} (↑(Ioi a) : Type u_1)
s : Set α
hs : s ∈ 𝓝ˢ (Iic a)
⊢ ∃ (i : α), a < i ∧ Iio i ⊆ s
have hs₁ : s ∈ 𝓝 a ∧ Iio a ⊆ s
Tactic: rw [nhdsSet_Iic, mem_sup, mem_principal] at hs
Cleared hypotheses: hs
-- Lean 4 proof step from Mathlib.Topology.Order.NhdsSet (goal)
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
a : α
h : Nonempty.{u_1 + 1} (↑(Ioi a) : Type u_1)
s : Set α
hs : s ∈ 𝓝 a ∧ Iio a ⊆ s
⊢ ∃ (i : α), a < i ∧ Iio i ⊆ s
have rcases : ∀ (b : α) (hab : a < b) (hbs : Ico a b ⊆ s), ∃ (i : α), a < i ∧ Iio i ⊆ s
Tactic: rcases exists_Ico_subset_of_mem_nhds hs.1 (Set.nonempty_coe_sort.1 h) with ⟨b, hab, hbs⟩
-- Lean 4 proof step from Mathlib.Topology.Order.NhdsSet (hypothesis)
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
a : α
inst_3 : (𝓝[>] a).NeBot
⊢ (𝓝ˢ (Iic a)).HasBasis (fun (x : α) ↦ a < x) Iic
have this : Nonempty.{u_1 + 1} (↑(Ioi a) : Type u_1)
Tactic: have : Nonempty (Ioi a) :=
    (Filter.nonempty_of_mem (self_mem_nhdsWithin : Ioi a ∈ 𝓝[>] a)).to_subtype
-- Lean 4 proof step from Mathlib.Topology.Order.NhdsSet (goal)
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
a : α
inst_3 : (𝓝[>] a).NeBot
this : Nonempty.{u_1 + 1} (↑(Ioi a) : Type u_1)
⊢ (𝓝ˢ (Iic a)).HasBasis (fun (x : α) ↦ a < x) Iic
have refine : ∀ (c : α) (hc : a < c), ∃ (i' : α), a < i' ∧ Iic i' ⊆ Iio c
Tactic: refine (hasBasis_nhdsSet_Iic_Iio _).to_hasBasis
    (fun c hc ↦ ?_) (fun _ h ↦ ⟨_, h, Iio_subset_Iic_self⟩)
-- Lean 4 proof step from Mathlib.Topology.Order.OrderClosed (goal)
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : Preorder α
inst_2 : ClosedIicTopology α
s : Set α
a : α
⊢ a ∈ upperBounds (closure[inst] s) ↔ a ∈ upperBounds s
have simp_rw : closure[inst] s ⊆ Iic a ↔ s ⊆ Iic a
Tactic: simp_rw [mem_upperBounds_iff_subset_Iic, isClosed_Iic.closure_subset_iff]
-- Lean 4 proof step from Mathlib.Topology.Order.OrderClosed (goal)
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : Preorder α
inst_2 : ClosedIicTopology α
a : α
⊢ Disjoint (𝓝 a) atBot ↔ ¬IsBot a
have mp : Disjoint (𝓝 a) atBot → ¬IsBot a
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.Order.OrderClosed (goal)
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : Preorder α
inst_2 : ClosedIicTopology α
a : α
mp : Disjoint (𝓝 a) atBot → ¬IsBot a
⊢ Disjoint (𝓝 a) atBot ↔ ¬IsBot a
have mpr : ¬IsBot a → Disjoint (𝓝 a) atBot
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.Order.OrderClosed (hypothesis)
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : Preorder α
inst_2 : ClosedIicTopology α
a : α
hd : Disjoint (𝓝 a) atBot
hbot : IsBot a
⊢ False
have hd₁ : (Iic a)ᶜ ∈ 𝓝 a
Tactic: rw [hbot.atBot_eq, disjoint_principal_right] at hd
Cleared hypotheses: hd, hbot
-- Lean 4 proof step from Mathlib.Topology.Order.OrderClosed (goal)
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : Preorder α
inst_2 : ClosedIicTopology α
a : α
⊢ ¬IsBot a → Disjoint (𝓝 a) atBot
have mpr : (∃ (x : α), ¬a ≤ x) → Disjoint (𝓝 a) atBot
Tactic: simp only [IsBot, not_forall]
-- Lean 4 proof step from Mathlib.Topology.Order.OrderClosed (goal)
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : Preorder α
inst_2 : ClosedIicTopology α
a b : α
hb : ¬a ≤ b
⊢ Disjoint (𝓝 a) atBot
have mpr : (Iic b)ᶜ ∈ 𝓝 a
Tactic: refine disjoint_of_disjoint_of_mem disjoint_compl_left ?_ (Iic_mem_atBot b)
-- Lean 4 proof step from Mathlib.Topology.Order.OrderClosed (hypothesis)
Goal:
α : Type u
ι : Type u_1
F : Filter ι
inst : F.NeBot
inst_1 : ConditionallyCompleteLinearOrder α
inst_2 : TopologicalSpace α
inst_3 : ClosedIicTopology α
a : α
f : ι → α
hlt : ∀ (i : ι), f i < a
hlim : Tendsto f F (𝓝 a)
⊢ ⋃ (i : ι), Iic (f i) = Iio a
have obs : a ∉ range f
Tactic: have obs : a ∉ range f := by
    rw [mem_range]
    rintro ⟨i, rfl⟩
    exact (hlt i).false
-- Lean 4 proof step from Mathlib.Topology.Order.OrderClosed (goal)
Goal:
α : Type u
ι : Type u_1
F : Filter ι
inst : F.NeBot
inst_1 : ConditionallyCompleteLinearOrder α
inst_2 : TopologicalSpace α
inst_3 : ClosedIicTopology α
a : α
f : ι → α
hlt : ∀ (i : ι), f i < a
hlim : Tendsto f F (𝓝 a)
obs : a ∉ range f
⊢ ⋃ (i : ι), Iic (f i) = Iio a
have rw : ⋃ x ∈ range f, Iic x = Iio a
Tactic: rw [← biUnion_range, (IsLUB.range_of_tendsto (le_of_lt <| hlt ·) hlim).biUnion_Iic_eq_Iio obs]
-- Lean 4 proof step from Mathlib.Topology.Order.OrderClosed (goal)
Goal:
α : Type u
ι : Type u_1
F : Filter ι
inst : F.NeBot
inst_1 : ConditionallyCompleteLinearOrder α
inst_2 : TopologicalSpace α
inst_3 : ClosedIicTopology α
a : α
f : ι → α
hlt : ∀ (i : ι), f i < a
hlim : Tendsto f F (𝓝 a)
obs : a ∉ range f
rw : ⋃ x ∈ range f, Iic x = Iio a
⊢ ⋃ (i : ι), Iic (f i) = Iio a
have rw₁ : Iio a = Iio a
Tactic: rw [← biUnion_range, (IsLUB.range_of_tendsto (le_of_lt <| hlt ·) hlim).biUnion_Iic_eq_Iio obs]
-- Lean 4 proof step from Mathlib.Topology.Order.OrderClosed (goal)
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : ClosedIicTopology α
a : α
⊢ IsOpen[inst] (Ioi a)
have rw : IsOpen[inst] (Iic a)ᶜ
Tactic: rw [← compl_Iic]
-- Lean 4 proof step from Mathlib.Topology.Order.OrderClosed (goal)
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : ClosedIicTopology α
s : Set α
hs : Dense s
htop : ∀ (x : α), IsTop x → x ∈ s
x : α
⊢ ∃ y ∈ s, x ≤ y
have pos : ∀ (hx : IsTop x), ∃ y ∈ s, x ≤ y
Tactic: by_cases hx : IsTop x
-- Lean 4 proof step from Mathlib.Topology.Order.OrderClosed (goal)
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : ClosedIicTopology α
s : Set α
hs : Dense s
htop : ∀ (x : α), IsTop x → x ∈ s
x : α
pos : ∀ (hx : IsTop x), ∃ y ∈ s, x ≤ y
⊢ ∃ y ∈ s, x ≤ y
have neg : ∀ (hx : ¬IsTop x), ∃ y ∈ s, x ≤ y
Tactic: by_cases hx : IsTop x
-- Lean 4 proof step from Mathlib.Topology.Order.OrderClosed (hypothesis)
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : ClosedIicTopology α
s : Set α
hs : Dense s
htop : ∀ (x : α), IsTop x → x ∈ s
x : α
hx : ¬IsTop x
⊢ ∃ y ∈ s, x ≤ y
have hx₁ : ∃ (x_1 : α), x < x_1
Tactic: simp only [IsTop, not_forall, not_le] at hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Topology.Order.OrderClosed (goal)
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : ClosedIicTopology α
s : Set α
hs : Dense s
htop : ∀ (x : α), IsTop x → x ∈ s
x : α
hx : ∃ (x_1 : α), x < x_1
⊢ ∃ y ∈ s, x ≤ y
have neg : ∀ (y : α) (hys : y ∈ s) (hy : x < y), ∃ y ∈ s, x ≤ y
Tactic: rcases hs.exists_mem_open isOpen_Ioi hx with ⟨y, hys, hy : x < y⟩
-- Lean 4 proof step from Mathlib.Topology.Order.OrderClosed (goal)
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : ClosedIicTopology α
a : α
inst_3 : PredOrder α
⊢ 𝓝[<] a = ⊥
have if : ∀ (h : IsMin a), 𝓝[<] a = ⊥
Tactic: if h : IsMin a then simp [h.Iio_eq]
  else exact (Order.pred_covBy_of_not_isMin h).nhdsLT
-- Lean 4 proof step from Mathlib.Topology.Order.OrderClosed (goal)
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : ClosedIicTopology α
a : α
inst_3 : PredOrder α
if : ∀ (h : IsMin a), 𝓝[<] a = ⊥
⊢ 𝓝[<] a = ⊥
have if₁ : ∀ (h : ¬IsMin a), 𝓝[<] a = ⊥
Tactic: if h : IsMin a then simp [h.Iio_eq]
  else exact (Order.pred_covBy_of_not_isMin h).nhdsLT
-- Lean 4 proof step from Mathlib.Topology.Order.OrderClosed (goal)
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : ClosedIicTopology α
inst_3 : PredOrder α
a : α
⊢ 𝓝[>] a = 𝓝[≠] a
have rw : 𝓝[>] a = 𝓝[<] a ⊔ 𝓝[>] a
Tactic: rw [← nhdsLT_sup_nhdsGT, PredOrder.nhdsLT, bot_sup_eq]
-- Lean 4 proof step from Mathlib.Topology.Order.OrderClosed (goal)
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : ClosedIicTopology α
inst_3 : PredOrder α
a : α
rw : 𝓝[>] a = 𝓝[<] a ⊔ 𝓝[>] a
⊢ 𝓝[>] a = 𝓝[≠] a
have rw₁ : 𝓝[>] a = ⊥ ⊔ 𝓝[>] a
Tactic: rw [← nhdsLT_sup_nhdsGT, PredOrder.nhdsLT, bot_sup_eq]
-- Lean 4 proof step from Mathlib.Topology.Order.OrderClosed (goal)
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : ClosedIicTopology α
inst_3 : PredOrder α
a : α
rw : 𝓝[>] a = 𝓝[<] a ⊔ 𝓝[>] a
rw₁ : 𝓝[>] a = ⊥ ⊔ 𝓝[>] a
⊢ 𝓝[>] a = 𝓝[≠] a
have rw₂ : 𝓝[>] a = 𝓝[>] a
Tactic: rw [← nhdsLT_sup_nhdsGT, PredOrder.nhdsLT, bot_sup_eq]
-- Lean 4 proof step from Mathlib.Topology.Order.OrderClosed (goal)
Goal:
α : Type u
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : ClosedIicTopology α
inst_3 : PredOrder α
a : α
⊢ 𝓝[≥] a = 𝓝 a
have rw : 𝓝[≥] a = 𝓝[<] a ⊔ 𝓝[≥] a
Tactic: rw [← nhdsLT_sup_nhdsGE, PredOrder.nhdsLT, bot_sup_eq]