mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.MetricSpace.GromovHausdorff

Goal state before:
pp: X : Type u
inst✝⁵ : MetricSpace X
inst✝⁴ : CompactSpace X
inst✝³ : Nonempty X
Y : Type v
inst✝² : MetricSpace Y
inst✝¹ : CompactSpace Y
inst✝ : Nonempty Y
inhabited_h✝ : Inhabited X
inhabited_h : Inhabited Y
p q : NonemptyCompacts ↥(lp (fun n ↦ ℝ) ∞)
hp : ⟦p⟧ = toGHSpace X
hq : ⟦q⟧ = toGHSpace Y
bound : hausdorffDist ↑p ↑q < diam univ + 1 + diam univ
Φ : X → ↥(lp (fun n ↦ ℝ) ∞)
Φisom : Isometry Φ
Φrange : range Φ = ↑p
Ψ : Y → ↥(lp (fun n ↦ ℝ) ∞)
Ψisom : Isometry Ψ
Ψrange : range Ψ = ↑q
xX : X
h✝ : xX ∈ univ
y : ↥(lp (fun n ↦ ℝ) ∞)
hy : y ∈ range Ψ
z : Y
dy : dist (Φ xX) (Ψ z) < diam univ + 1 + diam univ
hzy : Ψ z = y
DΦ : diam (range Φ) = diam univ
DΨ : diam (range Ψ) = diam univ
⊢ diam (range Φ) + dist (Φ xX) (Ψ z) + diam (range Ψ) ≤ diam univ + (diam univ + 1 + diam univ) + diam univ

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Order.LowerUpperTopology

Goal state before:
pp: α : Type u_1
inst✝² : Preorder α
inst✝¹ : TopologicalSpace α
inst✝ : IsLower α
⊢ IsTopologicalBasis (lowerBasis α)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Order.LowerUpperTopology

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝³ : Preorder α
inst✝² : TopologicalSpace α
inst✝¹ : IsLower α
inst✝ : TopologicalSpace β
f : β → α
⊢ Continuous[inst✝, inst✝²] f ↔ ∀ (a : α), IsClosed[inst✝] (f ⁻¹' Ici a)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Order.LowerUpperTopology

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : PartialOrder α
inst✝¹ : TopologicalSpace α
inst✝ : IsLower α
x y : α
h : Inseparable x y
⊢ Ici x = Ici y

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Order.LowerUpperTopology

Goal state before:
pp: α : Type u_1
inst✝² : LinearOrder α
inst✝¹ : TopologicalSpace α
inst✝ : IsLower α
⊢ inst✝¹ = generateFrom {s | ∃ a, (Ici a)ᶜ = s}

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Order.LowerUpperTopology

Goal state before:
pp: α : Type u_1
inst✝² : LinearOrder α
inst✝¹ : TopologicalSpace α
inst✝ : IsLower α
⊢ ∀ ⦃s : Set α⦄,
    s ∈ {s | ∃ a, (Ici a)ᶜ = s} → ∀ ⦃t : Set α⦄, t ∈ {s | ∃ a, (Ici a)ᶜ = s} → s ∩ t ∈ {s | ∃ a, (Ici a)ᶜ = s}

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Order.LowerUpperTopology

Goal state before:
pp: α : Type u_1
inst✝² : LinearOrder α
inst✝¹ : TopologicalSpace α
inst✝ : IsLower α
β : Type u_3
f : β → α
l : Filter β
x : α
⊢ Filter.Tendsto f l (𝓝 x) ↔ ∀ (y : α), x < y → ∀ᶠ (z : β) in l, f z < y

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Order.UpperLowerSetTopology

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁵ : Preorder α
inst✝⁴ : Preorder β
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : Topology.IsUpperSet α
inst✝ : Topology.IsUpperSet β
f : α → β
⊢ Monotone f ↔ Continuous[inst✝³, inst✝²] f

Tactic:
by

Goal state after:
Module: Mathlib.Topology.MetricSpace.GromovHausdorff

Goal state before:
pp: X : Type u
inst✝⁵ : MetricSpace X
inst✝⁴ : CompactSpace X
inst✝³ : Nonempty X
Y : Type v
inst✝² : MetricSpace Y
inst✝¹ : CompactSpace Y
inst✝ : Nonempty Y
inhabited_h✝ : Inhabited X
inhabited_h : Inhabited Y
p q : NonemptyCompacts ↥(lp (fun n ↦ ℝ) ∞)
hp : ⟦p⟧ = toGHSpace X
hq : ⟦q⟧ = toGHSpace Y
bound : hausdorffDist ↑p ↑q < diam univ + 1 + diam univ
Φ : X → ↥(lp (fun n ↦ ℝ) ∞)
Φisom : Isometry Φ
Φrange : range Φ = ↑p
Ψ : Y → ↥(lp (fun n ↦ ℝ) ∞)
Ψisom : Isometry Ψ
Ψrange : range Ψ = ↑q
xX : X
h✝ : xX ∈ univ
y : ↥(lp (fun n ↦ ℝ) ∞)
hy : y ∈ range Ψ
z : Y
dy : dist (Φ xX) (Ψ z) < diam univ + 1 + diam univ
hzy : Ψ z = y
DΦ : diam (range Φ) = diam univ
DΨ : diam (range Ψ) = diam univ
⊢ diam univ + (diam univ + 1 + diam univ) + diam univ = 2 * diam univ + 1 + 2 * diam univ

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Order.UpperLowerSetTopology

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁵ : Preorder α
inst✝⁴ : Preorder β
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : Topology.IsUpperSet α
inst✝ : IsUpper β
f : α → β
hf : Monotone f
⊢ Continuous[inst✝³, inst✝²] f

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Order.UpperLowerSetTopology

Goal state before:
pp: α : Type u_1
inst✝² : Preorder α
t₁ t₂ : TopologicalSpace α
inst✝¹ : Topology.IsUpperSet α
inst✝ : IsUpper α
s : Set α
hs : IsOpen[t₂] s
⊢ IsOpen[t₁] s

Tactic:
by

Goal state after:
Module: Mathlib.Topology.MetricSpace.GromovHausdorff

Goal state before:
pp: X : Type u
inst✝⁵ : MetricSpace X
inst✝⁴ : CompactSpace X
inst✝³ : Nonempty X
Y : Type v
inst✝² : MetricSpace Y
inst✝¹ : CompactSpace Y
inst✝ : Nonempty Y
inhabited_h✝ : Inhabited X
inhabited_h : Inhabited Y
p q : NonemptyCompacts ↥(lp (fun n ↦ ℝ) ∞)
hp : ⟦p⟧ = toGHSpace X
hq : ⟦q⟧ = toGHSpace Y
bound : hausdorffDist ↑p ↑q < diam univ + 1 + diam univ
Φ : X → ↥(lp (fun n ↦ ℝ) ∞)
Φisom : Isometry Φ
Φrange : range Φ = ↑p
Ψ : Y → ↥(lp (fun n ↦ ℝ) ∞)
Ψisom : Isometry Ψ
Ψrange : range Ψ = ↑q
⊢ diam (range Φ ∪ range Ψ) ≤ 2 * diam univ + 1 + 2 * diam univ

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Order.UpperLowerSetTopology

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : Preorder α
inst✝¹ : TopologicalSpace α
inst✝ : Topology.IsLowerSet α
s : Set α
⊢ OrderDual.instTopologicalSpace = upperSet αᵒᵈ

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Order.LowerUpperTopology

Goal state before:
pp: α : Type u_1
inst✝¹ : CompleteLinearOrder α
t : TopologicalSpace α
inst✝ : IsLower α
U : Set α
hU : ¬U = univ
hO : IsOpen[t] U
S : Set (Set α)
hS1 : S ⊆ insert univ {s | ∃ a, (Ici a)ᶜ = s}
hS2 : U = ⋃₀ S
⊢ univ ∉ S

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Order.UpperLowerSetTopology

Goal state before:
pp: α : Type u_1
inst✝² : Preorder α
inst✝¹ : TopologicalSpace α
inst✝ : Topology.IsLowerSet α
s : Set α
⊢ IsOpen[inst✝¹] s ↔ IsLowerSet s

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Order.UpperLowerSetTopology

Goal state before:
pp: α : Type u_1
inst✝² : Preorder α
inst✝¹ : TopologicalSpace α
inst✝ : Topology.IsLowerSet α
s : Set α
⊢ IsClosed[inst✝¹] s ↔ IsUpperSet s

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Order.UpperLowerSetTopology

Goal state before:
pp: α : Type u_1
inst✝² : Preorder α
inst✝¹ : TopologicalSpace α
inst✝ : Topology.IsLowerSet α
a : α
⊢ closure[inst✝¹] {a} = Ici a

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Order.UpperLowerSetTopology

Goal state before:
pp: α : Type u_1
inst✝² : Preorder α
inst✝¹ : TopologicalSpace α
inst✝ : Topology.IsLowerSet α
a b : α
⊢ a ⤳ b ↔ a ≤ b

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Order.UpperLowerSetTopology

Goal state before:
pp: α : Type u_1
inst✝² : Preorder α
inst✝¹ : TopologicalSpace α
inst✝ : Topology.IsLowerSet α
s : Set α
⊢ nhdsKer s = ↑(lowerClosure s)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Order.UpperLowerSetTopology

Goal state before:
pp: α : Type u_1
inst✝² : Preorder α
inst✝¹ : TopologicalSpace α
inst✝ : Topology.IsLowerSet α
a : α
⊢ nhdsKer {a} = Iic a

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Order.UpperLowerSetTopology

Goal state before:
pp: α : Type u_1
inst✝² : Preorder α
inst✝¹ : TopologicalSpace α
inst✝ : Topology.IsLowerSet α
a : α
⊢ 𝓝 a = 𝓟 (Iic a)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Order.UpperLowerSetTopology

Goal state before:
pp: α : Type u_1
inst✝² : Preorder α
inst✝¹ : TopologicalSpace α
inst✝ : Topology.IsLowerSet α
s : Set α
⊢ 𝓝ˢ s = 𝓟 ↑(lowerClosure s)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Order.UpperLowerSetTopology

Goal state before:
pp: α : Type u_4
inst✝¹ : TopologicalSpace α
inst✝ : Preorder α
hα : ∀ (a : α), 𝓝 a = 𝓟 (Iic a)
⊢ inst✝¹ = lowerSet α

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Order.UpperLowerSetTopology

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁵ : Preorder α
inst✝⁴ : Preorder β
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : Topology.IsLowerSet α
inst✝ : Topology.IsLowerSet β
f : α → β
⊢ Monotone f ↔ Continuous[inst✝³, inst✝²] f

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Order.UpperLowerSetTopology

Goal state before:
pp: α : Type u_1
inst✝² : Preorder α
t₁ t₂ : TopologicalSpace α
inst✝¹ : Topology.IsLowerSet α
inst✝ : IsLower α
s : Set α
hs : IsOpen[t₂] s
⊢ IsOpen[t₁] s

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Order.UpperLowerSetTopology

Goal state before:
pp: α : Type u_1
inst✝¹ : Preorder α
inst✝ : TopologicalSpace α
⊢ Topology.IsUpperSet αᵒᵈ ↔ Topology.IsLowerSet α

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Order.UpperLowerSetTopology

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
a b : α
⊢ Iic (toUpperSet b) ⊆ Iic (toUpperSet a) ↔ b ≤ a

Tactic:
Iic_subset_Iic,

Goal state after:
α : Type u_1
inst✝ : Preorder α
a b : α
⊢ toUpperSet b ≤ toUpperSet a ↔ b ≤ a
Module: Mathlib.Topology.Order.UpperLowerSetTopology

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
a b : α
⊢ toUpperSet a ⤳ toUpperSet b ↔ b ≤ a

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Order.UpperLowerSetTopology

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
a b : α
⊢ toLowerSet a ⤳ toLowerSet b ↔ a ≤ b

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Order.ScottTopology

Goal state before:
pp: α✝ : Type u_1
β : Type u_2
α : Type u_3
D : Set (Set α)
inst✝ : Preorder α
s t : Set α
hs :
  ∀ ⦃d : Set α⦄,
    d ∈ D → d.Nonempty → DirectedOn (fun x1 x2 ↦ x1 ≤ x2) d → ∀ ⦃a : α⦄, IsLUB d a → a ∈ s → ∃ b ∈ d, Ici b ∩ d ⊆ s
ht :
  ∀ ⦃d : Set α⦄,
    d ∈ D → d.Nonempty → DirectedOn (fun x1 x2 ↦ x1 ≤ x2) d → ∀ ⦃a : α⦄, IsLUB d a → a ∈ t → ∃ b ∈ d, Ici b ∩ d ⊆ t
d : Set α
hd₀ : d ∈ D
hd₁ : d.Nonempty
hd₂ : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) d
a : α
hd₃ : IsLUB d a
ha : a ∈ s ∩ t
⊢ ∃ b ∈ d, Ici b ∩ d ⊆ s ∩ t

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Order.ScottTopology

Goal state before:
pp: α✝ : Type u_1
β : Type u_2
α : Type u_3
D : Set (Set α)
inst✝ : Preorder α
s : Set (Set α)
h :
  ∀ t ∈ s,
    ∀ ⦃d : Set α⦄,
      d ∈ D → d.Nonempty → DirectedOn (fun x1 x2 ↦ x1 ≤ x2) d → ∀ ⦃a : α⦄, IsLUB d a → a ∈ t → ∃ b ∈ d, Ici b ∩ d ⊆ t
d : Set α
hd₀ : d ∈ D
hd₁ : d.Nonempty
hd₂ : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) d
a : α
hd₃ : IsLUB d a
x✝ : a ∈ ⋃₀ s
s₀ : Set α
hs₀s : s₀ ∈ s
has₀ : a ∈ s₀
⊢ ∃ b ∈ d, Ici b ∩ d ⊆ ⋃₀ s

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Order.ScottTopology

Goal state before:
pp: α : Type u_1
s : Set α
D : Set (Set α)
inst✝¹ : Preorder α
t : TopologicalSpace α
inst✝ : IsScottHausdorff α D
⊢ IsOpen[t] s ↔
    ∀ ⦃d : Set α⦄,
      d ∈ D → d.Nonempty → DirectedOn (fun x1 x2 ↦ x1 ≤ x2) d → ∀ ⦃a : α⦄, IsLUB d a → a ∈ s → ∃ b ∈ d, Ici b ∩ d ⊆ s

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Order.ScottTopology

Goal state before:
pp: α : Type u_1
s : Set α
D : Set (Set α)
inst✝¹ : Preorder α
t : TopologicalSpace α
inst✝ : IsScottHausdorff α D
hDL : IsLowerSet D
⊢ IsOpen[t] s ↔ DirSupInaccOn D s

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Order.ScottTopology

Goal state before:
pp: α : Type u_1
s : Set α
D : Set (Set α)
inst✝¹ : Preorder α
t : TopologicalSpace α
inst✝ : IsScottHausdorff α D
hDL : IsLowerSet D
⊢ IsClosed[t] s ↔ DirSupClosedOn D s

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Order.ScottTopology

Goal state before:
pp: α : Type u_1
s : Set α
inst✝¹ : Preorder α
t : TopologicalSpace α
inst✝ : IsScottHausdorff α univ
⊢ IsOpen[t] s ↔ DirSupInacc s

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Order.ScottTopology

Goal state before:
pp: α : Type u_1
s : Set α
inst✝¹ : Preorder α
t : TopologicalSpace α
inst✝ : IsScottHausdorff α univ
⊢ IsClosed[t] s ↔ DirSupClosed s

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Order.ScottTopology

Goal state before:
pp: α : Type u_1
D : Set (Set α)
inst✝² : Preorder α
inst✝¹ : TopologicalSpace α
s : Set α
inst✝ : IsScott α D
⊢ IsOpen[inst✝¹] s ↔ IsUpperSet s ∧ IsOpen[scottHausdorff α D] s

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Order.ScottTopology

Goal state before:
pp: α : Type u_1
D : Set (Set α)
inst✝² : Preorder α
inst✝¹ : TopologicalSpace α
s : Set α
inst✝ : IsScott α D
⊢ IsOpen[inst✝¹] s ↔ IsUpperSet s ∧ DirSupInaccOn D s

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Order.ScottTopology

Goal state before:
pp: α : Type u_1
inst✝² : Preorder α
inst✝¹ : TopologicalSpace α
s : Set α
inst✝ : IsScott α univ
⊢ IsClosed[inst✝¹] s ↔ IsLowerSet s ∧ DirSupClosed s

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Order.ScottTopology

Goal state before:
pp: α : Type u_1
inst✝² : Preorder α
inst✝¹ : TopologicalSpace α
s : Set α
inst✝ : IsScott α univ
⊢ ↑(lowerClosure s) ⊆ closure[inst✝¹] s

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Order.ScottTopology

Goal state before:
pp: α : Type u_1
inst✝² : Preorder α
inst✝¹ : TopologicalSpace α
a : α
inst✝ : IsScott α univ
⊢ {a} ⊆ Iic a

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Order.ScottTopology

Goal state before:
pp: α : Type u_1
inst✝² : Preorder α
inst✝¹ : TopologicalSpace α
a : α
inst✝ : IsScott α univ
⊢ Iic a ⊆ closure[inst✝¹] {a}

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Order.ScottTopology

Goal state before:
pp: α : Type u_1
β : Type u_2
D : Set (Set α)
inst✝⁵ : Preorder α
inst✝⁴ : TopologicalSpace α
inst✝³ : Preorder β
inst✝² : TopologicalSpace β
inst✝¹ : IsScott β univ
f : α → β
inst✝ : IsScott α D
hf : Continuous[inst✝⁴, inst✝²] f
x✝ b : α
hab : x✝ ≤ b
⊢ f x✝ ≤ f b

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Order.LowerUpperTopology

Goal state before:
pp: α : Type u_1
inst✝¹ : CompleteLinearOrder α
t : TopologicalSpace α
inst✝ : IsLower α
U : Set α
⊢ IsOpen[t] U ↔ U = univ ∨ ∃ a, (Ici a)ᶜ = U

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Order.LowerUpperTopology

Goal state before:
pp: α : Type u_1
inst✝² : Preorder α
inst✝¹ : TopologicalSpace α
inst✝ : IsUpper α
s : Set α
⊢ IsOpen[inst✝¹] s ↔ GenerateOpen {t | ∃ a, (Iic a)ᶜ = t} s

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Order.ScottTopology

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁵ : Preorder α
inst✝⁴ : TopologicalSpace α
inst✝³ : Preorder β
inst✝² : TopologicalSpace β
inst✝¹ : IsScott β univ
f : α → β
D : Set (Set α)
inst✝ : IsScott α D
hD : ∀ (a b : α), a ≤ b → {a, b} ∈ D
⊢ ScottContinuousOn D f ↔ Continuous[inst✝⁴, inst✝²] f

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Order.ScottTopology

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : PartialOrder α
inst✝¹ : TopologicalSpace α
inst✝ : IsScott α univ
x y : α
h : Inseparable x y
⊢ Iic x = Iic y

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Order.LowerUpperTopology

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁷ : Preorder α
inst✝⁶ : TopologicalSpace α
inst✝⁵ : IsLower α
inst✝⁴ : OrderBot α
inst✝³ : Preorder β
inst✝² : TopologicalSpace β
inst✝¹ : IsLower β
inst✝ : OrderBot β
s : Set α
hs : s.Finite
t : Set β
ht : t.Finite
x✝¹ : TopologicalSpace (α × β) := lower (α × β)
a : α
x✝ : a ∈ s
⊢ (Ici (a, ⊥))ᶜ = (Prod.fst ⁻¹' Ici a)ᶜ

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Order.LowerUpperTopology

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁷ : Preorder α
inst✝⁶ : TopologicalSpace α
inst✝⁵ : IsLower α
inst✝⁴ : OrderBot α
inst✝³ : Preorder β
inst✝² : TopologicalSpace β
inst✝¹ : IsLower β
inst✝ : OrderBot β
s : Set α
hs : s.Finite
t : Set β
ht : t.Finite
x✝¹ : TopologicalSpace (α × β) := lower (α × β)
b : β
x✝ : b ∈ t
⊢ (Ici (⊥, b))ᶜ = (Prod.snd ⁻¹' Ici b)ᶜ

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Order.LowerUpperTopology

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁷ : Preorder α
inst✝⁶ : TopologicalSpace α
inst✝⁵ : IsLower α
inst✝⁴ : OrderBot α
inst✝³ : Preorder β
inst✝² : TopologicalSpace β
inst✝¹ : IsLower β
inst✝ : OrderBot β
⊢ instTopologicalSpaceProd = lower (α × β)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Order.ScottTopology

Goal state before:
pp: α : Type u_1
inst✝² : CompleteLinearOrder α
inst✝¹ : TopologicalSpace α
inst✝ : IsScott α univ
U : Set α
⊢ IsOpen[inst✝¹] U ↔ U = univ ∨ ∃ a, (Iic a)ᶜ = U

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Order.LowerUpperTopology

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁷ : Preorder α
inst✝⁶ : TopologicalSpace α
inst✝⁵ : IsUpper α
inst✝⁴ : OrderTop α
inst✝³ : Preorder β
inst✝² : TopologicalSpace β
inst✝¹ : IsUpper β
inst✝ : OrderTop β
⊢ instTopologicalSpaceProd = upper (α × β)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Order.LowerUpperTopology

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁵ : CompleteLattice α
inst✝⁴ : CompleteLattice β
inst✝³ : TopologicalSpace α
inst✝² : IsLower α
inst✝¹ : TopologicalSpace β
inst✝ : IsLower β
f : sInfHom α β
⊢ Continuous[inst✝³, inst✝¹] ⇑f

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Order.ScottTopology

Goal state before:
pp: α : Type u_1
inst✝ : CompleteLinearOrder α
⊢ scott α univ = upper α

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Order.LowerUpperTopology

Goal state before:
pp: α : Type u_1
inst✝¹ : Preorder α
inst✝ : TopologicalSpace α
⊢ IsUpper αᵒᵈ ↔ IsLower α

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Order.ScottTopology

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : CompleteLinearOrder α
inst✝¹ : TopologicalSpace α
inst✝ : IsUpper α
⊢ inst✝¹ = scott α univ

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Order.ScottTopology

Goal state before:
pp: α : Type u_1
inst✝² : Preorder α
s : Set α
inst✝¹ : TopologicalSpace α
inst✝ : IsScott α univ
x✝² x✝¹ : α
x✝ : x✝² ≤ x✝¹
⊢ {x✝², x✝¹} ∈ univ

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Order.LowerUpperTopology

Goal state before:
pp: h : Set Prop
hs : h ∈ {∅, {True}}
⊢ h ∈ {s | ∃ a, (Iic a)ᶜ = s}

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Order.ScottTopology

Goal state before:
pp: α : Type u_1
inst✝² : Preorder α
s : Set α
inst✝¹ : TopologicalSpace α
inst✝ : IsScott α univ
⊢ IsOpen[inst✝¹] s ↔ ScottContinuous fun x ↦ x ∈ s

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Order.ScottTopology

Goal state before:
pp: α : Type u_1
inst✝² : Preorder α
inst✝¹ : TopologicalSpace α
inst✝ : IsScott α univ
⊢ scottHausdorff α univ ≤ inst✝¹

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Order.LowerUpperTopology

Goal state before:
pp: ⊢ {s | ∃ a, (Iic a)ᶜ = s} ⊆ {∅, {True}}

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Order.LowerUpperTopology

Goal state before:
pp: ⊢ sierpinskiSpace = upper Prop

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Order.ScottTopology

Goal state before:
pp: α : Type u_1
inst✝² : Preorder α
inst✝¹ : TopologicalSpace α
inst✝ : IsLower α
⊢ scottHausdorff α univ ≤ inst✝¹

Tactic:
by

Goal state after:
Module: Mathlib.Topology.OmegaCompletePartialOrder

Goal state before:
pp: α : Type u_1
inst✝² : OmegaCompletePartialOrder α
inst✝¹ : TopologicalSpace α
inst✝ : IsScott α (range fun c ↦ range ⇑c)
f : α → Prop
a b : α
hab : a ≤ b
⊢ {a, b} ∈ range fun c ↦ range ⇑c

Tactic:
by

Goal state after:
Module: Mathlib.Topology.OmegaCompletePartialOrder

Goal state before:
pp: α : Type u_1
inst✝² : OmegaCompletePartialOrder α
inst✝¹ : TopologicalSpace α
inst✝ : IsScott α (range fun c ↦ range ⇑c)
f : α → Prop
⊢ ωScottContinuous f ↔ Continuous[inst✝¹, _] f

Tactic:
by

Goal state after:
Module: Mathlib.Topology.OmegaCompletePartialOrder

Goal state before:
pp: α : Type u
inst✝ : Preorder α
c : Chain α
x : α
⊢ IsωSup c x ↔ IsLUB (range ⇑c) x

Tactic:
by

Goal state after:
Module: Mathlib.Topology.OmegaCompletePartialOrder

Goal state before:
pp: α : Type u
inst✝ : OmegaCompletePartialOrder α
s : Set (Set α)
hs : ∀ t ∈ s, IsOpen α t
⊢ IsOpen α (⋃₀ s)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.OmegaCompletePartialOrder

Goal state before:
pp: α : Type u_1
inst✝ : OmegaCompletePartialOrder α
c : Chain α
⊢ IsωSup c (ωSup c)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Specialization

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
⊢ ∀ {a b : α}, (toUpperSet.trans toEquiv) a ≤ (toUpperSet.trans toEquiv) b ↔ a ≤ b

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Specialization

Goal state before:
pp: α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : AlexandrovDiscrete α
s : Set (WithUpperSet (Specialization α))
⊢ IsOpen[inst✝¹] (⇑(toEquiv.trans toUpperSet) ⁻¹' s) ↔ IsOpen[instTopologicalSpace] s

Tactic:
simp [Set.preimage_comp]

Goal state after:
Module: Mathlib.Topology.Specialization

Goal state before:
pp: α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : AlexandrovDiscrete α
s : Set (WithUpperSet (Specialization α))
⊢ IsOpen[inst✝¹] (⇑(toEquiv.trans toUpperSet) ⁻¹' s) ↔ IsOpen[instTopologicalSpace] s

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Order.Category.AlexDisc

Goal state before:
pp: X Y : AlexDisc
f g : X ⟶ Y
h : (forget₂ AlexDisc TopCat).map f = (forget₂ AlexDisc TopCat).map g
⊢ f = g

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Order.Category.AlexDisc

Goal state before:
pp: α β : AlexDisc
e : ↑α.toTopCat ≃ₜ ↑β.toTopCat
⊢ ConcreteCategory.ofHom ↑e ≫ ConcreteCategory.ofHom ↑e.symm = 𝟙 α

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Order.Category.AlexDisc

Goal state before:
pp: α β : AlexDisc
e : ↑α.toTopCat ≃ₜ ↑β.toTopCat
⊢ ConcreteCategory.ofHom ↑e.symm ≫ ConcreteCategory.ofHom ↑e = 𝟙 β

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Order.Category.AlexDisc

Goal state before:
pp: X : AlexDisc
⊢ ↑((𝟭 AlexDisc).obj X).toTopCat ≃ₜ
    ↑(((forget₂ AlexDisc TopCat ⋙ topToPreord) ⋙
              { obj := fun X ↦ AlexDisc.of (WithUpperSet ↑X),
                map := fun {X Y} f ↦ ConcreteCategory.ofHom (WithUpperSet.map (Preord.Hom.hom f)),
                map_id := alexDiscEquivPreord._proof_1, map_comp := @alexDiscEquivPreord._proof_2 }).obj
          X).toTopCat

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Order.Category.AlexDisc

Goal state before:
pp: X : Preord
⊢ ↑(({ obj := fun X ↦ AlexDisc.of (WithUpperSet ↑X),
              map := fun {X Y} f ↦ ConcreteCategory.ofHom (WithUpperSet.map (Preord.Hom.hom f)),
              map_id := alexDiscEquivPreord._proof_1, map_comp := @alexDiscEquivPreord._proof_2 } ⋙
            forget₂ AlexDisc TopCat ⋙ topToPreord).obj
        X) ≃o
    ↑((𝟭 Preord).obj X)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Order.Category.FrameAdjunction

Goal state before:
pp: L : Type u_1
inst✝ : CompleteLattice L
a b : L
⊢ {x | x (a ⊓ b)} = {x | x a} ⊓ {x | x b}

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Order.Category.FrameAdjunction

Goal state before:
pp: L : Type u_1
inst✝ : CompleteLattice L
⊢ {x | x ⊤} = ⊤

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Order.Category.FrameAdjunction

Goal state before:
pp: L : Type u_1
inst✝ : CompleteLattice L
S : Set L
⊢ {x | x (sSup S)} = sSup ((fun u ↦ {x | x u}) '' S)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Order.Category.FrameAdjunction

Goal state before:
pp: L : Type u_1
inst✝ : CompleteLattice L
⊢ {x | x ⊤} = univ

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Order.Category.FrameAdjunction

Goal state before:
pp: L : Type u_1
inst✝ : CompleteLattice L
⊢ ∀ (s t : Set (PT L)), (∃ u, {x | x u} = s) → (∃ u, {x | x u} = t) → ∃ u, {x | x u} = s ∩ t

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Order.Category.FrameAdjunction

Goal state before:
pp: L : Type u_1
inst✝ : CompleteLattice L
S : Set (Set (PT L))
hS : ∀ t ∈ S, ∃ u, {x | x u} = t
⊢ ∃ u, {x | x u} = ⋃₀ S

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Order.Category.FrameAdjunction

Goal state before:
pp: L : Type u_1
inst✝ : CompleteLattice L
X✝ Y✝ : Locale
f : X✝ ⟶ Y✝
⊢ ∀ (s : Set (PT ↑(Opposite.unop Y✝))), IsOpen s → IsOpen ((fun p ↦ FrameHom.comp p (Frm.Hom.hom f.unop)) ⁻¹' s)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Order.Category.FrameAdjunction

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
L : Locale
x : X
S : Set (Opens X)
⊢ (x ∈ sSup S) = sSup ((fun x_1 ↦ x ∈ x_1) '' S)

Tactic:
by

Goal state after: