awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Order.LowerUpperTopology
Goal:
α : Type u_1
inst : Preorder α
inst_1 : TopologicalSpace α
inst_2 : IsLower α
F : Set α
hF : F.Finite
⊢ Membership.mem (γ := Set (Set α))
    ((fun (f : Set (Set α)) ↦ ⋂₀ f) '' {f : Set (Set α) | f.Finite ∧ f ⊆ {s : Set α | ∃ (a : α), (Ici a)ᶜ = s}})
    (⋂ i ∈ F, (Ici i)ᶜ)

Tactic:
⟨(fun a => (Ici a)ᶜ) '' F, ⟨hF.image _, image_subset_iff.2 fun _ _ => ⟨_, rfl⟩⟩, ?_⟩

Premises used: Iff.mpr, Set.Ici, Set.Mem, Compl.compl, setOf, Set.Finite.image, And.intro, Exists.intro, Set.image, Set.image_subset_iff, rfl
-- Module: Mathlib.Topology.Order.LowerUpperTopology
Goal:
α : Type u_1
inst : Preorder α
inst_1 : TopologicalSpace α
inst_2 : IsLower α
F : Set α
hF : F.Finite
h : Eq.{u_1 + 1} (α := Set α) ((fun (f : Set (Set α)) ↦ ⋂₀ f) ((fun (a : α) ↦ (Ici a)ᶜ) '' F)) (⋂ i ∈ F, (Ici i)ᶜ)
⊢ Membership.mem (γ := Set (Set α))
    ((fun (f : Set (Set α)) ↦ ⋂₀ f) '' {f : Set (Set α) | f.Finite ∧ f ⊆ {s : Set α | ∃ (a : α), (Ici a)ᶜ = s}})
    (⋂ i ∈ F, (Ici i)ᶜ)

Tactic:
refine ⟨(fun a => (Ici a)ᶜ) '' F, ⟨hF.image _, image_subset_iff.2 fun _ _ => ⟨_, rfl⟩⟩, ?_⟩
-- Module: Mathlib.Topology.Order.LowerUpperTopology
Goal:
α : Type u_1
inst : Preorder α
inst_1 : TopologicalSpace α
inst_2 : IsLower α
F : Set α
hF : F.Finite
⊢ Eq.{u_1 + 1} (α := Set α) ((fun (f : Set (Set α)) ↦ ⋂₀ f) ((fun (a : α) ↦ (Ici a)ᶜ) '' F)) (⋂ i ∈ F, (Ici i)ᶜ)

Tactic:
simp only [sInter_image]

Premises used: Set.sInter_image
-- Module: Mathlib.Topology.Order.LowerUpperTopology
Goal:
α : Type u_1
inst : Preorder α
inst_1 : TopologicalSpace α
inst_2 : IsLower α
F : Set (Set α)
hF : F.Finite
hs : F ⊆ {s : Set α | ∃ (a : α), (Ici a)ᶜ = s}
⊢ Finite.{u_1 + 1} (↑F : Type u_1)

Tactic:
haveI := hF.to_subtype
-- Module: Mathlib.Topology.Order.LowerUpperTopology
Goal:
α : Type u_1
inst : Preorder α
inst_1 : TopologicalSpace α
inst_2 : IsLower α
F : Set (Set α)
hF : F.Finite
hs : F ⊆ {s : Set α | ∃ (a : α), (Ici a)ᶜ = s}
this : Finite.{u_1 + 1} (↑F : Type u_1)
⊢ ∀ (x : { a : Set α // a ∈ F }), Membership.mem (γ := Set (Set α)) {s : Set α | ∃ (a : α), (Ici a)ᶜ = s} (↑x : Set α)

Tactic:
rw [subset_def, Subtype.forall'] at hs

Premises used: Set.subset_def, Subtype.forall'
-- Module: Mathlib.Topology.Order.LowerUpperTopology
Goal:
α : Type u_1
inst : Preorder α
inst_1 : TopologicalSpace α
inst_2 : IsLower α
F : Set (Set α)
hF : F.Finite
hs : F ⊆ {s : Set α | ∃ (a : α), (Ici a)ᶜ = s}
this : Finite.{u_1 + 1} (↑F : Type u_1)
hs₁ :
  ∀ (x : { a : Set α // a ∈ F }), Membership.mem (γ := Set (Set α)) {s : Set α | ∃ (a : α), (Ici a)ᶜ = s} (↑x : Set α)
⊢ Finite.{u_1 + 1} (↑F : Type u_1)

Tactic:
rw [subset_def, Subtype.forall'] at hs

Premises used: Set.subset_def, Subtype.forall'
-- Module: Mathlib.Topology.Order.LowerUpperTopology
Goal:
α : Type u_1
inst : Preorder α
inst_1 : TopologicalSpace α
inst_2 : IsLower α
F : Set (Set α)
hF : F.Finite
hs :
  ∀ (x : { a : Set α // a ∈ F }), Membership.mem (γ := Set (Set α)) {s : Set α | ∃ (a : α), (Ici a)ᶜ = s} (↑x : Set α)
this : Finite.{u_1 + 1} (↑F : Type u_1)
h :
  ∀ (f : (x : { a : Set α // a ∈ F }) → α) (hf : ∀ (x : { a : Set α // a ∈ F }), (Ici (f x))ᶜ = (↑x : Set α)),
    Membership.mem (γ := Set (Set α)) {s : Set α | ∃ (t : Set α), t.Finite ∧ ⋂ i ∈ t, (Ici i)ᶜ = s}
      ((fun (f : Set (Set α)) ↦ ⋂₀ f) F)
⊢ Membership.mem (γ := Set (Set α)) {s : Set α | ∃ (t : Set α), t.Finite ∧ ⋂ i ∈ t, (Ici i)ᶜ = s}
    ((fun (f : Set (Set α)) ↦ ⋂₀ f) F)

Tactic:
choose f hf using hs
-- Module: Mathlib.Topology.Order.LowerUpperTopology
Goal:
α : Type u_1
inst : Preorder α
inst_1 : TopologicalSpace α
inst_2 : IsLower α
F : Set (Set α)
hF : F.Finite
this : Finite.{u_1 + 1} (↑F : Type u_1)
f : (x : { a : Set α // a ∈ F }) → α
hf : ∀ (x : { a : Set α // a ∈ F }), (Ici (f x))ᶜ = (↑x : Set α)
simp_rw simp_rw₁ : ⋂ i ∈ range f, (Ici i)ᶜ = ⋂₀ F
simp_rw₂ : ⋂ (y : { a : Set α // a ∈ F }), (Ici (f y))ᶜ = ⋂₀ F
simp_rw₃ : ⋂ (y : { a : Set α // a ∈ F }), (↑y : Set α) = ⋂₀ F
⊢ Eq.{u_1 + 1} (α := Set α) (⋂ i ∈ range f, (Ici i)ᶜ) ((fun (f : Set (Set α)) ↦ ⋂₀ f) F)

Tactic:
simp_rw [biInter_range, hf, sInter_eq_iInter]

Premises used: Set.sInter_eq_iInter, Set.biInter_range
-- Module: Mathlib.Topology.Order.LowerUpperTopology
Goal:
α : Type u_1
inst : Preorder α
inst_1 : TopologicalSpace α
inst_2 : IsLower α
F : Set (Set α)
hF : F.Finite
this : Finite.{u_1 + 1} (↑F : Type u_1)
f : (x : { a : Set α // a ∈ F }) → α
hf : ∀ (x : { a : Set α // a ∈ F }), (Ici (f x))ᶜ = (↑x : Set α)
⊢ Membership.mem (γ := Set (Set α)) {s : Set α | ∃ (t : Set α), t.Finite ∧ ⋂ i ∈ t, (Ici i)ᶜ = s}
    ((fun (f : Set (Set α)) ↦ ⋂₀ f) F)

Tactic:
exact ⟨_, finite_range f, by simp_rw [biInter_range, hf, sInter_eq_iInter]⟩
-- Module: Mathlib.Topology.Order.LowerUpperTopology
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : TopologicalSpace α
inst_2 : IsLower α
inst_3 : TopologicalSpace β
f : β → α
obtain : ∀ [IsLower α], Continuous[inst_3, lower α] f ↔ ∀ (a : α), IsClosed[inst_3] (f ⁻¹' Ici a)
⊢ Continuous[inst_3, inst_1] f ↔ ∀ (a : α), IsClosed[inst_3] (f ⁻¹' Ici a)

Tactic:
obtain rfl := IsLower.topology_eq α

Premises used: Topology.IsLower.topology_eq, rfl
-- Module: Mathlib.Topology.Order.LowerUpperTopology
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : TopologicalSpace β
f : β → α
inst_2 : IsLower α
⊢ Continuous[inst_1, lower α] f ↔ ∀ (a : α), IsClosed[inst_1] (f ⁻¹' Ici a)

Tactic:
simp [continuous_generateFrom_iff]

Premises used: continuous_generateFrom_iff
-- Module: Mathlib.Topology.Order.LowerUpperTopology
Goal:
α : Type u_1
β : Type u_2
inst : PartialOrder α
inst_1 : TopologicalSpace α
inst_2 : IsLower α
x y : α
h : Inseparable x y
⊢ Ici x = Ici y

Tactic:
simpa only [inseparable_iff_closure_eq, closure_singleton] using h

Premises used: inseparable_iff_closure_eq, Topology.IsLower.closure_singleton
-- Module: Mathlib.Topology.Order.LowerUpperTopology
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : IsLower α
rw : lower α = generateFrom {s : Set α | ∃ (a : α), (Ici a)ᶜ = s}
rw₁ rw₂ :
  Eq.{u_1 + 1} (α := TopologicalSpace α) (generateFrom {s : Set α | ∃ (a : α), (Ici a)ᶜ = s})
    (generateFrom {s : Set α | ∃ (a : α), (Ici a)ᶜ = s})
⊢ inst_1 = generateFrom {s : Set α | ∃ (a : α), (Ici a)ᶜ = s}

Tactic:
rw [topology_eq α, lower]

Premises used: Topology.IsLower.topology_eq, Topology.lower
-- Module: Mathlib.Topology.Order.LowerUpperTopology
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : IsLower α
b c : α
h : (Ici (min b c))ᶜ = (Ici b)ᶜ ∩ (Ici c)ᶜ
⊢ Membership.mem (γ := Set (Set α)) {s : Set α | ∃ (a : α), (Ici a)ᶜ = s} ((Ici b)ᶜ ∩ (Ici c)ᶜ)

Tactic:
use b ⊓ c
-- Module: Mathlib.Topology.Order.LowerUpperTopology
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : IsLower α
b c : α
h : Iio (min b c) = (Ici b)ᶜ ∩ (Ici c)ᶜ
h₁ : Iio (min b c) = Iio b ∩ (Ici c)ᶜ
h₂ : Iio (min b c) = Iio b ∩ Iio c
h₃ h₄ : Iio (min b c) = Iio (min b c)
⊢ (Ici (min b c))ᶜ = (Ici b)ᶜ ∩ (Ici c)ᶜ

Tactic:
rw [compl_Ici, compl_Ici, compl_Ici, Iio_inter_Iio]

Premises used: Set.Iio_inter_Iio, Set.compl_Ici
-- Module: Mathlib.Topology.Order.LowerUpperTopology
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : TopologicalSpace α
inst_2 : IsLower α
β : Type u_3
f : β → α
l : Filter β
x : α
⊢ Filter.Tendsto f l (𝓝 x) ↔ ∀ (y : α), x < y → ∀ᶠ (z : β) in l, f z < y

Tactic:
simp only [tendsto_nhds_iff_not_le, not_le]

Premises used: not_le, Topology.IsLower.tendsto_nhds_iff_not_le
-- Module: Mathlib.Topology.Order.LowerUpperTopology
Goal:
α : Type u_1
inst : CompleteLinearOrder α
t : TopologicalSpace α
inst_1 : IsLower α
U : Set α
pos : ∀ (hU : U = univ), IsOpen[t] U ↔ U = univ ∨ ∃ (a : α), (Ici a)ᶜ = U
neg : ∀ (hU : ¬U = univ), IsOpen[t] U ↔ U = univ ∨ ∃ (a : α), (Ici a)ᶜ = U
⊢ IsOpen[t] U ↔ U = univ ∨ ∃ (a : α), (Ici a)ᶜ = U

Tactic:
by_cases hU : U = univ

Premises used: Set.univ
-- Module: Mathlib.Topology.Order.LowerUpperTopology
Goal:
α : Type u_1
inst : CompleteLinearOrder α
t : TopologicalSpace α
inst_1 : IsLower α
U : Set α
hU : U = univ
⊢ IsOpen[t] U ↔ U = univ ∨ ∃ (a : α), (Ici a)ᶜ = U

Tactic:
simp only [hU, isOpen_univ, compl_Ici, true_or]

Premises used: true_or, isOpen_univ, Set.compl_Ici
-- Module: Mathlib.Topology.Order.LowerUpperTopology
Goal:
α : Type u_1
inst : CompleteLinearOrder α
t : TopologicalSpace α
inst_1 : IsLower α
U : Set α
hU : ¬U = univ
⊢ IsOpen[t] U ↔ U = univ ∨ ∃ (a : α), (Ici a)ᶜ = U

Tactic:
⟨?_, isTopologicalBasis_insert_univ_subbasis.isOpen⟩

Premises used: TopologicalSpace.IsTopologicalBasis.isOpen, Iff.intro, Topology.IsLower.isTopologicalBasis_insert_univ_subbasis
-- Module: Mathlib.Topology.Order.LowerUpperTopology
Goal:
α : Type u_1
inst : CompleteLinearOrder α
t : TopologicalSpace α
inst_1 : IsLower α
U : Set α
hU : ¬U = univ
neg : IsOpen[t] U → U = univ ∨ ∃ (a : α), (Ici a)ᶜ = U
⊢ IsOpen[t] U ↔ U = univ ∨ ∃ (a : α), (Ici a)ᶜ = U

Tactic:
refine ⟨?_, isTopologicalBasis_insert_univ_subbasis.isOpen⟩
-- Module: Mathlib.Topology.Order.LowerUpperTopology
Goal:
α : Type u_1
inst : CompleteLinearOrder α
t : TopologicalSpace α
inst_1 : IsLower α
U : Set α
hU : ¬U = univ
hO : IsOpen[t] U
neg : ∃ (a : α), (Ici a)ᶜ = U
⊢ U = univ ∨ ∃ (a : α), (Ici a)ᶜ = U

Tactic:
apply Or.inr

Premises used: Or.inr
-- Module: Mathlib.Topology.Order.LowerUpperTopology
Goal:
α : Type u_1
inst : CompleteLinearOrder α
t : TopologicalSpace α
inst_1 : IsLower α
U : Set α
hU : ¬U = univ
hO : IsOpen[t] U
⊢ ∃ S ⊆ insert univ {s : Set α | ∃ (a : α), (Ici a)ᶜ = s}, U = ⋃₀ S

Tactic:
IsTopologicalBasis.open_eq_sUnion isTopologicalBasis_insert_univ_subbasis hO

Premises used: TopologicalSpace.IsTopologicalBasis.open_eq_sUnion, Topology.IsLower.isTopologicalBasis_insert_univ_subbasis
-- Module: Mathlib.Topology.Order.LowerUpperTopology
Goal:
α : Type u_1
inst : CompleteLinearOrder α
t : TopologicalSpace α
inst_1 : IsLower α
U : Set α
hU : ¬U = univ
hO : IsOpen[t] U
a : (∃ (a : α), (Ici a)ᶜ = U) ↔ ∃ S ⊆ insert univ {s : Set α | ∃ (a : α), (Ici a)ᶜ = s}, U = ⋃₀ S
⊢ ∃ (a : α), (Ici a)ᶜ = U

Tactic:
convert! IsTopologicalBasis.open_eq_sUnion isTopologicalBasis_insert_univ_subbasis hO

Premises used: TopologicalSpace.IsTopologicalBasis.open_eq_sUnion, Topology.IsLower.isTopologicalBasis_insert_univ_subbasis
-- Module: Mathlib.Topology.Order.LowerUpperTopology
Goal:
α : Type u_1
inst : CompleteLinearOrder α
t : TopologicalSpace α
inst_1 : IsLower α
U : Set α
hU : ¬U = univ
hO : IsOpen[t] U
a : (∃ (a : α), (Ici a)ᶜ = U) → ∃ S ⊆ insert univ {s : Set α | ∃ (a : α), (Ici a)ᶜ = s}, U = ⋃₀ S
a₁ : (∃ S ⊆ insert univ {s : Set α | ∃ (a : α), (Ici a)ᶜ = s}, U = ⋃₀ S) → ∃ (a : α), (Ici a)ᶜ = U
⊢ (∃ (a : α), (Ici a)ᶜ = U) ↔ ∃ S ⊆ insert univ {s : Set α | ∃ (a : α), (Ici a)ᶜ = s}, U = ⋃₀ S

Tactic:
constructor
-- Module: Mathlib.Topology.Order.LowerUpperTopology
Goal:
α : Type u_1
inst : CompleteLinearOrder α
t : TopologicalSpace α
inst_1 : IsLower α
U : Set α
hU : ¬U = univ
hO : IsOpen[t] U
a : α
ha : (Ici a)ᶜ = U
h : Subset (α := Set (Set α)) {U} (insert univ {s : Set α | ∃ (a : α), (Ici a)ᶜ = s}) ∧ U = ⋃₀ {U}
⊢ ∃ S ⊆ insert univ {s : Set α | ∃ (a : α), (Ici a)ᶜ = s}, U = ⋃₀ S

Tactic:
use {U}
-- Module: Mathlib.Topology.Order.LowerUpperTopology
Goal:
α : Type u_1
inst : CompleteLinearOrder α
t : TopologicalSpace α
inst_1 : IsLower α
U : Set α
hU : ¬U = univ
hO : IsOpen[t] U
a : α
ha : (Ici a)ᶜ = U
h : Subset (α := Set (Set α)) {U} (insert univ {s : Set α | ∃ (a : α), (Ici a)ᶜ = s})
h₁ : U = ⋃₀ {U}
⊢ Subset (α := Set (Set α)) {U} (insert univ {s : Set α | ∃ (a : α), (Ici a)ᶜ = s}) ∧ U = ⋃₀ {U}

Tactic:
constructor
-- Module: Mathlib.Topology.Order.LowerUpperTopology
Goal:
α : Type u_1
inst : CompleteLinearOrder α
t : TopologicalSpace α
inst_1 : IsLower α
U : Set α
hU : ¬U = univ
hO : IsOpen[t] U
a : α
ha : (Ici a)ᶜ = U
apply : Membership.mem (γ := Set (Set α)) {s : Set α | ∃ (a : α), (Ici a)ᶜ = s} U
⊢ Subset (α := Set (Set α)) {U} (insert univ {s : Set α | ∃ (a : α), (Ici a)ᶜ = s})

Tactic:
apply subset_trans (singleton_subset_iff.mpr _) (subset_insert _ _)

Premises used: Iff.mpr, Set.singleton_subset_iff, subset_trans, Set.subset_insert
-- Module: Mathlib.Topology.Order.LowerUpperTopology
Goal:
α : Type u_1
inst : CompleteLinearOrder α
t : TopologicalSpace α
inst_1 : IsLower α
U : Set α
hU : ¬U = univ
hO : IsOpen[t] U
a : α
ha : (Ici a)ᶜ = U
w : α
h : (Ici a)ᶜ = U
⊢ Membership.mem (γ := Set (Set α)) {s : Set α | ∃ (a : α), (Ici a)ᶜ = s} U

Tactic:
use a
-- Module: Mathlib.Topology.Order.LowerUpperTopology
Goal:
α : Type u_1
inst : CompleteLinearOrder α
t : TopologicalSpace α
inst_1 : IsLower α
U : Set α
hU : ¬U = univ
hO : IsOpen[t] U
a : α
ha : (Ici a)ᶜ = U
h h₁ : U = U
⊢ U = ⋃₀ {U}

Tactic:
rw [sUnion_singleton]

Premises used: Set.sUnion_singleton
-- Module: Mathlib.Topology.Order.LowerUpperTopology
Goal:
α : Type u_1
inst : CompleteLinearOrder α
t : TopologicalSpace α
inst_1 : IsLower α
U : Set α
hU : ¬U = univ
hO : IsOpen[t] U
S : Set (Set α)
hS1 : S ⊆ insert univ {s : Set α | ∃ (a : α), (Ici a)ᶜ = s}
hS2 : U = ⋃₀ S
by_contra : ∀ (hUS' : univ ∈ S), False
⊢ univ ∉ S

Tactic:
by_contra hUS'
-- Module: Mathlib.Topology.Order.LowerUpperTopology
Goal:
α : Type u_1
inst : CompleteLinearOrder α
t : TopologicalSpace α
inst_1 : IsLower α
U : Set α
hU : ¬U = univ
hO : IsOpen[t] U
S : Set (Set α)
hS1 : S ⊆ insert univ {s : Set α | ∃ (a : α), (Ici a)ᶜ = s}
hS2 : U = ⋃₀ S
hUS' : univ ∈ S
apply : U = univ
⊢ False

Tactic:
apply hU
-- Module: Mathlib.Topology.Order.LowerUpperTopology
Goal:
α : Type u_1
inst : CompleteLinearOrder α
t : TopologicalSpace α
inst_1 : IsLower α
U : Set α
hU : ¬U = univ
hO : IsOpen[t] U
S : Set (Set α)
hS1 : S ⊆ insert univ {s : Set α | ∃ (a : α), (Ici a)ᶜ = s}
hS2 : U = ⋃₀ S
hUS' : univ ∈ S
rw : ⋃₀ S = univ
⊢ U = univ

Tactic:
rw [hS2]
-- Module: Mathlib.Topology.Order.LowerUpperTopology
Goal:
α : Type u_1
inst : CompleteLinearOrder α
t : TopologicalSpace α
inst_1 : IsLower α
U : Set α
hU : ¬U = univ
hO : IsOpen[t] U
S : Set (Set α)
hS1 : S ⊆ insert univ {s : Set α | ∃ (a : α), (Ici a)ᶜ = s}
hS2 : U = ⋃₀ S
hUS' : univ ∈ S
⊢ ⋃₀ S = univ

Tactic:
sUnion_eq_univ_iff.mpr (fun a => ⟨univ, hUS', trivial⟩)

Premises used: Iff.mpr, trivial, Set.univ, And.intro, Exists.intro, Set.sUnion_eq_univ_iff
-- Module: Mathlib.Topology.Order.LowerUpperTopology
Goal:
α : Type u_1
inst : CompleteLinearOrder α
t : TopologicalSpace α
inst_1 : IsLower α
U : Set α
hU : ¬U = univ
hO : IsOpen[t] U
S : Set (Set α)
hS1 : S ⊆ insert univ {s : Set α | ∃ (a : α), (Ici a)ᶜ = s}
hS2 : U = ⋃₀ S
hUS' : univ ∈ S
⊢ ⋃₀ S = univ

Tactic:
exact sUnion_eq_univ_iff.mpr (fun a => ⟨univ, hUS', trivial⟩)

Premises used: Iff.mpr, trivial, Set.univ, And.intro, Exists.intro, Set.sUnion_eq_univ_iff
-- Module: Mathlib.Topology.Order.LowerUpperTopology
Goal:
α : Type u_1
inst : CompleteLinearOrder α
t : TopologicalSpace α
inst_1 : IsLower α
U : Set α
hU : ¬U = univ
hO : IsOpen[t] U
S : Set (Set α)
hS1 : S ⊆ insert univ {s : Set α | ∃ (a : α), (Ici a)ᶜ = s}
hS2 : U = ⋃₀ S
⊢ univ ∉ S

Tactic:
have hUS : univ ∉ S := by
      by_contra hUS'
      apply hU
      rw [hS2]
      exact sUnion_eq_univ_iff.mpr (fun a => ⟨univ, hUS', trivial⟩)
-- Module: Mathlib.Topology.Order.LowerUpperTopology
Goal:
α : Type u_1
inst : CompleteLinearOrder α
t : TopologicalSpace α
inst_1 : IsLower α
U : Set α
hU : ¬U = univ
hO : IsOpen[t] U
S : Set (Set α)
hS1 : S ⊆ insert univ {s : Set α | ∃ (a : α), (Ici a)ᶜ = s}
hS2 : U = ⋃₀ S
hUS : univ ∉ S
h : (Ici (sSup {a : α | (Ici a)ᶜ ∈ S}))ᶜ = U
⊢ ∃ (a : α), (Ici a)ᶜ = U

Tactic:
use sSup {a | (Ici a)ᶜ ∈ S}

Premises used: Set.Ici, Compl.compl, setOf, Membership.mem, SupSet.sSup
-- Module: Mathlib.Topology.Order.LowerUpperTopology
Goal:
α : Type u_1
inst : CompleteLinearOrder α
t : TopologicalSpace α
inst_1 : IsLower α
U : Set α
hU : ¬U = univ
hO : IsOpen[t] U
S : Set (Set α)
hS1 : S ⊆ insert univ {s : Set α | ∃ (a : α), (Ici a)ᶜ = s}
hS2 : U = ⋃₀ S
hUS : univ ∉ S
h : Ici (sSup {a : α | (Ici a)ᶜ ∈ S}) = ⋂₀ (compl '' S)
⊢ (Ici (sSup {a : α | (Ici a)ᶜ ∈ S}))ᶜ = U

Tactic:
rw [hS2, sUnion_eq_compl_sInter_compl, compl_inj_iff]

Premises used: Set.sUnion_eq_compl_sInter_compl, compl_inj_iff
-- Module: Mathlib.Topology.Order.LowerUpperTopology
Goal:
α : Type u_1
inst : CompleteLinearOrder α
t : TopologicalSpace α
inst_1 : IsLower α
U : Set α
hU : ¬U = univ
hO : IsOpen[t] U
S : Set (Set α)
hS1 : S ⊆ insert univ {s : Set α | ∃ (a : α), (Ici a)ᶜ = s}
hS2 : U = ⋃₀ S
hUS : univ ∉ S
h : Ici (sSup {a : α | (Ici a)ᶜ ∈ S}) ≤ ⋂₀ (compl '' S)
h₁ : ⋂₀ (compl '' S) ≤ Ici (sSup {a : α | (Ici a)ᶜ ∈ S})
⊢ Ici (sSup {a : α | (Ici a)ᶜ ∈ S}) = ⋂₀ (compl '' S)

Tactic:
apply le_antisymm

Premises used: le_antisymm
-- Module: Mathlib.Topology.Order.LowerUpperTopology
Goal:
α : Type u_1
inst : CompleteLinearOrder α
t : TopologicalSpace α
inst_1 : IsLower α
U : Set α
hU : ¬U = univ
hO : IsOpen[t] U
S : Set (Set α)
hS1 : S ⊆ insert univ {s : Set α | ∃ (a : α), (Ici a)ᶜ = s}
hS2 : U = ⋃₀ S
hUS : univ ∉ S
b : α
hb : Membership.mem (γ := Set α) (Ici (sSup {a : α | (Ici a)ᶜ ∈ S})) b
h : ∀ (i : Set α) (i_1 : i ∈ S), b ∉ i
⊢ b ∈ ⋂₀ (compl '' S)

Tactic:
simp only [sInter_image, mem_iInter, mem_compl_iff]

Premises used: Set.mem_iInter, Set.sInter_image, Set.mem_compl_iff
-- Module: Mathlib.Topology.Order.LowerUpperTopology
Goal:
α : Type u_1
inst : CompleteLinearOrder α
t : TopologicalSpace α
inst_1 : IsLower α
U : Set α
hU : ¬U = univ
hO : IsOpen[t] U
S : Set (Set α)
hS1 : S ⊆ insert univ {s : Set α | ∃ (a : α), (Ici a)ᶜ = s}
hS2 : U = ⋃₀ S
hUS : univ ∉ S
b : α
hb : Membership.mem (γ := Set α) (Ici (sSup {a : α | (Ici a)ᶜ ∈ S})) b
s : Set α
hs : s ∈ S
h : ∀ (a : α) (ha : (Ici a)ᶜ = s), b ∉ s
⊢ b ∉ s

Tactic:
obtain ⟨a, ha⟩ := (subset_insert_iff_of_notMem hUS).mp hS1 hs

Premises used: Set.subset_insert_iff_of_notMem, Iff.mp
-- Module: Mathlib.Topology.Order.LowerUpperTopology
Goal:
α : Type u_1
inst : CompleteLinearOrder α
t : TopologicalSpace α
inst_1 : IsLower α
U : Set α
hU : ¬U = univ
hO : IsOpen[t] U
S : Set (Set α)
hS1 : S ⊆ insert univ {s : Set α | ∃ (a : α), (Ici a)ᶜ = s}
hS2 : U = ⋃₀ S
hUS : univ ∉ S
b : α
hb : Membership.mem (γ := Set α) (Ici (sSup {a : α | (Ici a)ᶜ ∈ S})) b
s : Set α
hs : s ∈ S
a : α
ha : (Ici a)ᶜ = s
h : ∀ (hU : ¬⋃₀ S = univ) (hO : IsOpen[t] (⋃₀ S)) (hs : (Ici a)ᶜ ∈ S), b ∉ (Ici a)ᶜ
⊢ b ∉ s

Tactic:
subst hS2 ha
-- Module: Mathlib.Topology.Order.LowerUpperTopology
Goal:
α : Type u_1
inst : CompleteLinearOrder α
t : TopologicalSpace α
inst_1 : IsLower α
S : Set (Set α)
hS1 : S ⊆ insert univ {s : Set α | ∃ (a : α), (Ici a)ᶜ = s}
hUS : univ ∉ S
b : α
hb : Membership.mem (γ := Set α) (Ici (sSup {a : α | (Ici a)ᶜ ∈ S})) b
a : α
hU : ¬⋃₀ S = univ
hO : IsOpen[t] (⋃₀ S)
hs : (Ici a)ᶜ ∈ S
⊢ b ∉ (Ici a)ᶜ

Tactic:
simp_all only [compl_Ici, mem_Ici, sSup_le_iff, mem_setOf_eq, mem_Iio, not_lt]

Premises used: Set.mem_Iio, Set.mem_setOf_eq, not_lt, Set.mem_Ici, Set.compl_Ici, sSup_le_iff
-- Module: Mathlib.Topology.Order.LowerUpperTopology
Goal:
α : Type u_1
inst : CompleteLinearOrder α
t : TopologicalSpace α
inst_1 : IsLower α
U : Set α
hU : ¬U = univ
hO : IsOpen[t] U
S : Set (Set α)
hS1 : S ⊆ insert univ {s : Set α | ∃ (a : α), (Ici a)ᶜ = s}
hS2 : U = ⋃₀ S
hUS : univ ∉ S
b : α
hb : b ∈ ⋂₀ (compl '' S)
h : ∀ (b_1 : α), Membership.mem (γ := Set α) {a : α | (Ici a)ᶜ ∈ S} b_1 → b_1 ≤ b
⊢ Membership.mem (γ := Set α) (Ici (sSup {a : α | (Ici a)ᶜ ∈ S})) b

Tactic:
rw [mem_Ici, sSup_le_iff]

Premises used: Set.mem_Ici, sSup_le_iff
-- Module: Mathlib.Topology.Order.LowerUpperTopology
Goal:
α : Type u_1
inst : CompleteLinearOrder α
t : TopologicalSpace α
inst_1 : IsLower α
U : Set α
hU : ¬U = univ
hO : IsOpen[t] U
S : Set (Set α)
hS1 : S ⊆ insert univ {s : Set α | ∃ (a : α), (Ici a)ᶜ = s}
hS2 : U = ⋃₀ S
hUS : univ ∉ S
b : α
hb : b ∈ ⋂₀ (compl '' S)
c : α
hc : Membership.mem (γ := Set α) {a : α | (Ici a)ᶜ ∈ S} c
⊢ ∀ (i : Set α) (i_1 : i ∈ S), b ∈ iᶜ

Tactic:
simp only [sInter_image, mem_iInter] at hb

Premises used: Set.mem_iInter, Set.sInter_image
-- Module: Mathlib.Topology.Order.LowerUpperTopology
Goal:
α : Type u_1
inst : CompleteLinearOrder α
t : TopologicalSpace α
inst_1 : IsLower α
U : Set α
hU : ¬U = univ
hO : IsOpen[t] U
S : Set (Set α)
hS1 : S ⊆ insert univ {s : Set α | ∃ (a : α), (Ici a)ᶜ = s}
hS2 : U = ⋃₀ S
hUS : univ ∉ S
b c : α
hc : Membership.mem (γ := Set α) {a : α | (Ici a)ᶜ ∈ S} c
hb : ∀ (i : Set α) (i_1 : i ∈ S), b ∈ iᶜ
h : b ∉ (Ici c)ᶜ
⊢ c ≤ b

Tactic:
rw [← not_lt, ← mem_Iio, ← compl_Ici]

Premises used: Set.mem_Iio, not_lt, Set.compl_Ici
-- Module: Mathlib.Topology.Order.LowerUpperTopology
Goal:
α : Type u_1
inst : CompleteLinearOrder α
t : TopologicalSpace α
inst_1 : IsLower α
U : Set α
hU : ¬U = univ
hO : IsOpen[t] U
S : Set (Set α)
hS1 : S ⊆ insert univ {s : Set α | ∃ (a : α), (Ici a)ᶜ = s}
hS2 : U = ⋃₀ S
hUS : univ ∉ S
b c : α
hc : Membership.mem (γ := Set α) {a : α | (Ici a)ᶜ ∈ S} c
hb : ∀ (i : Set α) (i_1 : i ∈ S), b ∈ iᶜ
⊢ b ∉ (Ici c)ᶜ

Tactic:
hb _ hc

Premises used: Set.Mem, setOf, Not
-- Module: Mathlib.Topology.Order.LowerUpperTopology
Goal:
α : Type u_1
inst : CompleteLinearOrder α
t : TopologicalSpace α
inst_1 : IsLower α
U : Set α
hU : ¬U = univ
hO : IsOpen[t] U
S : Set (Set α)
hS1 : S ⊆ insert univ {s : Set α | ∃ (a : α), (Ici a)ᶜ = s}
hS2 : U = ⋃₀ S
hUS : univ ∉ S
b c : α
hc : Membership.mem (γ := Set α) {a : α | (Ici a)ᶜ ∈ S} c
hb : ∀ (i : Set α) (i_1 : i ∈ S), b ∈ iᶜ
⊢ b ∉ (Ici c)ᶜ

Tactic:
exact hb _ hc
-- Module: Mathlib.Topology.Order.LowerUpperTopology
Goal:
α : Type u_1
inst : Preorder α
inst_1 : TopologicalSpace α
inst_2 : IsUpper α
⊢ inst_1 = upper α

Tactic:
topology_eq_upperTopology

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

Tactic:
rw [topology_eq α]

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

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

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

Premises used: Iff.mpr, Topology.IsUpper.isOpen_iff_generate_Iic_compl, Compl.compl, TopologicalSpace.GenerateOpen.basic, ClosedIicTopology.mk, Exists.intro, Iff.mp, Set.Iic, isOpen_compl_iff, rfl
-- Module: Mathlib.Topology.Order.LowerUpperTopology
Goal:
α : Type u_1
inst : Preorder α
inst_1 : TopologicalSpace α
inst_2 : IsUpper α
s : Set α
h : s.Finite
⊢ IsClosed[inst_1] (↑(lowerClosure s) : Set α)

Tactic:
IsLower.isClosed_upperClosure (α := αᵒᵈ) h

Premises used: Set.Mem, setOf, Topology.IsLower.isClosed_upperClosure, OrderDual
-- Module: Mathlib.Topology.Order.LowerUpperTopology
Goal:
α : Type u_1
inst : Preorder α
inst_1 : TopologicalSpace α
inst_2 : IsUpper α
s : Set α
h : IsOpen[inst_1] s
⊢ IsUpperSet s

Tactic:
IsLower.isLowerSet_of_isOpen (α := αᵒᵈ) h

Premises used: Set.Mem, IsUpperSet, Topology.IsLower.isLowerSet_of_isOpen, OrderDual
-- Module: Mathlib.Topology.Order.LowerUpperTopology
Goal:
α : Type u_1
inst : Preorder α
inst_1 : TopologicalSpace α
inst_2 : IsUpper α
s : Set α
h : IsClosed[inst_1] s
⊢ IsLowerSet s

Tactic:
isUpperSet_compl.1 <| isUpperSet_of_isOpen h.isOpen_compl

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

Tactic:
IsLower.tendsto_nhds_iff_not_le (α := αᵒᵈ)

Premises used: Topology.IsLower.tendsto_nhds_iff_not_le, OrderDual
-- Module: Mathlib.Topology.Order.LowerUpperTopology
Goal:
α : Type u_1
inst : Preorder α
inst_1 : TopologicalSpace α
inst_2 : IsUpper α
a : α
⊢ closure[inst_1] {a} = Iic a

Tactic:
IsLower.closure_singleton (α := αᵒᵈ) _

Premises used: setOf, Set.Iic, OrderDual, Topology.IsLower.closure_singleton