awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.OpenPartialHomeomorph.Defs (goal)
Goal:
X : Type u_1
Y : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
e : OpenPartialHomeomorph X Y
e' : PartialEquiv X Y
h : e.toPartialEquiv = e'
⊢ e.replaceEquiv e' h = e
have mk : ∀ (toPartialEquiv : PartialEquiv X Y) (open_source : IsOpen[inst] toPartialEquiv.source)
  (open_target : IsOpen[inst_1] toPartialEquiv.target)
  (continuousOn_toFun : ContinuousOn (↑toPartialEquiv : X → Y) toPartialEquiv.source)
  (continuousOn_invFun : ContinuousOn toPartialEquiv.invFun toPartialEquiv.target)
  (h :
    { toPartialEquiv := toPartialEquiv, open_source := open_source, open_target := open_target,
          continuousOn_toFun := continuousOn_toFun, continuousOn_invFun := continuousOn_invFun :
          OpenPartialHomeomorph X Y }.toPartialEquiv =
      e'),
  { toPartialEquiv := toPartialEquiv, open_source := open_source, open_target := open_target,
          continuousOn_toFun := continuousOn_toFun, continuousOn_invFun := continuousOn_invFun :
          OpenPartialHomeomorph X Y }.replaceEquiv
      e' h =
    { toPartialEquiv := toPartialEquiv, open_source := open_source, open_target := open_target,
      continuousOn_toFun := continuousOn_toFun, continuousOn_invFun := continuousOn_invFun }
Tactic: cases e
Cleared hypotheses: e, h
-- Lean 4 proof step from Mathlib.Topology.OpenPartialHomeomorph.Defs (goal)
Goal:
X : Type u_1
Y : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
e' toPartialEquiv : PartialEquiv X Y
open_source : IsOpen[inst] toPartialEquiv.source
open_target : IsOpen[inst_1] toPartialEquiv.target
continuousOn_toFun : ContinuousOn (↑toPartialEquiv : X → Y) toPartialEquiv.source
continuousOn_invFun : ContinuousOn toPartialEquiv.invFun toPartialEquiv.target
h :
  { toPartialEquiv := toPartialEquiv, open_source := open_source, open_target := open_target,
        continuousOn_toFun := continuousOn_toFun, continuousOn_invFun := continuousOn_invFun :
        OpenPartialHomeomorph X Y }.toPartialEquiv =
    e'
⊢ { toPartialEquiv := toPartialEquiv, open_source := open_source, open_target := open_target,
          continuousOn_toFun := continuousOn_toFun, continuousOn_invFun := continuousOn_invFun :
          OpenPartialHomeomorph X Y }.replaceEquiv
      e' h =
    { toPartialEquiv := toPartialEquiv, open_source := open_source, open_target := open_target,
      continuousOn_toFun := continuousOn_toFun, continuousOn_invFun := continuousOn_invFun }
have mk : { toPartialEquiv := toPartialEquiv, open_source := open_source, open_target := open_target,
        continuousOn_toFun := continuousOn_toFun, continuousOn_invFun := continuousOn_invFun :
        OpenPartialHomeomorph X Y }.replaceEquiv
    { toPartialEquiv := toPartialEquiv, open_source := open_source, open_target := open_target,
        continuousOn_toFun := continuousOn_toFun, continuousOn_invFun := continuousOn_invFun :
        OpenPartialHomeomorph X Y }.toPartialEquiv
    sorry =
  { toPartialEquiv := toPartialEquiv, open_source := open_source, open_target := open_target,
    continuousOn_toFun := continuousOn_toFun, continuousOn_invFun := continuousOn_invFun }
Tactic: subst e'
Cleared hypotheses: e', h
-- Lean 4 proof step from Mathlib.Topology.OpenPartialHomeomorph.IsImage (goal)
Goal:
X : Type u_1
Y : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
e : OpenPartialHomeomorph X Y
s : Set X
t : Set Y
⊢ e.IsImage s t ↔ e.target ∩ (↑e.symm : Y → X) ⁻¹' (e.source ∩ s) = e.target ∩ t
have rw : e.target ∩ (↑e.symm : Y → X) ⁻¹' s = e.target ∩ t ↔ e.target ∩ (↑e.symm : Y → X) ⁻¹' (e.source ∩ s) = e.target ∩ t
Tactic: rw [iff_symm_preimage_eq, ← image_source_inter_eq, ← image_source_inter_eq']
-- Lean 4 proof step from Mathlib.Topology.OpenPartialHomeomorph.IsImage (goal)
Goal:
X : Type u_1
Y : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
e : OpenPartialHomeomorph X Y
s : Set X
t : Set Y
rw : e.target ∩ (↑e.symm : Y → X) ⁻¹' s = e.target ∩ t ↔ e.target ∩ (↑e.symm : Y → X) ⁻¹' (e.source ∩ s) = e.target ∩ t
⊢ e.IsImage s t ↔ e.target ∩ (↑e.symm : Y → X) ⁻¹' (e.source ∩ s) = e.target ∩ t
have rw₁ : e.target ∩ (↑e.symm : Y → X) ⁻¹' s = e.target ∩ t ↔ (↑e : X → Y) '' (e.source ∩ s) = e.target ∩ t
Tactic: rw [iff_symm_preimage_eq, ← image_source_inter_eq, ← image_source_inter_eq']
-- Lean 4 proof step from Mathlib.Topology.OpenPartialHomeomorph.IsImage (goal)
Goal:
X : Type u_1
Y : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
e : OpenPartialHomeomorph X Y
s : Set X
t : Set Y
rw : e.target ∩ (↑e.symm : Y → X) ⁻¹' s = e.target ∩ t ↔ e.target ∩ (↑e.symm : Y → X) ⁻¹' (e.source ∩ s) = e.target ∩ t
rw₁ : e.target ∩ (↑e.symm : Y → X) ⁻¹' s = e.target ∩ t ↔ (↑e : X → Y) '' (e.source ∩ s) = e.target ∩ t
⊢ e.IsImage s t ↔ e.target ∩ (↑e.symm : Y → X) ⁻¹' (e.source ∩ s) = e.target ∩ t
have rw₂ : (↑e : X → Y) '' (e.source ∩ s) = e.target ∩ t ↔ (↑e : X → Y) '' (e.source ∩ s) = e.target ∩ t
Tactic: rw [iff_symm_preimage_eq, ← image_source_inter_eq, ← image_source_inter_eq']
-- Lean 4 proof step from Mathlib.Topology.OpenPartialHomeomorph.IsImage (goal)
Goal:
X : Type u_1
Y : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
e : OpenPartialHomeomorph X Y
s : Set X
t : Set Y
x : X
h : e.IsImage s t
hx : x ∈ e.source
⊢ map (↑e : X → Y) (𝓝[s] x) = 𝓝[t] (↑e : X → Y) x
have rw : 𝓝[(↑e : X → Y) '' (e.source ∩ s)] (↑e : X → Y) x = 𝓝[t] (↑e : X → Y) x
Tactic: rw [e.map_nhdsWithin_eq hx, h.image_eq, e.nhdsWithin_target_inter (e.map_source hx)]
-- Lean 4 proof step from Mathlib.Topology.OpenPartialHomeomorph.IsImage (goal)
Goal:
X : Type u_1
Y : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
e : OpenPartialHomeomorph X Y
s : Set X
t : Set Y
x : X
h : e.IsImage s t
hx : x ∈ e.source
rw : 𝓝[(↑e : X → Y) '' (e.source ∩ s)] (↑e : X → Y) x = 𝓝[t] (↑e : X → Y) x
⊢ map (↑e : X → Y) (𝓝[s] x) = 𝓝[t] (↑e : X → Y) x
have rw₁ : 𝓝[e.target ∩ t] (↑e : X → Y) x = 𝓝[t] (↑e : X → Y) x
Tactic: rw [e.map_nhdsWithin_eq hx, h.image_eq, e.nhdsWithin_target_inter (e.map_source hx)]
-- Lean 4 proof step from Mathlib.Topology.OpenPartialHomeomorph.IsImage (goal)
Goal:
X : Type u_1
Y : Type u_3
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
e : OpenPartialHomeomorph X Y
s : Set X
t : Set Y
x : X
h : e.IsImage s t
hx : x ∈ e.source
rw : 𝓝[(↑e : X → Y) '' (e.source ∩ s)] (↑e : X → Y) x = 𝓝[t] (↑e : X → Y) x
rw₁ : 𝓝[e.target ∩ t] (↑e : X → Y) x = 𝓝[t] (↑e : X → Y) x
⊢ map (↑e : X → Y) (𝓝[s] x) = 𝓝[t] (↑e : X → Y) x
have rw₂ : 𝓝[t] (↑e : X → Y) x = 𝓝[t] (↑e : X → Y) x
Tactic: rw [e.map_nhdsWithin_eq hx, h.image_eq, e.nhdsWithin_target_inter (e.map_source hx)]
-- Lean 4 proof step from Mathlib.Topology.OpenPartialHomeomorph.IsImage (goal)
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
⊢ (e.restr s).toPartialEquiv = e.restr s
have rw : e.restr (interior s) = e.restr s
Tactic: rw [e.restr_toPartialEquiv, hs.interior_eq]
-- Lean 4 proof step from Mathlib.Topology.OpenPartialHomeomorph.IsImage (goal)
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
⊢ (e.restr s).toPartialEquiv = e.restr s
have rw₁ : e.restr s = e.restr s
Tactic: rw [e.restr_toPartialEquiv, hs.interior_eq]
-- Lean 4 proof step from Mathlib.Topology.OpenPartialHomeomorph.IsImage (goal)
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
have refine : (e.restr (e.source ∩ s)).source = (e.restr s).source
Tactic: refine OpenPartialHomeomorph.ext _ _ (fun x => rfl) (fun x => rfl) ?_
-- Lean 4 proof step from Mathlib.Topology.OpenPartialHomeomorph.IsImage (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
⊢ Eq (α := OpenPartialHomeomorph X X) (ofSet univ ⋯) (OpenPartialHomeomorph.refl X)
have h : ∀ (x : X), (↑(ofSet univ sorry) : X → X) x = (↑(OpenPartialHomeomorph.refl X) : X → X) x
Tactic: ext
-- Lean 4 proof step from Mathlib.Topology.OpenPartialHomeomorph.IsImage (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
h : ∀ (x : X), (↑(ofSet univ ⋯) : X → X) x = (↑(OpenPartialHomeomorph.refl X) : X → X) x
⊢ Eq (α := OpenPartialHomeomorph X X) (ofSet univ ⋯) (OpenPartialHomeomorph.refl X)
have hinv : ∀ (x : X),
  (↑(OpenPartialHomeomorph.symm (ofSet univ sorry)) : X → X) x =
    (↑(OpenPartialHomeomorph.symm (OpenPartialHomeomorph.refl X)) : X → X) x
Tactic: ext
-- Lean 4 proof step from Mathlib.Topology.OpenPartialHomeomorph.IsImage (goal)
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
⊢ Eq (α := OpenPartialHomeomorph X X) (ofSet univ ⋯) (OpenPartialHomeomorph.refl X)
have hs : ∀ (x : X),
  Membership.mem (γ := Set X) (PartialEquiv.source (toPartialEquiv (ofSet univ sorry))) x ↔
    x ∈ (toPartialEquiv (OpenPartialHomeomorph.refl X)).source
Tactic: ext
-- Lean 4 proof step from Mathlib.Topology.OpenPartialHomeomorph.IsImage (goal)
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.restr e'.source ≈ e'.restr e.source
have left : (e.restr e'.source).source = (e'.restr e.source).source
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.OpenPartialHomeomorph.IsImage (goal)
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
⊢ e.restr e'.source ≈ e'.restr e.source
have right : EqOn (↑(e.restr e'.source) : X → Y) (↑(e'.restr e.source) : X → Y) (e.restr e'.source).source
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.OpenPartialHomeomorph.IsImage (goal)
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.restr e'.source).source = (e'.restr e.source).source
have left : (e.restr e'.source).source = e'.source ∩ e.source
Tactic: rw [e'.restr_source' _ e.open_source]
-- Lean 4 proof step from Mathlib.Topology.OpenPartialHomeomorph.IsImage (goal)
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.restr e'.source).source = e'.source ∩ e.source
have left : e.source ∩ e'.source = e'.source ∩ e.source
Tactic: rw [e.restr_source' _ e'.open_source]
-- Lean 4 proof step from Mathlib.Topology.OpenPartialHomeomorph.IsImage (goal)
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.restr e'.source).source
have right : EqOn (↑(e.restr e'.source) : X → Y) (↑(e'.restr e.source) : X → Y) (e.source ∩ e'.source)
Tactic: rw [e.restr_source' _ e'.open_source]
-- Lean 4 proof step from Mathlib.Topology.OpenPartialHomeomorph.IsImage (goal)
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)
have right : EqOn (↑(e.restr e'.source) : X → Y) (↑e : X → Y) (e.source ∩ e'.source)
Tactic: refine (EqOn.trans ?_ h).trans ?_
-- Lean 4 proof step from Mathlib.Topology.OpenPartialHomeomorph.IsImage (goal)
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)
⊢ EqOn (↑(e.restr e'.source) : X → Y) (↑(e'.restr e.source) : X → Y) (e.source ∩ e'.source)
have right₁ : EqOn (↑e' : X → Y) (↑(e'.restr e.source) : X → Y) (e.source ∩ e'.source)
Tactic: refine (EqOn.trans ?_ h).trans ?_
-- Lean 4 proof step from Mathlib.Topology.OpenPartialHomeomorph.IsImage (goal)
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 ≈ e.restr s'
have left : (e.restr s).source = (e.restr s').source
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.OpenPartialHomeomorph.IsImage (goal)
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
⊢ e.restr s ≈ e.restr s'
have right : EqOn (↑(e.restr s) : X → Y) (↑(e.restr s') : X → Y) (e.restr s).source
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.Order.AtTopBotIxx (goal)
Goal:
X : Type u_1
inst : LinearOrder X
inst_1 : TopologicalSpace X
inst_2 : OrderTopology X
s : Set X
b : X
⊢ 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)
have 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)
Tactic: rcases s.eq_empty_or_nonempty with rfl | hsne
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.Topology.Order.AtTopBotIxx (goal)
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)
⊢ 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)
have 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)
Tactic: rcases s.eq_empty_or_nonempty with rfl | hsne
-- Lean 4 proof step from Mathlib.Topology.Order.AtTopBotIxx (hypothesis)
Goal:
X : Type u_1
inst : LinearOrder X
inst_1 : TopologicalSpace X
inst_2 : OrderTopology X
s : Set X
b : X
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)
have this : Nonempty.{u_1 + 1} (↑s : Type u_1)
Tactic: have := hsne.to_subtype
-- Lean 4 proof step from Mathlib.Topology.Order.AtTopBotIxx (goal)
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)
⊢ 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)
have 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
Tactic: simp only [hsne, true_imp_iff]
-- Lean 4 proof step from Mathlib.Topology.Order.AtTopBotIxx (goal)
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)
⊢ 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
have 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
Tactic: by_cases hsub : s ⊆ Iio b
-- Lean 4 proof step from Mathlib.Topology.Order.AtTopBotIxx (goal)
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
⊢ 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
have 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
Tactic: by_cases hsub : s ⊆ Iio b
-- Lean 4 proof step from Mathlib.Topology.Order.AtTopBotIxx (goal)
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
⊢ 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
have 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
Tactic: simp only [hsub, true_and]
-- Lean 4 proof step from Mathlib.Topology.Order.AtTopBotIxx (goal)
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
⊢ Eq (α := Filter { x : X // x ∈ s }) (comap (Subtype.val (p := fun (x : X) ↦ x ∈ s)) (𝓝[<] b)) atTop ↔
    ∀ a < b, (s ∩ Ioo a b).Nonempty
have 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
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.Order.AtTopBotIxx (goal)
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 ↔
    ∀ a < b, (s ∩ Ioo a b).Nonempty
have 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
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.Order.AtTopBotIxx (hypothesis)
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
⊢ (s ∩ Ioo a b).Nonempty
have 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)
Tactic: have := preimage_mem_comap (m := ((↑) : s → X)) (Ioo_mem_nhdsLT ha)
-- Lean 4 proof step from Mathlib.Topology.Order.AtTopBotIxx (hypothesis)
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)
⊢ (s ∩ Ioo a b).Nonempty
have this₁ : Membership.mem (γ := Filter { x : X // x ∈ s }) atTop (Subtype.val (p := fun (x : X) ↦ x ∈ s) ⁻¹' Ioo a b)
Tactic: rw [h] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Topology.Order.AtTopBotIxx (goal)
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)
⊢ (s ∩ Ioo a b).Nonempty
have 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
Tactic: rcases Filter.nonempty_of_mem this with ⟨⟨c, hcs⟩, hc⟩
-- Lean 4 proof step from Mathlib.Topology.Order.AtTopBotIxx (goal)
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
have pos : ∀ i < b, ∃ (i' : { x : X // x ∈ s }), True ∧ Ici i' ⊆ Subtype.val (p := fun (x : X) ↦ x ∈ s) ⁻¹' Ioo i b
Tactic: refine (nhdsLT_basis_of_exists_lt (hsne.mono hsub)).comap _ |>.ext atTop_basis ?_ ?_
-- Lean 4 proof step from Mathlib.Topology.Order.AtTopBotIxx (goal)
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
⊢ Eq (α := Filter { x : X // x ∈ s }) (comap (Subtype.val (p := fun (x : X) ↦ x ∈ s)) (𝓝[<] b)) atTop
have pos₁ : ∀ (i' : { x : X // x ∈ s }), True → ∃ i < b, Subtype.val (p := fun (x : X) ↦ x ∈ s) ⁻¹' Ioo i b ⊆ Ici i'
Tactic: refine (nhdsLT_basis_of_exists_lt (hsne.mono hsub)).comap _ |>.ext atTop_basis ?_ ?_
-- Lean 4 proof step from Mathlib.Topology.Order.AtTopBotIxx (goal)
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
⊢ ∃ (i' : { x : X // x ∈ s }), True ∧ Ici i' ⊆ Subtype.val (p := fun (x : X) ↦ x ∈ s) ⁻¹' Ioo a b
have 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
Tactic: rcases h a hab with ⟨c, hcs, hc⟩
-- Lean 4 proof step from Mathlib.Topology.Order.AtTopBotIxx (goal)
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
⊢ ∃ (i' : { x : X // x ∈ s }), True ∧ Ici i' ⊆ Subtype.val (p := fun (x : X) ↦ x ∈ s) ⁻¹' Ioo a b
have h₁ : True ∧ Ici (Subtype.mk (p := fun (x : X) ↦ x ∈ s) c hcs) ⊆ Subtype.val (p := fun (x : X) ↦ x ∈ s) ⁻¹' Ioo a b
Tactic: use ⟨c, hcs⟩
-- Lean 4 proof step from Mathlib.Topology.Order.AtTopBotIxx (goal)
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
has : a ∈ s
⊢ ∃ i < b, Subtype.val (p := fun (x : X) ↦ x ∈ s) ⁻¹' Ioo i b ⊆ Ici (Subtype.mk (p := fun (x : X) ↦ x ∈ s) a has)
have right : Subtype.val (p := fun (x : X) ↦ x ∈ s) ⁻¹' Ioo a b ⊆ Ici (Subtype.mk (p := fun (x : X) ↦ x ∈ s) a has)
Tactic: use a, hsub has