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

Goal state before:
pp: case inr
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
I : diam (range Φ ∪ range Ψ) ≤ 2 * diam univ + 1 + 2 * diam univ
f : X ⊕ Y → ↥(lp (fun n ↦ ℝ) ∞) :=
  fun x ↦
    match x with
    | inl y => Φ y
    | inr z => Ψ z
F : (X ⊕ Y) × (X ⊕ Y) → ℝ := fun p ↦ dist (f p.1) (f p.2)
x y : X ⊕ Y
val✝ : Y
⊢ f (inr val✝) ∈ range Φ ∪ range Ψ

Tactic:
·

Goal state after:
case inr
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
I : diam (range Φ ∪ range Ψ) ≤ 2 * diam univ + 1 + 2 * diam univ
f : X ⊕ Y → ↥(lp (fun n ↦ ℝ) ∞) :=
  fun x ↦
    match x with
    | inl y => Φ y
    | inr z => Ψ z
F : (X ⊕ Y) × (X ⊕ Y) → ℝ := fun p ↦ dist (f p.1) (f p.2)
x y : X ⊕ Y
val✝ : Y
⊢ f (inr val✝) ∈ range Φ ∪ range Ψ
Module: Mathlib.Topology.Order.Completion

Goal state before:
pp: case refine_1
α : Type u_1
inst✝⁴ : LinearOrder α
inst✝³ : TopologicalSpace α
inst✝² : OrderTopology α
inst✝¹ : TopologicalSpace (DedekindCut α)
inst✝ : OrderTopology (DedekindCut α)
c : DedekindCut α
⊢ IsOpen ((fun a ↦ principal a) ⁻¹' Ioi c)

pp: case refine_2
α : Type u_1
inst✝⁴ : LinearOrder α
inst✝³ : TopologicalSpace α
inst✝² : OrderTopology α
inst✝¹ : TopologicalSpace (DedekindCut α)
inst✝ : OrderTopology (DedekindCut α)
c : DedekindCut α
⊢ IsOpen ((fun a ↦ principal a) ⁻¹' Iio c)

Tactic:
·

Goal state after:
case refine_1
α : Type u_1
inst✝⁴ : LinearOrder α
inst✝³ : TopologicalSpace α
inst✝² : OrderTopology α
inst✝¹ : TopologicalSpace (DedekindCut α)
inst✝ : OrderTopology (DedekindCut α)
c : DedekindCut α
⊢ IsOpen ((fun a ↦ principal a) ⁻¹' Ioi c)
Module: Mathlib.Topology.Order.Completion

Goal state before:
pp: case refine_2
α : Type u_1
inst✝⁴ : LinearOrder α
inst✝³ : TopologicalSpace α
inst✝² : OrderTopology α
inst✝¹ : TopologicalSpace (DedekindCut α)
inst✝ : OrderTopology (DedekindCut α)
c : DedekindCut α
⊢ IsOpen ((fun a ↦ principal a) ⁻¹' Iio c)

Tactic:
·

Goal state after:
case refine_2
α : Type u_1
inst✝⁴ : LinearOrder α
inst✝³ : TopologicalSpace α
inst✝² : OrderTopology α
inst✝¹ : TopologicalSpace (DedekindCut α)
inst✝ : OrderTopology (DedekindCut α)
c : DedekindCut α
⊢ IsOpen ((fun a ↦ principal a) ⁻¹' Iio c)
Module: Mathlib.Topology.Order.Completion

Goal state before:
pp: case inl
α : Type u_1
inst✝ : LinearOrder α
x : α
q : ℚ
hx₁ : IsSuccPrelimit x → 0 ≤ q
hx₂ : IsPredPrelimit x → q ≤ 0
y : α
r : ℚ
hy₁ : IsSuccPrelimit y → 0 ≤ r
hy₂ : IsPredPrelimit y → r ≤ 0
h : x < y
⊢ ∃ a, ⟨toLex (x, q), ⋯⟩ < a ∧ a < ⟨toLex (y, r), ⋯⟩

pp: case inr
α : Type u_1
inst✝ : LinearOrder α
x : α
q : ℚ
hx₁ : IsSuccPrelimit x → 0 ≤ q
hx₂ : IsPredPrelimit x → q ≤ 0
r : ℚ
h : q < r
hy₁ : IsSuccPrelimit x → 0 ≤ r
hy₂ : IsPredPrelimit x → r ≤ 0
⊢ ∃ a, ⟨toLex (x, q), ⋯⟩ < a ∧ a < ⟨toLex (x, r), ⋯⟩

Tactic:
·

Goal state after:
case inl
α : Type u_1
inst✝ : LinearOrder α
x : α
q : ℚ
hx₁ : IsSuccPrelimit x → 0 ≤ q
hx₂ : IsPredPrelimit x → q ≤ 0
y : α
r : ℚ
hy₁ : IsSuccPrelimit y → 0 ≤ r
hy₂ : IsPredPrelimit y → r ≤ 0
h : x < y
⊢ ∃ a, ⟨toLex (x, q), ⋯⟩ < a ∧ a < ⟨toLex (y, r), ⋯⟩
Module: Mathlib.Topology.Order.Completion

Goal state before:
pp: case pos
α : Type u_1
inst✝ : LinearOrder α
x : α
q : ℚ
hx₁ : IsSuccPrelimit x → 0 ≤ q
hx₂ : IsPredPrelimit x → q ≤ 0
y : α
r : ℚ
hy₁ : IsSuccPrelimit y → 0 ≤ r
hy₂ : IsPredPrelimit y → r ≤ 0
h : x < y
hx : IsPredPrelimit x
⊢ ∃ a, ⟨toLex (x, q), ⋯⟩ < a ∧ a < ⟨toLex (y, r), ⋯⟩

pp: case neg
α : Type u_1
inst✝ : LinearOrder α
x : α
q : ℚ
hx₁ : IsSuccPrelimit x → 0 ≤ q
hx₂ : IsPredPrelimit x → q ≤ 0
y : α
r : ℚ
hy₁ : IsSuccPrelimit y → 0 ≤ r
hy₂ : IsPredPrelimit y → r ≤ 0
h : x < y
hx : ¬IsPredPrelimit x
⊢ ∃ a, ⟨toLex (x, q), ⋯⟩ < a ∧ a < ⟨toLex (y, r), ⋯⟩

Tactic:
·

Goal state after:
case pos
α : Type u_1
inst✝ : LinearOrder α
x : α
q : ℚ
hx₁ : IsSuccPrelimit x → 0 ≤ q
hx₂ : IsPredPrelimit x → q ≤ 0
y : α
r : ℚ
hy₁ : IsSuccPrelimit y → 0 ≤ r
hy₂ : IsPredPrelimit y → r ≤ 0
h : x < y
hx : IsPredPrelimit x
⊢ ∃ a, ⟨toLex (x, q), ⋯⟩ < a ∧ a < ⟨toLex (y, r), ⋯⟩
Module: Mathlib.Topology.Order.HullKernel

Goal state before:
pp: case mp
α : Type u_1
inst✝³ : SemilatticeInf α
T : Set α
inst✝² : OrderTop α
inst✝¹ : TopologicalSpace α
inst✝ : IsLower α
hT : ∀ p ∈ T, InfPrime p
R : Set ↑T
ha : ∃ a, (hull T a)ᶜ = R
⊢ ∃ a, a.Finite ∧ (Subtype.val ⁻¹' ↑(upperClosure a))ᶜ = R

pp: case mpr
α : Type u_1
inst✝³ : SemilatticeInf α
T : Set α
inst✝² : OrderTop α
inst✝¹ : TopologicalSpace α
inst✝ : IsLower α
hT : ∀ p ∈ T, InfPrime p
R : Set ↑T
ha : ∃ a, a.Finite ∧ (Subtype.val ⁻¹' ↑(upperClosure a))ᶜ = R
⊢ ∃ a, (hull T a)ᶜ = R

Tactic:
·

Goal state after:
case mp
α : Type u_1
inst✝³ : SemilatticeInf α
T : Set α
inst✝² : OrderTop α
inst✝¹ : TopologicalSpace α
inst✝ : IsLower α
hT : ∀ p ∈ T, InfPrime p
R : Set ↑T
ha : ∃ a, (hull T a)ᶜ = R
⊢ ∃ a, a.Finite ∧ (Subtype.val ⁻¹' ↑(upperClosure a))ᶜ = R
Module: Mathlib.Topology.Order.HullKernel

Goal state before:
pp: case mpr
α : Type u_1
inst✝³ : SemilatticeInf α
T : Set α
inst✝² : OrderTop α
inst✝¹ : TopologicalSpace α
inst✝ : IsLower α
hT : ∀ p ∈ T, InfPrime p
R : Set ↑T
ha : ∃ a, a.Finite ∧ (Subtype.val ⁻¹' ↑(upperClosure a))ᶜ = R
⊢ ∃ a, (hull T a)ᶜ = R

Tactic:
·

Goal state after:
case mpr
α : Type u_1
inst✝³ : SemilatticeInf α
T : Set α
inst✝² : OrderTop α
inst✝¹ : TopologicalSpace α
inst✝ : IsLower α
hT : ∀ p ∈ T, InfPrime p
R : Set ↑T
ha : ∃ a, a.Finite ∧ (Subtype.val ⁻¹' ↑(upperClosure a))ᶜ = R
⊢ ∃ a, (hull T a)ᶜ = R
Module: Mathlib.Topology.Order.Completion

Goal state before:
pp: case neg.refine_1
α : Type u_1
inst✝ : LinearOrder α
x : α
q : ℚ
hx₁ : IsSuccPrelimit x → 0 ≤ q
hx₂ : IsPredPrelimit x → q ≤ 0
y : α
r : ℚ
hy₁ : IsSuccPrelimit y → 0 ≤ r
hy₂ : IsPredPrelimit y → r ≤ 0
h : x < y
hx : ¬IsPredPrelimit x
s : ℚ
hs : 0 < s ∧ q < s
⊢ (IsSuccPrelimit (ofLex (toLex (x, s))).1 → 0 ≤ (ofLex (toLex (x, s))).2) ∧
    (IsPredPrelimit (ofLex (toLex (x, s))).1 → (ofLex (toLex (x, s))).2 ≤ 0)

pp: case neg.refine_2
α : Type u_1
inst✝ : LinearOrder α
x : α
q : ℚ
hx₁ : IsSuccPrelimit x → 0 ≤ q
hx₂ : IsPredPrelimit x → q ≤ 0
y : α
r : ℚ
hy₁ : IsSuccPrelimit y → 0 ≤ r
hy₂ : IsPredPrelimit y → r ≤ 0
h : x < y
hx : ¬IsPredPrelimit x
s : ℚ
hs : 0 < s ∧ q < s
⊢ ⟨toLex (x, q), ⋯⟩ < ⟨toLex (x, s), ?neg.refine_1✝⟩ ∧ ⟨toLex (x, s), ?neg.refine_1✝⟩ < ⟨toLex (y, r), ⋯⟩

Tactic:
·

Goal state after:
case neg.refine_1
α : Type u_1
inst✝ : LinearOrder α
x : α
q : ℚ
hx₁ : IsSuccPrelimit x → 0 ≤ q
hx₂ : IsPredPrelimit x → q ≤ 0
y : α
r : ℚ
hy₁ : IsSuccPrelimit y → 0 ≤ r
hy₂ : IsPredPrelimit y → r ≤ 0
h : x < y
hx : ¬IsPredPrelimit x
s : ℚ
hs : 0 < s ∧ q < s
⊢ (IsSuccPrelimit (ofLex (toLex (x, s))).1 → 0 ≤ (ofLex (toLex (x, s))).2) ∧
    (IsPredPrelimit (ofLex (toLex (x, s))).1 → (ofLex (toLex (x, s))).2 ≤ 0)
Module: Mathlib.Topology.Order.Completion

Goal state before:
pp: case neg.refine_2
α : Type u_1
inst✝ : LinearOrder α
x : α
q : ℚ
hx₁ : IsSuccPrelimit x → 0 ≤ q
hx₂ : IsPredPrelimit x → q ≤ 0
y : α
r : ℚ
hy₁ : IsSuccPrelimit y → 0 ≤ r
hy₂ : IsPredPrelimit y → r ≤ 0
h : x < y
hx : ¬IsPredPrelimit x
s : ℚ
hs : 0 < s ∧ q < s
⊢ ⟨toLex (x, q), ⋯⟩ < ⟨toLex (x, s), ⋯⟩ ∧ ⟨toLex (x, s), ⋯⟩ < ⟨toLex (y, r), ⋯⟩

Tactic:
·

Goal state after:
case neg.refine_2
α : Type u_1
inst✝ : LinearOrder α
x : α
q : ℚ
hx₁ : IsSuccPrelimit x → 0 ≤ q
hx₂ : IsPredPrelimit x → q ≤ 0
y : α
r : ℚ
hy₁ : IsSuccPrelimit y → 0 ≤ r
hy₂ : IsPredPrelimit y → r ≤ 0
h : x < y
hx : ¬IsPredPrelimit x
s : ℚ
hs : 0 < s ∧ q < s
⊢ ⟨toLex (x, q), ⋯⟩ < ⟨toLex (x, s), ⋯⟩ ∧ ⟨toLex (x, s), ⋯⟩ < ⟨toLex (y, r), ⋯⟩
Module: Mathlib.Topology.Order.Completion

Goal state before:
pp: case inr
α : Type u_1
inst✝ : LinearOrder α
x : α
q : ℚ
hx₁ : IsSuccPrelimit x → 0 ≤ q
hx₂ : IsPredPrelimit x → q ≤ 0
r : ℚ
h : q < r
hy₁ : IsSuccPrelimit x → 0 ≤ r
hy₂ : IsPredPrelimit x → r ≤ 0
⊢ ∃ a, ⟨toLex (x, q), ⋯⟩ < a ∧ a < ⟨toLex (x, r), ⋯⟩

Tactic:
·

Goal state after:
case inr
α : Type u_1
inst✝ : LinearOrder α
x : α
q : ℚ
hx₁ : IsSuccPrelimit x → 0 ≤ q
hx₂ : IsPredPrelimit x → q ≤ 0
r : ℚ
h : q < r
hy₁ : IsSuccPrelimit x → 0 ≤ r
hy₂ : IsPredPrelimit x → r ≤ 0
⊢ ∃ a, ⟨toLex (x, q), ⋯⟩ < a ∧ a < ⟨toLex (x, r), ⋯⟩
Module: Mathlib.Topology.Order.HullKernel

Goal state before:
pp: α : Type u_1
inst✝³ : SemilatticeInf α
T : Set α
inst✝² : OrderTop α
inst✝¹ : TopologicalSpace α
inst✝ : IsLower α
hT : ∀ p ∈ T, InfPrime p
⊢ IsTopologicalBasis {S | ∃ a, (hull T a)ᶜ = S}

Tactic:
convert! isTopologicalBasis_subtype Topology.IsLower.isTopologicalBasis (· ∈ T)
  ext R
  simp only [preimage_compl, mem_ofPred_eq, IsLower.lowerBasis, mem_image, exists_exists_and_eq_and]
  constructor <;> intro ha
  · obtain ⟨a, ha'⟩ := ha
    use {a}
    rw [← (Function.Injective.preimage_image Subtype.val_injective R), ← ha']
    simp only [finite_singleton, upperClosure_singleton, UpperSet.coe_Ici, image_val_compl,
      Subtype.image_preimage_coe, sdiff_self_inter, preimage_sdiff, Subtype.coe_preimage_self,
      true_and]
    exact compl_eq_univ_sdiff (Subtype.val ⁻¹' Ici a)
  · obtain ⟨F, hF⟩ := ha
    lift F to Finset α using hF.1
    use Finset.inf F id
    ext
    simp [hull_finsetInf hT, ← hF.2]

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

Goal state before:
pp: case inr.refine_1
α : Type u_1
inst✝ : LinearOrder α
x : α
q : ℚ
hx₁ : IsSuccPrelimit x → 0 ≤ q
hx₂ : IsPredPrelimit x → q ≤ 0
r : ℚ
h : q < r
hy₁ : IsSuccPrelimit x → 0 ≤ r
hy₂ : IsPredPrelimit x → r ≤ 0
s : ℚ
hs : q < s
hs' : s < r
⊢ (IsSuccPrelimit (ofLex (toLex (x, s))).1 → 0 ≤ (ofLex (toLex (x, s))).2) ∧
    (IsPredPrelimit (ofLex (toLex (x, s))).1 → (ofLex (toLex (x, s))).2 ≤ 0)

pp: case inr.refine_2
α : Type u_1
inst✝ : LinearOrder α
x : α
q : ℚ
hx₁ : IsSuccPrelimit x → 0 ≤ q
hx₂ : IsPredPrelimit x → q ≤ 0
r : ℚ
h : q < r
hy₁ : IsSuccPrelimit x → 0 ≤ r
hy₂ : IsPredPrelimit x → r ≤ 0
s : ℚ
hs : q < s
hs' : s < r
⊢ ⟨toLex (x, q), ⋯⟩ < ⟨toLex (x, s), ?inr.refine_1⟩ ∧ ⟨toLex (x, s), ?inr.refine_1⟩ < ⟨toLex (x, r), ⋯⟩

Tactic:
·

Goal state after:
case inr.refine_1
α : Type u_1
inst✝ : LinearOrder α
x : α
q : ℚ
hx₁ : IsSuccPrelimit x → 0 ≤ q
hx₂ : IsPredPrelimit x → q ≤ 0
r : ℚ
h : q < r
hy₁ : IsSuccPrelimit x → 0 ≤ r
hy₂ : IsPredPrelimit x → r ≤ 0
s : ℚ
hs : q < s
hs' : s < r
⊢ (IsSuccPrelimit (ofLex (toLex (x, s))).1 → 0 ≤ (ofLex (toLex (x, s))).2) ∧
    (IsPredPrelimit (ofLex (toLex (x, s))).1 → (ofLex (toLex (x, s))).2 ≤ 0)
Module: Mathlib.Topology.Order.Completion

Goal state before:
pp: case inr.refine_2
α : Type u_1
inst✝ : LinearOrder α
x : α
q : ℚ
hx₁ : IsSuccPrelimit x → 0 ≤ q
hx₂ : IsPredPrelimit x → q ≤ 0
r : ℚ
h : q < r
hy₁ : IsSuccPrelimit x → 0 ≤ r
hy₂ : IsPredPrelimit x → r ≤ 0
s : ℚ
hs : q < s
hs' : s < r
⊢ ⟨toLex (x, q), ⋯⟩ < ⟨toLex (x, s), ⋯⟩ ∧ ⟨toLex (x, s), ⋯⟩ < ⟨toLex (x, r), ⋯⟩

Tactic:
·

Goal state after:
case inr.refine_2
α : Type u_1
inst✝ : LinearOrder α
x : α
q : ℚ
hx₁ : IsSuccPrelimit x → 0 ≤ q
hx₂ : IsPredPrelimit x → q ≤ 0
r : ℚ
h : q < r
hy₁ : IsSuccPrelimit x → 0 ≤ r
hy₂ : IsPredPrelimit x → r ≤ 0
s : ℚ
hs : q < s
hs' : s < r
⊢ ⟨toLex (x, q), ⋯⟩ < ⟨toLex (x, s), ⋯⟩ ∧ ⟨toLex (x, s), ⋯⟩ < ⟨toLex (x, r), ⋯⟩
Module: Mathlib.Topology.Order.HullKernel

Goal state before:
pp: case mp
α : Type u_1
inst✝² : CompleteLattice α
T : Set α
inst✝¹ : TopologicalSpace α
inst✝ : IsLower α
hT : ∀ p ∈ T, InfPrime p
S : Set ↑T
h : IsOpen[instTopologicalSpaceSubtype] S
⊢ ∃ a, S = (hull T a)ᶜ

pp: case mpr
α : Type u_1
inst✝² : CompleteLattice α
T : Set α
inst✝¹ : TopologicalSpace α
inst✝ : IsLower α
hT : ∀ p ∈ T, InfPrime p
S : Set ↑T
h : ∃ a, S = (hull T a)ᶜ
⊢ IsOpen[instTopologicalSpaceSubtype] S

Tactic:
·

Goal state after:
case mp
α : Type u_1
inst✝² : CompleteLattice α
T : Set α
inst✝¹ : TopologicalSpace α
inst✝ : IsLower α
hT : ∀ p ∈ T, InfPrime p
S : Set ↑T
h : IsOpen[instTopologicalSpaceSubtype] S
⊢ ∃ a, S = (hull T a)ᶜ
Module: Mathlib.Topology.Order.Completion

Goal state before:
pp: case refine_1
α : Type u_1
inst✝² : LinearOrder α
inst✝¹ : TopologicalSpace α
inst✝ : OrderTopology α
x : α
q : ℚ
x✝ : (IsSuccPrelimit x → 0 ≤ q) ∧ (IsPredPrelimit x → q ≤ 0)
hx₁ : IsSuccPrelimit x → 0 ≤ q
hx₂ : IsPredPrelimit x → q ≤ 0
⊢ IsOpen (⇑some ⁻¹' Ioi ⟨toLex (x, q), ⋯⟩)

pp: case refine_2
α : Type u_1
inst✝² : LinearOrder α
inst✝¹ : TopologicalSpace α
inst✝ : OrderTopology α
x : α
q : ℚ
x✝ : (IsSuccPrelimit x → 0 ≤ q) ∧ (IsPredPrelimit x → q ≤ 0)
hx₁ : IsSuccPrelimit x → 0 ≤ q
hx₂ : IsPredPrelimit x → q ≤ 0
⊢ IsOpen (⇑some ⁻¹' Iio ⟨toLex (x, q), ⋯⟩)

Tactic:
·

Goal state after:
case refine_1
α : Type u_1
inst✝² : LinearOrder α
inst✝¹ : TopologicalSpace α
inst✝ : OrderTopology α
x : α
q : ℚ
x✝ : (IsSuccPrelimit x → 0 ≤ q) ∧ (IsPredPrelimit x → q ≤ 0)
hx₁ : IsSuccPrelimit x → 0 ≤ q
hx₂ : IsPredPrelimit x → q ≤ 0
⊢ IsOpen (⇑some ⁻¹' Ioi ⟨toLex (x, q), ⋯⟩)
Module: Mathlib.Topology.Order.Completion

Goal state before:
pp: case refine_1.inl
α : Type u_1
inst✝² : LinearOrder α
inst✝¹ : TopologicalSpace α
inst✝ : OrderTopology α
x : α
q : ℚ
x✝ : (IsSuccPrelimit x → 0 ≤ q) ∧ (IsPredPrelimit x → q ≤ 0)
hx₁ : IsSuccPrelimit x → 0 ≤ q
hx₂ : IsPredPrelimit x → q ≤ 0
hq : 0 ≤ q
⊢ IsOpen (⇑some ⁻¹' Ioi ⟨toLex (x, q), ⋯⟩)

pp: case refine_1.inr
α : Type u_1
inst✝² : LinearOrder α
inst✝¹ : TopologicalSpace α
inst✝ : OrderTopology α
x : α
q : ℚ
x✝ : (IsSuccPrelimit x → 0 ≤ q) ∧ (IsPredPrelimit x → q ≤ 0)
hx₁ : IsSuccPrelimit x → 0 ≤ q
hx₂ : IsPredPrelimit x → q ≤ 0
hq : q < 0
⊢ IsOpen (⇑some ⁻¹' Ioi ⟨toLex (x, q), ⋯⟩)

Tactic:
·

Goal state after:
case refine_1.inl
α : Type u_1
inst✝² : LinearOrder α
inst✝¹ : TopologicalSpace α
inst✝ : OrderTopology α
x : α
q : ℚ
x✝ : (IsSuccPrelimit x → 0 ≤ q) ∧ (IsPredPrelimit x → q ≤ 0)
hx₁ : IsSuccPrelimit x → 0 ≤ q
hx₂ : IsPredPrelimit x → q ≤ 0
hq : 0 ≤ q
⊢ IsOpen (⇑some ⁻¹' Ioi ⟨toLex (x, q), ⋯⟩)
Module: Mathlib.Topology.Order.Completion

Goal state before:
pp: case refine_1.inl
α : Type u_1
inst✝² : LinearOrder α
inst✝¹ : TopologicalSpace α
inst✝ : OrderTopology α
x : α
q : ℚ
x✝ : (IsSuccPrelimit x → 0 ≤ q) ∧ (IsPredPrelimit x → q ≤ 0)
hx₁ : IsSuccPrelimit x → 0 ≤ q
hx₂ : IsPredPrelimit x → q ≤ 0
hq : 0 ≤ q
⊢ IsOpen (⇑some ⁻¹' Ioi ⟨toLex (x, q), ⋯⟩)

pp: case refine_1.inr
α : Type u_1
inst✝² : LinearOrder α
inst✝¹ : TopologicalSpace α
inst✝ : OrderTopology α
x : α
q : ℚ
x✝ : (IsSuccPrelimit x → 0 ≤ q) ∧ (IsPredPrelimit x → q ≤ 0)
hx₁ : IsSuccPrelimit x → 0 ≤ q
hx₂ : IsPredPrelimit x → q ≤ 0
hq : q < 0
⊢ IsOpen (⇑some ⁻¹' Ioi ⟨toLex (x, q), ⋯⟩)

Tactic:
· convert isOpen_Ioi (a := x)
      ext
      simp [some, Prod.Lex.lt_iff, hq.not_gt]

Goal state after:
case refine_1.inr
α : Type u_1
inst✝² : LinearOrder α
inst✝¹ : TopologicalSpace α
inst✝ : OrderTopology α
x : α
q : ℚ
x✝ : (IsSuccPrelimit x → 0 ≤ q) ∧ (IsPredPrelimit x → q ≤ 0)
hx₁ : IsSuccPrelimit x → 0 ≤ q
hx₂ : IsPredPrelimit x → q ≤ 0
hq : q < 0
⊢ IsOpen (⇑some ⁻¹' Ioi ⟨toLex (x, q), ⋯⟩)
Module: Mathlib.Topology.Order.Completion

Goal state before:
pp: case refine_1.inr
α : Type u_1
inst✝² : LinearOrder α
inst✝¹ : TopologicalSpace α
inst✝ : OrderTopology α
x : α
q : ℚ
x✝ : (IsSuccPrelimit x → 0 ≤ q) ∧ (IsPredPrelimit x → q ≤ 0)
hx₁ : IsSuccPrelimit x → 0 ≤ q
hx₂ : IsPredPrelimit x → q ≤ 0
hq : q < 0
⊢ IsOpen (⇑some ⁻¹' Ioi ⟨toLex (x, q), ⋯⟩)

Tactic:
·

Goal state after:
case refine_1.inr
α : Type u_1
inst✝² : LinearOrder α
inst✝¹ : TopologicalSpace α
inst✝ : OrderTopology α
x : α
q : ℚ
x✝ : (IsSuccPrelimit x → 0 ≤ q) ∧ (IsPredPrelimit x → q ≤ 0)
hx₁ : IsSuccPrelimit x → 0 ≤ q
hx₂ : IsPredPrelimit x → q ≤ 0
hq : q < 0
⊢ IsOpen (⇑some ⁻¹' Ioi ⟨toLex (x, q), ⋯⟩)
Module: Mathlib.Topology.Order.HullKernel

Goal state before:
pp: case mpr
α : Type u_1
inst✝² : CompleteLattice α
T : Set α
inst✝¹ : TopologicalSpace α
inst✝ : IsLower α
hT : ∀ p ∈ T, InfPrime p
S : Set ↑T
h : ∃ a, S = (hull T a)ᶜ
⊢ IsOpen[instTopologicalSpaceSubtype] S

Tactic:
·

Goal state after:
case mpr
α : Type u_1
inst✝² : CompleteLattice α
T : Set α
inst✝¹ : TopologicalSpace α
inst✝ : IsLower α
hT : ∀ p ∈ T, InfPrime p
S : Set ↑T
h : ∃ a, S = (hull T a)ᶜ
⊢ IsOpen[instTopologicalSpaceSubtype] S
Module: Mathlib.Topology.Order.Completion

Goal state before:
pp: case refine_2
α : Type u_1
inst✝² : LinearOrder α
inst✝¹ : TopologicalSpace α
inst✝ : OrderTopology α
x : α
q : ℚ
x✝ : (IsSuccPrelimit x → 0 ≤ q) ∧ (IsPredPrelimit x → q ≤ 0)
hx₁ : IsSuccPrelimit x → 0 ≤ q
hx₂ : IsPredPrelimit x → q ≤ 0
⊢ IsOpen (⇑some ⁻¹' Iio ⟨toLex (x, q), ⋯⟩)

Tactic:
·

Goal state after:
case refine_2
α : Type u_1
inst✝² : LinearOrder α
inst✝¹ : TopologicalSpace α
inst✝ : OrderTopology α
x : α
q : ℚ
x✝ : (IsSuccPrelimit x → 0 ≤ q) ∧ (IsPredPrelimit x → q ≤ 0)
hx₁ : IsSuccPrelimit x → 0 ≤ q
hx₂ : IsPredPrelimit x → q ≤ 0
⊢ IsOpen (⇑some ⁻¹' Iio ⟨toLex (x, q), ⋯⟩)
Module: Mathlib.Topology.Order.Completion

Goal state before:
pp: case refine_2.inl
α : Type u_1
inst✝² : LinearOrder α
inst✝¹ : TopologicalSpace α
inst✝ : OrderTopology α
x : α
q : ℚ
x✝ : (IsSuccPrelimit x → 0 ≤ q) ∧ (IsPredPrelimit x → q ≤ 0)
hx₁ : IsSuccPrelimit x → 0 ≤ q
hx₂ : IsPredPrelimit x → q ≤ 0
hq : q ≤ 0
⊢ IsOpen (⇑some ⁻¹' Iio ⟨toLex (x, q), ⋯⟩)

pp: case refine_2.inr
α : Type u_1
inst✝² : LinearOrder α
inst✝¹ : TopologicalSpace α
inst✝ : OrderTopology α
x : α
q : ℚ
x✝ : (IsSuccPrelimit x → 0 ≤ q) ∧ (IsPredPrelimit x → q ≤ 0)
hx₁ : IsSuccPrelimit x → 0 ≤ q
hx₂ : IsPredPrelimit x → q ≤ 0
hq : 0 < q
⊢ IsOpen (⇑some ⁻¹' Iio ⟨toLex (x, q), ⋯⟩)

Tactic:
·

Goal state after:
case refine_2.inl
α : Type u_1
inst✝² : LinearOrder α
inst✝¹ : TopologicalSpace α
inst✝ : OrderTopology α
x : α
q : ℚ
x✝ : (IsSuccPrelimit x → 0 ≤ q) ∧ (IsPredPrelimit x → q ≤ 0)
hx₁ : IsSuccPrelimit x → 0 ≤ q
hx₂ : IsPredPrelimit x → q ≤ 0
hq : q ≤ 0
⊢ IsOpen (⇑some ⁻¹' Iio ⟨toLex (x, q), ⋯⟩)
Module: Mathlib.Topology.Order.Completion

Goal state before:
pp: case refine_2.inr
α : Type u_1
inst✝² : LinearOrder α
inst✝¹ : TopologicalSpace α
inst✝ : OrderTopology α
x : α
q : ℚ
x✝ : (IsSuccPrelimit x → 0 ≤ q) ∧ (IsPredPrelimit x → q ≤ 0)
hx₁ : IsSuccPrelimit x → 0 ≤ q
hx₂ : IsPredPrelimit x → q ≤ 0
hq : 0 < q
⊢ IsOpen (⇑some ⁻¹' Iio ⟨toLex (x, q), ⋯⟩)

Tactic:
·

Goal state after:
case refine_2.inr
α : Type u_1
inst✝² : LinearOrder α
inst✝¹ : TopologicalSpace α
inst✝ : OrderTopology α
x : α
q : ℚ
x✝ : (IsSuccPrelimit x → 0 ≤ q) ∧ (IsPredPrelimit x → q ≤ 0)
hx₁ : IsSuccPrelimit x → 0 ≤ q
hx₂ : IsPredPrelimit x → q ≤ 0
hq : 0 < q
⊢ IsOpen (⇑some ⁻¹' Iio ⟨toLex (x, q), ⋯⟩)
Module: Mathlib.Topology.Order.HullKernel

Goal state before:
pp: case left
α : Type u_1
inst✝² : CompleteLattice α
T : Set α
inst✝¹ : TopologicalSpace α
inst✝ : IsLower α
hT : ∀ p ∈ T, InfPrime p
hG : OrderGenerates T
S : Set ↑T
⊢ ⋂₀ {t | IsClosed[instTopologicalSpaceSubtype] t ∧ S ⊆ t} ⊆ hull T (kernel S)

pp: case right
α : Type u_1
inst✝² : CompleteLattice α
T : Set α
inst✝¹ : TopologicalSpace α
inst✝ : IsLower α
hT : ∀ p ∈ T, InfPrime p
hG : OrderGenerates T
S : Set ↑T
⊢ hull T (kernel S) ⊆ ⋂₀ {t | IsClosed[instTopologicalSpaceSubtype] t ∧ S ⊆ t}

Tactic:
·

Goal state after:
case left
α : Type u_1
inst✝² : CompleteLattice α
T : Set α
inst✝¹ : TopologicalSpace α
inst✝ : IsLower α
hT : ∀ p ∈ T, InfPrime p
hG : OrderGenerates T
S : Set ↑T
⊢ ⋂₀ {t | IsClosed[instTopologicalSpaceSubtype] t ∧ S ⊆ t} ⊆ hull T (kernel S)
Module: Mathlib.Topology.Order.HullKernel

Goal state before:
pp: case right
α : Type u_1
inst✝² : CompleteLattice α
T : Set α
inst✝¹ : TopologicalSpace α
inst✝ : IsLower α
hT : ∀ p ∈ T, InfPrime p
hG : OrderGenerates T
S : Set ↑T
⊢ hull T (kernel S) ⊆ ⋂₀ {t | IsClosed[instTopologicalSpaceSubtype] t ∧ S ⊆ t}

Tactic:
·

Goal state after:
case right
α : Type u_1
inst✝² : CompleteLattice α
T : Set α
inst✝¹ : TopologicalSpace α
inst✝ : IsLower α
hT : ∀ p ∈ T, InfPrime p
hG : OrderGenerates T
S : Set ↑T
⊢ hull T (kernel S) ⊆ ⋂₀ {t | IsClosed[instTopologicalSpaceSubtype] t ∧ S ⊆ t}
Module: Mathlib.Topology.Order.HullKernel

Goal state before:
pp: case right
α : Type u_1
inst✝² : CompleteLattice α
T : Set α
inst✝¹ : TopologicalSpace α
inst✝ : IsLower α
hT : ∀ p ∈ T, InfPrime p
hG : OrderGenerates T
S : Set ↑T
⊢ ∀ t' ∈ {t | IsClosed[instTopologicalSpaceSubtype] t ∧ S ⊆ t}, hull T (kernel S) ⊆ t'

Tactic:
intro R hR

Goal state after:
case right
α : Type u_1
inst✝² : CompleteLattice α
T : Set α
inst✝¹ : TopologicalSpace α
inst✝ : IsLower α
hT : ∀ p ∈ T, InfPrime p
hG : OrderGenerates T
S R : Set ↑T
hR : R ∈ {t | IsClosed[instTopologicalSpaceSubtype] t ∧ S ⊆ t}
⊢ hull T (kernel S) ⊆ R
Module: Mathlib.Topology.Order.NhdsSet

Goal state before:
pp: case inl
α : Type u_1
inst✝² : LinearOrder α
inst✝¹ : TopologicalSpace α
inst✝ : OrderClosedTopology α
a : α
h : a ≤ a
⊢ 𝓝ˢ (Icc a a) = 𝓝 a ⊔ 𝓝 a ⊔ 𝓟 (Ioo a a)

pp: case inr
α : Type u_1
inst✝² : LinearOrder α
inst✝¹ : TopologicalSpace α
inst✝ : OrderClosedTopology α
a b : α
h : a ≤ b
hlt : a < b
⊢ 𝓝ˢ (Icc a b) = 𝓝 a ⊔ 𝓝 b ⊔ 𝓟 (Ioo a b)

Tactic:
·

Goal state after:
case inl
α : Type u_1
inst✝² : LinearOrder α
inst✝¹ : TopologicalSpace α
inst✝ : OrderClosedTopology α
a : α
h : a ≤ a
⊢ 𝓝ˢ (Icc a a) = 𝓝 a ⊔ 𝓝 a ⊔ 𝓟 (Ioo a a)
Module: Mathlib.Topology.Order.NhdsSet

Goal state before:
pp: case inr
α : Type u_1
inst✝² : LinearOrder α
inst✝¹ : TopologicalSpace α
inst✝ : OrderClosedTopology α
a b : α
h : a ≤ b
hlt : a < b
⊢ 𝓝ˢ (Icc a b) = 𝓝 a ⊔ 𝓝 b ⊔ 𝓟 (Ioo a b)

Tactic:
·

Goal state after:
case inr
α : Type u_1
inst✝² : LinearOrder α
inst✝¹ : TopologicalSpace α
inst✝ : OrderClosedTopology α
a b : α
h : a ≤ b
hlt : a < b
⊢ 𝓝ˢ (Icc a b) = 𝓝 a ⊔ 𝓝 b ⊔ 𝓟 (Ioo a b)
Module: Mathlib.Topology.Order.Priestley

Goal state before:
pp: case inl
α : Type u_1
inst✝² : TopologicalSpace α
inst✝¹ : PartialOrder α
inst✝ : PriestleySpace α
x y : α
h✝ : x ≠ y
h : ¬x ≤ y
⊢ ∃ U, IsClopen U ∧ (IsUpperSet U ∨ IsLowerSet U) ∧ x ∈ U ∧ y ∉ U

pp: case inr
α : Type u_1
inst✝² : TopologicalSpace α
inst✝¹ : PartialOrder α
inst✝ : PriestleySpace α
x y : α
h✝ : x ≠ y
h : ¬y ≤ x
⊢ ∃ U, IsClopen U ∧ (IsUpperSet U ∨ IsLowerSet U) ∧ x ∈ U ∧ y ∉ U

Tactic:
·

Goal state after:
case inl
α : Type u_1
inst✝² : TopologicalSpace α
inst✝¹ : PartialOrder α
inst✝ : PriestleySpace α
x y : α
h✝ : x ≠ y
h : ¬x ≤ y
⊢ ∃ U, IsClopen U ∧ (IsUpperSet U ∨ IsLowerSet U) ∧ x ∈ U ∧ y ∉ U
Module: Mathlib.Topology.Order.Priestley

Goal state before:
pp: case inr
α : Type u_1
inst✝² : TopologicalSpace α
inst✝¹ : PartialOrder α
inst✝ : PriestleySpace α
x y : α
h✝ : x ≠ y
h : ¬y ≤ x
⊢ ∃ U, IsClopen U ∧ (IsUpperSet U ∨ IsLowerSet U) ∧ x ∈ U ∧ y ∉ U

Tactic:
·

Goal state after:
case inr
α : Type u_1
inst✝² : TopologicalSpace α
inst✝¹ : PartialOrder α
inst✝ : PriestleySpace α
x y : α
h✝ : x ≠ y
h : ¬y ≤ x
⊢ ∃ U, IsClopen U ∧ (IsUpperSet U ∨ IsLowerSet U) ∧ x ∈ U ∧ y ∉ U