awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.OpenPartialHomeomorph.IsImage
Goal:
X : Type u_1
Y : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
e : OpenPartialHomeomorph X Y
s : Set X
hs : IsOpen[inst] s
rw : e.restr (interior s) = e.restr s
rw₁ rw₂ : e.restr s = e.restr s
⊢ (e.restr s).toPartialEquiv = e.restr s

Tactic:
rw [e.restr_toPartialEquiv, hs.interior_eq]

Premises used: OpenPartialHomeomorph.restr_toPartialEquiv, IsOpen.interior_eq
-- Module: Mathlib.Topology.OpenPartialHomeomorph.IsImage
Goal:
X : Type u_1
Y : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
e : OpenPartialHomeomorph X Y
s : Set X
h : e.source ⊆ s
⊢ e.restr s = e

Tactic:
toPartialEquiv_injective <| PartialEquiv.restr_eq_of_source_subset <|
    interior_maximal h e.open_source

Premises used: PartialEquiv.restr_eq_of_source_subset, OpenPartialHomeomorph.open_source, interior_maximal, OpenPartialHomeomorph.toPartialEquiv_injective
-- Module: Mathlib.Topology.OpenPartialHomeomorph.IsImage
Goal:
X : Type u_1
Y : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
e : OpenPartialHomeomorph X Y
⊢ e.restr univ = e

Tactic:
restr_eq_of_source_subset (subset_univ _)

Premises used: Set.subset_univ, OpenPartialHomeomorph.restr_eq_of_source_subset
-- Module: Mathlib.Topology.OpenPartialHomeomorph.IsImage
Goal:
X : Type u_1
Y : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
e : OpenPartialHomeomorph X Y
s : Set X
⊢ e.restr (e.source ∩ s) = e.restr s

Tactic:
OpenPartialHomeomorph.ext _ _ (fun x => rfl) (fun x => rfl) ?_

Premises used: OpenPartialHomeomorph.ext, rfl
-- Module: Mathlib.Topology.OpenPartialHomeomorph.IsImage
Goal:
X : Type u_1
Y : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
e : OpenPartialHomeomorph X Y
s : Set X
refine : (e.restr (e.source ∩ s)).source = (e.restr s).source
⊢ e.restr (e.source ∩ s) = e.restr s

Tactic:
refine OpenPartialHomeomorph.ext _ _ (fun x => rfl) (fun x => rfl) ?_

Premises used: OpenPartialHomeomorph.ext, rfl
-- Module: Mathlib.Topology.OpenPartialHomeomorph.IsImage
Goal:
X : Type u_1
Y : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
e : OpenPartialHomeomorph X Y
s : Set X
⊢ (e.restr (e.source ∩ s)).source = (e.restr s).source

Tactic:
simp [e.open_source.interior_eq, ← inter_assoc]

Premises used: OpenPartialHomeomorph.open_source, IsOpen.interior_eq, Set.inter_assoc
-- Module: Mathlib.Topology.OpenPartialHomeomorph.IsImage
Goal:
X : Type u_1
inst : TopologicalSpace X
s : Set X
hs : IsOpen[inst] s
⊢ (ofSet s hs).toPartialEquiv = PartialEquiv.ofSet s

Tactic:
rfl

Premises used: PartialEquiv.ofSet, rfl
-- Module: Mathlib.Topology.OpenPartialHomeomorph.IsImage
Goal:
X : Type u_1
inst : TopologicalSpace X
s : Set X
hs : IsOpen[inst] s
⊢ (ofSet s hs).symm = ofSet s hs

Tactic:
rfl

Premises used: OpenPartialHomeomorph.ofSet, PartialEquiv.ofSet, PartialEquiv.symm, rfl, OpenPartialHomeomorph.symm
-- Module: Mathlib.Topology.OpenPartialHomeomorph.IsImage
Goal:
X : Type u_1
inst : TopologicalSpace X
h : ∀ (x : X), (↑(ofSet univ ⋯) : X → X) x = (↑(OpenPartialHomeomorph.refl X) : X → X) x
hinv :
  ∀ (x : X),
    (↑(OpenPartialHomeomorph.symm (ofSet univ ⋯)) : X → X) x =
      (↑(OpenPartialHomeomorph.symm (OpenPartialHomeomorph.refl X)) : X → X) x
hs :
  ∀ (x : X),
    Membership.mem (γ := Set X) (PartialEquiv.source (toPartialEquiv (ofSet univ ⋯))) x ↔
      x ∈ (toPartialEquiv (OpenPartialHomeomorph.refl X)).source
⊢ Eq (α := OpenPartialHomeomorph X X) (ofSet univ ⋯) (OpenPartialHomeomorph.refl X)

Tactic:
ext
-- Module: Mathlib.Topology.OpenPartialHomeomorph.IsImage
Goal:
X : Type u_1
inst : TopologicalSpace X
x : X
⊢ (↑(ofSet univ ⋯) : X → X) x = (↑(OpenPartialHomeomorph.refl X) : X → X) x

Tactic:
simp
-- Module: Mathlib.Topology.OpenPartialHomeomorph.IsImage
Goal:
X : Type u_1
inst : TopologicalSpace X
x : X
⊢ (↑(OpenPartialHomeomorph.symm (ofSet univ ⋯)) : X → X) x =
    (↑(OpenPartialHomeomorph.symm (OpenPartialHomeomorph.refl X)) : X → X) x

Tactic:
simp
-- Module: Mathlib.Topology.OpenPartialHomeomorph.IsImage
Goal:
X : Type u_1
inst : TopologicalSpace X
x : X
⊢ Membership.mem (γ := Set X) (PartialEquiv.source (toPartialEquiv (ofSet univ ⋯))) x ↔
    x ∈ (toPartialEquiv (OpenPartialHomeomorph.refl X)).source

Tactic:
simp
-- Module: Mathlib.Topology.OpenPartialHomeomorph.IsImage
Goal:
X : Type u_1
Y : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
e e' : OpenPartialHomeomorph X Y
⊢ e.EqOnSource e' ↔ e.EqOnSource e'.toPartialEquiv

Tactic:
Iff.rfl

Premises used: Iff.rfl, OpenPartialHomeomorph.toFun', PartialEquiv.EqOnSource
-- Module: Mathlib.Topology.OpenPartialHomeomorph.IsImage
Goal:
X : Type u_1
Y : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
e : OpenPartialHomeomorph X Y
⊢ e ≈ e

Tactic:
Setoid.refl _

Premises used: Setoid.refl
-- Module: Mathlib.Topology.OpenPartialHomeomorph.IsImage
Goal:
X : Type u_1
Y : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
e e' : OpenPartialHomeomorph X Y
h : e ≈ e'
⊢ e.symm ≈ e'.symm

Tactic:
PartialEquiv.EqOnSource.symm' h

Premises used: OpenPartialHomeomorph.toFun', OpenPartialHomeomorph.EqOnSource, PartialEquiv.EqOnSource.symm'
-- Module: Mathlib.Topology.OpenPartialHomeomorph.IsImage
Goal:
X : Type u_1
Y : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
e e' : OpenPartialHomeomorph X Y
h : e ≈ e'
⊢ e.source = e'.source

Tactic:
h.1

Premises used: And.left
-- Module: Mathlib.Topology.OpenPartialHomeomorph.IsImage
Goal:
X : Type u_1
Y : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
e e' : OpenPartialHomeomorph X Y
h : e ≈ e'
⊢ e.target = e'.target

Tactic:
h.symm'.1

Premises used: And.left, OpenPartialHomeomorph.EqOnSource.symm'
-- Module: Mathlib.Topology.OpenPartialHomeomorph.IsImage
Goal:
X : Type u_1
Y : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
e e' : OpenPartialHomeomorph X Y
h : e ≈ e'
⊢ EqOn (↑e : X → Y) (↑e' : X → Y) e.source

Tactic:
h.2

Premises used: And.right
-- Module: Mathlib.Topology.OpenPartialHomeomorph.IsImage
Goal:
X : Type u_1
Y : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
e e' : OpenPartialHomeomorph X Y
h : e ≈ e'
⊢ EqOn (↑e.symm : Y → X) (↑e'.symm : Y → X) e.target

Tactic:
h.symm'.2

Premises used: And.right, OpenPartialHomeomorph.EqOnSource.symm'
-- Module: Mathlib.Topology.OpenPartialHomeomorph.IsImage
Goal:
X : Type u_1
Y : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
e e' : OpenPartialHomeomorph X Y
he : e ≈ e'
s : Set X
⊢ e.restr s ≈ e'.restr s

Tactic:
PartialEquiv.EqOnSource.restr he _

Premises used: PartialEquiv.EqOnSource.restr, OpenPartialHomeomorph.toFun', OpenPartialHomeomorph.EqOnSource
-- Module: Mathlib.Topology.OpenPartialHomeomorph.IsImage
Goal:
X : Type u_1
Y : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
e e' : OpenPartialHomeomorph X Y
h : EqOn (↑e : X → Y) (↑e' : X → Y) (e.source ∩ e'.source)
left : (e.restr e'.source).source = (e'.restr e.source).source
right : EqOn (↑(e.restr e'.source) : X → Y) (↑(e'.restr e.source) : X → Y) (e.restr e'.source).source
⊢ e.restr e'.source ≈ e'.restr e.source

Tactic:
constructor
-- Module: Mathlib.Topology.OpenPartialHomeomorph.IsImage
Goal:
X : Type u_1
Y : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
e e' : OpenPartialHomeomorph X Y
h : EqOn (↑e : X → Y) (↑e' : X → Y) (e.source ∩ e'.source)
left : (e.restr e'.source).source = e'.source ∩ e.source
⊢ (e.restr e'.source).source = (e'.restr e.source).source

Tactic:
rw [e'.restr_source' _ e.open_source]

Premises used: OpenPartialHomeomorph.open_source, OpenPartialHomeomorph.restr_source'
-- Module: Mathlib.Topology.OpenPartialHomeomorph.IsImage
Goal:
X : Type u_1
Y : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
e e' : OpenPartialHomeomorph X Y
h : EqOn (↑e : X → Y) (↑e' : X → Y) (e.source ∩ e'.source)
left : e.source ∩ e'.source = e'.source ∩ e.source
⊢ (e.restr e'.source).source = e'.source ∩ e.source

Tactic:
rw [e.restr_source' _ e'.open_source]

Premises used: OpenPartialHomeomorph.open_source, OpenPartialHomeomorph.restr_source'
-- Module: Mathlib.Topology.OpenPartialHomeomorph.IsImage
Goal:
X : Type u_1
Y : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
e e' : OpenPartialHomeomorph X Y
h : EqOn (↑e : X → Y) (↑e' : X → Y) (e.source ∩ e'.source)
⊢ e.source ∩ e'.source = e'.source ∩ e.source

Tactic:
Set.inter_comm _ _

Premises used: Set.inter_comm
-- Module: Mathlib.Topology.OpenPartialHomeomorph.IsImage
Goal:
X : Type u_1
Y : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
e e' : OpenPartialHomeomorph X Y
h : EqOn (↑e : X → Y) (↑e' : X → Y) (e.source ∩ e'.source)
⊢ e.source ∩ e'.source = e'.source ∩ e.source

Tactic:
exact Set.inter_comm _ _

Premises used: Set.inter_comm
-- Module: Mathlib.Topology.OpenPartialHomeomorph.IsImage
Goal:
X : Type u_1
Y : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
e e' : OpenPartialHomeomorph X Y
h : EqOn (↑e : X → Y) (↑e' : X → Y) (e.source ∩ e'.source)
right : EqOn (↑(e.restr e'.source) : X → Y) (↑(e'.restr e.source) : X → Y) (e.source ∩ e'.source)
⊢ EqOn (↑(e.restr e'.source) : X → Y) (↑(e'.restr e.source) : X → Y) (e.restr e'.source).source

Tactic:
rw [e.restr_source' _ e'.open_source]

Premises used: OpenPartialHomeomorph.open_source, OpenPartialHomeomorph.restr_source'
-- Module: Mathlib.Topology.OpenPartialHomeomorph.IsImage
Goal:
X : Type u_1
Y : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
e e' : OpenPartialHomeomorph X Y
h : EqOn (↑e : X → Y) (↑e' : X → Y) (e.source ∩ e'.source)
⊢ EqOn (↑(e.restr e'.source) : X → Y) (↑(e'.restr e.source) : X → Y) (e.source ∩ e'.source)

Tactic:
(EqOn.trans ?_ h).trans ?_

Premises used: Set.EqOn.trans
-- Module: Mathlib.Topology.OpenPartialHomeomorph.IsImage
Goal:
X : Type u_1
Y : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
e e' : OpenPartialHomeomorph X Y
h : EqOn (↑e : X → Y) (↑e' : X → Y) (e.source ∩ e'.source)
right : EqOn (↑(e.restr e'.source) : X → Y) (↑e : X → Y) (e.source ∩ e'.source)
right₁ : EqOn (↑e' : X → Y) (↑(e'.restr e.source) : X → Y) (e.source ∩ e'.source)
⊢ EqOn (↑(e.restr e'.source) : X → Y) (↑(e'.restr e.source) : X → Y) (e.source ∩ e'.source)

Tactic:
refine (EqOn.trans ?_ h).trans ?_

Premises used: Set.EqOn.trans
-- Module: Mathlib.Topology.OpenPartialHomeomorph.IsImage
Goal:
X : Type u_1
Y : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
e e' : OpenPartialHomeomorph X Y
h : EqOn (↑e : X → Y) (↑e' : X → Y) (e.source ∩ e'.source)
⊢ EqOn (↑(e.restr e'.source) : X → Y) (↑e : X → Y) (e.source ∩ e'.source)

Tactic:
simp only [mfld_simps, eqOn_refl]

Premises used: Set.eqOn_refl
-- Module: Mathlib.Topology.OpenPartialHomeomorph.IsImage
Goal:
X : Type u_1
Y : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
e e' : OpenPartialHomeomorph X Y
h : EqOn (↑e : X → Y) (↑e' : X → Y) (e.source ∩ e'.source)
⊢ EqOn (↑e' : X → Y) (↑(e'.restr e.source) : X → Y) (e.source ∩ e'.source)

Tactic:
simp only [mfld_simps, eqOn_refl]

Premises used: Set.eqOn_refl
-- Module: Mathlib.Topology.OpenPartialHomeomorph.IsImage
Goal:
X : Type u_1
Y : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
e e' : OpenPartialHomeomorph X Y
h : e ≈ e'
s : e.source = univ
t : e.target = univ
⊢ e = e'

Tactic:
toPartialEquiv_injective <| PartialEquiv.eq_of_eqOnSource_univ _ _ h s t

Premises used: OpenPartialHomeomorph.toPartialEquiv_injective, PartialEquiv.eq_of_eqOnSource_univ
-- Module: Mathlib.Topology.OpenPartialHomeomorph.IsImage
Goal:
X : Type u_1
Y : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
e : OpenPartialHomeomorph X Y
s s' : Set X
hss' : e.source ∩ interior s = e.source ∩ interior s'
left : (e.restr s).source = (e.restr s').source
right : EqOn (↑(e.restr s) : X → Y) (↑(e.restr s') : X → Y) (e.restr s).source
⊢ e.restr s ≈ e.restr s'

Tactic:
constructor
-- Module: Mathlib.Topology.OpenPartialHomeomorph.IsImage
Goal:
X : Type u_1
Y : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
e : OpenPartialHomeomorph X Y
s s' : Set X
hss' : e.source ∩ interior s = e.source ∩ interior s'
⊢ (e.restr s).source = (e.restr s').source

Tactic:
simpa [e.restr_source]

Premises used: OpenPartialHomeomorph.restr_source
-- Module: Mathlib.Topology.OpenPartialHomeomorph.IsImage
Goal:
X : Type u_1
Y : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
e : OpenPartialHomeomorph X Y
s s' : Set X
hss' : e.source ∩ interior s = e.source ∩ interior s'
⊢ EqOn (↑(e.restr s) : X → Y) (↑(e.restr s') : X → Y) (e.restr s).source

Tactic:
simp [Set.eqOn_refl]

Premises used: Set.eqOn_refl
-- Module: Mathlib.Topology.OpenPartialHomeomorph.IsImage
Goal:
X : Type u_1
Y : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
e : OpenPartialHomeomorph X Y
s : Set X
⊢ e.source ∩ interior (e.source ∩ s) = e.source ∩ interior s

Tactic:
simp [interior_eq_iff_isOpen.mpr e.open_source]

Premises used: Iff.mpr, OpenPartialHomeomorph.open_source, interior_eq_iff_isOpen
-- Module: Mathlib.Topology.OpenPartialHomeomorph.IsImage
Goal:
X : Type u_1
inst : TopologicalSpace X
⊢ Eq (α := OpenPartialHomeomorph X X) (toOpenPartialHomeomorph (Homeomorph.refl X)) (OpenPartialHomeomorph.refl X)

Tactic:
rfl

Premises used: rfl, OpenPartialHomeomorph.refl
-- Module: Mathlib.Topology.OpenPartialHomeomorph.IsImage
Goal:
X : Type u_1
Y : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
e : X ≃ₜ Y
⊢ e.symm.toOpenPartialHomeomorph = e.toOpenPartialHomeomorph.symm

Tactic:
rfl

Premises used: Equiv.toPartialEquivOfImageEq, Homeomorph.toOpenPartialHomeomorphOfImageEq, Set.univ, setOf, PartialEquiv.symm, rfl, OpenPartialHomeomorph.symm, Homeomorph.toOpenPartialHomeomorph
-- Module: Mathlib.Topology.Order.AtTopBotIxx
Goal:
X : Type u_1
inst : LinearOrder X
inst_1 : TopologicalSpace X
inst_2 : OrderTopology X
s : Set X
b : X
inl :
  Eq (α := Filter { x : X // Membership.mem (γ := Set X) ∅ x })
      (comap (Subtype.val (p := fun (x : X) ↦ Membership.mem (γ := Set X) ∅ x)) (𝓝[<] b)) atTop ↔
    ∅ ⊆ Iio b ∧ (Set.Nonempty.{u_1} (α := X) ∅ → ∀ a < b, (∅ ∩ Ioo a b).Nonempty)
inr :
  ∀ (hsne : s.Nonempty),
    Eq (α := Filter { x : X // x ∈ s }) (comap (Subtype.val (p := fun (x : X) ↦ x ∈ s)) (𝓝[<] b)) atTop ↔
      s ⊆ Iio b ∧ (s.Nonempty → ∀ a < b, (s ∩ Ioo a b).Nonempty)
⊢ Eq (α := Filter { x : X // x ∈ s }) (comap (Subtype.val (p := fun (x : X) ↦ x ∈ s)) (𝓝[<] b)) atTop ↔
    s ⊆ Iio b ∧ (s.Nonempty → ∀ a < b, (s ∩ Ioo a b).Nonempty)

Tactic:
rcases s.eq_empty_or_nonempty with rfl | hsne

Premises used: Set.eq_empty_or_nonempty, rfl
-- Module: Mathlib.Topology.Order.AtTopBotIxx
Goal:
X : Type u_1
inst : LinearOrder X
inst_1 : TopologicalSpace X
inst_2 : OrderTopology X
b : X
⊢ Eq (α := Filter { x : X // Membership.mem (γ := Set X) ∅ x })
      (comap (Subtype.val (p := fun (x : X) ↦ Membership.mem (γ := Set X) ∅ x)) (𝓝[<] b)) atTop ↔
    ∅ ⊆ Iio b ∧ (Set.Nonempty.{u_1} (α := X) ∅ → ∀ a < b, (∅ ∩ Ioo a b).Nonempty)

Tactic:
simp [eq_iff_true_of_subsingleton]

Premises used: eq_iff_true_of_subsingleton
-- Module: Mathlib.Topology.Order.AtTopBotIxx
Goal:
X : Type u_1
inst : LinearOrder X
inst_1 : TopologicalSpace X
inst_2 : OrderTopology X
s : Set X
b : X
hsne : s.Nonempty
⊢ Nonempty.{u_1 + 1} (↑s : Type u_1)

Tactic:
have := hsne.to_subtype
-- Module: Mathlib.Topology.Order.AtTopBotIxx
Goal:
X : Type u_1
inst : LinearOrder X
inst_1 : TopologicalSpace X
inst_2 : OrderTopology X
s : Set X
b : X
hsne : s.Nonempty
this : Nonempty.{u_1 + 1} (↑s : Type u_1)
inr :
  Eq (α := Filter { x : X // x ∈ s }) (comap (Subtype.val (p := fun (x : X) ↦ x ∈ s)) (𝓝[<] b)) atTop ↔
    s ⊆ Iio b ∧ ∀ a < b, (s ∩ Ioo a b).Nonempty
⊢ Eq (α := Filter { x : X // x ∈ s }) (comap (Subtype.val (p := fun (x : X) ↦ x ∈ s)) (𝓝[<] b)) atTop ↔
    s ⊆ Iio b ∧ (s.Nonempty → ∀ a < b, (s ∩ Ioo a b).Nonempty)

Tactic:
simp only [hsne, true_imp_iff]

Premises used: true_imp_iff
-- Module: Mathlib.Topology.Order.AtTopBotIxx
Goal:
X : Type u_1
inst : LinearOrder X
inst_1 : TopologicalSpace X
inst_2 : OrderTopology X
s : Set X
b : X
hsne : s.Nonempty
this : Nonempty.{u_1 + 1} (↑s : Type u_1)
pos :
  ∀ (hsub : s ⊆ Iio b),
    Eq (α := Filter { x : X // x ∈ s }) (comap (Subtype.val (p := fun (x : X) ↦ x ∈ s)) (𝓝[<] b)) atTop ↔
      s ⊆ Iio b ∧ ∀ a < b, (s ∩ Ioo a b).Nonempty
neg :
  ∀ (hsub : ¬s ⊆ Iio b),
    Eq (α := Filter { x : X // x ∈ s }) (comap (Subtype.val (p := fun (x : X) ↦ x ∈ s)) (𝓝[<] b)) atTop ↔
      s ⊆ Iio b ∧ ∀ a < b, (s ∩ Ioo a b).Nonempty
⊢ Eq (α := Filter { x : X // x ∈ s }) (comap (Subtype.val (p := fun (x : X) ↦ x ∈ s)) (𝓝[<] b)) atTop ↔
    s ⊆ Iio b ∧ ∀ a < b, (s ∩ Ioo a b).Nonempty

Tactic:
by_cases hsub : s ⊆ Iio b

Premises used: Set.Iio
-- Module: Mathlib.Topology.Order.AtTopBotIxx
Goal:
X : Type u_1
inst : LinearOrder X
inst_1 : TopologicalSpace X
inst_2 : OrderTopology X
s : Set X
b : X
hsne : s.Nonempty
this : Nonempty.{u_1 + 1} (↑s : Type u_1)
hsub : s ⊆ Iio b
pos :
  Eq (α := Filter { x : X // x ∈ s }) (comap (Subtype.val (p := fun (x : X) ↦ x ∈ s)) (𝓝[<] b)) atTop ↔
    ∀ a < b, (s ∩ Ioo a b).Nonempty
⊢ Eq (α := Filter { x : X // x ∈ s }) (comap (Subtype.val (p := fun (x : X) ↦ x ∈ s)) (𝓝[<] b)) atTop ↔
    s ⊆ Iio b ∧ ∀ a < b, (s ∩ Ioo a b).Nonempty

Tactic:
simp only [hsub, true_and]

Premises used: true_and
-- Module: Mathlib.Topology.Order.AtTopBotIxx
Goal:
X : Type u_1
inst : LinearOrder X
inst_1 : TopologicalSpace X
inst_2 : OrderTopology X
s : Set X
b : X
hsne : s.Nonempty
this : Nonempty.{u_1 + 1} (↑s : Type u_1)
hsub : s ⊆ Iio b
pos :
  Eq (α := Filter { x : X // x ∈ s }) (comap (Subtype.val (p := fun (x : X) ↦ x ∈ s)) (𝓝[<] b)) atTop →
    ∀ a < b, (s ∩ Ioo a b).Nonempty
pos₁ :
  (∀ a < b, (s ∩ Ioo a b).Nonempty) →
    Eq (α := Filter { x : X // x ∈ s }) (comap (Subtype.val (p := fun (x : X) ↦ x ∈ s)) (𝓝[<] b)) atTop
⊢ Eq (α := Filter { x : X // x ∈ s }) (comap (Subtype.val (p := fun (x : X) ↦ x ∈ s)) (𝓝[<] b)) atTop ↔
    ∀ a < b, (s ∩ Ioo a b).Nonempty

Tactic:
constructor
-- Module: Mathlib.Topology.Order.AtTopBotIxx
Goal:
X : Type u_1
inst : LinearOrder X
inst_1 : TopologicalSpace X
inst_2 : OrderTopology X
s : Set X
b : X
hsne : s.Nonempty
this : Nonempty.{u_1 + 1} (↑s : Type u_1)
hsub : s ⊆ Iio b
h : Eq (α := Filter { x : X // x ∈ s }) (comap (Subtype.val (p := fun (x : X) ↦ x ∈ s)) (𝓝[<] b)) atTop
a : X
ha : a < b
⊢ Membership.mem (γ := Filter { x : X // x ∈ s }) (comap (Subtype.val (p := fun (x : X) ↦ x ∈ s)) (𝓝[<] b))
    (Subtype.val (p := fun (x : X) ↦ x ∈ s) ⁻¹' Ioo a b)

Tactic:
have := preimage_mem_comap (m := ((↑) : s → X)) (Ioo_mem_nhdsLT ha)
-- Module: Mathlib.Topology.Order.AtTopBotIxx
Goal:
X : Type u_1
inst : LinearOrder X
inst_1 : TopologicalSpace X
inst_2 : OrderTopology X
s : Set X
b : X
hsne : s.Nonempty
this_1 : Nonempty.{u_1 + 1} (↑s : Type u_1)
hsub : s ⊆ Iio b
h : Eq (α := Filter { x : X // x ∈ s }) (comap (Subtype.val (p := fun (x : X) ↦ x ∈ s)) (𝓝[<] b)) atTop
a : X
ha : a < b
this :
  Membership.mem (γ := Filter { x : X // x ∈ s }) (comap (Subtype.val (p := fun (x : X) ↦ x ∈ s)) (𝓝[<] b))
    (Subtype.val (p := fun (x : X) ↦ x ∈ s) ⁻¹' Ioo a b)
⊢ Membership.mem (γ := Filter { x : X // x ∈ s }) atTop (Subtype.val (p := fun (x : X) ↦ x ∈ s) ⁻¹' Ioo a b)

Tactic:
rw [h] at this
-- Module: Mathlib.Topology.Order.AtTopBotIxx
Goal:
X : Type u_1
inst : LinearOrder X
inst_1 : TopologicalSpace X
inst_2 : OrderTopology X
s : Set X
b : X
hsne : s.Nonempty
this_1 : Nonempty.{u_1 + 1} (↑s : Type u_1)
hsub : s ⊆ Iio b
h : Eq (α := Filter { x : X // x ∈ s }) (comap (Subtype.val (p := fun (x : X) ↦ x ∈ s)) (𝓝[<] b)) atTop
a : X
ha : a < b
this : Membership.mem (γ := Filter { x : X // x ∈ s }) atTop (Subtype.val (p := fun (x : X) ↦ x ∈ s) ⁻¹' Ioo a b)
pos :
  ∀ (c : X) (hcs : c ∈ s)
    (hc :
      Membership.mem (γ := Set { x : X // x ∈ s }) (Subtype.val (p := fun (x : X) ↦ x ∈ s) ⁻¹' Ioo a b)
        (Subtype.mk (p := fun (x : X) ↦ x ∈ s) c hcs)),
    (s ∩ Ioo a b).Nonempty
⊢ (s ∩ Ioo a b).Nonempty

Tactic:
rcases Filter.nonempty_of_mem this with ⟨⟨c, hcs⟩, hc⟩

Premises used: Filter.nonempty_of_mem
-- Module: Mathlib.Topology.Order.AtTopBotIxx
Goal:
X : Type u_1
inst : LinearOrder X
inst_1 : TopologicalSpace X
inst_2 : OrderTopology X
s : Set X
b : X
hsne : s.Nonempty
this_1 : Nonempty.{u_1 + 1} (↑s : Type u_1)
hsub : s ⊆ Iio b
h : Eq (α := Filter { x : X // x ∈ s }) (comap (Subtype.val (p := fun (x : X) ↦ x ∈ s)) (𝓝[<] b)) atTop
a : X
ha : a < b
this : Membership.mem (γ := Filter { x : X // x ∈ s }) atTop (Subtype.val (p := fun (x : X) ↦ x ∈ s) ⁻¹' Ioo a b)
c : X
hcs : c ∈ s
hc :
  Membership.mem (γ := Set { x : X // x ∈ s }) (Subtype.val (p := fun (x : X) ↦ x ∈ s) ⁻¹' Ioo a b)
    (Subtype.mk (p := fun (x : X) ↦ x ∈ s) c hcs)
⊢ (s ∩ Ioo a b).Nonempty

Tactic:
⟨c, hcs, hc⟩

Premises used: Set.Nonempty, And.intro, Exists.intro
-- Module: Mathlib.Topology.Order.AtTopBotIxx
Goal:
X : Type u_1
inst : LinearOrder X
inst_1 : TopologicalSpace X
inst_2 : OrderTopology X
s : Set X
b : X
hsne : s.Nonempty
this_1 : Nonempty.{u_1 + 1} (↑s : Type u_1)
hsub : s ⊆ Iio b
h : Eq (α := Filter { x : X // x ∈ s }) (comap (Subtype.val (p := fun (x : X) ↦ x ∈ s)) (𝓝[<] b)) atTop
a : X
ha : a < b
this : Membership.mem (γ := Filter { x : X // x ∈ s }) atTop (Subtype.val (p := fun (x : X) ↦ x ∈ s) ⁻¹' Ioo a b)
c : X
hcs : c ∈ s
hc :
  Membership.mem (γ := Set { x : X // x ∈ s }) (Subtype.val (p := fun (x : X) ↦ x ∈ s) ⁻¹' Ioo a b)
    (Subtype.mk (p := fun (x : X) ↦ x ∈ s) c hcs)
⊢ (s ∩ Ioo a b).Nonempty

Tactic:
exact ⟨c, hcs, hc⟩
-- Module: Mathlib.Topology.Order.AtTopBotIxx
Goal:
X : Type u_1
inst : LinearOrder X
inst_1 : TopologicalSpace X
inst_2 : OrderTopology X
s : Set X
b : X
hsne : s.Nonempty
this : Nonempty.{u_1 + 1} (↑s : Type u_1)
hsub : s ⊆ Iio b
h : ∀ a < b, (s ∩ Ioo a b).Nonempty
⊢ Eq (α := Filter { x : X // x ∈ s }) (comap (Subtype.val (p := fun (x : X) ↦ x ∈ s)) (𝓝[<] b)) atTop

Tactic:
(nhdsLT_basis_of_exists_lt (hsne.mono hsub)).comap _ |>.ext atTop_basis ?_ ?_

Premises used: Filter.atTop_basis, nhdsLT_basis_of_exists_lt, Set.Nonempty.mono, Filter.HasBasis.comap, Filter.HasBasis.ext
-- Module: Mathlib.Topology.Order.AtTopBotIxx
Goal:
X : Type u_1
inst : LinearOrder X
inst_1 : TopologicalSpace X
inst_2 : OrderTopology X
s : Set X
b : X
hsne : s.Nonempty
this : Nonempty.{u_1 + 1} (↑s : Type u_1)
hsub : s ⊆ Iio b
h : ∀ a < b, (s ∩ Ioo a b).Nonempty
pos : ∀ i < b, ∃ (i' : { x : X // x ∈ s }), True ∧ Ici i' ⊆ Subtype.val (p := fun (x : X) ↦ x ∈ s) ⁻¹' Ioo i b
pos₁ : ∀ (i' : { x : X // x ∈ s }), True → ∃ i < b, Subtype.val (p := fun (x : X) ↦ x ∈ s) ⁻¹' Ioo i b ⊆ Ici i'
⊢ Eq (α := Filter { x : X // x ∈ s }) (comap (Subtype.val (p := fun (x : X) ↦ x ∈ s)) (𝓝[<] b)) atTop

Tactic:
refine (nhdsLT_basis_of_exists_lt (hsne.mono hsub)).comap _ |>.ext atTop_basis ?_ ?_

Premises used: Filter.atTop_basis, nhdsLT_basis_of_exists_lt, Set.Nonempty.mono, Filter.HasBasis.comap, Filter.HasBasis.ext
-- Module: Mathlib.Topology.Order.AtTopBotIxx
Goal:
X : Type u_1
inst : LinearOrder X
inst_1 : TopologicalSpace X
inst_2 : OrderTopology X
s : Set X
b : X
hsne : s.Nonempty
this : Nonempty.{u_1 + 1} (↑s : Type u_1)
hsub : s ⊆ Iio b
h : ∀ a < b, (s ∩ Ioo a b).Nonempty
a : X
hab : a < b
pos :
  ∀ (c : X) (hcs : c ∈ s) (hc : c ∈ Ioo a b),
    ∃ (i' : { x : X // x ∈ s }), True ∧ Ici i' ⊆ Subtype.val (p := fun (x : X) ↦ x ∈ s) ⁻¹' Ioo a b
⊢ ∃ (i' : { x : X // x ∈ s }), True ∧ Ici i' ⊆ Subtype.val (p := fun (x : X) ↦ x ∈ s) ⁻¹' Ioo a b

Tactic:
rcases h a hab with ⟨c, hcs, hc⟩
-- Module: Mathlib.Topology.Order.AtTopBotIxx
Goal:
X : Type u_1
inst : LinearOrder X
inst_1 : TopologicalSpace X
inst_2 : OrderTopology X
s : Set X
b : X
hsne : s.Nonempty
this : Nonempty.{u_1 + 1} (↑s : Type u_1)
hsub : s ⊆ Iio b
h : ∀ a < b, (s ∩ Ioo a b).Nonempty
a : X
hab : a < b
c : X
hcs : c ∈ s
hc : c ∈ Ioo a b
h₁ : True ∧ Ici (Subtype.mk (p := fun (x : X) ↦ x ∈ s) c hcs) ⊆ Subtype.val (p := fun (x : X) ↦ x ∈ s) ⁻¹' Ioo a b
⊢ ∃ (i' : { x : X // x ∈ s }), True ∧ Ici i' ⊆ Subtype.val (p := fun (x : X) ↦ x ∈ s) ⁻¹' Ioo a b

Tactic:
use ⟨c, hcs⟩