awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Order.ScottTopology
Goal:
α : Type u_1
inst : Preorder α
inst_1 : TopologicalSpace α
s : Set α
inst_2 : IsScott α univ
⊢ IsClosed[inst_1] s → IsLowerSet s

Tactic:
fun h ↦
  (isClosed_iff_isLowerSet_and_dirSupClosed.mp h).left

Premises used: Topology.IsScott.isClosed_iff_isLowerSet_and_dirSupClosed, And.left, Iff.mp
-- Module: Mathlib.Topology.Order.ScottTopology
Goal:
α : Type u_1
inst : Preorder α
inst_1 : TopologicalSpace α
s : Set α
inst_2 : IsScott α univ
⊢ IsClosed[inst_1] s → DirSupClosed s

Tactic:
fun h ↦
  (isClosed_iff_isLowerSet_and_dirSupClosed.mp h).right

Premises used: Topology.IsScott.isClosed_iff_isLowerSet_and_dirSupClosed, And.right, Iff.mp
-- Module: Mathlib.Topology.Order.ScottTopology
Goal:
α : Type u_1
inst : Preorder α
inst_1 : TopologicalSpace α
s : Set α
inst_2 : IsScott α univ
⊢ closure[upperSet α] s ⊆ closure[scott α univ] s

Tactic:
closure.mono (@upperSet_le_scott α _)

Premises used: Topology.upperSet_le_scott, closure.mono
-- Module: Mathlib.Topology.Order.ScottTopology
Goal:
α : Type u_1
inst : Preorder α
inst_1 : TopologicalSpace α
s : Set α
inst_2 : IsScott α univ
h : (↑(lowerClosure s) : Set α) = closure[upperSet α] s
h₁ : inst_1 = scott α univ
⊢ (↑(lowerClosure s) : Set α) ⊆ closure[inst_1] s

Tactic:
convert! closure.mono (@upperSet_le_scott α _)

Premises used: Topology.upperSet_le_scott, closure.mono
-- Module: Mathlib.Topology.Order.ScottTopology
Goal:
α : Type u_1
inst : Preorder α
inst_1 : TopologicalSpace α
s : Set α
inst_2 : IsScott α univ
rw : Topology.IsUpperSet α
⊢ (↑(lowerClosure s) : Set α) = closure[upperSet α] s

Tactic:
rw [@IsUpperSet.closure_eq_lowerClosure α _ (upperSet α) ?_ s]

Premises used: Topology.IsUpperSet.closure_eq_lowerClosure
-- Module: Mathlib.Topology.Order.ScottTopology
Goal:
α : Type u_1
inst : Preorder α
inst_1 : TopologicalSpace α
s : Set α
inst_2 : IsScott α univ
⊢ Topology.IsUpperSet α

Tactic:
infer_instance
-- Module: Mathlib.Topology.Order.ScottTopology
Goal:
α : Type u_1
inst : Preorder α
inst_1 : TopologicalSpace α
s : Set α
inst_2 : IsScott α univ
⊢ inst_1 = scott α univ

Tactic:
topology_eq α univ

Premises used: Topology.IsScott.topology_eq, Set.univ
-- Module: Mathlib.Topology.Order.ScottTopology
Goal:
α : Type u_1
inst : Preorder α
inst_1 : TopologicalSpace α
s : Set α
inst_2 : IsScott α univ
⊢ inst_1 = scott α univ

Tactic:
exact topology_eq α univ

Premises used: Topology.IsScott.topology_eq, Set.univ
-- Module: Mathlib.Topology.Order.ScottTopology
Goal:
α : Type u_1
inst : Preorder α
inst_1 : TopologicalSpace α
a : α
inst_2 : IsScott α univ
rw : a ∈ Iic a
rw₁ rw₂ : a ≤ a
⊢ {a} ⊆ Iic a

Tactic:
rw [singleton_subset_iff, mem_Iic]

Premises used: Set.singleton_subset_iff, Set.mem_Iic
-- Module: Mathlib.Topology.Order.ScottTopology
Goal:
α : Type u_1
inst : Preorder α
inst_1 : TopologicalSpace α
a : α
inst_2 : IsScott α univ
rw : (↑(lowerClosure {a}) : Set α) ≤ closure[inst_1] {a}
⊢ Iic a ≤ closure[inst_1] {a}

Tactic:
rw [← LowerSet.coe_Iic, ← lowerClosure_singleton]

Premises used: lowerClosure_singleton, LowerSet.coe_Iic
-- Module: Mathlib.Topology.Order.ScottTopology
Goal:
α : Type u_1
inst : Preorder α
inst_1 : TopologicalSpace α
a : α
inst_2 : IsScott α univ
⊢ (↑(lowerClosure {a}) : Set α) ≤ closure[inst_1] {a}

Tactic:
apply lowerClosure_subset_closure

Premises used: Topology.IsScott.lowerClosure_subset_closure
-- Module: Mathlib.Topology.Order.ScottTopology
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
by_contra : ∀ (h : ¬f x ≤ f b), False
⊢ f x ≤ f b

Tactic:
by_contra h
-- Module: Mathlib.Topology.Order.ScottTopology
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
h : ¬f x ≤ f b
⊢ False

Tactic:
simpa only [mem_compl_iff, mem_preimage, mem_Iic, le_refl, not_true]
    using isUpperSet_of_isOpen (D := D) ((isOpen_compl_iff.2 isClosed_Iic).preimage hf) hab h

Premises used: Topology.IsScott.isUpperSet_of_isOpen, Iff.mpr, le_refl, isClosed_Iic, Set.mem_Iic, not_true, IsOpen.preimage, isOpen_compl_iff, Set.mem_compl_iff, Set.mem_preimage
-- Module: Mathlib.Topology.Order.ScottTopology
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

Tactic:
⟨fun h ↦ continuous_def.2 fun u hu ↦ ?_, ?_⟩

Premises used: Iff.mpr, Iff.intro, continuous_def
-- Module: Mathlib.Topology.Order.ScottTopology
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)
refine_2 : Continuous[inst_1, inst_3] f → ScottContinuousOn D f
⊢ ScottContinuousOn D f ↔ Continuous[inst_1, inst_3] f

Tactic:
refine ⟨fun h ↦ continuous_def.2 fun u hu ↦ ?_, ?_⟩
-- Module: Mathlib.Topology.Order.ScottTopology
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
refine_1 : IsUpperSet (f ⁻¹' u) ∧ DirSupInaccOn D (f ⁻¹' u)
⊢ IsOpen[inst_1] (f ⁻¹' u)

Tactic:
rw [isOpen_iff_isUpperSet_and_dirSupInaccOn (D := D)]

Premises used: Topology.IsScott.isOpen_iff_isUpperSet_and_dirSupInaccOn
-- Module: Mathlib.Topology.Order.ScottTopology
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
⊢ IsUpperSet (f ⁻¹' u) ∧ DirSupInaccOn D (f ⁻¹' u)

Tactic:
⟨(isUpperSet_of_isOpen (D := univ) hu).preimage (h.monotone D hD),
      fun t h₀ hd₁ hd₂ a hd₃ ha ↦ image_inter_nonempty_iff.mp <|
        (isOpen_iff_isUpperSet_and_dirSupInaccOn (D := univ).mp hu).2 trivial (Nonempty.image f hd₁)
        (directedOn_image.mpr (hd₂.mono @(h.monotone D hD))) (h h₀ hd₁ hd₂ hd₃) ha⟩

Premises used: Topology.IsScott.isUpperSet_of_isOpen, Iff.mpr, trivial, ScottContinuousOn.monotone, IsUpperSet.preimage, directedOn_image, DirectedOn.mono, And.right, Set.Nonempty.image, And.intro, Iff.mp, Topology.IsScott.isOpen_iff_isUpperSet_and_dirSupInaccOn, Set.image_inter_nonempty_iff
-- Module: Mathlib.Topology.Order.ScottTopology
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
⊢ IsUpperSet (f ⁻¹' u) ∧ DirSupInaccOn D (f ⁻¹' u)

Tactic:
exact ⟨(isUpperSet_of_isOpen (D := univ) hu).preimage (h.monotone D hD),
      fun t h₀ hd₁ hd₂ a hd₃ ha ↦ image_inter_nonempty_iff.mp <|
        (isOpen_iff_isUpperSet_and_dirSupInaccOn (D := univ).mp hu).2 trivial (Nonempty.image f hd₁)
        (directedOn_image.mpr (hd₂.mono @(h.monotone D hD))) (h h₀ hd₁ hd₂ hd₃) ha⟩
-- Module: Mathlib.Topology.Order.ScottTopology
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

Tactic:
fun hf t h₀ d₁ d₂ a d₃ ↦
      ⟨(monotone_of_continuous (D := D) hf).mem_upperBounds_image d₃.1,
      fun b hb ↦ ?_⟩

Premises used: IsLeast, Topology.IsScott.monotone_of_continuous, And.left, Monotone.mem_upperBounds_image, And.intro, IsLUB, ScottContinuousOn
-- Module: Mathlib.Topology.Order.ScottTopology
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_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
⊢ Continuous[inst_1, inst_3] f → ScottContinuousOn D f

Tactic:
refine fun hf t h₀ d₁ d₂ a d₃ ↦
      ⟨(monotone_of_continuous (D := D) hf).mem_upperBounds_image d₃.1,
      fun b hb ↦ ?_⟩
-- Module: Mathlib.Topology.Order.ScottTopology
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)
refine_2 : ∀ (h : ¬f a ≤ b), False
⊢ f a ≤ b

Tactic:
by_contra h
-- Module: Mathlib.Topology.Order.ScottTopology
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)ᶜ
⊢ IsOpen[inst_1] (f ⁻¹' u)

Tactic:
have hu : IsOpen (f ⁻¹' u) := isClosed_Iic.isOpen_compl.preimage hf
-- Module: Mathlib.Topology.Order.ScottTopology
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)
⊢ IsUpperSet (f ⁻¹' u) ∧ DirSupInaccOn D (f ⁻¹' u)

Tactic:
rw [isOpen_iff_isUpperSet_and_dirSupInaccOn (D := D)] at hu

Premises used: Topology.IsScott.isOpen_iff_isUpperSet_and_dirSupInaccOn
-- Module: Mathlib.Topology.Order.ScottTopology
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)
refine_2 : ∀ (c : α) (hcd : c ∈ t) (hfcb : c ∈ f ⁻¹' u), False
⊢ False

Tactic:
obtain ⟨c, hcd, hfcb⟩ := hu.2 h₀ d₁ d₂ d₃ h

Premises used: And.right
-- Module: Mathlib.Topology.Order.ScottTopology
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
⊢ ∀ 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

Premises used: and_imp, Set.mem_image, forall_exists_index, upperBounds, Set.mem_setOf, forall_apply_eq_imp_iff₂
-- Module: Mathlib.Topology.Order.ScottTopology
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 : β
h : ¬f a ≤ b
u : Set β := (Iic b)ᶜ
hu : IsUpperSet (f ⁻¹' u) ∧ DirSupInaccOn D (f ⁻¹' u)
c : α
hcd : c ∈ t
hfcb : c ∈ f ⁻¹' u
hb : ∀ a ∈ t, f a ≤ b
⊢ False

Tactic:
hfcb <| hb _ hcd
-- Module: Mathlib.Topology.Order.ScottTopology
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 : β
h : ¬f a ≤ b
u : Set β := (Iic b)ᶜ
hu : IsUpperSet (f ⁻¹' u) ∧ DirSupInaccOn D (f ⁻¹' u)
c : α
hcd : c ∈ t
hfcb : c ∈ f ⁻¹' u
hb : ∀ a ∈ t, f a ≤ b
⊢ False

Tactic:
exact hfcb <| hb _ hcd
-- Module: Mathlib.Topology.Order.ScottTopology
Goal:
α : Type u_1
β : Type u_2
inst : PartialOrder α
inst_1 : TopologicalSpace α
inst_2 : IsScott α univ
x y : α
h : Inseparable x y
⊢ Iic x = Iic y

Tactic:
simpa only [inseparable_iff_closure_eq, IsScott.closure_singleton] using h

Premises used: inseparable_iff_closure_eq, Topology.IsScott.closure_singleton
-- Module: Mathlib.Topology.Order.ScottTopology
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
mpr : (U = univ ∨ ∃ (a : α), (Iic a)ᶜ = U) → IsOpen[inst_1] U
⊢ IsOpen[inst_1] U ↔ U = univ ∨ ∃ (a : α), (Iic a)ᶜ = U

Tactic:
constructor
-- Module: Mathlib.Topology.Order.ScottTopology
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
mp₁ : ∀ (neUc : Uᶜ.Nonempty), U = univ ∨ ∃ (a : α), (Iic a)ᶜ = U
⊢ U = univ ∨ ∃ (a : α), (Iic a)ᶜ = U

Tactic:
rcases eq_empty_or_nonempty Uᶜ with eUc | neUc

Premises used: Compl.compl, Set.eq_empty_or_nonempty
-- Module: Mathlib.Topology.Order.ScottTopology
Goal:
α : Type u_1
inst : CompleteLinearOrder α
inst_1 : TopologicalSpace α
inst_2 : IsScott α univ
U : Set α
hU : IsOpen[inst_1] U
eUc : Uᶜ = ∅
⊢ U = univ ∨ ∃ (a : α), (Iic a)ᶜ = U

Tactic:
Or.inl (compl_empty_iff.mp eUc)

Premises used: Set.compl_empty_iff, Iff.mp, Or.inl
-- Module: Mathlib.Topology.Order.ScottTopology
Goal:
α : Type u_1
inst : CompleteLinearOrder α
inst_1 : TopologicalSpace α
inst_2 : IsScott α univ
U : Set α
hU : IsOpen[inst_1] U
eUc : Uᶜ = ∅
⊢ U = univ ∨ ∃ (a : α), (Iic a)ᶜ = U

Tactic:
exact Or.inl (compl_empty_iff.mp eUc)

Premises used: Set.compl_empty_iff, Iff.mp, Or.inl
-- Module: Mathlib.Topology.Order.ScottTopology
Goal:
α : Type u_1
inst : CompleteLinearOrder α
inst_1 : TopologicalSpace α
inst_2 : IsScott α univ
U : Set α
hU : IsOpen[inst_1] U
neUc : Uᶜ.Nonempty
mp : ∃ (a : α), (Iic a)ᶜ = U
⊢ U = univ ∨ ∃ (a : α), (Iic a)ᶜ = U

Tactic:
apply Or.inr

Premises used: Or.inr
-- Module: Mathlib.Topology.Order.ScottTopology
Goal:
α : Type u_1
inst : CompleteLinearOrder α
inst_1 : TopologicalSpace α
inst_2 : IsScott α univ
U : Set α
hU : IsOpen[inst_1] U
neUc : Uᶜ.Nonempty
h : (Iic (sSup Uᶜ))ᶜ = U
⊢ ∃ (a : α), (Iic a)ᶜ = U

Tactic:
use sSup Uᶜ

Premises used: Compl.compl, SupSet.sSup
-- Module: Mathlib.Topology.Order.ScottTopology
Goal:
α : Type u_1
inst : CompleteLinearOrder α
inst_1 : TopologicalSpace α
inst_2 : IsScott α univ
U : Set α
hU : IsOpen[inst_1] U
neUc : Uᶜ.Nonempty
h : Uᶜ ≤ Iic (sSup Uᶜ) ∧ Iic (sSup Uᶜ) ≤ Uᶜ
⊢ (Iic (sSup Uᶜ))ᶜ = U

Tactic:
rw [compl_eq_comm, le_antisymm_iff]

Premises used: le_antisymm_iff, compl_eq_comm
-- Module: Mathlib.Topology.Order.ScottTopology
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ᶜ

Tactic:
⟨fun _ ha ↦ le_sSup ha, (isLowerSet_of_isClosed hU.isClosed_compl).Iic_subset ?_⟩

Premises used: IsLowerSet.Iic_subset, IsOpen.isClosed_compl, And.intro, Topology.IsScott.isLowerSet_of_isClosed, le_sSup
-- Module: Mathlib.Topology.Order.ScottTopology
Goal:
α : Type u_1
inst : CompleteLinearOrder α
inst_1 : TopologicalSpace α
inst_2 : IsScott α univ
U : Set α
hU : IsOpen[inst_1] U
neUc : Uᶜ.Nonempty
h : sSup Uᶜ ∈ Uᶜ
⊢ Uᶜ ≤ Iic (sSup Uᶜ) ∧ Iic (sSup Uᶜ) ≤ Uᶜ

Tactic:
refine ⟨fun _ ha ↦ le_sSup ha, (isLowerSet_of_isClosed hU.isClosed_compl).Iic_subset ?_⟩
-- Module: Mathlib.Topology.Order.ScottTopology
Goal:
α : Type u_1
inst : CompleteLinearOrder α
inst_1 : TopologicalSpace α
inst_2 : IsScott α univ
U : Set α
hU : IsOpen[inst_1] U
neUc : Uᶜ.Nonempty
⊢ sSup Uᶜ ∈ Uᶜ

Tactic:
dirSupClosed_iff_forall_sSup.mp (dirSupClosed_of_isClosed hU.isClosed_compl) le_rfl neUc
        (isChain_of_trichotomous Uᶜ).directedOn

Premises used: dirSupClosed_iff_forall_sSup, le_rfl, Set.Mem, Compl.compl, setOf, IsChain.directedOn, IsOpen.isClosed_compl, Iff.mp, isChain_of_trichotomous, Topology.IsScott.dirSupClosed_of_isClosed
-- Module: Mathlib.Topology.Order.ScottTopology
Goal:
α : Type u_1
inst : CompleteLinearOrder α
inst_1 : TopologicalSpace α
inst_2 : IsScott α univ
U : Set α
hU : IsOpen[inst_1] U
neUc : Uᶜ.Nonempty
⊢ sSup Uᶜ ∈ Uᶜ

Tactic:
exact dirSupClosed_iff_forall_sSup.mp (dirSupClosed_of_isClosed hU.isClosed_compl) le_rfl neUc
        (isChain_of_trichotomous Uᶜ).directedOn

Premises used: dirSupClosed_iff_forall_sSup, le_rfl, Compl.compl, IsChain.directedOn, IsOpen.isClosed_compl, Iff.mp, isChain_of_trichotomous, Topology.IsScott.dirSupClosed_of_isClosed
-- Module: Mathlib.Topology.Order.ScottTopology
Goal:
α : Type u_1
inst : CompleteLinearOrder α
inst_1 : TopologicalSpace α
inst_2 : IsScott α univ
⊢ IsOpen[inst_1] univ

Tactic:
isOpen_univ

Premises used: isOpen_univ
-- Module: Mathlib.Topology.Order.ScottTopology
Goal:
α : Type u_1
inst : CompleteLinearOrder α
inst_1 : TopologicalSpace α
inst_2 : IsScott α univ
⊢ IsOpen[inst_1] univ

Tactic:
exact isOpen_univ

Premises used: isOpen_univ
-- Module: Mathlib.Topology.Order.ScottTopology
Goal:
α : Type u_1
inst : CompleteLinearOrder α
inst_1 : TopologicalSpace α
inst_2 : IsScott α univ
a : α
⊢ IsOpen[inst_1] (Iic a)ᶜ

Tactic:
isClosed_Iic.isOpen_compl

Premises used: IsClosed.isOpen_compl
-- Module: Mathlib.Topology.Order.ScottTopology
Goal:
α : Type u_1
inst : CompleteLinearOrder α
inst_1 : TopologicalSpace α
inst_2 : IsScott α univ
a : α
⊢ IsOpen[inst_1] (Iic a)ᶜ

Tactic:
exact isClosed_Iic.isOpen_compl

Premises used: IsClosed.isOpen_compl
-- Module: Mathlib.Topology.Order.ScottTopology
Goal:
α : Type u_1
inst : CompleteLinearOrder α
this : TopologicalSpace α := upper α
a : ∀ (U : Set α), IsOpen[scott α univ] U ↔ IsOpen[upper α] U
⊢ scott α univ = upper α

Tactic:
ext U
-- Module: Mathlib.Topology.Order.ScottTopology
Goal:
α : Type u_1
inst : CompleteLinearOrder α
this : TopologicalSpace α := upper α
U : Set α
a : IsOpen[scott α univ] U ↔ U = univ ∨ ∃ (a : α), (Iic a)ᶜ = U
⊢ IsOpen[scott α univ] U ↔ IsOpen[upper α] U

Tactic:
rw [@Topology.IsUpper.isTopologicalSpace_basis _ _ (upper α)
    ({ topology_eq_upperTopology := rfl }) U]

Premises used: Topology.IsUpper.isTopologicalSpace_basis
-- Module: Mathlib.Topology.Order.ScottTopology
Goal:
α : Type u_1
inst : CompleteLinearOrder α
this_1 : TopologicalSpace α := upper α
U : Set α
this : TopologicalSpace α := scott α univ
a a₁ : (U = univ ∨ ∃ (a : α), (Iic a)ᶜ = U) ↔ U = univ ∨ ∃ (a : α), (Iic a)ᶜ = U
⊢ IsOpen[scott α univ] U ↔ U = univ ∨ ∃ (a : α), (Iic a)ᶜ = U

Tactic:
rw [@isOpen_iff_Iic_compl_or_univ _ _ (scott α univ) ({ topology_eq_scott := rfl }) U]

Premises used: Topology.IsScott.isOpen_iff_Iic_compl_or_univ
-- Module: Mathlib.Topology.Order.ScottTopology
Goal:
α : Type u_1
β : Type u_2
inst : CompleteLinearOrder α
inst_1 : TopologicalSpace α
inst_2 : IsUpper α
rw : inst_1 = upper α
⊢ inst_1 = scott α univ

Tactic:
rw [scott_eq_upper_of_completeLinearOrder]

Premises used: Topology.IsScott.scott_eq_upper_of_completeLinearOrder
-- Module: Mathlib.Topology.Order.ScottTopology
Goal:
α : Type u_1
β : Type u_2
inst : CompleteLinearOrder α
inst_1 : TopologicalSpace α
inst_2 : IsUpper α
⊢ inst_1 = upper α

Tactic:
IsUpper.topology_eq α

Premises used: Topology.IsUpper.topology_eq
-- Module: Mathlib.Topology.Order.ScottTopology
Goal:
α : Type u_1
β : Type u_2
inst : CompleteLinearOrder α
inst_1 : TopologicalSpace α
inst_2 : IsUpper α
⊢ inst_1 = upper α

Tactic:
exact IsUpper.topology_eq α

Premises used: Topology.IsUpper.topology_eq
-- Module: Mathlib.Topology.Order.ScottTopology
Goal:
α : Type u_1
inst : Preorder α
s : Set α
inst_1 : TopologicalSpace α
inst_2 : IsScott α univ
x x_1 : α
h : x ≤ x_1
⊢ Membership.mem (γ := Set (Set α)) univ {x, x_1}

Tactic:
trivial
-- Module: Mathlib.Topology.Order.ScottTopology
Goal:
α : Type u_1
inst : Preorder α
s : Set α
inst_1 : TopologicalSpace α
inst_2 : IsScott α univ
rw : IsOpen[inst_1] s ↔ Continuous[inst_1, _] fun (x : α) ↦ x ∈ s
⊢ IsOpen[inst_1] s ↔ ScottContinuous (β := Prop) fun (x : α) ↦ x ∈ s

Tactic:
rw [← scottContinuousOn_univ, scottContinuousOn_iff_continuous (fun _ _ _ ↦ by trivial)]

Premises used: scottContinuousOn_univ, Topology.IsScott.scottContinuousOn_iff_continuous
-- Module: Mathlib.Topology.Order.ScottTopology
Goal:
α : Type u_1
inst : Preorder α
s : Set α
inst_1 : TopologicalSpace α
inst_2 : IsScott α univ
⊢ IsOpen[inst_1] s ↔ Continuous[inst_1, _] fun (x : α) ↦ x ∈ s

Tactic:
isOpen_iff_continuous_mem

Premises used: isOpen_iff_continuous_mem
-- Module: Mathlib.Topology.Order.ScottTopology
Goal:
α : Type u_1
inst : Preorder α
s : Set α
inst_1 : TopologicalSpace α
inst_2 : IsScott α univ
⊢ IsOpen[inst_1] s ↔ Continuous[inst_1, _] fun (x : α) ↦ x ∈ s

Tactic:
exact isOpen_iff_continuous_mem

Premises used: isOpen_iff_continuous_mem
-- Module: Mathlib.Topology.Order.ScottTopology
Goal:
α : Type u_1
⊢ Eq.{u_1 + 1} (α := WithScott α ≃ α) (Equiv.symm toScott) ofScott

Tactic:
rfl

Premises used: Topology.WithScott, Equiv.symm, Equiv.refl, Topology.WithScott.ofScott, rfl
-- Module: Mathlib.Topology.Order.ScottTopology
Goal:
α : Type u_1
⊢ Eq.{u_1 + 1} (α := α ≃ WithScott α) (Equiv.symm ofScott) toScott

Tactic:
rfl

Premises used: Topology.WithScott.toScott, Topology.WithScott, Equiv.symm, Equiv.refl, rfl
-- Module: Mathlib.Topology.Order.ScottTopology
Goal:
α : Type u_1
a : WithScott α
⊢ (toScott : (a : α) → WithScott α) ((ofScott : (a : WithScott α) → α) a : α) = a

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Order.ScottTopology
Goal:
α : Type u_1
a : α
⊢ (ofScott : (a : WithScott α) → α) ((toScott : (a : α) → WithScott α) a : WithScott α) = a

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Order.ScottTopology
Goal:
α : Type u_1
a b : α
⊢ Eq (α := WithScott α) ((toScott : (a : α) → WithScott α) a : WithScott α)
      ((toScott : (a : α) → WithScott α) b : WithScott α) ↔
    a = b

Tactic:
Iff.rfl

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

Tactic:
Iff.rfl

Premises used: Iff.rfl, Topology.WithScott
-- Module: Mathlib.Topology.Order.ScottTopology
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
⊢ IsScott.{u_1} (WithScott α) univ

Tactic:
⟨rfl⟩

Premises used: Topology.IsScott.mk, rfl