awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Order.LawsonTopology
Goal:
α : Type u_1
inst : Preorder α
inst_1 : TopologicalSpace α
inst_2 : IsLawson α
lawsonBasis_image2 :
  lawsonBasis α =
    image2
      (fun (x : Set (WithLower α)) (x_1 : Set (WithScott α)) ↦
        (⇑WithLower.toLower : (a : α) → WithLower α) ⁻¹' x ∩ (⇑WithScott.toScott : (a : α) → WithScott α) ⁻¹' x_1)
      (IsLower.lowerBasis (WithLower α)) {U : Set (WithScott α) | IsOpen[scott α univ] U}
⊢ IsTopologicalBasis.{u_1} (α := α)
    (image2
      (fun (x1 : Set (WithLower α)) (x2 : Set (WithScott α)) ↦
        (⇑WithLower.toLower : (a : α) → WithLower α) ⁻¹' x1 ∩ (⇑WithScott.toScott : (a : α) → WithScott α) ⁻¹' x2)
      (IsLower.lowerBasis (WithLower α)) {U : Set (WithScott α) | IsOpen[WithScott.instTopologicalSpace] U})

Tactic:
IsTopologicalBasis.inf_induced IsLower.isTopologicalBasis
      (isTopologicalBasis_opens (α := WithScott α)) WithLower.toLower WithScott.toScott

Premises used: Topology.WithScott.toScott, TopologicalSpace.IsTopologicalBasis.inf_induced, TopologicalSpace.isTopologicalBasis_opens, Topology.IsLower.isTopologicalBasis, Topology.WithLower.toLower, DFunLike.coe
-- Module: Mathlib.Topology.Order.LawsonTopology
Goal:
α : Type u_1
inst : Preorder α
inst_1 : TopologicalSpace α
inst_2 : IsLawson α
lawsonBasis_image2 :
  lawsonBasis α =
    image2
      (fun (x : Set (WithLower α)) (x_1 : Set (WithScott α)) ↦
        (⇑WithLower.toLower : (a : α) → WithLower α) ⁻¹' x ∩ (⇑WithScott.toScott : (a : α) → WithScott α) ⁻¹' x_1)
      (IsLower.lowerBasis (WithLower α)) {U : Set (WithScott α) | IsOpen[scott α univ] U}
h :
  inst_1 =
    induced (Y := WithLower α) (⇑WithLower.toLower : (a : α) → WithLower α) WithLower.instTopologicalSpace ⊓
      induced (Y := WithScott α) (⇑WithScott.toScott : (a : α) → WithScott α) WithScott.instTopologicalSpace
⊢ IsTopologicalBasis.{u_1} (α := α)
    (image2
      (fun (x : Set (WithLower α)) (x_1 : Set (WithScott α)) ↦
        (⇑WithLower.toLower : (a : α) → WithLower α) ⁻¹' x ∩ (⇑WithScott.toScott : (a : α) → WithScott α) ⁻¹' x_1)
      (IsLower.lowerBasis (WithLower α)) {U : Set (WithScott α) | IsOpen[scott α univ] U})

Tactic:
convert!
    IsTopologicalBasis.inf_induced IsLower.isTopologicalBasis
      (isTopologicalBasis_opens (α := WithScott α)) WithLower.toLower WithScott.toScott

Premises used: Topology.WithScott.toScott, TopologicalSpace.IsTopologicalBasis.inf_induced, TopologicalSpace.isTopologicalBasis_opens, Topology.IsLower.isTopologicalBasis, Topology.WithLower.toLower, DFunLike.coe
-- Module: Mathlib.Topology.Order.LawsonTopology
Goal:
α : Type u_1
inst : Preorder α
inst_1 : TopologicalSpace α
inst_2 : IsLawson α
lawsonBasis_image2 :
  lawsonBasis α =
    image2
      (fun (x : Set (WithLower α)) (x_1 : Set (WithScott α)) ↦
        (⇑WithLower.toLower : (a : α) → WithLower α) ⁻¹' x ∩ (⇑WithScott.toScott : (a : α) → WithScott α) ⁻¹' x_1)
      (IsLower.lowerBasis (WithLower α)) {U : Set (WithScott α) | IsOpen[scott α univ] U}
h :
  lower α ⊓ scott α univ =
    induced (Y := WithLower α) (⇑WithLower.toLower : (a : α) → WithLower α) WithLower.instTopologicalSpace ⊓
      induced (Y := WithScott α) (⇑WithScott.toScott : (a : α) → WithScott α) WithScott.instTopologicalSpace
⊢ inst_1 =
    induced (Y := WithLower α) (⇑WithLower.toLower : (a : α) → WithLower α) WithLower.instTopologicalSpace ⊓
      induced (Y := WithScott α) (⇑WithScott.toScott : (a : α) → WithScott α) WithScott.instTopologicalSpace

Tactic:
rw [@topology_eq_lawson α _ _ _, lawson]

Premises used: Topology.lawson, Topology.IsLawson.topology_eq_lawson
-- Module: Mathlib.Topology.Order.LawsonTopology
Goal:
α : Type u_1
inst : Preorder α
inst_1 : TopologicalSpace α
inst_2 : IsLawson α
lawsonBasis_image2 :
  lawsonBasis α =
    image2
      (fun (x : Set (WithLower α)) (x_1 : Set (WithScott α)) ↦
        (⇑WithLower.toLower : (a : α) → WithLower α) ⁻¹' x ∩ (⇑WithScott.toScott : (a : α) → WithScott α) ⁻¹' x_1)
      (IsLower.lowerBasis (WithLower α)) {U : Set (WithScott α) | IsOpen[scott α univ] U}
apply : lower α = induced (Y := WithLower α) (⇑WithLower.toLower : (a : α) → WithLower α) WithLower.instTopologicalSpace
apply₁ :
  scott α univ = induced (Y := WithScott α) (⇑WithScott.toScott : (a : α) → WithScott α) WithScott.instTopologicalSpace
⊢ lower α ⊓ scott α univ =
    induced (Y := WithLower α) (⇑WithLower.toLower : (a : α) → WithLower α) WithLower.instTopologicalSpace ⊓
      induced (Y := WithScott α) (⇑WithScott.toScott : (a : α) → WithScott α) WithScott.instTopologicalSpace

Tactic:
apply (congrArg₂ min _) _

Premises used: congrArg₂, Min.min
-- Module: Mathlib.Topology.Order.LawsonTopology
Goal:
α : Type u_1
inst : Preorder α
inst_1 : TopologicalSpace α
inst_2 : IsLawson α
lawsonBasis_image2 :
  lawsonBasis α =
    image2
      (fun (x : Set (WithLower α)) (x_1 : Set (WithScott α)) ↦
        (⇑WithLower.toLower : (a : α) → WithLower α) ⁻¹' x ∩ (⇑WithScott.toScott : (a : α) → WithScott α) ⁻¹' x_1)
      (IsLower.lowerBasis (WithLower α)) {U : Set (WithScott α) | IsOpen[scott α univ] U}
x : TopologicalSpace α := lower α
⊢ lower α = induced (Y := WithLower α) (⇑WithLower.toLower : (a : α) → WithLower α) WithLower.instTopologicalSpace

Tactic:
(@IsLower.withLowerHomeomorph α ‹_› (lower α) ⟨rfl⟩).isInducing.eq_induced

Premises used: Homeomorph.isInducing, Topology.IsLower.withLowerHomeomorph, Topology.WithLower, Topology.IsInducing.eq_induced
-- Module: Mathlib.Topology.Order.LawsonTopology
Goal:
α : Type u_1
inst : Preorder α
inst_1 : TopologicalSpace α
inst_2 : IsLawson α
lawsonBasis_image2 :
  lawsonBasis α =
    image2
      (fun (x : Set (WithLower α)) (x_1 : Set (WithScott α)) ↦
        (⇑WithLower.toLower : (a : α) → WithLower α) ⁻¹' x ∩ (⇑WithScott.toScott : (a : α) → WithScott α) ⁻¹' x_1)
      (IsLower.lowerBasis (WithLower α)) {U : Set (WithScott α) | IsOpen[scott α univ] U}
x : TopologicalSpace α := lower α
⊢ lower α = induced (Y := WithLower α) (⇑WithLower.toLower : (a : α) → WithLower α) WithLower.instTopologicalSpace

Tactic:
exact (@IsLower.withLowerHomeomorph α ‹_› (lower α) ⟨rfl⟩).isInducing.eq_induced

Premises used: Homeomorph.isInducing, Topology.IsLower.withLowerHomeomorph, Topology.IsInducing.eq_induced
-- Module: Mathlib.Topology.Order.LawsonTopology
Goal:
α : Type u_1
inst : Preorder α
inst_1 : TopologicalSpace α
inst_2 : IsLawson α
lawsonBasis_image2 :
  lawsonBasis α =
    image2
      (fun (x : Set (WithLower α)) (x_1 : Set (WithScott α)) ↦
        (⇑WithLower.toLower : (a : α) → WithLower α) ⁻¹' x ∩ (⇑WithScott.toScott : (a : α) → WithScott α) ⁻¹' x_1)
      (IsLower.lowerBasis (WithLower α)) {U : Set (WithScott α) | IsOpen[scott α univ] U}
x : TopologicalSpace α := scott α univ
⊢ scott α univ = induced (Y := WithScott α) (⇑WithScott.toScott : (a : α) → WithScott α) WithScott.instTopologicalSpace

Tactic:
(@IsScott.withScottHomeomorph α _ (scott α univ) ⟨rfl⟩).isInducing.eq_induced

Premises used: Homeomorph.isInducing, Topology.WithScott.instTopologicalSpace._aux_1, Topology.WithScott, Topology.IsScott.withScottHomeomorph, Topology.IsInducing.eq_induced
-- Module: Mathlib.Topology.Order.LawsonTopology
Goal:
α : Type u_1
inst : Preorder α
inst_1 : TopologicalSpace α
inst_2 : IsLawson α
lawsonBasis_image2 :
  lawsonBasis α =
    image2
      (fun (x : Set (WithLower α)) (x_1 : Set (WithScott α)) ↦
        (⇑WithLower.toLower : (a : α) → WithLower α) ⁻¹' x ∩ (⇑WithScott.toScott : (a : α) → WithScott α) ⁻¹' x_1)
      (IsLower.lowerBasis (WithLower α)) {U : Set (WithScott α) | IsOpen[scott α univ] U}
x : TopologicalSpace α := scott α univ
⊢ scott α univ = induced (Y := WithScott α) (⇑WithScott.toScott : (a : α) → WithScott α) WithScott.instTopologicalSpace

Tactic:
exact (@IsScott.withScottHomeomorph α _ (scott α univ) ⟨rfl⟩).isInducing.eq_induced

Premises used: Homeomorph.isInducing, Topology.IsScott.withScottHomeomorph, Topology.IsInducing.eq_induced
-- Module: Mathlib.Topology.Order.LawsonTopology
Goal:
α : Type u_1
⊢ Eq.{u_1 + 1} (α := WithLawson α ≃ α) (Equiv.symm toLawson) ofLawson

Tactic:
rfl

Premises used: Topology.WithLawson.ofLawson, Equiv.symm, Equiv.refl, rfl, Topology.WithLawson
-- Module: Mathlib.Topology.Order.LawsonTopology
Goal:
α : Type u_1
⊢ Eq.{u_1 + 1} (α := α ≃ WithLawson α) (Equiv.symm ofLawson) toLawson

Tactic:
rfl

Premises used: Topology.WithLawson.toLawson, Equiv.symm, Equiv.refl, rfl, Topology.WithLawson
-- Module: Mathlib.Topology.Order.LawsonTopology
Goal:
α : Type u_1
a : WithLawson α
⊢ (toLawson : (a : α) → WithLawson α) ((ofLawson : (a : WithLawson α) → α) a : α) = a

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Order.LawsonTopology
Goal:
α : Type u_1
a : α
⊢ (ofLawson : (a : WithLawson α) → α) ((toLawson : (a : α) → WithLawson α) a : WithLawson α) = a

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Order.LawsonTopology
Goal:
α : Type u_1
a b : α
⊢ Eq (α := WithLawson α) ((toLawson : (a : α) → WithLawson α) a : WithLawson α)
      ((toLawson : (a : α) → WithLawson α) b : WithLawson α) ↔
    a = b

Tactic:
Iff.rfl

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

Tactic:
Iff.rfl

Premises used: Iff.rfl, Topology.WithLawson
-- Module: Mathlib.Topology.Order.LawsonTopology
Goal:
α : Type u_1
inst : Preorder α
⊢ IsLawson.{u_1} (WithLawson α)

Tactic:
⟨rfl⟩

Premises used: Topology.IsLawson.mk, rfl
-- Module: Mathlib.Topology.Order.LawsonTopology
Goal:
α : Type u_1
inst : Preorder α
S : Set α
⊢ IsOpen[instTopologicalSpace] ((⇑ofLawson : (a : WithLawson α) → α) ⁻¹' S) ↔ TopologicalSpace.IsOpen S

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf, Set.preimage, IsOpen, Topology.WithLawson
-- Module: Mathlib.Topology.Order.LawsonTopology
Goal:
α : Type u_1
inst : Preorder α
S : Set α
⊢ IsClosed[instTopologicalSpace] ((⇑ofLawson : (a : WithLawson α) → α) ⁻¹' S) ↔ IsClosed[lawson α] S

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf, Set.preimage, Topology.WithLawson.instTopologicalSpace._aux_1, Topology.WithLawson
-- Module: Mathlib.Topology.Order.LawsonTopology
Goal:
α : Type u_1
inst : Preorder α
T : Set (WithLawson α)
⊢ IsOpen[instTopologicalSpace] T ↔ TopologicalSpace.IsOpen (X := α) ((⇑toLawson : (a : α) → WithLawson α) ⁻¹' T)

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf, Set.preimage, IsOpen, Topology.WithLawson
-- Module: Mathlib.Topology.Order.LawsonTopology
Goal:
α : Type u_1
inst : Preorder α
⊢ lawson α ≤ scott α univ

Tactic:
inf_le_right

Premises used: inf_le_right
-- Module: Mathlib.Topology.Order.LawsonTopology
Goal:
α : Type u_1
inst : Preorder α
⊢ lawson α ≤ lower α

Tactic:
inf_le_left

Premises used: inf_le_left
-- Module: Mathlib.Topology.Order.LawsonTopology
Goal:
α : Type u_1
inst : Preorder α
⊢ scottHausdorff α univ ≤ lawson α

Tactic:
le_inf scottHausdorff_le_lower scottHausdorff_le_scott

Premises used: le_inf, Topology.scottHausdorff_le_scott, Topology.scottHausdorff_le_lower
-- Module: Mathlib.Topology.Order.LawsonTopology
Goal:
α : Type u_1
inst : Preorder α
s : Set α
h : IsClosed[WithScott.instTopologicalSpace] ((⇑WithScott.ofScott : (a : WithScott α) → α) ⁻¹' s)
⊢ IsClosed[WithLawson.instTopologicalSpace] ((⇑WithLawson.ofLawson : (a : WithLawson α) → α) ⁻¹' s)

Tactic:
h.mono lawson_le_scott

Premises used: Topology.lawson_le_scott, IsClosed.mono, Topology.WithLawson
-- Module: Mathlib.Topology.Order.LawsonTopology
Goal:
α : Type u_1
inst : Preorder α
s : Set α
h : IsClosed[WithLower.instTopologicalSpace] ((⇑WithLower.ofLower : (a : WithLower α) → α) ⁻¹' s)
⊢ IsClosed[WithLawson.instTopologicalSpace] ((⇑WithLawson.ofLawson : (a : WithLawson α) → α) ⁻¹' s)

Tactic:
h.mono lawson_le_lower

Premises used: IsClosed.mono, Topology.lawson_le_lower, Topology.WithLawson
-- Module: Mathlib.Topology.Order.LawsonTopology
Goal:
α : Type u_1
inst : Preorder α
s : Set α
h : IsUpperSet s
⊢ IsOpen[WithLawson.instTopologicalSpace] ((⇑WithLawson.ofLawson : (a : WithLawson α) → α) ⁻¹' s) ↔
    IsOpen[WithScott.instTopologicalSpace] ((⇑WithScott.ofScott : (a : WithScott α) → α) ⁻¹' s)

Tactic:
⟨fun hs => IsScott.isOpen_iff_isUpperSet_and_scottHausdorff_open (D := univ).mpr
    ⟨h, (scottHausdorff_le_lawson s) hs⟩, lawson_le_scott _⟩

Premises used: Topology.lawson_le_scott, Iff.mpr, Topology.scottHausdorff_le_lawson, And.intro, Iff.intro, Topology.IsScott.isOpen_iff_isUpperSet_and_scottHausdorff_open
-- Module: Mathlib.Topology.Order.LawsonTopology
Goal:
α : Type u_1
inst : Preorder α
L S : TopologicalSpace α
inst_1 : IsLawson α
inst_2 : IsScott α univ
rw : lawson α ≤ scott α univ
⊢ L ≤ S

Tactic:
rw [@IsScott.topology_eq α univ _ S _, @IsLawson.topology_eq_lawson α _ L _]

Premises used: Topology.IsScott.topology_eq, Set.univ, Topology.IsLawson.topology_eq_lawson
-- Module: Mathlib.Topology.Order.LawsonTopology
Goal:
α : Type u_1
inst : Preorder α
L S : TopologicalSpace α
inst_1 : IsLawson α
inst_2 : IsScott α univ
⊢ lawson α ≤ scott α univ

Tactic:
inf_le_right

Premises used: inf_le_right
-- Module: Mathlib.Topology.Order.LawsonTopology
Goal:
α : Type u_1
inst : Preorder α
L S : TopologicalSpace α
inst_1 : IsLawson α
inst_2 : IsScott α univ
⊢ lawson α ≤ scott α univ

Tactic:
exact inf_le_right

Premises used: inf_le_right
-- Module: Mathlib.Topology.Order.LawsonTopology
Goal:
α : Type u_1
inst : Preorder α
L : TopologicalSpace α
inst_1 : IsLawson α
rw : scottHausdorff α univ ≤ lawson α
⊢ scottHausdorff α univ ≤ L

Tactic:
rw [@IsLawson.topology_eq_lawson α _ L _]

Premises used: Topology.IsLawson.topology_eq_lawson
-- Module: Mathlib.Topology.Order.LawsonTopology
Goal:
α : Type u_1
inst : Preorder α
L : TopologicalSpace α
inst_1 : IsLawson α
⊢ scottHausdorff α univ ≤ lawson α

Tactic:
scottHausdorff_le_lawson

Premises used: Topology.scottHausdorff_le_lawson
-- Module: Mathlib.Topology.Order.LawsonTopology
Goal:
α : Type u_1
inst : Preorder α
L : TopologicalSpace α
inst_1 : IsLawson α
⊢ scottHausdorff α univ ≤ lawson α

Tactic:
exact scottHausdorff_le_lawson

Premises used: Topology.scottHausdorff_le_lawson
-- Module: Mathlib.Topology.Order.LawsonTopology
Goal:
α : Type u_1
inst : Preorder α
L S : TopologicalSpace α
inst_1 : IsLawson α
inst_2 : IsScott α univ
s : Set α
h : IsUpperSet s
rw : IsOpen[lawson α] s ↔ IsOpen[scott α univ] s
⊢ IsOpen[L] s ↔ IsOpen[S] s

Tactic:
rw [@IsLawson.topology_eq_lawson α _ L _, @IsScott.topology_eq α univ _ S _]

Premises used: Topology.IsScott.topology_eq, Set.univ, Topology.IsLawson.topology_eq_lawson
-- Module: Mathlib.Topology.Order.LawsonTopology
Goal:
α : Type u_1
inst : Preorder α
L S : TopologicalSpace α
inst_1 : IsLawson α
inst_2 : IsScott α univ
s : Set α
h : IsUpperSet s
⊢ IsOpen[lawson α] s ↔ IsOpen[scott α univ] s

Tactic:
lawsonOpen_iff_scottOpen_of_isUpperSet h

Premises used: Topology.WithScott.instTopologicalSpace._aux_1, Set.Mem, setOf, Topology.WithScott, Set.preimage, Topology.WithLawson.instTopologicalSpace._aux_1, Topology.lawsonOpen_iff_scottOpen_of_isUpperSet, Topology.WithLawson
-- Module: Mathlib.Topology.Order.LawsonTopology
Goal:
α : Type u_1
inst : Preorder α
L S : TopologicalSpace α
inst_1 : IsLawson α
inst_2 : IsScott α univ
s : Set α
h : IsUpperSet s
⊢ IsOpen[lawson α] s ↔ IsOpen[scott α univ] s

Tactic:
exact lawsonOpen_iff_scottOpen_of_isUpperSet h

Premises used: Topology.lawsonOpen_iff_scottOpen_of_isUpperSet
-- Module: Mathlib.Topology.Order.LawsonTopology
Goal:
α : Type u_1
inst : Preorder α
L S : TopologicalSpace α
inst_1 : IsLawson α
inst_2 : IsScott α univ
s : Set α
h : IsLowerSet s
rw : IsOpen[L] sᶜ ↔ IsClosed[S] s
rw₁ : IsOpen[L] sᶜ ↔ IsOpen[S] sᶜ
rw₂ rw₃ : IsOpen[S] sᶜ ↔ IsOpen[S] sᶜ
⊢ IsClosed[L] s ↔ IsClosed[S] s

Tactic:
rw [← @isOpen_compl_iff, ← isOpen_compl_iff,
    (lawsonOpen_iff_scottOpen_of_isUpperSet' L S _ (isUpperSet_compl.mpr h))]

Premises used: Iff.mpr, Topology.lawsonOpen_iff_scottOpen_of_isUpperSet', isUpperSet_compl, isOpen_compl_iff
-- Module: Mathlib.Topology.Order.LawsonTopology
Goal:
α : Type u_1
inst : Preorder α
L S : TopologicalSpace α
inst_1 : IsLawson α
inst_2 : IsScott α univ
s : Set α
h : IsLowerSet s
rw : IsLowerSet s ∧ DirSupClosed s ↔ DirSupClosed s
⊢ IsClosed[L] s ↔ DirSupClosed s

Tactic:
rw [lawsonClosed_iff_scottClosed_of_isLowerSet L S _ h,
    @IsScott.isClosed_iff_isLowerSet_and_dirSupClosed]

Premises used: Topology.IsScott.isClosed_iff_isLowerSet_and_dirSupClosed, Topology.lawsonClosed_iff_scottClosed_of_isLowerSet
-- Module: Mathlib.Topology.Order.LawsonTopology
Goal:
α : Type u_1
inst : Preorder α
L S : TopologicalSpace α
inst_1 : IsLawson α
inst_2 : IsScott α univ
s : Set α
h : IsLowerSet s
⊢ IsLowerSet s ∧ DirSupClosed s ↔ DirSupClosed s

Tactic:
simp_all
-- Module: Mathlib.Topology.Order.LawsonTopology
Goal:
α : Type u_1
inst : PartialOrder α
inst_1 : TopologicalSpace α
inst_2 : IsLawson α
a : α
simp : IsClosed[lawson α] {a}
⊢ IsClosed[inst_1] {a}

Tactic:
simp +instances only [IsLawson.topology_eq_lawson]

Premises used: Topology.IsLawson.topology_eq_lawson
-- Module: Mathlib.Topology.Order.LawsonTopology
Goal:
α : Type u_1
inst : PartialOrder α
inst_1 : TopologicalSpace α
inst_2 : IsLawson α
a : α
rw :
  IsClosed[WithLawson.instTopologicalSpace]
    ((⇑WithLawson.ofLawson : (a : WithLawson α) → α) ⁻¹'
      ((↑(upperClosure {a}) : Set α) ∩ (↑(lowerClosure {a}) : Set α)))
⊢ IsClosed[lawson α] {a}

Tactic:
rw [← (Set.OrdConnected.upperClosure_inter_lowerClosure ordConnected_singleton),
      ← WithLawson.isClosed_preimage_ofLawson]

Premises used: Topology.WithLawson.isClosed_preimage_ofLawson, Set.ordConnected_singleton, Set.OrdConnected.upperClosure_inter_lowerClosure
-- Module: Mathlib.Topology.Order.LawsonTopology
Goal:
α : Type u_1
inst : PartialOrder α
inst_1 : TopologicalSpace α
inst_2 : IsLawson α
a : α
apply : IsClosed[WithLawson.instTopologicalSpace] (↑(lowerClosure {a}) : Set α)
⊢ IsClosed[WithLawson.instTopologicalSpace]
    ((⇑WithLawson.ofLawson : (a : WithLawson α) → α) ⁻¹'
      ((↑(upperClosure {a}) : Set α) ∩ (↑(lowerClosure {a}) : Set α)))

Tactic:
apply IsClosed.inter
      (lawsonClosed_of_lowerClosed _ (IsLower.isClosed_upperClosure (finite_singleton a)))

Premises used: Topology.lawsonClosed_of_lowerClosed, Topology.IsLower.isClosed_upperClosure, IsClosed.inter, Set.finite_singleton
-- Module: Mathlib.Topology.Order.LawsonTopology
Goal:
α : Type u_1
inst : PartialOrder α
inst_1 : TopologicalSpace α
inst_2 : IsLawson α
a : α
rw :
  IsClosed[WithLawson.instTopologicalSpace]
    ((⇑WithLawson.ofLawson : (a : WithLawson (WithLawson α)) → WithLawson α) ⁻¹' Iic a)
⊢ IsClosed[WithLawson.instTopologicalSpace] (↑(lowerClosure {a}) : Set α)

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

Premises used: lowerClosure_singleton, LowerSet.coe_Iic, Topology.WithLawson.isClosed_preimage_ofLawson
-- Module: Mathlib.Topology.Order.LawsonTopology
Goal:
α : Type u_1
inst : PartialOrder α
inst_1 : TopologicalSpace α
inst_2 : IsLawson α
a : α
⊢ IsClosed[WithLawson.instTopologicalSpace]
    ((⇑WithLawson.ofLawson : (a : WithLawson (WithLawson α)) → WithLawson α) ⁻¹' Iic a)

Tactic:
lawsonClosed_of_scottClosed _ isClosed_Iic

Premises used: isClosed_Iic, Topology.lawsonClosed_of_scottClosed
-- Module: Mathlib.Topology.Order.LawsonTopology
Goal:
α : Type u_1
inst : PartialOrder α
inst_1 : TopologicalSpace α
inst_2 : IsLawson α
a : α
⊢ IsClosed[WithLawson.instTopologicalSpace]
    ((⇑WithLawson.ofLawson : (a : WithLawson (WithLawson α)) → WithLawson α) ⁻¹' Iic a)

Tactic:
exact lawsonClosed_of_scottClosed _ isClosed_Iic
-- Module: Mathlib.Topology.Order.LeftRight
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : Preorder α
a : α
inst_2 : (𝓝[<] a).NeBot
⊢ ∃ᶠ (x : α) in 𝓝 a, x < a

Tactic:
frequently_iff_neBot.2 ‹_›

Premises used: Iff.mpr, Filter.frequently_iff_neBot
-- Module: Mathlib.Topology.Order.LeftRight
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : Preorder α
a : α
inst_2 : (𝓝[<] a).NeBot
p : α → Prop
h : ∀ᶠ (x : α) in 𝓝 a, p x
⊢ ∃ b < a, p b

Tactic:
((frequently_lt_nhds a).and_eventually h).exists

Premises used: frequently_lt_nhds, Filter.Frequently.and_eventually, Filter.Frequently.exists
-- Module: Mathlib.Topology.Order.LeftRight
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : Preorder α
a b : α
H₂ : a ≤ b
⊢ (𝓝[Ici a] b).NeBot

Tactic:
nhdsWithin_neBot_of_mem H₂

Premises used: nhdsWithin_neBot_of_mem
-- Module: Mathlib.Topology.Order.LeftRight
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : Preorder α
a : α
⊢ (𝓝[≤] a).NeBot

Tactic:
nhdsWithin_Iic_neBot (le_refl a)

Premises used: le_refl, nhdsWithin_Iic_neBot
-- Module: Mathlib.Topology.Order.LeftRight
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : Preorder α
a : α
⊢ 𝓝[<] a ≤ 𝓝[≠] a

Tactic:
nhdsWithin_mono a fun _ => ne_of_lt

Premises used: ne_of_lt, nhdsWithin_mono
-- Module: Mathlib.Topology.Order.LeftRight
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : Preorder α
inst_2 : ∀ (x : α), (𝓝[<] x).NeBot
s : Set α
hs : IsAntichain (fun (x1 x2 : α) ↦ x1 ≤ x2) s
⊢ interior s = ∅

Tactic:
eq_empty_of_forall_notMem fun x hx ↦ ?_

Premises used: Set.eq_empty_of_forall_notMem
-- Module: Mathlib.Topology.Order.LeftRight
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : Preorder α
inst_2 : ∀ (x : α), (𝓝[<] x).NeBot
s : Set α
hs : IsAntichain (fun (x1 x2 : α) ↦ x1 ≤ x2) s
refine : ∀ (x : α) (hx : x ∈ interior s), False
⊢ interior s = ∅

Tactic:
refine eq_empty_of_forall_notMem fun x hx ↦ ?_

Premises used: Set.eq_empty_of_forall_notMem
-- Module: Mathlib.Topology.Order.LeftRight
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : Preorder α
inst_2 : ∀ (x : α), (𝓝[<] x).NeBot
s : Set α
hs : IsAntichain (fun (x1 x2 : α) ↦ x1 ≤ x2) s
x : α
hx : x ∈ interior s
⊢ ∀ᶠ (y : α) in 𝓝 x, y ∈ s

Tactic:
have : ∀ᶠ y in 𝓝 x, y ∈ s := mem_interior_iff_mem_nhds.1 hx
-- Module: Mathlib.Topology.Order.LeftRight
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : Preorder α
inst_2 : ∀ (x : α), (𝓝[<] x).NeBot
s : Set α
hs : IsAntichain (fun (x1 x2 : α) ↦ x1 ≤ x2) s
x : α
hx : x ∈ interior s
this : ∀ᶠ (y : α) in 𝓝 x, y ∈ s
rcases : ∀ (y : α) (hyx : y < x) (hys : y ∈ s), False
⊢ False

Tactic:
rcases this.exists_lt with ⟨y, hyx, hys⟩

Premises used: Filter.Eventually.exists_lt
-- Module: Mathlib.Topology.Order.LeftRight
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : Preorder α
inst_2 : ∀ (x : α), (𝓝[<] x).NeBot
s : Set α
hs : IsAntichain (fun (x1 x2 : α) ↦ x1 ≤ x2) s
x : α
hx : x ∈ interior s
this : ∀ᶠ (y : α) in 𝓝 x, y ∈ s
y : α
hyx : y < x
hys : y ∈ s
⊢ False

Tactic:
hs hys (interior_subset hx) hyx.ne hyx.le

Premises used: interior_subset, LT.lt.le, LT.lt.ne
-- Module: Mathlib.Topology.Order.LeftRight
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : Preorder α
inst_2 : ∀ (x : α), (𝓝[<] x).NeBot
s : Set α
hs : IsAntichain (fun (x1 x2 : α) ↦ x1 ≤ x2) s
x : α
hx : x ∈ interior s
this : ∀ᶠ (y : α) in 𝓝 x, y ∈ s
y : α
hyx : y < x
hys : y ∈ s
⊢ False

Tactic:
exact hs hys (interior_subset hx) hyx.ne hyx.le

Premises used: interior_subset, LT.lt.le, LT.lt.ne
-- Module: Mathlib.Topology.Order.LeftRight
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : Preorder α
inst_2 : ∀ (x : α), (𝓝[>] x).NeBot
s : Set α
hs : IsAntichain (fun (x1 x2 : α) ↦ x1 ≤ x2) s
⊢ interior s = ∅

Tactic:
have : ∀ x : αᵒᵈ, NeBot (𝓝[<] x) := ‹_›
  hs.to_dual.interior_eq_empty

Premises used: IsAntichain.interior_eq_empty, IsAntichain.to_dual, OrderDual
-- Module: Mathlib.Topology.Order.LeftRight
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : PartialOrder α
inst_2 : TopologicalSpace β
a : α
f : α → β
⊢ ContinuousWithinAt f (Ioi a) a ↔ ContinuousWithinAt f (Ici a) a

Tactic:
simp only [← Ici_diff_left, continuousWithinAt_diff_self]

Premises used: continuousWithinAt_diff_self, Set.Ici_diff_left
-- Module: Mathlib.Topology.Order.LeftRight
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : PartialOrder α
inst_2 : TopologicalSpace β
a : α
f : α → β
s : Set α
⊢ ContinuousWithinAt f (s ∩ Ioi a) a ↔ ContinuousWithinAt f (s ∩ Ici a) a

Tactic:
simp [← Ici_diff_left, ← inter_diff_assoc, continuousWithinAt_diff_self]

Premises used: continuousWithinAt_diff_self, Set.inter_diff_assoc, Set.Ici_diff_left