awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Order.UpperLowerSetTopology
Goal:
α : Type u_1
a b : WithUpperSet α
⊢ Eq (α := α) ((ofUpperSet : (a : WithUpperSet α) → α) a : α) ((ofUpperSet : (a : WithUpperSet α) → α) b : α) ↔ a = b

Tactic:
Iff.rfl

Premises used: Iff.rfl, Topology.WithUpperSet
-- Module: Mathlib.Topology.Order.UpperLowerSetTopology
Goal:
α : Type u_1
inst : Preorder α
a b : WithUpperSet α
⊢ LE.le (α := α) ((ofUpperSet : (a : WithUpperSet α) → α) a : α) ((ofUpperSet : (a : WithUpperSet α) → α) b : α) ↔ a ≤ b

Tactic:
Iff.rfl

Premises used: Iff.rfl
-- Module: Mathlib.Topology.Order.UpperLowerSetTopology
Goal:
α : Type u_1
inst : Preorder α
a b : α
⊢ LE.le (α := WithUpperSet α) ((toUpperSet : (a : α) → WithUpperSet α) a : WithUpperSet α)
      ((toUpperSet : (a : α) → WithUpperSet α) b : WithUpperSet α) ↔
    a ≤ b

Tactic:
Iff.rfl

Premises used: Iff.rfl
-- Module: Mathlib.Topology.Order.UpperLowerSetTopology
Goal:
α : Type u_1
⊢ Eq.{u_1 + 1} (α := WithLowerSet α ≃ α) (Equiv.symm toLowerSet) ofLowerSet

Tactic:
rfl

Premises used: Topology.WithLowerSet.ofLowerSet, Equiv.symm, Topology.WithLowerSet, Equiv.refl, rfl
-- Module: Mathlib.Topology.Order.UpperLowerSetTopology
Goal:
α : Type u_1
⊢ Eq.{u_1 + 1} (α := α ≃ WithLowerSet α) (Equiv.symm ofLowerSet) toLowerSet

Tactic:
rfl

Premises used: Equiv.symm, Topology.WithLowerSet, Equiv.refl, rfl, Topology.WithLowerSet.toLowerSet
-- Module: Mathlib.Topology.Order.UpperLowerSetTopology
Goal:
α : Type u_1
a : WithLowerSet α
⊢ (toLowerSet : (a : α) → WithLowerSet α) ((ofLowerSet : (a : WithLowerSet α) → α) a : α) = a

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Order.UpperLowerSetTopology
Goal:
α : Type u_1
a : α
⊢ (ofLowerSet : (a : WithLowerSet α) → α) ((toLowerSet : (a : α) → WithLowerSet α) a : WithLowerSet α) = a

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Order.UpperLowerSetTopology
Goal:
α : Type u_1
a b : α
⊢ Eq (α := WithLowerSet α) ((toLowerSet : (a : α) → WithLowerSet α) a : WithLowerSet α)
      ((toLowerSet : (a : α) → WithLowerSet α) b : WithLowerSet α) ↔
    a = b

Tactic:
Iff.rfl

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

Tactic:
Iff.rfl

Premises used: Iff.rfl, Topology.WithLowerSet
-- Module: Mathlib.Topology.Order.UpperLowerSetTopology
Goal:
α : Type u_1
inst : Preorder α
a b : WithLowerSet α
⊢ LE.le (α := α) ((ofLowerSet : (a : WithLowerSet α) → α) a : α) ((ofLowerSet : (a : WithLowerSet α) → α) b : α) ↔ a ≤ b

Tactic:
Iff.rfl

Premises used: Iff.rfl
-- Module: Mathlib.Topology.Order.UpperLowerSetTopology
Goal:
α : Type u_1
inst : Preorder α
a b : α
⊢ LE.le (α := WithLowerSet α) ((toLowerSet : (a : α) → WithLowerSet α) a : WithLowerSet α)
      ((toLowerSet : (a : α) → WithLowerSet α) b : WithLowerSet α) ↔
    a ≤ b

Tactic:
Iff.rfl

Premises used: Iff.rfl
-- Module: Mathlib.Topology.Order.UpperLowerSetTopology
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : Preorder α
⊢ Topology.IsUpperSet.{u_1} (WithUpperSet α)

Tactic:
⟨rfl⟩

Premises used: Topology.IsUpperSet.mk, rfl
-- Module: Mathlib.Topology.Order.UpperLowerSetTopology
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : Preorder α
this : TopologicalSpace α := upperSet α
⊢ Topology.IsUpperSet α

Tactic:
⟨rfl⟩

Premises used: Topology.IsUpperSet.mk, rfl
-- Module: Mathlib.Topology.Order.UpperLowerSetTopology
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : Preorder α
this : TopologicalSpace α := upperSet α
⊢ Topology.IsUpperSet α

Tactic:
exact ⟨rfl⟩
-- Module: Mathlib.Topology.Order.UpperLowerSetTopology
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : Preorder α
⊢ Topology.IsLowerSet.{u_1} (WithLowerSet α)

Tactic:
⟨rfl⟩

Premises used: Topology.IsLowerSet.mk, rfl
-- Module: Mathlib.Topology.Order.UpperLowerSetTopology
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : Preorder α
this : TopologicalSpace α := lowerSet α
⊢ Topology.IsLowerSet α

Tactic:
⟨rfl⟩

Premises used: Topology.IsLowerSet.mk, rfl
-- Module: Mathlib.Topology.Order.UpperLowerSetTopology
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : Preorder α
this : TopologicalSpace α := lowerSet α
⊢ Topology.IsLowerSet α

Tactic:
exact ⟨rfl⟩
-- Module: Mathlib.Topology.Order.UpperLowerSetTopology
Goal:
α : Type u_1
inst : Preorder α
inst_1 : TopologicalSpace α
inst_2 : Topology.IsUpperSet α
⊢ inst_1 = upperSet α

Tactic:
topology_eq_upperSetTopology

Premises used: Topology.IsUpperSet.topology_eq_upperSetTopology
-- Module: Mathlib.Topology.Order.UpperLowerSetTopology
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : Preorder α
inst_1 : TopologicalSpace α
inst_2 : Topology.IsUpperSet α
s : Set α
a : ∀ (x : Set αᵒᵈ), IsOpen[OrderDual.instTopologicalSpace] x ↔ IsOpen[lowerSet αᵒᵈ] x
⊢ Eq.{u_1 + 1} (α := TopologicalSpace αᵒᵈ) OrderDual.instTopologicalSpace (lowerSet αᵒᵈ)

Tactic:
ext
-- Module: Mathlib.Topology.Order.UpperLowerSetTopology
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : Preorder α
inst_1 : TopologicalSpace α
inst_2 : Topology.IsUpperSet α
s : Set α
x : Set αᵒᵈ
a a₁ : IsOpen[OrderDual.instTopologicalSpace] x ↔ IsOpen[lowerSet αᵒᵈ] x
⊢ IsOpen[OrderDual.instTopologicalSpace] x ↔ IsOpen[lowerSet αᵒᵈ] x

Tactic:
rw [IsUpperSet.topology_eq α]

Premises used: Topology.IsUpperSet.topology_eq
-- Module: Mathlib.Topology.Order.UpperLowerSetTopology
Goal:
α : Type u_1
inst : Preorder α
inst_1 : TopologicalSpace α
inst_2 : Topology.IsUpperSet α
s : Set α
rw : IsOpen[upperSet α] s ↔ IsUpperSet s
⊢ IsOpen[inst_1] s ↔ IsUpperSet s

Tactic:
rw [topology_eq α]

Premises used: Topology.IsUpperSet.topology_eq
-- Module: Mathlib.Topology.Order.UpperLowerSetTopology
Goal:
α : Type u_1
inst : Preorder α
inst_1 : TopologicalSpace α
inst_2 : Topology.IsUpperSet α
s : Set α
⊢ IsOpen[upperSet α] s ↔ IsUpperSet s

Tactic:
rfl
-- Module: Mathlib.Topology.Order.UpperLowerSetTopology
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : Preorder α
inst_1 : TopologicalSpace α
inst_2 : Topology.IsUpperSet α
s : Set α
S : Set (Set α)
⊢ (∀ s ∈ S, IsOpen[inst_1] s) → IsOpen[inst_1] (⋂₀ S)

Tactic:
simpa only [isOpen_iff_isUpperSet] using isUpperSet_sInter (α := α)

Premises used: Topology.IsUpperSet.isOpen_iff_isUpperSet, isUpperSet_sInter
-- Module: Mathlib.Topology.Order.UpperLowerSetTopology
Goal:
α : Type u_1
inst : Preorder α
inst_1 : TopologicalSpace α
inst_2 : Topology.IsUpperSet α
s : Set α
rw : IsOpen[inst_1] sᶜ ↔ IsLowerSet s
rw₁ : IsUpperSet sᶜ ↔ IsLowerSet s
rw₂ : IsLowerSet sᶜᶜ ↔ IsLowerSet s
rw₃ rw₄ : IsLowerSet s ↔ IsLowerSet s
⊢ IsClosed[inst_1] s ↔ IsLowerSet s

Tactic:
rw [← isOpen_compl_iff, isOpen_iff_isUpperSet,
    isLowerSet_compl.symm, compl_compl]

Premises used: compl_compl, Topology.IsUpperSet.isOpen_iff_isUpperSet, isLowerSet_compl, Iff.symm, isOpen_compl_iff
-- Module: Mathlib.Topology.Order.UpperLowerSetTopology
Goal:
α : Type u_1
inst : Preorder α
inst_1 : TopologicalSpace α
inst_2 : Topology.IsUpperSet α
s : Set α
rw : closure[inst_1] s ⊆ (↑(lowerClosure s) : Set α) ∧ (↑(lowerClosure s) : Set α) ⊆ closure[inst_1] s
⊢ closure[inst_1] s = (↑(lowerClosure s) : Set α)

Tactic:
rw [subset_antisymm_iff]

Premises used: subset_antisymm_iff
-- Module: Mathlib.Topology.Order.UpperLowerSetTopology
Goal:
α : Type u_1
inst : Preorder α
inst_1 : TopologicalSpace α
inst_2 : Topology.IsUpperSet α
s : Set α
⊢ closure[inst_1] s ⊆ (↑(lowerClosure s) : Set α) ∧ (↑(lowerClosure s) : Set α) ⊆ closure[inst_1] s

Tactic:
⟨?_, lowerClosure_min subset_closure (isClosed_iff_isLower.1 isClosed_closure)⟩

Premises used: subset_closure, Topology.IsUpperSet.isClosed_iff_isLower, And.intro, Iff.mp, lowerClosure_min, isClosed_closure
-- Module: Mathlib.Topology.Order.UpperLowerSetTopology
Goal:
α : Type u_1
inst : Preorder α
inst_1 : TopologicalSpace α
inst_2 : Topology.IsUpperSet α
s : Set α
refine : closure[inst_1] s ⊆ (↑(lowerClosure s) : Set α)
⊢ closure[inst_1] s ⊆ (↑(lowerClosure s) : Set α) ∧ (↑(lowerClosure s) : Set α) ⊆ closure[inst_1] s

Tactic:
refine ⟨?_, lowerClosure_min subset_closure (isClosed_iff_isLower.1 isClosed_closure)⟩
-- Module: Mathlib.Topology.Order.UpperLowerSetTopology
Goal:
α : Type u_1
inst : Preorder α
inst_1 : TopologicalSpace α
inst_2 : Topology.IsUpperSet α
s : Set α
apply : IsClosed[inst_1] (↑(lowerClosure s) : Set α)
⊢ closure[inst_1] s ⊆ (↑(lowerClosure s) : Set α)

Tactic:
apply closure_minimal subset_lowerClosure _

Premises used: subset_lowerClosure, closure_minimal
-- Module: Mathlib.Topology.Order.UpperLowerSetTopology
Goal:
α : Type u_1
inst : Preorder α
inst_1 : TopologicalSpace α
inst_2 : Topology.IsUpperSet α
s : Set α
rw : IsLowerSet (↑(lowerClosure s) : Set α)
⊢ IsClosed[inst_1] (↑(lowerClosure s) : Set α)

Tactic:
rw [isClosed_iff_isLower]

Premises used: Topology.IsUpperSet.isClosed_iff_isLower
-- Module: Mathlib.Topology.Order.UpperLowerSetTopology
Goal:
α : Type u_1
inst : Preorder α
inst_1 : TopologicalSpace α
inst_2 : Topology.IsUpperSet α
s : Set α
⊢ IsLowerSet (↑(lowerClosure s) : Set α)

Tactic:
LowerSet.lower (lowerClosure s)

Premises used: LowerSet.lower, lowerClosure
-- Module: Mathlib.Topology.Order.UpperLowerSetTopology
Goal:
α : Type u_1
inst : Preorder α
inst_1 : TopologicalSpace α
inst_2 : Topology.IsUpperSet α
s : Set α
⊢ IsLowerSet (↑(lowerClosure s) : Set α)

Tactic:
exact LowerSet.lower (lowerClosure s)

Premises used: LowerSet.lower, lowerClosure
-- Module: Mathlib.Topology.Order.UpperLowerSetTopology
Goal:
α : Type u_1
inst : Preorder α
inst_1 : TopologicalSpace α
inst_2 : Topology.IsUpperSet α
a : α
rw : (↑(LowerSet.Iic a) : Set α) = Iic a
⊢ closure[inst_1] {a} = Iic a

Tactic:
rw [closure_eq_lowerClosure, lowerClosure_singleton]

Premises used: lowerClosure_singleton, Topology.IsUpperSet.closure_eq_lowerClosure
-- Module: Mathlib.Topology.Order.UpperLowerSetTopology
Goal:
α : Type u_1
inst : Preorder α
inst_1 : TopologicalSpace α
inst_2 : Topology.IsUpperSet α
a : α
⊢ (↑(LowerSet.Iic a) : Set α) = Iic a

Tactic:
rfl
-- Module: Mathlib.Topology.Order.UpperLowerSetTopology
Goal:
α : Type u_1
inst : Preorder α
inst_1 : TopologicalSpace α
inst_2 : Topology.IsUpperSet α
a b : α
⊢ a ⤳ b ↔ b ≤ a

Tactic:
simp only [specializes_iff_closure_subset, closure_singleton, Iic_subset_Iic]

Premises used: Set.Iic_subset_Iic, Topology.IsUpperSet.closure_singleton, specializes_iff_closure_subset
-- Module: Mathlib.Topology.Order.UpperLowerSetTopology
Goal:
α : Type u_1
inst : Preorder α
inst_1 : TopologicalSpace α
inst_2 : Topology.IsUpperSet α
s : Set α
h : ∀ (x : α), x ∈ nhdsKer s ↔ x ∈ (↑(upperClosure s) : Set α)
⊢ nhdsKer s = (↑(upperClosure s) : Set α)

Tactic:
ext
-- Module: Mathlib.Topology.Order.UpperLowerSetTopology
Goal:
α : Type u_1
inst : Preorder α
inst_1 : TopologicalSpace α
inst_2 : Topology.IsUpperSet α
s : Set α
x : α
⊢ x ∈ nhdsKer s ↔ x ∈ (↑(upperClosure s) : Set α)

Tactic:
simp [mem_nhdsKer_iff_specializes, specializes_iff_le]

Premises used: mem_nhdsKer_iff_specializes, Topology.IsUpperSet.specializes_iff_le
-- Module: Mathlib.Topology.Order.UpperLowerSetTopology
Goal:
α : Type u_1
inst : Preorder α
inst_1 : TopologicalSpace α
inst_2 : Topology.IsUpperSet α
a : α
rw : (↑(upperClosure {a}) : Set α) = Ici a
rw₁ : (↑(UpperSet.Ici a) : Set α) = Ici a
rw₂ rw₃ : Ici a = Ici a
⊢ nhdsKer {a} = Ici a

Tactic:
rw [nhdsKer_eq_upperClosure, upperClosure_singleton, UpperSet.coe_Ici]

Premises used: UpperSet.coe_Ici, Topology.IsUpperSet.nhdsKer_eq_upperClosure, upperClosure_singleton
-- Module: Mathlib.Topology.Order.UpperLowerSetTopology
Goal:
α : Type u_1
inst : Preorder α
inst_1 : TopologicalSpace α
inst_2 : Topology.IsUpperSet α
a : α
rw : 𝓟 (nhdsKer {a}) = 𝓟 (Ici a)
rw₁ rw₂ : 𝓟 (Ici a) = 𝓟 (Ici a)
⊢ 𝓝 a = 𝓟 (Ici a)

Tactic:
rw [← principal_nhdsKer_singleton, nhdsKer_singleton]

Premises used: principal_nhdsKer_singleton, Topology.IsUpperSet.nhdsKer_singleton
-- Module: Mathlib.Topology.Order.UpperLowerSetTopology
Goal:
α : Type u_1
inst : Preorder α
inst_1 : TopologicalSpace α
inst_2 : Topology.IsUpperSet α
s : Set α
rw : 𝓟 (nhdsKer s) = 𝓟 (↑(upperClosure s) : Set α)
rw₁ rw₂ : 𝓟 (↑(upperClosure s) : Set α) = 𝓟 (↑(upperClosure s) : Set α)
⊢ 𝓝ˢ s = 𝓟 (↑(upperClosure s) : Set α)

Tactic:
rw [← principal_nhdsKer, nhdsKer_eq_upperClosure]

Premises used: Topology.IsUpperSet.nhdsKer_eq_upperClosure, principal_nhdsKer
-- Module: Mathlib.Topology.Order.UpperLowerSetTopology
Goal:
α : Type u_4
inst : TopologicalSpace α
inst_1 : Preorder α
hα : ∀ (a : α), 𝓝 a = 𝓟 (Ici a)
⊢ inst = upperSet α

Tactic:
simp [TopologicalSpace.ext_iff_nhds, hα, nhds_eq_principal_Ici]

Premises used: TopologicalSpace.ext_iff_nhds, Topology.IsUpperSet.nhds_eq_principal_Ici
-- Module: Mathlib.Topology.Order.UpperLowerSetTopology
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
⊢ Topology.IsUpperSet Prop

Tactic:
simp [Topology.isUpperSet_iff_nhds, Prop.forall]

Premises used: Topology.isUpperSet_iff_nhds, Prop.forall
-- Module: Mathlib.Topology.Order.UpperLowerSetTopology
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
inst_2 : TopologicalSpace α
inst_3 : TopologicalSpace β
inst_4 : Topology.IsUpperSet α
inst_5 : Topology.IsUpperSet β
f : α → β
mp : Monotone f → Continuous[inst_2, inst_3] f
mpr : Continuous[inst_2, inst_3] f → Monotone f
⊢ Monotone f ↔ Continuous[inst_2, inst_3] f

Tactic:
constructor
-- Module: Mathlib.Topology.Order.UpperLowerSetTopology
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
inst_2 : TopologicalSpace α
inst_3 : TopologicalSpace β
inst_4 : Topology.IsUpperSet α
inst_5 : Topology.IsUpperSet β
f : α → β
hf : Monotone f
mp : ∀ (s : Set β), IsUpperSet s → IsUpperSet (f ⁻¹' s)
⊢ Continuous[inst_2, inst_3] f

Tactic:
simp_rw [continuous_def, isOpen_iff_isUpperSet]

Premises used: Topology.IsUpperSet.isOpen_iff_isUpperSet, continuous_def
-- Module: Mathlib.Topology.Order.UpperLowerSetTopology
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
inst_2 : TopologicalSpace α
inst_3 : TopologicalSpace β
inst_4 : Topology.IsUpperSet α
inst_5 : Topology.IsUpperSet β
f : α → β
hf : Monotone f
⊢ ∀ (s : Set β), IsUpperSet s → IsUpperSet (f ⁻¹' s)

Tactic:
fun _ hs ↦ IsUpperSet.preimage hs hf

Premises used: IsUpperSet.preimage
-- Module: Mathlib.Topology.Order.UpperLowerSetTopology
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
inst_2 : TopologicalSpace α
inst_3 : TopologicalSpace β
inst_4 : Topology.IsUpperSet α
inst_5 : Topology.IsUpperSet β
f : α → β
hf : Monotone f
⊢ ∀ (s : Set β), IsUpperSet s → IsUpperSet (f ⁻¹' s)

Tactic:
exact fun _ hs ↦ IsUpperSet.preimage hs hf

Premises used: IsUpperSet.preimage
-- Module: Mathlib.Topology.Order.UpperLowerSetTopology
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
inst_2 : TopologicalSpace α
inst_3 : TopologicalSpace β
inst_4 : Topology.IsUpperSet α
inst_5 : Topology.IsUpperSet β
f : α → β
hf : Continuous[inst_2, inst_3] f
a b : α
hab : a ≤ b
mpr :
  ∀ (hab : Membership.mem (γ := Set α) (closure[inst_2] {b}) a),
    Membership.mem (γ := Set β) (closure[inst_3] {f b}) (f a)
⊢ f a ≤ f b

Tactic:
rw [← mem_Iic, ← closure_singleton] at hab ⊢

Premises used: Set.mem_Iic, Topology.IsUpperSet.closure_singleton
-- Module: Mathlib.Topology.Order.UpperLowerSetTopology
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
inst_2 : TopologicalSpace α
inst_3 : TopologicalSpace β
inst_4 : Topology.IsUpperSet α
inst_5 : Topology.IsUpperSet β
f : α → β
hf : Continuous[inst_2, inst_3] f
a b : α
hab : Membership.mem (γ := Set α) (closure[inst_2] {b}) a
mpr : a ∈ closure[inst_2] (f ⁻¹' {f b})
⊢ Membership.mem (γ := Set β) (closure[inst_3] {f b}) (f a)

Tactic:
apply Continuous.closure_preimage_subset hf {f b}

Premises used: Singleton.singleton, Continuous.closure_preimage_subset
-- Module: Mathlib.Topology.Order.UpperLowerSetTopology
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
inst_2 : TopologicalSpace α
inst_3 : TopologicalSpace β
inst_4 : Topology.IsUpperSet α
inst_5 : Topology.IsUpperSet β
f : α → β
hf : Continuous[inst_2, inst_3] f
a b : α
hab : Membership.mem (γ := Set α) (closure[inst_2] {b}) a
mpr : closure[inst_2] {b} ⊆ closure[inst_2] (f ⁻¹' {f b})
⊢ a ∈ closure[inst_2] (f ⁻¹' {f b})

Tactic:
apply mem_of_mem_of_subset hab

Premises used: Set.mem_of_mem_of_subset
-- Module: Mathlib.Topology.Order.UpperLowerSetTopology
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
inst_2 : TopologicalSpace α
inst_3 : TopologicalSpace β
inst_4 : Topology.IsUpperSet α
inst_5 : Topology.IsUpperSet β
f : α → β
hf : Continuous[inst_2, inst_3] f
a b : α
hab : Membership.mem (γ := Set α) (closure[inst_2] {b}) a
mpr : {b} ⊆ f ⁻¹' {f b}
⊢ closure[inst_2] {b} ⊆ closure[inst_2] (f ⁻¹' {f b})

Tactic:
apply closure_mono

Premises used: closure_mono
-- Module: Mathlib.Topology.Order.UpperLowerSetTopology
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
inst_2 : TopologicalSpace α
inst_3 : TopologicalSpace β
inst_4 : Topology.IsUpperSet α
inst_5 : Topology.IsUpperSet β
f : α → β
hf : Continuous[inst_2, inst_3] f
a b : α
hab : Membership.mem (γ := Set α) (closure[inst_2] {b}) a
mpr : b ∈ f ⁻¹' {f b}
mpr₁ : Membership.mem (γ := Set β) {f b} (f b)
mpr₂ mpr₃ : f b = f b
⊢ {b} ⊆ f ⁻¹' {f b}

Tactic:
rw [singleton_subset_iff, mem_preimage, mem_singleton_iff]

Premises used: Set.singleton_subset_iff, Set.mem_singleton_iff, Set.mem_preimage
-- Module: Mathlib.Topology.Order.UpperLowerSetTopology
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
inst_2 : TopologicalSpace α
inst_3 : TopologicalSpace β
inst_4 : Topology.IsUpperSet α
inst_5 : IsUpper β
f : α → β
hf : Monotone f
simp_rw : ∀ (s : Set β), IsOpen[inst_3] s → IsUpperSet (f ⁻¹' s)
⊢ Continuous[inst_2, inst_3] f

Tactic:
simp_rw [continuous_def, isOpen_iff_isUpperSet]

Premises used: Topology.IsUpperSet.isOpen_iff_isUpperSet, continuous_def
-- Module: Mathlib.Topology.Order.UpperLowerSetTopology
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
inst_2 : TopologicalSpace α
inst_3 : TopologicalSpace β
inst_4 : Topology.IsUpperSet α
inst_5 : IsUpper β
f : α → β
hf : Monotone f
s : Set β
hs : IsOpen[inst_3] s
⊢ IsUpperSet (f ⁻¹' s)

Tactic:
(IsUpper.isUpperSet_of_isOpen hs).preimage hf

Premises used: IsUpperSet.preimage, Topology.IsUpper.isUpperSet_of_isOpen
-- Module: Mathlib.Topology.Order.UpperLowerSetTopology
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
inst_2 : TopologicalSpace α
inst_3 : TopologicalSpace β
inst_4 : Topology.IsUpperSet α
inst_5 : IsUpper β
f : α → β
hf : Monotone f
s : Set β
hs : IsOpen[inst_3] s
⊢ IsUpperSet (f ⁻¹' s)

Tactic:
exact (IsUpper.isUpperSet_of_isOpen hs).preimage hf

Premises used: IsUpperSet.preimage, Topology.IsUpper.isUpperSet_of_isOpen
-- Module: Mathlib.Topology.Order.UpperLowerSetTopology
Goal:
α : Type u_1
inst : Preorder α
t₁ t₂ : TopologicalSpace α
inst_1 : Topology.IsUpperSet α
inst_2 : IsUpper α
s : Set α
hs : IsOpen[t₂] s
rw : IsUpperSet s
⊢ IsOpen[t₁] s

Tactic:
rw [@isOpen_iff_isUpperSet α _ t₁]

Premises used: Topology.IsUpperSet.isOpen_iff_isUpperSet
-- Module: Mathlib.Topology.Order.UpperLowerSetTopology
Goal:
α : Type u_1
inst : Preorder α
t₁ t₂ : TopologicalSpace α
inst_1 : Topology.IsUpperSet α
inst_2 : IsUpper α
s : Set α
hs : IsOpen[t₂] s
⊢ IsUpperSet s

Tactic:
IsUpper.isUpperSet_of_isOpen hs

Premises used: Topology.IsUpper.isUpperSet_of_isOpen
-- Module: Mathlib.Topology.Order.UpperLowerSetTopology
Goal:
α : Type u_1
inst : Preorder α
t₁ t₂ : TopologicalSpace α
inst_1 : Topology.IsUpperSet α
inst_2 : IsUpper α
s : Set α
hs : IsOpen[t₂] s
⊢ IsUpperSet s

Tactic:
exact IsUpper.isUpperSet_of_isOpen hs

Premises used: Topology.IsUpper.isUpperSet_of_isOpen
-- Module: Mathlib.Topology.Order.UpperLowerSetTopology
Goal:
α : Type u_1
inst : Preorder α
inst_1 : TopologicalSpace α
inst_2 : Topology.IsLowerSet α
⊢ inst_1 = lowerSet α

Tactic:
topology_eq_lowerSetTopology

Premises used: Topology.IsLowerSet.topology_eq_lowerSetTopology
-- Module: Mathlib.Topology.Order.UpperLowerSetTopology
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : Preorder α
inst_1 : TopologicalSpace α
inst_2 : Topology.IsLowerSet α
s : Set α
a : ∀ (x : Set αᵒᵈ), IsOpen[OrderDual.instTopologicalSpace] x ↔ IsOpen[upperSet αᵒᵈ] x
⊢ Eq.{u_1 + 1} (α := TopologicalSpace αᵒᵈ) OrderDual.instTopologicalSpace (upperSet αᵒᵈ)

Tactic:
ext
-- Module: Mathlib.Topology.Order.UpperLowerSetTopology
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : Preorder α
inst_1 : TopologicalSpace α
inst_2 : Topology.IsLowerSet α
s : Set α
x : Set αᵒᵈ
a a₁ : IsOpen[OrderDual.instTopologicalSpace] x ↔ IsOpen[upperSet αᵒᵈ] x
⊢ IsOpen[OrderDual.instTopologicalSpace] x ↔ IsOpen[upperSet αᵒᵈ] x

Tactic:
rw [IsLowerSet.topology_eq α]

Premises used: Topology.IsLowerSet.topology_eq
-- Module: Mathlib.Topology.Order.UpperLowerSetTopology
Goal:
α : Type u_1
inst : Preorder α
inst_1 : TopologicalSpace α
inst_2 : Topology.IsLowerSet α
s : Set α
rw : IsOpen[lowerSet α] s ↔ IsLowerSet s
⊢ IsOpen[inst_1] s ↔ IsLowerSet s

Tactic:
rw [topology_eq α]

Premises used: Topology.IsLowerSet.topology_eq
-- Module: Mathlib.Topology.Order.UpperLowerSetTopology
Goal:
α : Type u_1
inst : Preorder α
inst_1 : TopologicalSpace α
inst_2 : Topology.IsLowerSet α
s : Set α
⊢ IsOpen[lowerSet α] s ↔ IsLowerSet s

Tactic:
rfl
-- Module: Mathlib.Topology.Order.UpperLowerSetTopology
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : Preorder α
inst_1 : TopologicalSpace α
inst_2 : Topology.IsLowerSet α
s : Set α
⊢ AlexandrovDiscrete α

Tactic:
IsUpperSet.toAlexandrovDiscrete (α := αᵒᵈ)

Premises used: Topology.IsUpperSet.toAlexandrovDiscrete, OrderDual
-- Module: Mathlib.Topology.Order.UpperLowerSetTopology
Goal:
α : Type u_1
inst : Preorder α
inst_1 : TopologicalSpace α
inst_2 : Topology.IsLowerSet α
s : Set α
rw : IsOpen[inst_1] sᶜ ↔ IsUpperSet s
rw₁ : IsLowerSet sᶜ ↔ IsUpperSet s
rw₂ : IsUpperSet sᶜᶜ ↔ IsUpperSet s
rw₃ rw₄ : IsUpperSet s ↔ IsUpperSet s
⊢ IsClosed[inst_1] s ↔ IsUpperSet s

Tactic:
rw [← isOpen_compl_iff, isOpen_iff_isLowerSet, isUpperSet_compl.symm, compl_compl]

Premises used: Topology.IsLowerSet.isOpen_iff_isLowerSet, compl_compl, isUpperSet_compl, Iff.symm, isOpen_compl_iff
-- Module: Mathlib.Topology.Order.UpperLowerSetTopology
Goal:
α : Type u_1
inst : Preorder α
inst_1 : TopologicalSpace α
inst_2 : Topology.IsLowerSet α
s : Set α
⊢ closure[inst_1] s = (↑(upperClosure s) : Set α)

Tactic:
IsUpperSet.closure_eq_lowerClosure (α := αᵒᵈ)

Premises used: Set.Mem, setOf, Topology.IsUpperSet.closure_eq_lowerClosure, OrderDual
-- Module: Mathlib.Topology.Order.UpperLowerSetTopology
Goal:
α : Type u_1
inst : Preorder α
inst_1 : TopologicalSpace α
inst_2 : Topology.IsLowerSet α
a : α
rw : (↑(UpperSet.Ici a) : Set α) = Ici a
⊢ closure[inst_1] {a} = Ici a

Tactic:
rw [closure_eq_upperClosure, upperClosure_singleton]

Premises used: Topology.IsLowerSet.closure_eq_upperClosure, upperClosure_singleton
-- Module: Mathlib.Topology.Order.UpperLowerSetTopology
Goal:
α : Type u_1
inst : Preorder α
inst_1 : TopologicalSpace α
inst_2 : Topology.IsLowerSet α
a : α
⊢ (↑(UpperSet.Ici a) : Set α) = Ici a

Tactic:
rfl
-- Module: Mathlib.Topology.Order.UpperLowerSetTopology
Goal:
α : Type u_1
inst : Preorder α
inst_1 : TopologicalSpace α
inst_2 : Topology.IsLowerSet α
a b : α
⊢ a ⤳ b ↔ a ≤ b

Tactic:
simp only [specializes_iff_closure_subset, closure_singleton, Ici_subset_Ici]

Premises used: Topology.IsLowerSet.closure_singleton, Set.Ici_subset_Ici, specializes_iff_closure_subset
-- Module: Mathlib.Topology.Order.UpperLowerSetTopology
Goal:
α : Type u_1
inst : Preorder α
inst_1 : TopologicalSpace α
inst_2 : Topology.IsLowerSet α
s : Set α
h : ∀ (x : α), x ∈ nhdsKer s ↔ x ∈ (↑(lowerClosure s) : Set α)
⊢ nhdsKer s = (↑(lowerClosure s) : Set α)

Tactic:
ext
-- Module: Mathlib.Topology.Order.UpperLowerSetTopology
Goal:
α : Type u_1
inst : Preorder α
inst_1 : TopologicalSpace α
inst_2 : Topology.IsLowerSet α
s : Set α
x : α
⊢ x ∈ nhdsKer s ↔ x ∈ (↑(lowerClosure s) : Set α)

Tactic:
simp [mem_nhdsKer_iff_specializes, specializes_iff_le]

Premises used: mem_nhdsKer_iff_specializes, Topology.IsLowerSet.specializes_iff_le