awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.Order.ScottTopology (goal)
Goal:
α : Type u_1
inst : Preorder α
inst_1 : TopologicalSpace α
s : Set α
inst_2 : IsScott α univ
⊢ (↑(lowerClosure s) : Set α) = closure[upperSet α] s
have rw : Topology.IsUpperSet α
Tactic: rw [@IsUpperSet.closure_eq_lowerClosure α _ (upperSet α) ?_ s]
-- Lean 4 proof step from Mathlib.Topology.Order.ScottTopology (goal)
Goal:
α : Type u_1
inst : Preorder α
inst_1 : TopologicalSpace α
a : α
inst_2 : IsScott α univ
⊢ {a} ⊆ Iic a
have rw : a ∈ Iic a
Tactic: rw [singleton_subset_iff, mem_Iic]
-- Lean 4 proof step from Mathlib.Topology.Order.ScottTopology (goal)
Goal:
α : Type u_1
inst : Preorder α
inst_1 : TopologicalSpace α
a : α
inst_2 : IsScott α univ
rw : a ∈ Iic a
⊢ {a} ⊆ Iic a
have rw₁ : a ≤ a
Tactic: rw [singleton_subset_iff, mem_Iic]
-- Lean 4 proof step from Mathlib.Topology.Order.ScottTopology (goal)
Goal:
α : Type u_1
inst : Preorder α
inst_1 : TopologicalSpace α
a : α
inst_2 : IsScott α univ
⊢ Iic a ≤ closure[inst_1] {a}
have rw : (↑(lowerClosure {a}) : Set α) ≤ closure[inst_1] {a}
Tactic: rw [← LowerSet.coe_Iic, ← lowerClosure_singleton]
-- Lean 4 proof step from Mathlib.Topology.Order.ScottTopology (goal)
Goal:
α : Type u_1
β : Type u_2
D : Set (Set α)
inst : Preorder α
inst_1 : TopologicalSpace α
inst_2 : Preorder β
inst_3 : TopologicalSpace β
inst_4 : IsScott β univ
f : α → β
inst_5 : IsScott α D
hf : Continuous[inst_1, inst_3] f
x b : α
hab : x ≤ b
⊢ f x ≤ f b
have by_contra : ∀ (h : ¬f x ≤ f b), False
Tactic: by_contra h
-- Lean 4 proof step from Mathlib.Topology.Order.ScottTopology (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : TopologicalSpace α
inst_2 : Preorder β
inst_3 : TopologicalSpace β
inst_4 : IsScott β univ
f : α → β
D : Set (Set α)
inst_5 : IsScott α D
hD : ∀ (a b : α), a ≤ b → {a, b} ∈ D
⊢ ScottContinuousOn D f ↔ Continuous[inst_1, inst_3] f
have refine_1 : ∀ (h : ScottContinuousOn D f) (u : Set β) (hu : IsOpen[inst_3] u), IsOpen[inst_1] (f ⁻¹' u)
Tactic: refine ⟨fun h ↦ continuous_def.2 fun u hu ↦ ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Order.ScottTopology (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : TopologicalSpace α
inst_2 : Preorder β
inst_3 : TopologicalSpace β
inst_4 : IsScott β univ
f : α → β
D : Set (Set α)
inst_5 : IsScott α D
hD : ∀ (a b : α), a ≤ b → {a, b} ∈ D
refine_1 : ∀ (h : ScottContinuousOn D f) (u : Set β) (hu : IsOpen[inst_3] u), IsOpen[inst_1] (f ⁻¹' u)
⊢ ScottContinuousOn D f ↔ Continuous[inst_1, inst_3] f
have refine_2 : Continuous[inst_1, inst_3] f → ScottContinuousOn D f
Tactic: refine ⟨fun h ↦ continuous_def.2 fun u hu ↦ ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Order.ScottTopology (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : TopologicalSpace α
inst_2 : Preorder β
inst_3 : TopologicalSpace β
inst_4 : IsScott β univ
f : α → β
D : Set (Set α)
inst_5 : IsScott α D
hD : ∀ (a b : α), a ≤ b → {a, b} ∈ D
h : ScottContinuousOn D f
u : Set β
hu : IsOpen[inst_3] u
⊢ IsOpen[inst_1] (f ⁻¹' u)
have refine_1 : IsUpperSet (f ⁻¹' u) ∧ DirSupInaccOn D (f ⁻¹' u)
Tactic: rw [isOpen_iff_isUpperSet_and_dirSupInaccOn (D := D)]
-- Lean 4 proof step from Mathlib.Topology.Order.ScottTopology (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : TopologicalSpace α
inst_2 : Preorder β
inst_3 : TopologicalSpace β
inst_4 : IsScott β univ
f : α → β
D : Set (Set α)
inst_5 : IsScott α D
hD : ∀ (a b : α), a ≤ b → {a, b} ∈ D
⊢ Continuous[inst_1, inst_3] f → ScottContinuousOn D f
have refine_2 : ∀ (hf : Continuous[inst_1, inst_3] f) (t : Set α) (h₀ : t ∈ D) (d₁ : t.Nonempty)
  (d₂ : DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) t) (a : α) (d₃ : IsLUB t a) (b : β) (hb : b ∈ upperBounds (f '' t)),
  f a ≤ b
Tactic: refine fun hf t h₀ d₁ d₂ a d₃ ↦
      ⟨(monotone_of_continuous (D := D) hf).mem_upperBounds_image d₃.1,
      fun b hb ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Order.ScottTopology (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : TopologicalSpace α
inst_2 : Preorder β
inst_3 : TopologicalSpace β
inst_4 : IsScott β univ
f : α → β
D : Set (Set α)
inst_5 : IsScott α D
hD : ∀ (a b : α), a ≤ b → {a, b} ∈ D
hf : Continuous[inst_1, inst_3] f
t : Set α
h₀ : t ∈ D
d₁ : t.Nonempty
d₂ : DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) t
a : α
d₃ : IsLUB t a
b : β
hb : b ∈ upperBounds (f '' t)
⊢ f a ≤ b
have refine_2 : ∀ (h : ¬f a ≤ b), False
Tactic: by_contra h
-- Lean 4 proof step from Mathlib.Topology.Order.ScottTopology (hypothesis)
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : TopologicalSpace α
inst_2 : Preorder β
inst_3 : TopologicalSpace β
inst_4 : IsScott β univ
f : α → β
D : Set (Set α)
inst_5 : IsScott α D
hD : ∀ (a b : α), a ≤ b → {a, b} ∈ D
hf : Continuous[inst_1, inst_3] f
t : Set α
h₀ : t ∈ D
d₁ : t.Nonempty
d₂ : DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) t
a : α
d₃ : IsLUB t a
b : β
hb : b ∈ upperBounds (f '' t)
h : ¬f a ≤ b
u : Set β := (Iic b)ᶜ
⊢ False
have hu : IsOpen[inst_1] (f ⁻¹' u)
Tactic: have hu : IsOpen (f ⁻¹' u) := isClosed_Iic.isOpen_compl.preimage hf
-- Lean 4 proof step from Mathlib.Topology.Order.ScottTopology (hypothesis)
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : TopologicalSpace α
inst_2 : Preorder β
inst_3 : TopologicalSpace β
inst_4 : IsScott β univ
f : α → β
D : Set (Set α)
inst_5 : IsScott α D
hD : ∀ (a b : α), a ≤ b → {a, b} ∈ D
hf : Continuous[inst_1, inst_3] f
t : Set α
h₀ : t ∈ D
d₁ : t.Nonempty
d₂ : DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) t
a : α
d₃ : IsLUB t a
b : β
hb : b ∈ upperBounds (f '' t)
h : ¬f a ≤ b
u : Set β := (Iic b)ᶜ
hu : IsOpen[inst_1] (f ⁻¹' u)
⊢ False
have hu₁ : IsUpperSet (f ⁻¹' u) ∧ DirSupInaccOn D (f ⁻¹' u)
Tactic: rw [isOpen_iff_isUpperSet_and_dirSupInaccOn (D := D)] at hu
Cleared hypotheses: hu
-- Lean 4 proof step from Mathlib.Topology.Order.ScottTopology (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : TopologicalSpace α
inst_2 : Preorder β
inst_3 : TopologicalSpace β
inst_4 : IsScott β univ
f : α → β
D : Set (Set α)
inst_5 : IsScott α D
hD : ∀ (a b : α), a ≤ b → {a, b} ∈ D
hf : Continuous[inst_1, inst_3] f
t : Set α
h₀ : t ∈ D
d₁ : t.Nonempty
d₂ : DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) t
a : α
d₃ : IsLUB t a
b : β
hb : b ∈ upperBounds (f '' t)
h : ¬f a ≤ b
u : Set β := (Iic b)ᶜ
hu : IsUpperSet (f ⁻¹' u) ∧ DirSupInaccOn D (f ⁻¹' u)
⊢ False
have refine_2 : ∀ (c : α) (hcd : c ∈ t) (hfcb : c ∈ f ⁻¹' u), False
Tactic: obtain ⟨c, hcd, hfcb⟩ := hu.2 h₀ d₁ d₂ d₃ h
-- Lean 4 proof step from Mathlib.Topology.Order.ScottTopology (hypothesis)
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : TopologicalSpace α
inst_2 : Preorder β
inst_3 : TopologicalSpace β
inst_4 : IsScott β univ
f : α → β
D : Set (Set α)
inst_5 : IsScott α D
hD : ∀ (a b : α), a ≤ b → {a, b} ∈ D
hf : Continuous[inst_1, inst_3] f
t : Set α
h₀ : t ∈ D
d₁ : t.Nonempty
d₂ : DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) t
a : α
d₃ : IsLUB t a
b : β
hb : b ∈ upperBounds (f '' t)
h : ¬f a ≤ b
u : Set β := (Iic b)ᶜ
hu : IsUpperSet (f ⁻¹' u) ∧ DirSupInaccOn D (f ⁻¹' u)
c : α
hcd : c ∈ t
hfcb : c ∈ f ⁻¹' u
⊢ False
have hb₁ : ∀ a ∈ t, f a ≤ b
Tactic: simp only [upperBounds, mem_image, forall_exists_index, and_imp, forall_apply_eq_imp_iff₂,
      mem_setOf] at hb
Cleared hypotheses: hb
-- Lean 4 proof step from Mathlib.Topology.Order.ScottTopology (goal)
Goal:
α : Type u_1
inst : CompleteLinearOrder α
inst_1 : TopologicalSpace α
inst_2 : IsScott α univ
U : Set α
⊢ IsOpen[inst_1] U ↔ U = univ ∨ ∃ (a : α), (Iic a)ᶜ = U
have mp : IsOpen[inst_1] U → U = univ ∨ ∃ (a : α), (Iic a)ᶜ = U
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.Order.ScottTopology (goal)
Goal:
α : Type u_1
inst : CompleteLinearOrder α
inst_1 : TopologicalSpace α
inst_2 : IsScott α univ
U : Set α
mp : IsOpen[inst_1] U → U = univ ∨ ∃ (a : α), (Iic a)ᶜ = U
⊢ IsOpen[inst_1] U ↔ U = univ ∨ ∃ (a : α), (Iic a)ᶜ = U
have mpr : (U = univ ∨ ∃ (a : α), (Iic a)ᶜ = U) → IsOpen[inst_1] U
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.Order.ScottTopology (goal)
Goal:
α : Type u_1
inst : CompleteLinearOrder α
inst_1 : TopologicalSpace α
inst_2 : IsScott α univ
U : Set α
hU : IsOpen[inst_1] U
⊢ U = univ ∨ ∃ (a : α), (Iic a)ᶜ = U
have mp : ∀ (eUc : Uᶜ = ∅), U = univ ∨ ∃ (a : α), (Iic a)ᶜ = U
Tactic: rcases eq_empty_or_nonempty Uᶜ with eUc | neUc
-- Lean 4 proof step from Mathlib.Topology.Order.ScottTopology (goal)
Goal:
α : Type u_1
inst : CompleteLinearOrder α
inst_1 : TopologicalSpace α
inst_2 : IsScott α univ
U : Set α
hU : IsOpen[inst_1] U
mp : ∀ (eUc : Uᶜ = ∅), U = univ ∨ ∃ (a : α), (Iic a)ᶜ = U
⊢ U = univ ∨ ∃ (a : α), (Iic a)ᶜ = U
have mp₁ : ∀ (neUc : Uᶜ.Nonempty), U = univ ∨ ∃ (a : α), (Iic a)ᶜ = U
Tactic: rcases eq_empty_or_nonempty Uᶜ with eUc | neUc
-- Lean 4 proof step from Mathlib.Topology.Order.ScottTopology (goal)
Goal:
α : Type u_1
inst : CompleteLinearOrder α
inst_1 : TopologicalSpace α
inst_2 : IsScott α univ
U : Set α
hU : IsOpen[inst_1] U
neUc : Uᶜ.Nonempty
⊢ U = univ ∨ ∃ (a : α), (Iic a)ᶜ = U
have mp : ∃ (a : α), (Iic a)ᶜ = U
Tactic: apply Or.inr
-- Lean 4 proof step from Mathlib.Topology.Order.ScottTopology (goal)
Goal:
α : Type u_1
inst : CompleteLinearOrder α
inst_1 : TopologicalSpace α
inst_2 : IsScott α univ
U : Set α
hU : IsOpen[inst_1] U
neUc : Uᶜ.Nonempty
⊢ ∃ (a : α), (Iic a)ᶜ = U
have h : (Iic (sSup Uᶜ))ᶜ = U
Tactic: use sSup Uᶜ
-- Lean 4 proof step from Mathlib.Topology.Order.ScottTopology (goal)
Goal:
α : Type u_1
inst : CompleteLinearOrder α
inst_1 : TopologicalSpace α
inst_2 : IsScott α univ
U : Set α
hU : IsOpen[inst_1] U
neUc : Uᶜ.Nonempty
⊢ (Iic (sSup Uᶜ))ᶜ = U
have h : Uᶜ ≤ Iic (sSup Uᶜ) ∧ Iic (sSup Uᶜ) ≤ Uᶜ
Tactic: rw [compl_eq_comm, le_antisymm_iff]
-- Lean 4 proof step from Mathlib.Topology.Order.ScottTopology (goal)
Goal:
α : Type u_1
inst : CompleteLinearOrder α
inst_1 : TopologicalSpace α
inst_2 : IsScott α univ
U : Set α
hU : IsOpen[inst_1] U
neUc : Uᶜ.Nonempty
⊢ Uᶜ ≤ Iic (sSup Uᶜ) ∧ Iic (sSup Uᶜ) ≤ Uᶜ
have h : sSup Uᶜ ∈ Uᶜ
Tactic: refine ⟨fun _ ha ↦ le_sSup ha, (isLowerSet_of_isClosed hU.isClosed_compl).Iic_subset ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Order.ScottTopology (goal)
Goal:
α : Type u_1
inst : CompleteLinearOrder α
this : TopologicalSpace α := upper α
⊢ scott α univ = upper α
have a : ∀ (U : Set α), IsOpen[scott α univ] U ↔ IsOpen[upper α] U
Tactic: ext U
-- Lean 4 proof step from Mathlib.Topology.Order.ScottTopology (goal)
Goal:
α : Type u_1
inst : CompleteLinearOrder α
this : TopologicalSpace α := upper α
U : Set α
⊢ IsOpen[scott α univ] U ↔ IsOpen[upper α] U
have a : IsOpen[scott α univ] U ↔ U = univ ∨ ∃ (a : α), (Iic a)ᶜ = U
Tactic: rw [@Topology.IsUpper.isTopologicalSpace_basis _ _ (upper α)
    ({ topology_eq_upperTopology := rfl }) U]
-- Lean 4 proof step from Mathlib.Topology.Order.ScottTopology (goal)
Goal:
α : Type u_1
inst : CompleteLinearOrder α
this_1 : TopologicalSpace α := upper α
U : Set α
this : TopologicalSpace α := scott α univ
⊢ IsOpen[scott α univ] U ↔ U = univ ∨ ∃ (a : α), (Iic a)ᶜ = U
have a : (U = univ ∨ ∃ (a : α), (Iic a)ᶜ = U) ↔ U = univ ∨ ∃ (a : α), (Iic a)ᶜ = U
Tactic: rw [@isOpen_iff_Iic_compl_or_univ _ _ (scott α univ) ({ topology_eq_scott := rfl }) U]
-- Lean 4 proof step from Mathlib.Topology.Order.ScottTopology (goal)
Goal:
α : Type u_1
β : Type u_2
inst : CompleteLinearOrder α
inst_1 : TopologicalSpace α
inst_2 : IsUpper α
⊢ inst_1 = scott α univ
have rw : inst_1 = upper α
Tactic: rw [scott_eq_upper_of_completeLinearOrder]
-- Lean 4 proof step from Mathlib.Topology.Order.ScottTopology (goal)
Goal:
α : Type u_1
inst : Preorder α
s : Set α
inst_1 : TopologicalSpace α
inst_2 : IsScott α univ
⊢ IsOpen[inst_1] s ↔ ScottContinuous (β := Prop) fun (x : α) ↦ x ∈ s
have rw : IsOpen[inst_1] s ↔ Continuous[inst_1, _] fun (x : α) ↦ x ∈ s
Tactic: rw [← scottContinuousOn_univ, scottContinuousOn_iff_continuous (fun _ _ _ ↦ by trivial)]
-- Lean 4 proof step from Mathlib.Topology.Order.ScottTopology (goal)
Goal:
α : Type u_1
inst : Preorder α
inst_1 : TopologicalSpace α
inst_2 : IsScott α univ
⊢ scottHausdorff α univ ≤ inst_1
have rw : scottHausdorff α univ ≤ upperSet α ⊔ scottHausdorff α univ
Tactic: rw [IsScott.topology_eq α univ, scott]
-- Lean 4 proof step from Mathlib.Topology.Order.ScottTopology (goal)
Goal:
α : Type u_1
inst : Preorder α
inst_1 : TopologicalSpace α
inst_2 : IsLower α
⊢ scottHausdorff α univ ≤ inst_1
have rw : scottHausdorff α univ ≤ lower α
Tactic: rw [IsLower.topology_eq α]
-- Lean 4 proof step from Mathlib.Topology.Order.SuccPred (goal)
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
a : α
inst_3 : SuccOrder α
ha : ¬IsSuccPrelimit a
⊢ IsOpen[inst_1] {a}
have obtain : ∀ (b : α) (hb : b ⋖ a), IsOpen[inst_1] {a}
Tactic: obtain ⟨b, hb⟩ := not_isSuccPrelimit_iff.1 ha
-- Lean 4 proof step from Mathlib.Topology.Order.SuccPred (goal)
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
a : α
inst_3 : SuccOrder α
ha : ¬IsSuccPrelimit a
b : α
hb : b ⋖ a
⊢ IsOpen[inst_1] {a}
have pos : ∀ (ha' : IsMax a), IsOpen[inst_1] {a}
Tactic: by_cases ha' : IsMax a
-- Lean 4 proof step from Mathlib.Topology.Order.SuccPred (goal)
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
a : α
inst_3 : SuccOrder α
ha : ¬IsSuccPrelimit a
b : α
hb : b ⋖ a
pos : ∀ (ha' : IsMax a), IsOpen[inst_1] {a}
⊢ IsOpen[inst_1] {a}
have neg : ∀ (ha' : ¬IsMax a), IsOpen[inst_1] {a}
Tactic: by_cases ha' : IsMax a
-- Lean 4 proof step from Mathlib.Topology.Order.SuccPred (goal)
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
a : α
inst_3 : SuccOrder α
ha : ¬IsSuccPrelimit a
b : α
hb : b ⋖ a
ha' : IsMax a
⊢ IsOpen[inst_1] {a}
have h : {a} = Set.Ioi b
Tactic: convert! isOpen_Ioi (a := b) using 1
-- Lean 4 proof step from Mathlib.Topology.Order.SuccPred (goal)
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
a : α
inst_3 : SuccOrder α
ha : ¬IsSuccPrelimit a
b : α
hb : b ⋖ a
ha' : IsMax a
⊢ {a} = Set.Ioi b
have h : {a} = Set.Ici a
Tactic: rw [hb.Ioi_eq]
-- Lean 4 proof step from Mathlib.Topology.Order.SuccPred (goal)
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
a : α
inst_3 : SuccOrder α
ha : ¬IsSuccPrelimit a
b : α
hb : b ⋖ a
ha' : ¬IsMax a
⊢ IsOpen[inst_1] {a}
have h : {a} = Set.Ioo b (Order.succ a)
Tactic: convert! isOpen_Ioo (a := b) (b := Order.succ a) using 1
-- Lean 4 proof step from Mathlib.Topology.Order.SuccPred (hypothesis)
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
a : α
inst_3 : SuccOrder α
inst_4 : NoMaxOrder α
⊢ IsOpen[inst_1] {a} ↔ ¬IsSuccLimit a
have a₁ : Nontrivial α
Tactic: nontriviality α
-- Lean 4 proof step from Mathlib.Topology.Order.SuccPred (goal)
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
a : α
inst_3 : SuccOrder α
inst_4 : NoMaxOrder α
h : Nontrivial α
⊢ IsOpen[inst_1] {a} ↔ ¬IsSuccLimit a
have refine_1 : ∀ (h : IsOpen[inst_1] {a}) (ha : IsSuccLimit a), False
Tactic: refine ⟨fun h ha ↦ ?_, fun ha ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Order.SuccPred (goal)
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
a : α
inst_3 : SuccOrder α
inst_4 : NoMaxOrder α
h : Nontrivial α
refine_1 : ∀ (h : IsOpen[inst_1] {a}) (ha : IsSuccLimit a), False
⊢ IsOpen[inst_1] {a} ↔ ¬IsSuccLimit a
have refine_2 : ∀ (ha : ¬IsSuccLimit a), IsOpen[inst_1] {a}
Tactic: refine ⟨fun h ha ↦ ?_, fun ha ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Order.SuccPred (goal)
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
a : α
inst_3 : SuccOrder α
inst_4 : NoMaxOrder α
h_1 : Nontrivial α
h : IsOpen[inst_1] {a}
ha : IsSuccLimit a
⊢ False
have refine_1 : ∀ (l u : α) (h₁ : a ∈ Set.Ioo l u) (h₂ : Set.Ioo l u ⊆ {a}), False
Tactic: obtain ⟨l, u, h₁, h₂⟩ := mem_nhds_iff_exists_Ioo_subset' (by simpa using ha.not_isMin)
      (by simpa only [not_isMax_iff] using not_isMax a) |>.mp (h.mem_nhds (Set.mem_singleton a))
-- Lean 4 proof step from Mathlib.Topology.Order.SuccPred (goal)
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
a : α
inst_3 : SuccOrder α
inst_4 : NoMaxOrder α
h_1 : Nontrivial α
h : IsOpen[inst_1] {a}
ha : IsSuccLimit a
l u : α
h₁ : a ∈ Set.Ioo l u
h₂ : Set.Ioo l u ⊆ {a}
⊢ False
have refine_1 : l ⋖ a
Tactic: refine ha.isSuccPrelimit l ?_
-- Lean 4 proof step from Mathlib.Topology.Order.SuccPred (goal)
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
a : α
inst_3 : SuccOrder α
inst_4 : NoMaxOrder α
h_1 : Nontrivial α
h : IsOpen[inst_1] {a}
ha : IsSuccLimit a
l u : α
h₁ : a ∈ Set.Ioo l u
h₂ : Set.Ioo l u ⊆ {a}
⊢ l ⋖ a
have refine_1 : Order.succ l = a
Tactic: rw [← succ_eq_iff_covBy]
-- Lean 4 proof step from Mathlib.Topology.Order.SuccPred (hypothesis)
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
a : α
inst_3 : SuccOrder α
inst_4 : NoMaxOrder α
h_1 : Nontrivial α
h : IsOpen[inst_1] {a}
ha : IsSuccLimit a
l u : α
h₁ : a ∈ Set.Ioo l u
h₂ : Set.Ioo l u ⊆ {a}
⊢ Order.succ l = a
have h₃ : l < a ∧ a < u
Tactic: simp only [Set.mem_Ioo, Set.subset_singleton_iff] at h₁ h₂
Cleared hypotheses: h₁, h₂
-- Lean 4 proof step from Mathlib.Topology.Order.SuccPred (hypothesis)
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
a : α
inst_3 : SuccOrder α
inst_4 : NoMaxOrder α
h_1 : Nontrivial α
h : IsOpen[inst_1] {a}
ha : IsSuccLimit a
l u : α
h₁ : a ∈ Set.Ioo l u
h₂ : Set.Ioo l u ⊆ {a}
h₃ : l < a ∧ a < u
⊢ Order.succ l = a
have h₄ : ∀ (y : α), l < y ∧ y < u → y = a
Tactic: simp only [Set.mem_Ioo, Set.subset_singleton_iff] at h₁ h₂
Cleared hypotheses: h₁, h₂
-- Lean 4 proof step from Mathlib.Topology.Order.SuccPred (goal)
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
a : α
inst_3 : SuccOrder α
inst_4 : NoMaxOrder α
h : Nontrivial α
ha : ¬IsSuccLimit a
⊢ IsOpen[inst_1] {a}
have refine_2 : ∀ (ha : IsMin a), IsOpen[inst_1] {a}
Tactic: obtain (ha | ha) := not_isSuccLimit_iff.mp ha
-- Lean 4 proof step from Mathlib.Topology.Order.SuccPred (goal)
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
a : α
inst_3 : SuccOrder α
inst_4 : NoMaxOrder α
h : Nontrivial α
ha : ¬IsSuccLimit a
refine_2 : ∀ (ha : IsMin a), IsOpen[inst_1] {a}
⊢ IsOpen[inst_1] {a}
have refine_2₁ : ∀ (ha : ¬IsSuccPrelimit a), IsOpen[inst_1] {a}
Tactic: obtain (ha | ha) := not_isSuccLimit_iff.mp ha
-- Lean 4 proof step from Mathlib.Topology.Order.SuccPred (goal)
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
a : α
inst_3 : SuccOrder α
inst_4 : NoMaxOrder α
h : Nontrivial α
ha_1 : ¬IsSuccLimit a
ha : IsMin a
⊢ IsOpen[inst_1] {a}
have h : {a} = Set.Iio (Order.succ a)
Tactic: convert! isOpen_Iio (a := Order.succ a) using 1
-- Lean 4 proof step from Mathlib.Topology.Order.SuccPred (goal)
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
inst_3 : SuccOrder α
inst_4 : NoMaxOrder α
s : Set α
⊢ IsOpen[inst_1] s ↔ ∀ o ∈ s, IsSuccLimit o → ∃ a < o, Set.Ioo a o ⊆ s
have refine : ∀ (o : α) (ho : o ∈ s), s ∈ 𝓝 o ↔ IsSuccLimit o → ∃ a < o, Set.Ioo a o ⊆ s
Tactic: refine isOpen_iff_mem_nhds.trans <| forall₂_congr fun o ho ↦ ?_
-- Lean 4 proof step from Mathlib.Topology.Order.SuccPred (goal)
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
inst_3 : SuccOrder α
inst_4 : NoMaxOrder α
s : Set α
o : α
ho : o ∈ s
⊢ s ∈ 𝓝 o ↔ IsSuccLimit o → ∃ a < o, Set.Ioo a o ⊆ s
have pos : ∀ (ho' : IsSuccLimit o), s ∈ 𝓝 o ↔ IsSuccLimit o → ∃ a < o, Set.Ioo a o ⊆ s
Tactic: by_cases ho' : IsSuccLimit o
-- Lean 4 proof step from Mathlib.Topology.Order.SuccPred (goal)
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
inst_3 : SuccOrder α
inst_4 : NoMaxOrder α
s : Set α
o : α
ho : o ∈ s
pos : ∀ (ho' : IsSuccLimit o), s ∈ 𝓝 o ↔ IsSuccLimit o → ∃ a < o, Set.Ioo a o ⊆ s
⊢ s ∈ 𝓝 o ↔ IsSuccLimit o → ∃ a < o, Set.Ioo a o ⊆ s
have neg : ∀ (ho' : ¬IsSuccLimit o), s ∈ 𝓝 o ↔ IsSuccLimit o → ∃ a < o, Set.Ioo a o ⊆ s
Tactic: by_cases ho' : IsSuccLimit o
-- Lean 4 proof step from Mathlib.Topology.Order.SuccPred (goal)
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
inst_3 : SuccOrder α
inst_4 : NoMaxOrder α
s : Set α
o : α
ho : o ∈ s
ho' : IsSuccLimit o
⊢ s ∈ 𝓝 o ↔ IsSuccLimit o → ∃ a < o, Set.Ioo a o ⊆ s
have pos : (∃ i < o, Set.Ioc i o ⊆ s) ↔ IsSuccLimit o → ∃ a < o, Set.Ioo a o ⊆ s
Tactic: rw [(SuccOrder.hasBasis_nhds_Ioc_of_exists_lt (not_isMin_iff.1 ho'.not_isMin)).mem_iff]
-- Lean 4 proof step from Mathlib.Topology.Order.SuccPred (goal)
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
inst_3 : SuccOrder α
inst_4 : NoMaxOrder α
a : α
s : Set α
ha : a ∈ frontier s
⊢ IsSuccLimit a
have rw : ¬IsOpen[inst_1] {a}
Tactic: rw [← isOpen_singleton_iff.not_left]
-- Lean 4 proof step from Mathlib.Topology.Order.SuccPred (hypothesis)
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : OrderTopology α
inst_3 : SuccOrder α
inst_4 : NoMaxOrder α
a : α
s : Set α
ha : a ∈ frontier s
⊢ ¬IsOpen[inst_1] {a}
have ha₁ : a ∈ closure[inst_1] s ∩ closure[inst_1] sᶜ
Tactic: rw [frontier_eq_closure_inter_closure] at ha
Cleared hypotheses: ha
-- Lean 4 proof step from Mathlib.Topology.Order.T5 (goal)
Goal:
X : Type u_1
inst : LinearOrder X
inst_1 : TopologicalSpace X
inst_2 : OrderTopology X
a : X
s : Set X
⊢ s.ordConnectedComponent a ∈ 𝓝 a ↔ s ∈ 𝓝 a
have refine : ∀ (h : s ∈ 𝓝 a), s.ordConnectedComponent a ∈ 𝓝 a
Tactic: refine ⟨fun h => mem_of_superset h ordConnectedComponent_subset, fun h => ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Order.T5 (goal)
Goal:
X : Type u_1
inst : LinearOrder X
inst_1 : TopologicalSpace X
inst_2 : OrderTopology X
a : X
s : Set X
h : s ∈ 𝓝 a
⊢ s.ordConnectedComponent a ∈ 𝓝 a
have rcases : ∀ (b c : X) (ha : a ∈ Icc b c) (ha' : Icc b c ∈ 𝓝 a) (hs : Icc b c ⊆ s), s.ordConnectedComponent a ∈ 𝓝 a
Tactic: rcases exists_Icc_mem_subset_of_mem_nhds h with ⟨b, c, ha, ha', hs⟩
-- Lean 4 proof step from Mathlib.Topology.Order.T5 (goal)
Goal:
X : Type u_1
inst : LinearOrder X
inst_1 : TopologicalSpace X
inst_2 : OrderTopology X
a : X
s t : Set X
hd : Disjoint s (closure[inst_1] t)
ha : a ∈ s
⊢ tᶜ ∈ 𝓝[≥] a
have refine : tᶜ ∈ 𝓝 a
Tactic: refine mem_nhdsWithin_of_mem_nhds ?_
-- Lean 4 proof step from Mathlib.Topology.Order.T5 (goal)
Goal:
X : Type u_1
inst : LinearOrder X
inst_1 : TopologicalSpace X
inst_2 : OrderTopology X
a : X
s t : Set X
hd : Disjoint s (closure[inst_1] t)
ha : a ∈ s
⊢ tᶜ ∈ 𝓝 a
have rw : a ∈ (closure[inst_1] t)ᶜ
Tactic: rw [← mem_interior_iff_mem_nhds, interior_compl]
-- Lean 4 proof step from Mathlib.Topology.Order.T5 (hypothesis)
Goal:
X : Type u_1
inst : LinearOrder X
inst_1 : TopologicalSpace X
inst_2 : OrderTopology X
a : X
s t : Set X
hd : Disjoint s (closure[inst_1] t)
ha : a ∈ s
⊢ (s.ordSeparatingSet t).ordConnectedSectionᶜ ∈ 𝓝[≥] a
have hmem : tᶜ ∈ 𝓝[≥] a
Tactic: have hmem : tᶜ ∈ 𝓝[≥] a := by
    refine mem_nhdsWithin_of_mem_nhds ?_
    rw [← mem_interior_iff_mem_nhds, interior_compl]
    exact disjoint_left.1 hd ha
-- Lean 4 proof step from Mathlib.Topology.Order.T5 (goal)
Goal:
X : Type u_1
inst : LinearOrder X
inst_1 : TopologicalSpace X
inst_2 : OrderTopology X
a : X
s t : Set X
hd : Disjoint s (closure[inst_1] t)
ha : a ∈ s
hmem : tᶜ ∈ 𝓝[≥] a
⊢ (s.ordSeparatingSet t).ordConnectedSectionᶜ ∈ 𝓝[≥] a
have rcases : ∀ (b : X) (hab : a ≤ b) (hmem' : Icc a b ∈ 𝓝[≥] a) (hsub : Icc a b ⊆ tᶜ),
  (s.ordSeparatingSet t).ordConnectedSectionᶜ ∈ 𝓝[≥] a
Tactic: rcases exists_Icc_mem_subset_of_mem_nhdsGE hmem with ⟨b, hab, hmem', hsub⟩