awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Order.IsNormal
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : WellFoundedLT α
inst_2 : TopologicalSpace α
inst_3 : OrderTopology α
inst_4 : LinearOrder β
inst_5 : WellFoundedLT β
inst_6 : TopologicalSpace β
inst_7 : OrderTopology β
f : α → β
hf : IsNormal f
b : β
a : α
ha : f ⁻¹' Iic b = Iio a
h : (f ⁻¹' Iic b).Nonempty
this : Nonempty α
⊢ Nonempty β

Tactic:
have : Nonempty β := ⟨b⟩
-- Module: Mathlib.Topology.Order.IsNormal
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : WellFoundedLT α
inst_2 : TopologicalSpace α
inst_3 : OrderTopology α
inst_4 : LinearOrder β
inst_5 : WellFoundedLT β
inst_6 : TopologicalSpace β
inst_7 : OrderTopology β
f : α → β
hf : IsNormal f
b : β
a : α
ha : f ⁻¹' Iic b = Iio a
h : (f ⁻¹' Iic b).Nonempty
this_1 : Nonempty α
this : Nonempty β
inr : IsClosed (Iic (sSup (f ⁻¹' Iic b)))
⊢ IsClosed (f ⁻¹' Iic b)

Tactic:
rw [hf.preimage_Iic h (ha ▸ bddAbove_Iio)]

Premises used: Eq.rec, bddAbove_Iio, Order.IsNormal.preimage_Iic, Eq.symm
-- Module: Mathlib.Topology.Order.IsNormal
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : WellFoundedLT α
inst_2 : TopologicalSpace α
inst_3 : OrderTopology α
inst_4 : LinearOrder β
inst_5 : WellFoundedLT β
inst_6 : TopologicalSpace β
inst_7 : OrderTopology β
f : α → β
hf : IsNormal f
b : β
a : α
ha : f ⁻¹' Iic b = Iio a
h : (f ⁻¹' Iic b).Nonempty
this_1 : Nonempty α
this : Nonempty β
⊢ IsClosed (Iic (sSup (f ⁻¹' Iic b)))

Tactic:
isClosed_Iic

Premises used: isClosed_Iic
-- Module: Mathlib.Topology.Order.IsNormal
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : WellFoundedLT α
inst_2 : TopologicalSpace α
inst_3 : OrderTopology α
inst_4 : LinearOrder β
inst_5 : WellFoundedLT β
inst_6 : TopologicalSpace β
inst_7 : OrderTopology β
f : α → β
hf : IsNormal f
b : β
a : α
ha : f ⁻¹' Iic b = Iio a
h : (f ⁻¹' Iic b).Nonempty
this_1 : Nonempty α
this : Nonempty β
⊢ IsClosed (Iic (sSup (f ⁻¹' Iic b)))

Tactic:
exact isClosed_Iic

Premises used: isClosed_Iic
-- Module: Mathlib.Topology.Order.IsNormal
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : WellFoundedLT α
inst_2 : TopologicalSpace α
inst_3 : OrderTopology α
inst_4 : LinearOrder β
inst_5 : WellFoundedLT β
inst_6 : TopologicalSpace β
inst_7 : OrderTopology β
f : α → β
hs : StrictMono f
hc : Continuous f
⊢ IsNormal f

Tactic:
⟨hs, fun {a} ha ↦ (isLUB_of_mem_closure ?_ ?_).2⟩

Premises used: Order.IsNormal.mk, And.right, isLUB_of_mem_closure
-- Module: Mathlib.Topology.Order.IsNormal
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : WellFoundedLT α
inst_2 : TopologicalSpace α
inst_3 : OrderTopology α
inst_4 : LinearOrder β
inst_5 : WellFoundedLT β
inst_6 : TopologicalSpace β
inst_7 : OrderTopology β
f : α → β
hs : StrictMono f
hc : Continuous f
refine_1 : ∀ {a : α} (ha : IsSuccLimit a), f a ∈ upperBounds (f '' Iio a)
refine_2 : ∀ {a : α} (ha : IsSuccLimit a), f a ∈ closure (f '' Iio a)
⊢ IsNormal f

Tactic:
refine ⟨hs, fun {a} ha ↦ (isLUB_of_mem_closure ?_ ?_).2⟩
-- Module: Mathlib.Topology.Order.IsNormal
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : WellFoundedLT α
inst_2 : TopologicalSpace α
inst_3 : OrderTopology α
inst_4 : LinearOrder β
inst_5 : WellFoundedLT β
inst_6 : TopologicalSpace β
inst_7 : OrderTopology β
f : α → β
hs : StrictMono f
hc : Continuous f
a : α
ha : IsSuccLimit a
b : α
hb : b ∈ Iio a
⊢ f b ≤ f a

Tactic:
(hs hb).le

Premises used: LT.lt.le
-- Module: Mathlib.Topology.Order.IsNormal
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : WellFoundedLT α
inst_2 : TopologicalSpace α
inst_3 : OrderTopology α
inst_4 : LinearOrder β
inst_5 : WellFoundedLT β
inst_6 : TopologicalSpace β
inst_7 : OrderTopology β
f : α → β
hs : StrictMono f
hc : Continuous f
a : α
ha : IsSuccLimit a
b : α
hb : b ∈ Iio a
⊢ f b ≤ f a

Tactic:
exact (hs hb).le

Premises used: LT.lt.le
-- Module: Mathlib.Topology.Order.IsNormal
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : WellFoundedLT α
inst_2 : TopologicalSpace α
inst_3 : OrderTopology α
inst_4 : LinearOrder β
inst_5 : WellFoundedLT β
inst_6 : TopologicalSpace β
inst_7 : OrderTopology β
f : α → β
hs : StrictMono f
hc : Continuous f
a : α
ha : IsSuccLimit a
apply : a ∈ closure (Iio a)
⊢ f a ∈ closure (f '' Iio a)

Tactic:
apply image_closure_subset_closure_image hc (mem_image_of_mem ..)

Premises used: Set.mem_image_of_mem, image_closure_subset_closure_image
-- Module: Mathlib.Topology.Order.IsNormal
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : WellFoundedLT α
inst_2 : TopologicalSpace α
inst_3 : OrderTopology α
inst_4 : LinearOrder β
inst_5 : WellFoundedLT β
inst_6 : TopologicalSpace β
inst_7 : OrderTopology β
f : α → β
hs : StrictMono f
hc : Continuous f
a : α
ha : IsSuccLimit a
⊢ a ∈ closure (Iio a)

Tactic:
ha.isLUB_Iio.mem_closure (Iio_nonempty.2 ha.1)

Premises used: Iff.mpr, IsLUB.mem_closure, Set.Iio_nonempty, Order.IsSuccLimit.isLUB_Iio, And.left
-- Module: Mathlib.Topology.Order.IsNormal
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : WellFoundedLT α
inst_2 : TopologicalSpace α
inst_3 : OrderTopology α
inst_4 : LinearOrder β
inst_5 : WellFoundedLT β
inst_6 : TopologicalSpace β
inst_7 : OrderTopology β
f : α → β
hs : StrictMono f
hc : Continuous f
a : α
ha : IsSuccLimit a
⊢ a ∈ closure (Iio a)

Tactic:
exact ha.isLUB_Iio.mem_closure (Iio_nonempty.2 ha.1)

Premises used: Iff.mpr, IsLUB.mem_closure, Set.Iio_nonempty, Order.IsSuccLimit.isLUB_Iio, And.left
-- Module: Mathlib.Topology.Order.LowerUpperTopology
Goal:
α : Type u_1
⊢ Eq.{u_1 + 1} (α := WithLower α ≃ α) (Equiv.symm toLower) ofLower

Tactic:
rfl

Premises used: Topology.WithLower.ofLower, Topology.WithLower, Equiv.symm, Equiv.refl, rfl
-- Module: Mathlib.Topology.Order.LowerUpperTopology
Goal:
α : Type u_1
⊢ Eq.{u_1 + 1} (α := α ≃ WithLower α) (Equiv.symm ofLower) toLower

Tactic:
rfl

Premises used: Topology.WithLower, Topology.WithLower.toLower, Equiv.symm, Equiv.refl, rfl
-- Module: Mathlib.Topology.Order.LowerUpperTopology
Goal:
α : Type u_1
a : WithLower α
⊢ (toLower : (a : α) → WithLower α) ((ofLower : (a : WithLower α) → α) a : α) = a

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Order.LowerUpperTopology
Goal:
α : Type u_1
a : α
⊢ (ofLower : (a : WithLower α) → α) ((toLower : (a : α) → WithLower α) a : WithLower α) = a

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Order.LowerUpperTopology
Goal:
α : Type u_1
a b : α
⊢ Eq (α := WithLower α) ((toLower : (a : α) → WithLower α) a : WithLower α)
      ((toLower : (a : α) → WithLower α) b : WithLower α) ↔
    a = b

Tactic:
Iff.rfl

Premises used: Iff.rfl, Topology.WithLower
-- Module: Mathlib.Topology.Order.LowerUpperTopology
Goal:
α : Type u_1
a b : WithLower α
⊢ Eq (α := α) ((ofLower : (a : WithLower α) → α) a : α) ((ofLower : (a : WithLower α) → α) b : α) ↔ a = b

Tactic:
Iff.rfl

Premises used: Iff.rfl, Topology.WithLower
-- Module: Mathlib.Topology.Order.LowerUpperTopology
Goal:
α : Type u_1
inst : Preorder α
x y : α
⊢ LE.le (α := WithLower α) ((toLower : (a : α) → WithLower α) x : WithLower α)
      ((toLower : (a : α) → WithLower α) y : WithLower α) ↔
    x ≤ y

Tactic:
.rfl

Premises used: Iff.rfl
-- Module: Mathlib.Topology.Order.LowerUpperTopology
Goal:
α : Type u_1
inst : Preorder α
x y : α
⊢ LT.lt (α := WithLower α) ((toLower : (a : α) → WithLower α) x : WithLower α)
      ((toLower : (a : α) → WithLower α) y : WithLower α) ↔
    x < y

Tactic:
.rfl

Premises used: Iff.rfl
-- Module: Mathlib.Topology.Order.LowerUpperTopology
Goal:
α : Type u_1
inst : Preorder α
x y : WithLower α
⊢ LE.le (α := α) ((ofLower : (a : WithLower α) → α) x : α) ((ofLower : (a : WithLower α) → α) y : α) ↔ x ≤ y

Tactic:
.rfl

Premises used: Iff.rfl
-- Module: Mathlib.Topology.Order.LowerUpperTopology
Goal:
α : Type u_1
inst : Preorder α
x y : WithLower α
⊢ LT.lt (α := α) ((ofLower : (a : WithLower α) → α) x : α) ((ofLower : (a : WithLower α) → α) y : α) ↔ x < y

Tactic:
.rfl

Premises used: Iff.rfl
-- Module: Mathlib.Topology.Order.LowerUpperTopology
Goal:
α : Type u_1
inst : Preorder α
s : Set α
⊢ IsOpen[instTopologicalSpace] ((⇑ofLower : (a : WithLower α) → α) ⁻¹' s) ↔ IsOpen[lower α] s

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf, Topology.WithLower, Set.preimage
-- Module: Mathlib.Topology.Order.LowerUpperTopology
Goal:
α : Type u_1
inst : Preorder α
T : Set (WithLower α)
⊢ IsOpen[instTopologicalSpace] T ↔ IsOpen[lower α] ((⇑toLower : (a : α) → WithLower α) ⁻¹' T)

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf, Topology.WithLower, Set.preimage
-- Module: Mathlib.Topology.Order.LowerUpperTopology
Goal:
α : Type u_1
inst : Preorder α
inst_1 : TopologicalSpace α
inst_2 : ClosedIciTopology α
a : WithLower α
⊢ IsOpen[inst_1] ((⇑toLower : (a : α) → WithLower α) ⁻¹' (Ici a)ᶜ)

Tactic:
isClosed_Ici.isOpen_compl

Premises used: IsClosed.isOpen_compl, Set.Mem, setOf, Topology.WithLower, Set.preimage, Not
-- Module: Mathlib.Topology.Order.LowerUpperTopology
Goal:
α : Type u_1
inst : Preorder α
inst_1 : TopologicalSpace α
inst_2 : ClosedIciTopology α
a : WithLower α
⊢ IsOpen[inst_1] ((⇑toLower : (a : α) → WithLower α) ⁻¹' (Ici a)ᶜ)

Tactic:
exact isClosed_Ici.isOpen_compl

Premises used: IsClosed.isOpen_compl
-- Module: Mathlib.Topology.Order.LowerUpperTopology
Goal:
α : Type u_3
⊢ Eq.{u_3 + 1} (α := WithUpper α ≃ α) (Equiv.symm toUpper) ofUpper

Tactic:
rfl

Premises used: Topology.WithUpper, Equiv.symm, Equiv.refl, Topology.WithUpper.ofUpper, rfl
-- Module: Mathlib.Topology.Order.LowerUpperTopology
Goal:
α : Type u_1
⊢ Eq.{u_1 + 1} (α := α ≃ WithUpper α) (Equiv.symm ofUpper) toUpper

Tactic:
rfl

Premises used: Topology.WithUpper, Topology.WithUpper.toUpper, Equiv.symm, Equiv.refl, rfl
-- Module: Mathlib.Topology.Order.LowerUpperTopology
Goal:
α : Type u_1
a : WithUpper α
⊢ (toUpper : (a : α) → WithUpper α) ((ofUpper : (a : WithUpper α) → α) a : α) = a

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Order.LowerUpperTopology
Goal:
α : Type u_1
a : α
⊢ (ofUpper : (a : WithUpper α) → α) ((toUpper : (a : α) → WithUpper α) a : WithUpper α) = a

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Order.LowerUpperTopology
Goal:
α : Type u_1
a b : α
⊢ Eq (α := WithUpper α) ((toUpper : (a : α) → WithUpper α) a : WithUpper α)
      ((toUpper : (a : α) → WithUpper α) b : WithUpper α) ↔
    a = b

Tactic:
Iff.rfl

Premises used: Iff.rfl, Topology.WithUpper
-- Module: Mathlib.Topology.Order.LowerUpperTopology
Goal:
α : Type u_1
a b : WithUpper α
⊢ Eq (α := α) ((ofUpper : (a : WithUpper α) → α) a : α) ((ofUpper : (a : WithUpper α) → α) b : α) ↔ a = b

Tactic:
Iff.rfl

Premises used: Iff.rfl, Topology.WithUpper
-- Module: Mathlib.Topology.Order.LowerUpperTopology
Goal:
α : Type u_1
inst : Preorder α
x y : α
⊢ LE.le (α := WithUpper α) ((toUpper : (a : α) → WithUpper α) x : WithUpper α)
      ((toUpper : (a : α) → WithUpper α) y : WithUpper α) ↔
    x ≤ y

Tactic:
.rfl

Premises used: Iff.rfl
-- Module: Mathlib.Topology.Order.LowerUpperTopology
Goal:
α : Type u_1
inst : Preorder α
x y : α
⊢ LT.lt (α := WithUpper α) ((toUpper : (a : α) → WithUpper α) x : WithUpper α)
      ((toUpper : (a : α) → WithUpper α) y : WithUpper α) ↔
    x < y

Tactic:
.rfl

Premises used: Iff.rfl
-- Module: Mathlib.Topology.Order.LowerUpperTopology
Goal:
α : Type u_1
inst : Preorder α
x y : WithUpper α
⊢ LE.le (α := α) ((ofUpper : (a : WithUpper α) → α) x : α) ((ofUpper : (a : WithUpper α) → α) y : α) ↔ x ≤ y

Tactic:
.rfl

Premises used: Iff.rfl
-- Module: Mathlib.Topology.Order.LowerUpperTopology
Goal:
α : Type u_1
inst : Preorder α
x y : WithUpper α
⊢ LT.lt (α := α) ((ofUpper : (a : WithUpper α) → α) x : α) ((ofUpper : (a : WithUpper α) → α) y : α) ↔ x < y

Tactic:
.rfl

Premises used: Iff.rfl
-- Module: Mathlib.Topology.Order.LowerUpperTopology
Goal:
α : Type u_1
inst : Preorder α
s : Set α
⊢ IsOpen[instTopologicalSpace] ((⇑ofUpper : (a : WithUpper α) → α) ⁻¹' s) ↔ TopologicalSpace.IsOpen s

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf, Topology.WithUpper, Set.preimage, IsOpen
-- Module: Mathlib.Topology.Order.LowerUpperTopology
Goal:
α : Type u_1
inst : Preorder α
s : Set (WithUpper α)
⊢ IsOpen[instTopologicalSpace] s ↔ TopologicalSpace.IsOpen (X := α) ((⇑toUpper : (a : α) → WithUpper α) ⁻¹' s)

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf, Topology.WithUpper, Set.preimage, IsOpen
-- Module: Mathlib.Topology.Order.LowerUpperTopology
Goal:
α : Type u_1
inst : Preorder α
inst_1 : TopologicalSpace α
inst_2 : ClosedIicTopology α
a : WithUpper α
⊢ IsOpen[inst_1] ((⇑toUpper : (a : α) → WithUpper α) ⁻¹' (Iic a)ᶜ)

Tactic:
isClosed_Iic.isOpen_compl

Premises used: IsClosed.isOpen_compl, Set.Mem, setOf, Topology.WithUpper, Set.preimage, Not
-- Module: Mathlib.Topology.Order.LowerUpperTopology
Goal:
α : Type u_1
inst : Preorder α
inst_1 : TopologicalSpace α
inst_2 : ClosedIicTopology α
a : WithUpper α
⊢ IsOpen[inst_1] ((⇑toUpper : (a : α) → WithUpper α) ⁻¹' (Iic a)ᶜ)

Tactic:
exact isClosed_Iic.isOpen_compl

Premises used: IsClosed.isOpen_compl
-- Module: Mathlib.Topology.Order.LowerUpperTopology
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
⊢ IsLower.{u_1} (WithLower α)

Tactic:
⟨rfl⟩

Premises used: rfl, Topology.IsLower.mk
-- Module: Mathlib.Topology.Order.LowerUpperTopology
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
⊢ IsUpper.{u_1} (WithUpper α)

Tactic:
⟨rfl⟩

Premises used: Topology.IsUpper.mk, rfl
-- Module: Mathlib.Topology.Order.LowerUpperTopology
Goal:
α : Type u_1
inst : Preorder α
inst_1 : TopologicalSpace α
inst_2 : IsLower α
⊢ inst_1 = lower α

Tactic:
topology_eq_lowerTopology

Premises used: Topology.IsLower.topology_eq_lowerTopology
-- Module: Mathlib.Topology.Order.LowerUpperTopology
Goal:
α : Type u_1
inst : Preorder α
inst_1 : TopologicalSpace α
inst_2 : IsLower α
s : Set α
rw : IsOpen[lower α] s ↔ GenerateOpen {t : Set α | ∃ (a : α), (Ici a)ᶜ = t} s
⊢ IsOpen[inst_1] s ↔ GenerateOpen {t : Set α | ∃ (a : α), (Ici a)ᶜ = t} s

Tactic:
rw [topology_eq α]

Premises used: Topology.IsLower.topology_eq
-- Module: Mathlib.Topology.Order.LowerUpperTopology
Goal:
α : Type u_1
inst : Preorder α
inst_1 : TopologicalSpace α
inst_2 : IsLower α
s : Set α
⊢ IsOpen[lower α] s ↔ GenerateOpen {t : Set α | ∃ (a : α), (Ici a)ᶜ = t} s

Tactic:
rfl
-- Module: Mathlib.Topology.Order.LowerUpperTopology
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : TopologicalSpace α
inst_2 : IsLower α
s : Set α
⊢ ClosedIciTopology α

Tactic:
⟨fun a ↦ isOpen_compl_iff.1 <| isOpen_iff_generate_Ici_compl.2 <| GenerateOpen.basic _ ⟨a, rfl⟩⟩

Premises used: Iff.mpr, Set.Ici, Compl.compl, TopologicalSpace.GenerateOpen.basic, Topology.IsLower.isOpen_iff_generate_Ici_compl, Exists.intro, Iff.mp, ClosedIciTopology.mk, isOpen_compl_iff, rfl
-- Module: Mathlib.Topology.Order.LowerUpperTopology
Goal:
α : Type u_1
inst : Preorder α
inst_1 : TopologicalSpace α
inst_2 : IsLower α
s : Set α
h : s.Finite
simp : IsClosed[inst_1] (⋃ i ∈ s, (↑(UpperSet.Ici i) : Set α))
⊢ IsClosed[inst_1] (↑(upperClosure s) : Set α)

Tactic:
simp only [← UpperSet.iInf_Ici, UpperSet.coe_iInf]

Premises used: UpperSet.coe_iInf, UpperSet.iInf_Ici
-- Module: Mathlib.Topology.Order.LowerUpperTopology
Goal:
α : Type u_1
inst : Preorder α
inst_1 : TopologicalSpace α
inst_2 : IsLower α
s : Set α
h : s.Finite
⊢ IsClosed[inst_1] (⋃ i ∈ s, (↑(UpperSet.Ici i) : Set α))

Tactic:
h.isClosed_biUnion fun _ _ => isClosed_Ici

Premises used: Set.Finite.isClosed_biUnion, isClosed_Ici
-- Module: Mathlib.Topology.Order.LowerUpperTopology
Goal:
α : Type u_1
inst : Preorder α
inst_1 : TopologicalSpace α
inst_2 : IsLower α
s : Set α
h : s.Finite
⊢ IsClosed[inst_1] (⋃ i ∈ s, (↑(UpperSet.Ici i) : Set α))

Tactic:
exact h.isClosed_biUnion fun _ _ => isClosed_Ici

Premises used: Set.Finite.isClosed_biUnion, isClosed_Ici
-- Module: Mathlib.Topology.Order.LowerUpperTopology
Goal:
α : Type u_1
inst : Preorder α
inst_1 : TopologicalSpace α
inst_2 : IsLower α
s : Set α
h : IsOpen[inst_1] s
⊢ GenerateOpen {t : Set α | ∃ (a : α), (Ici a)ᶜ = t} s

Tactic:
replace h := isOpen_iff_generate_Ici_compl.1 h
-- Module: Mathlib.Topology.Order.LowerUpperTopology
Goal:
α : Type u_1
inst : Preorder α
inst_1 : TopologicalSpace α
inst_2 : IsLower α
s u : Set α
h' : Membership.mem (γ := Set (Set α)) {t : Set α | ∃ (a : α), (Ici a)ᶜ = t} u
basic : ∀ (a : α), IsLowerSet (Ici a)ᶜ
⊢ IsLowerSet u

Tactic:
obtain ⟨a, rfl⟩ := h'

Premises used: rfl
-- Module: Mathlib.Topology.Order.LowerUpperTopology
Goal:
α : Type u_1
inst : Preorder α
inst_1 : TopologicalSpace α
inst_2 : IsLower α
s : Set α
a : α
⊢ IsLowerSet (Ici a)ᶜ

Tactic:
(isUpperSet_Ici a).compl

Premises used: IsUpperSet.compl, isUpperSet_Ici
-- Module: Mathlib.Topology.Order.LowerUpperTopology
Goal:
α : Type u_1
inst : Preorder α
inst_1 : TopologicalSpace α
inst_2 : IsLower α
s : Set α
a : α
⊢ IsLowerSet (Ici a)ᶜ

Tactic:
exact (isUpperSet_Ici a).compl

Premises used: IsUpperSet.compl, isUpperSet_Ici
-- Module: Mathlib.Topology.Order.LowerUpperTopology
Goal:
α : Type u_1
inst : Preorder α
inst_1 : TopologicalSpace α
inst_2 : IsLower α
s : Set α
⊢ IsLowerSet.{u_1} (α := α) univ

Tactic:
isLowerSet_univ

Premises used: isLowerSet_univ
-- Module: Mathlib.Topology.Order.LowerUpperTopology
Goal:
α : Type u_1
inst : Preorder α
inst_1 : TopologicalSpace α
inst_2 : IsLower α
s : Set α
⊢ IsLowerSet.{u_1} (α := α) univ

Tactic:
exact isLowerSet_univ

Premises used: isLowerSet_univ
-- Module: Mathlib.Topology.Order.LowerUpperTopology
Goal:
α : Type u_1
inst : Preorder α
inst_1 : TopologicalSpace α
inst_2 : IsLower α
s u v : Set α
h : GenerateOpen {t : Set α | ∃ (a : α), (Ici a)ᶜ = t} u
h_1 : GenerateOpen {t : Set α | ∃ (a : α), (Ici a)ᶜ = t} v
hu2 : IsLowerSet u
hv2 : IsLowerSet v
⊢ IsLowerSet (u ∩ v)

Tactic:
hu2.inter hv2

Premises used: IsLowerSet.inter
-- Module: Mathlib.Topology.Order.LowerUpperTopology
Goal:
α : Type u_1
inst : Preorder α
inst_1 : TopologicalSpace α
inst_2 : IsLower α
s u v : Set α
h : GenerateOpen {t : Set α | ∃ (a : α), (Ici a)ᶜ = t} u
h_1 : GenerateOpen {t : Set α | ∃ (a : α), (Ici a)ᶜ = t} v
hu2 : IsLowerSet u
hv2 : IsLowerSet v
⊢ IsLowerSet (u ∩ v)

Tactic:
exact hu2.inter hv2

Premises used: IsLowerSet.inter
-- Module: Mathlib.Topology.Order.LowerUpperTopology
Goal:
α : Type u_1
inst : Preorder α
inst_1 : TopologicalSpace α
inst_2 : IsLower α
s : Set α
S : Set (Set α)
h : ∀ s ∈ S, GenerateOpen {t : Set α | ∃ (a : α), (Ici a)ᶜ = t} s
ih : ∀ s ∈ S, IsLowerSet s
⊢ IsLowerSet (⋃₀ S)

Tactic:
isLowerSet_sUnion ih

Premises used: isLowerSet_sUnion
-- Module: Mathlib.Topology.Order.LowerUpperTopology
Goal:
α : Type u_1
inst : Preorder α
inst_1 : TopologicalSpace α
inst_2 : IsLower α
s : Set α
S : Set (Set α)
h : ∀ s ∈ S, GenerateOpen {t : Set α | ∃ (a : α), (Ici a)ᶜ = t} s
ih : ∀ s ∈ S, IsLowerSet s
⊢ IsLowerSet (⋃₀ S)

Tactic:
exact isLowerSet_sUnion ih

Premises used: isLowerSet_sUnion
-- Module: Mathlib.Topology.Order.LowerUpperTopology
Goal:
α : Type u_1
inst : Preorder α
inst_1 : TopologicalSpace α
inst_2 : IsLower α
s : Set α
h : GenerateOpen {t : Set α | ∃ (a : α), (Ici a)ᶜ = t} s
basic : ∀ (u : Set α) (h' : Membership.mem (γ := Set (Set α)) {t : Set α | ∃ (a : α), (Ici a)ᶜ = t} u), IsLowerSet u
univ : IsLowerSet.{u_1} (α := α) Set.univ
inter :
  ∀ (u v : Set α),
    GenerateOpen {t : Set α | ∃ (a : α), (Ici a)ᶜ = t} u →
      GenerateOpen {t : Set α | ∃ (a : α), (Ici a)ᶜ = t} v →
        ∀ (hu2 : IsLowerSet u) (hv2 : IsLowerSet v), IsLowerSet (u ∩ v)
sUnion :
  ∀ (S : Set (Set α)),
    (∀ s ∈ S, GenerateOpen {t : Set α | ∃ (a : α), (Ici a)ᶜ = t} s) → ∀ (ih : ∀ s ∈ S, IsLowerSet s), IsLowerSet (⋃₀ S)
⊢ IsLowerSet s

Tactic:
induction h with
  | basic u h' => obtain ⟨a, rfl⟩ := h'; exact (isUpperSet_Ici a).compl
  | univ => exact isLowerSet_univ
  | inter u v _ _ hu2 hv2 => exact hu2.inter hv2
  | sUnion _ _ ih => exact isLowerSet_sUnion ih

Premises used: isLowerSet_univ, Set.univ, Set.sUnion, rfl
-- Module: Mathlib.Topology.Order.LowerUpperTopology
Goal:
α : Type u_1
inst : Preorder α
inst_1 : TopologicalSpace α
inst_2 : IsLower α
s : Set α
h : IsClosed[inst_1] s
⊢ IsUpperSet s

Tactic:
isLowerSet_compl.1 <| isLowerSet_of_isOpen h.isOpen_compl

Premises used: IsClosed.isOpen_compl, isLowerSet_compl, Iff.mp, Topology.IsLower.isLowerSet_of_isOpen
-- Module: Mathlib.Topology.Order.LowerUpperTopology
Goal:
α : Type u_1
inst : Preorder α
inst_1 : TopologicalSpace α
inst_2 : IsLower α
β : Type u_3
f : β → α
l : Filter β
x : α
⊢ Filter.Tendsto f l (𝓝 x) ↔ ∀ (y : α), ¬y ≤ x → ∀ᶠ (z : β) in l, ¬y ≤ f z

Tactic:
simp +instances [topology_eq_lowerTopology, tendsto_nhds_generateFrom_iff, Filter.Eventually, Ici,
    compl_setOf]

Premises used: TopologicalSpace.tendsto_nhds_generateFrom_iff, Set.Ici, Topology.IsLower.topology_eq_lowerTopology, Filter.Eventually, Set.compl_setOf
-- Module: Mathlib.Topology.Order.LowerUpperTopology
Goal:
α : Type u_1
inst : Preorder α
inst_1 : TopologicalSpace α
inst_2 : IsLower α
a : α
⊢ closure[inst_1] {a} = Ici a

Tactic:
Subset.antisymm ((closure_minimal fun _ h => h.ge) <| isClosed_Ici) <|
    (isUpperSet_of_isClosed isClosed_closure).Ici_subset <| subset_closure rfl

Premises used: Set.Subset.antisymm, subset_closure, closure_minimal, IsUpperSet.Ici_subset, Topology.IsLower.isUpperSet_of_isClosed, isClosed_closure, isClosed_Ici, rfl
-- Module: Mathlib.Topology.Order.LowerUpperTopology
Goal:
α : Type u_1
inst : Preorder α
inst_1 : TopologicalSpace α
inst_2 : IsLower α
⊢ IsTopologicalBasis.{u_1} (α := α)
    ((fun (f : Set (Set α)) ↦ ⋂₀ f) '' {f : Set (Set α) | f.Finite ∧ f ⊆ {s : Set α | ∃ (a : α), (Ici a)ᶜ = s}})

Tactic:
isTopologicalBasis_of_subbasis (topology_eq α)

Premises used: TopologicalSpace.isTopologicalBasis_of_subbasis, Topology.IsLower.topology_eq
-- Module: Mathlib.Topology.Order.LowerUpperTopology
Goal:
α : Type u_1
inst : Preorder α
inst_1 : TopologicalSpace α
inst_2 : IsLower α
h :
  lowerBasis α =
    (fun (f : Set (Set α)) ↦ ⋂₀ f) '' {f : Set (Set α) | f.Finite ∧ f ⊆ {s : Set α | ∃ (a : α), (Ici a)ᶜ = s}}
⊢ IsTopologicalBasis (lowerBasis α)

Tactic:
convert! isTopologicalBasis_of_subbasis (topology_eq α)

Premises used: TopologicalSpace.isTopologicalBasis_of_subbasis, Topology.IsLower.topology_eq
-- Module: Mathlib.Topology.Order.LowerUpperTopology
Goal:
α : Type u_1
inst : Preorder α
inst_1 : TopologicalSpace α
inst_2 : IsLower α
h :
  Eq.{u_1 + 1} (α := Set (Set α)) {s : Set α | ∃ (t : Set α), t.Finite ∧ ⋂ i ∈ t, (Ici i)ᶜ = s}
    ((fun (f : Set (Set α)) ↦ ⋂₀ f) '' {f : Set (Set α) | f.Finite ∧ f ⊆ {s : Set α | ∃ (a : α), (Ici a)ᶜ = s}})
⊢ lowerBasis α =
    (fun (f : Set (Set α)) ↦ ⋂₀ f) '' {f : Set (Set α) | f.Finite ∧ f ⊆ {s : Set α | ∃ (a : α), (Ici a)ᶜ = s}}

Tactic:
simp_rw [lowerBasis, coe_upperClosure, compl_iUnion]

Premises used: Topology.IsLower.lowerBasis, Set.compl_iUnion, coe_upperClosure
-- Module: Mathlib.Topology.Order.LowerUpperTopology
Goal:
α : Type u_1
inst : Preorder α
inst_1 : TopologicalSpace α
inst_2 : IsLower α
h :
  ∀ (s : Set α),
    Membership.mem (γ := Set (Set α)) {s : Set α | ∃ (t : Set α), t.Finite ∧ ⋂ i ∈ t, (Ici i)ᶜ = s} s ↔
      Membership.mem (γ := Set (Set α))
        ((fun (f : Set (Set α)) ↦ ⋂₀ f) '' {f : Set (Set α) | f.Finite ∧ f ⊆ {s : Set α | ∃ (a : α), (Ici a)ᶜ = s}}) s
⊢ Eq.{u_1 + 1} (α := Set (Set α)) {s : Set α | ∃ (t : Set α), t.Finite ∧ ⋂ i ∈ t, (Ici i)ᶜ = s}
    ((fun (f : Set (Set α)) ↦ ⋂₀ f) '' {f : Set (Set α) | f.Finite ∧ f ⊆ {s : Set α | ∃ (a : α), (Ici a)ᶜ = s}})

Tactic:
ext s
-- Module: Mathlib.Topology.Order.LowerUpperTopology
Goal:
α : Type u_1
inst : Preorder α
inst_1 : TopologicalSpace α
inst_2 : IsLower α
s : Set α
h :
  Membership.mem (γ := Set (Set α)) {s : Set α | ∃ (t : Set α), t.Finite ∧ ⋂ i ∈ t, (Ici i)ᶜ = s} s →
    Membership.mem (γ := Set (Set α))
      ((fun (f : Set (Set α)) ↦ ⋂₀ f) '' {f : Set (Set α) | f.Finite ∧ f ⊆ {s : Set α | ∃ (a : α), (Ici a)ᶜ = s}}) s
h₁ :
  Membership.mem (γ := Set (Set α))
      ((fun (f : Set (Set α)) ↦ ⋂₀ f) '' {f : Set (Set α) | f.Finite ∧ f ⊆ {s : Set α | ∃ (a : α), (Ici a)ᶜ = s}}) s →
    Membership.mem (γ := Set (Set α)) {s : Set α | ∃ (t : Set α), t.Finite ∧ ⋂ i ∈ t, (Ici i)ᶜ = s} s
⊢ Membership.mem (γ := Set (Set α)) {s : Set α | ∃ (t : Set α), t.Finite ∧ ⋂ i ∈ t, (Ici i)ᶜ = s} s ↔
    Membership.mem (γ := Set (Set α))
      ((fun (f : Set (Set α)) ↦ ⋂₀ f) '' {f : Set (Set α) | f.Finite ∧ f ⊆ {s : Set α | ∃ (a : α), (Ici a)ᶜ = s}}) s

Tactic:
constructor