awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Order.WithTop
Goal:
ι : Type u_1
inst : Preorder ι
ts : TopologicalSpace ι
ht : OrderTopology ι
inst_1 : SecondCountableTopology ι
x₀ : ι
c : Set ι
c_count : c.Countable
hc : ts = generateFrom {s : Set ι | ∃ a ∈ c, s = Ioi a ∨ s = Iio a}
c' : Set ι
c'_count : c'.Countable
hc' : Dense c'
x₁ : ι := if h : ∃ (x : ι), Ioi x = ∅ then h.choose (p := fun (x : ι) ↦ Ioi x = ∅) else x₀
d : Set (WithTop ι) := WithTop.some '' c ∪ WithTop.some '' c' ∪ {⊤} ∪ {(↑x₁ : WithTop ι)}
basis : Set (Set ι) :=
  {s : Set ι | ∃ (f : Set ι) (g : Set ι), f ⊆ c ∧ g ⊆ c ∧ f.Finite ∧ g.Finite ∧ s = (⋂ a ∈ f, Ioi a) ∩ ⋂ a ∈ g, Iio a}
h_basis : IsTopologicalBasis basis
a b : ι
hb_1 : a < b
f g : Set ι
hfc : f ⊆ c
hgc : g ⊆ c
f_fin : f.Finite
g_fin : g.Finite
hb : Membership.mem (γ := Set ι) ((⋂ a ∈ f, Ioi a) ∩ ⋂ a ∈ g, Iio a) b
hfg : (⋂ a ∈ f, Ioi a) ∩ ⋂ a ∈ g, Iio a ⊆ Ioi a
inr : g.Finite
inr₁ : ∀ i ∈ g, IsOpen[generateFrom {s : Set (WithTop ι) | ∃ a ∈ d, s = Ioi a ∨ s = Iio a}] (Iio (↑i : WithTop ι))
⊢ IsOpen[generateFrom {s : Set (WithTop ι) | ∃ a ∈ d, s = Ioi a ∨ s = Iio a}] (⋂ z ∈ g, Iio (↑z : WithTop ι))

Tactic:
apply @Finite.isOpen_biInter _ _ (generateFrom {s | ∃ a ∈ d, s = Ioi a ∨ s = Iio a})

Premises used: Set.Finite.isOpen_biInter
-- Module: Mathlib.Topology.Order.WithTop
Goal:
ι : Type u_1
inst : Preorder ι
ts : TopologicalSpace ι
ht : OrderTopology ι
inst_1 : SecondCountableTopology ι
x₀ : ι
c : Set ι
c_count : c.Countable
hc : ts = generateFrom {s : Set ι | ∃ a ∈ c, s = Ioi a ∨ s = Iio a}
c' : Set ι
c'_count : c'.Countable
hc' : Dense c'
x₁ : ι := if h : ∃ (x : ι), Ioi x = ∅ then h.choose (p := fun (x : ι) ↦ Ioi x = ∅) else x₀
d : Set (WithTop ι) := WithTop.some '' c ∪ WithTop.some '' c' ∪ {⊤} ∪ {(↑x₁ : WithTop ι)}
basis : Set (Set ι) :=
  {s : Set ι | ∃ (f : Set ι) (g : Set ι), f ⊆ c ∧ g ⊆ c ∧ f.Finite ∧ g.Finite ∧ s = (⋂ a ∈ f, Ioi a) ∩ ⋂ a ∈ g, Iio a}
h_basis : IsTopologicalBasis basis
a b : ι
hb_1 : a < b
f g : Set ι
hfc : f ⊆ c
hgc : g ⊆ c
f_fin : f.Finite
g_fin : g.Finite
hb : Membership.mem (γ := Set ι) ((⋂ a ∈ f, Ioi a) ∩ ⋂ a ∈ g, Iio a) b
hfg : (⋂ a ∈ f, Ioi a) ∩ ⋂ a ∈ g, Iio a ⊆ Ioi a
⊢ g.Finite

Tactic:
g_fin
-- Module: Mathlib.Topology.Order.WithTop
Goal:
ι : Type u_1
inst : Preorder ι
ts : TopologicalSpace ι
ht : OrderTopology ι
inst_1 : SecondCountableTopology ι
x₀ : ι
c : Set ι
c_count : c.Countable
hc : ts = generateFrom {s : Set ι | ∃ a ∈ c, s = Ioi a ∨ s = Iio a}
c' : Set ι
c'_count : c'.Countable
hc' : Dense c'
x₁ : ι := if h : ∃ (x : ι), Ioi x = ∅ then h.choose (p := fun (x : ι) ↦ Ioi x = ∅) else x₀
d : Set (WithTop ι) := WithTop.some '' c ∪ WithTop.some '' c' ∪ {⊤} ∪ {(↑x₁ : WithTop ι)}
basis : Set (Set ι) :=
  {s : Set ι | ∃ (f : Set ι) (g : Set ι), f ⊆ c ∧ g ⊆ c ∧ f.Finite ∧ g.Finite ∧ s = (⋂ a ∈ f, Ioi a) ∩ ⋂ a ∈ g, Iio a}
h_basis : IsTopologicalBasis basis
a b : ι
hb_1 : a < b
f g : Set ι
hfc : f ⊆ c
hgc : g ⊆ c
f_fin : f.Finite
g_fin : g.Finite
hb : Membership.mem (γ := Set ι) ((⋂ a ∈ f, Ioi a) ∩ ⋂ a ∈ g, Iio a) b
hfg : (⋂ a ∈ f, Ioi a) ∩ ⋂ a ∈ g, Iio a ⊆ Ioi a
⊢ g.Finite

Tactic:
exact g_fin
-- Module: Mathlib.Topology.Order.WithTop
Goal:
ι : Type u_1
inst : Preorder ι
ts : TopologicalSpace ι
ht : OrderTopology ι
inst_1 : SecondCountableTopology ι
x₀ : ι
c : Set ι
c_count : c.Countable
hc : ts = generateFrom {s : Set ι | ∃ a ∈ c, s = Ioi a ∨ s = Iio a}
c' : Set ι
c'_count : c'.Countable
hc' : Dense c'
x₁ : ι := if h : ∃ (x : ι), Ioi x = ∅ then h.choose (p := fun (x : ι) ↦ Ioi x = ∅) else x₀
d : Set (WithTop ι) := WithTop.some '' c ∪ WithTop.some '' c' ∪ {⊤} ∪ {(↑x₁ : WithTop ι)}
basis : Set (Set ι) :=
  {s : Set ι | ∃ (f : Set ι) (g : Set ι), f ⊆ c ∧ g ⊆ c ∧ f.Finite ∧ g.Finite ∧ s = (⋂ a ∈ f, Ioi a) ∩ ⋂ a ∈ g, Iio a}
h_basis : IsTopologicalBasis basis
a b : ι
hb_1 : a < b
f g : Set ι
hfc : f ⊆ c
hgc : g ⊆ c
f_fin : f.Finite
g_fin : g.Finite
hb : Membership.mem (γ := Set ι) ((⋂ a ∈ f, Ioi a) ∩ ⋂ a ∈ g, Iio a) b
hfg : (⋂ a ∈ f, Ioi a) ∩ ⋂ a ∈ g, Iio a ⊆ Ioi a
i : ι
hi : i ∈ g
inr :
  Membership.mem (γ := Set (Set (WithTop ι))) {s : Set (WithTop ι) | ∃ a ∈ d, s = Ioi a ∨ s = Iio a}
    (Iio (↑i : WithTop ι))
⊢ IsOpen[generateFrom {s : Set (WithTop ι) | ∃ a ∈ d, s = Ioi a ∨ s = Iio a}] (Iio (↑i : WithTop ι))

Tactic:
apply isOpen_generateFrom_of_mem

Premises used: TopologicalSpace.isOpen_generateFrom_of_mem
-- Module: Mathlib.Topology.Order.WithTop
Goal:
ι : Type u_1
inst : Preorder ι
ts : TopologicalSpace ι
ht : OrderTopology ι
inst_1 : SecondCountableTopology ι
x₀ : ι
c : Set ι
c_count : c.Countable
hc : ts = generateFrom {s : Set ι | ∃ a ∈ c, s = Ioi a ∨ s = Iio a}
c' : Set ι
c'_count : c'.Countable
hc' : Dense c'
x₁ : ι := if h : ∃ (x : ι), Ioi x = ∅ then h.choose (p := fun (x : ι) ↦ Ioi x = ∅) else x₀
d : Set (WithTop ι) := WithTop.some '' c ∪ WithTop.some '' c' ∪ {⊤} ∪ {(↑x₁ : WithTop ι)}
basis : Set (Set ι) :=
  {s : Set ι | ∃ (f : Set ι) (g : Set ι), f ⊆ c ∧ g ⊆ c ∧ f.Finite ∧ g.Finite ∧ s = (⋂ a ∈ f, Ioi a) ∩ ⋂ a ∈ g, Iio a}
h_basis : IsTopologicalBasis basis
a b : ι
hb_1 : a < b
f g : Set ι
hfc : f ⊆ c
hgc : g ⊆ c
f_fin : f.Finite
g_fin : g.Finite
hb : Membership.mem (γ := Set ι) ((⋂ a ∈ f, Ioi a) ∩ ⋂ a ∈ g, Iio a) b
hfg : (⋂ a ∈ f, Ioi a) ∩ ⋂ a ∈ g, Iio a ⊆ Ioi a
i : ι
hi : i ∈ g
⊢ Membership.mem (γ := Set (Set (WithTop ι))) {s : Set (WithTop ι) | ∃ a ∈ d, s = Ioi a ∨ s = Iio a}
    (Iio (↑i : WithTop ι))

Tactic:
grind
-- Module: Mathlib.Topology.Order.WithTop
Goal:
ι : Type u_1
inst : Preorder ι
ts : TopologicalSpace ι
ht : OrderTopology ι
inst_1 : SecondCountableTopology ι
x₀ : ι
c : Set ι
c_count : c.Countable
hc : ts = generateFrom {s : Set ι | ∃ a ∈ c, s = Ioi a ∨ s = Iio a}
c' : Set ι
c'_count : c'.Countable
hc' : Dense c'
x₁ : ι := if h : ∃ (x : ι), Ioi x = ∅ then h.choose (p := fun (x : ι) ↦ Ioi x = ∅) else x₀
d : Set (WithTop ι) := WithTop.some '' c ∪ WithTop.some '' c' ∪ {⊤} ∪ {(↑x₁ : WithTop ι)}
basis : Set (Set ι) :=
  {s : Set ι | ∃ (f : Set ι) (g : Set ι), f ⊆ c ∧ g ⊆ c ∧ f.Finite ∧ g.Finite ∧ s = (⋂ a ∈ f, Ioi a) ∩ ⋂ a ∈ g, Iio a}
h_basis : IsTopologicalBasis basis
inr : Membership.mem (γ := Set (Set (WithTop ι))) {s : Set (WithTop ι) | ∃ a ∈ d, s = Ioi a ∨ s = Iio a} (Iio ⊤)
⊢ IsOpen[generateFrom {s : Set (WithTop ι) | ∃ a ∈ d, s = Ioi a ∨ s = Iio a}] (Iio ⊤)

Tactic:
apply isOpen_generateFrom_of_mem

Premises used: TopologicalSpace.isOpen_generateFrom_of_mem
-- Module: Mathlib.Topology.Order.WithTop
Goal:
ι : Type u_1
inst : Preorder ι
ts : TopologicalSpace ι
ht : OrderTopology ι
inst_1 : SecondCountableTopology ι
x₀ : ι
c : Set ι
c_count : c.Countable
hc : ts = generateFrom {s : Set ι | ∃ a ∈ c, s = Ioi a ∨ s = Iio a}
c' : Set ι
c'_count : c'.Countable
hc' : Dense c'
x₁ : ι := if h : ∃ (x : ι), Ioi x = ∅ then h.choose (p := fun (x : ι) ↦ Ioi x = ∅) else x₀
d : Set (WithTop ι) := WithTop.some '' c ∪ WithTop.some '' c' ∪ {⊤} ∪ {(↑x₁ : WithTop ι)}
basis : Set (Set ι) :=
  {s : Set ι | ∃ (f : Set ι) (g : Set ι), f ⊆ c ∧ g ⊆ c ∧ f.Finite ∧ g.Finite ∧ s = (⋂ a ∈ f, Ioi a) ∩ ⋂ a ∈ g, Iio a}
h_basis : IsTopologicalBasis basis
⊢ ⊤ ∈ d ∧ (Eq.{u_1 + 1} (α := Set (WithTop ι)) (Iio ⊤) (Ioi ⊤) ∨ Eq.{u_1 + 1} (α := Set (WithTop ι)) (Iio ⊤) (Iio ⊤))

Tactic:
simp [d]
-- Module: Mathlib.Topology.Order.WithTop
Goal:
ι : Type u_1
inst : Preorder ι
ts : TopologicalSpace ι
ht : OrderTopology ι
inst_1 : SecondCountableTopology ι
x₀ : ι
c : Set ι
c_count : c.Countable
hc : ts = generateFrom {s : Set ι | ∃ a ∈ c, s = Ioi a ∨ s = Iio a}
c' : Set ι
c'_count : c'.Countable
hc' : Dense c'
x₁ : ι := if h : ∃ (x : ι), Ioi x = ∅ then h.choose (p := fun (x : ι) ↦ Ioi x = ∅) else x₀
d : Set (WithTop ι) := WithTop.some '' c ∪ WithTop.some '' c' ∪ {⊤} ∪ {(↑x₁ : WithTop ι)}
basis : Set (Set ι) :=
  {s : Set ι | ∃ (f : Set ι) (g : Set ι), f ⊆ c ∧ g ⊆ c ∧ f.Finite ∧ g.Finite ∧ s = (⋂ a ∈ f, Ioi a) ∩ ⋂ a ∈ g, Iio a}
h_basis : IsTopologicalBasis basis
⊢ Membership.mem (γ := Set (Set (WithTop ι))) {s : Set (WithTop ι) | ∃ a ∈ d, s = Ioi a ∨ s = Iio a} (Iio ⊤)

Tactic:
exact ⟨⊤, by simp [d]⟩
-- Module: Mathlib.Topology.Order.WithTop
Goal:
ι : Type u_1
inst : Preorder ι
ts : TopologicalSpace ι
ht : OrderTopology ι
inst_1 : SecondCountableTopology ι
x₀ : ι
c : Set ι
c_count : c.Countable
hc : ts = generateFrom {s : Set ι | ∃ a ∈ c, s = Ioi a ∨ s = Iio a}
c' : Set ι
c'_count : c'.Countable
hc' : Dense c'
x₁ : ι := if h : ∃ (x : ι), Ioi x = ∅ then h.choose (p := fun (x : ι) ↦ Ioi x = ∅) else x₀
d : Set (WithTop ι) := WithTop.some '' c ∪ WithTop.some '' c' ∪ {⊤} ∪ {(↑x₁ : WithTop ι)}
basis : Set (Set ι) :=
  {s : Set ι | ∃ (f : Set ι) (g : Set ι), f ⊆ c ∧ g ⊆ c ∧ f.Finite ∧ g.Finite ∧ s = (⋂ a ∈ f, Ioi a) ∩ ⋂ a ∈ g, Iio a}
h_basis : IsTopologicalBasis basis
a : ι
inr :
  ∀ x ∈ Iio (↑a : WithTop ι),
    ∃ t ⊆ Iio (↑a : WithTop ι), IsOpen[generateFrom {s : Set (WithTop ι) | ∃ a ∈ d, s = Ioi a ∨ s = Iio a}] t ∧ x ∈ t
⊢ IsOpen[generateFrom {s : Set (WithTop ι) | ∃ a ∈ d, s = Ioi a ∨ s = Iio a}] (Iio (↑a : WithTop ι))

Tactic:
rw [@isOpen_iff_forall_mem_open]

Premises used: isOpen_iff_forall_mem_open
-- Module: Mathlib.Topology.Order.WithTop
Goal:
ι : Type u_1
inst : Preorder ι
ts : TopologicalSpace ι
ht : OrderTopology ι
inst_1 : SecondCountableTopology ι
x₀ : ι
c : Set ι
c_count : c.Countable
hc : ts = generateFrom {s : Set ι | ∃ a ∈ c, s = Ioi a ∨ s = Iio a}
c' : Set ι
c'_count : c'.Countable
hc' : Dense c'
x₁ : ι := if h : ∃ (x : ι), Ioi x = ∅ then h.choose (p := fun (x : ι) ↦ Ioi x = ∅) else x₀
d : Set (WithTop ι) := WithTop.some '' c ∪ WithTop.some '' c' ∪ {⊤} ∪ {(↑x₁ : WithTop ι)}
basis : Set (Set ι) :=
  {s : Set ι | ∃ (f : Set ι) (g : Set ι), f ⊆ c ∧ g ⊆ c ∧ f.Finite ∧ g.Finite ∧ s = (⋂ a ∈ f, Ioi a) ∩ ⋂ a ∈ g, Iio a}
h_basis : IsTopologicalBasis basis
a : ι
hb : ⊤ ∈ Iio (↑a : WithTop ι)
⊢ ∃ t ⊆ Iio (↑a : WithTop ι), IsOpen[generateFrom {s : Set (WithTop ι) | ∃ a ∈ d, s = Ioi a ∨ s = Iio a}] t ∧ ⊤ ∈ t

Tactic:
simp at hb
-- Module: Mathlib.Topology.Order.WithTop
Goal:
ι : Type u_1
inst : Preorder ι
ts : TopologicalSpace ι
ht : OrderTopology ι
inst_1 : SecondCountableTopology ι
x₀ : ι
c : Set ι
c_count : c.Countable
hc : ts = generateFrom {s : Set ι | ∃ a ∈ c, s = Ioi a ∨ s = Iio a}
c' : Set ι
c'_count : c'.Countable
hc' : Dense c'
x₁ : ι := if h : ∃ (x : ι), Ioi x = ∅ then h.choose (p := fun (x : ι) ↦ Ioi x = ∅) else x₀
d : Set (WithTop ι) := WithTop.some '' c ∪ WithTop.some '' c' ∪ {⊤} ∪ {(↑x₁ : WithTop ι)}
basis : Set (Set ι) :=
  {s : Set ι | ∃ (f : Set ι) (g : Set ι), f ⊆ c ∧ g ⊆ c ∧ f.Finite ∧ g.Finite ∧ s = (⋂ a ∈ f, Ioi a) ∩ ⋂ a ∈ g, Iio a}
h_basis : IsTopologicalBasis basis
a b : ι
hb : (↑b : WithTop ι) ∈ Iio (↑a : WithTop ι)
⊢ b < a

Tactic:
simp only [mem_Iio, WithTop.coe_lt_coe] at hb

Premises used: Set.mem_Iio, WithTop.coe_lt_coe
-- Module: Mathlib.Topology.Order.WithTop
Goal:
ι : Type u_1
inst : Preorder ι
ts : TopologicalSpace ι
ht : OrderTopology ι
inst_1 : SecondCountableTopology ι
x₀ : ι
c : Set ι
c_count : c.Countable
hc : ts = generateFrom {s : Set ι | ∃ a ∈ c, s = Ioi a ∨ s = Iio a}
c' : Set ι
c'_count : c'.Countable
hc' : Dense c'
x₁ : ι := if h : ∃ (x : ι), Ioi x = ∅ then h.choose (p := fun (x : ι) ↦ Ioi x = ∅) else x₀
d : Set (WithTop ι) := WithTop.some '' c ∪ WithTop.some '' c' ∪ {⊤} ∪ {(↑x₁ : WithTop ι)}
basis : Set (Set ι) :=
  {s : Set ι | ∃ (f : Set ι) (g : Set ι), f ⊆ c ∧ g ⊆ c ∧ f.Finite ∧ g.Finite ∧ s = (⋂ a ∈ f, Ioi a) ∩ ⋂ a ∈ g, Iio a}
h_basis : IsTopologicalBasis basis
a b : ι
hb : b < a
⊢ ∃ t ∈ basis, b ∈ t ∧ t ⊆ Iio a

Tactic:
h_basis.isOpen_iff.1 (isOpen_Iio' a) b hb

Premises used: TopologicalSpace.IsTopologicalBasis.isOpen_iff, isOpen_Iio', Iff.mp
-- Module: Mathlib.Topology.Order.WithTop
Goal:
ι : Type u_1
inst : Preorder ι
ts : TopologicalSpace ι
ht : OrderTopology ι
inst_1 : SecondCountableTopology ι
x₀ : ι
c : Set ι
c_count : c.Countable
hc : ts = generateFrom {s : Set ι | ∃ a ∈ c, s = Ioi a ∨ s = Iio a}
c' : Set ι
c'_count : c'.Countable
hc' : Dense c'
x₁ : ι := if h : ∃ (x : ι), Ioi x = ∅ then h.choose (p := fun (x : ι) ↦ Ioi x = ∅) else x₀
d : Set (WithTop ι) := WithTop.some '' c ∪ WithTop.some '' c' ∪ {⊤} ∪ {(↑x₁ : WithTop ι)}
basis : Set (Set ι) :=
  {s : Set ι | ∃ (f : Set ι) (g : Set ι), f ⊆ c ∧ g ⊆ c ∧ f.Finite ∧ g.Finite ∧ s = (⋂ a ∈ f, Ioi a) ∩ ⋂ a ∈ g, Iio a}
h_basis : IsTopologicalBasis basis
a b : ι
hb : b < a
inr :
  ∀ (f g : Set ι) (hfc : f ⊆ c) (hgc : g ⊆ c) (f_fin : f.Finite) (g_fin : g.Finite)
    (hb : Membership.mem (γ := Set ι) ((⋂ a ∈ f, Ioi a) ∩ ⋂ a ∈ g, Iio a) b)
    (hfg : (⋂ a ∈ f, Ioi a) ∩ ⋂ a ∈ g, Iio a ⊆ Iio a),
    ∃ t ⊆ Iio (↑a : WithTop ι),
      IsOpen[generateFrom {s : Set (WithTop ι) | ∃ a ∈ d, s = Ioi a ∨ s = Iio a}] t ∧ (↑b : WithTop ι) ∈ t
⊢ ∃ t ⊆ Iio (↑a : WithTop ι),
    IsOpen[generateFrom {s : Set (WithTop ι) | ∃ a ∈ d, s = Ioi a ∨ s = Iio a}] t ∧ (↑b : WithTop ι) ∈ t

Tactic:
obtain ⟨t, ⟨f, g, hfc, hgc, f_fin, g_fin, rfl⟩, hb, hfg⟩ :
          ∃ t ∈ basis, b ∈ t ∧ t ⊆ Iio a := h_basis.isOpen_iff.1 (isOpen_Iio' a) b hb

Premises used: TopologicalSpace.IsTopologicalBasis.isOpen_iff, isOpen_Iio', Iff.mp, Set.Iio, rfl
-- Module: Mathlib.Topology.Order.WithTop
Goal:
ι : Type u_1
inst : Preorder ι
ts : TopologicalSpace ι
ht : OrderTopology ι
inst_1 : SecondCountableTopology ι
x₀ : ι
c : Set ι
c_count : c.Countable
hc : ts = generateFrom {s : Set ι | ∃ a ∈ c, s = Ioi a ∨ s = Iio a}
c' : Set ι
c'_count : c'.Countable
hc' : Dense c'
x₁ : ι := if h : ∃ (x : ι), Ioi x = ∅ then h.choose (p := fun (x : ι) ↦ Ioi x = ∅) else x₀
d : Set (WithTop ι) := WithTop.some '' c ∪ WithTop.some '' c' ∪ {⊤} ∪ {(↑x₁ : WithTop ι)}
basis : Set (Set ι) :=
  {s : Set ι | ∃ (f : Set ι) (g : Set ι), f ⊆ c ∧ g ⊆ c ∧ f.Finite ∧ g.Finite ∧ s = (⋂ a ∈ f, Ioi a) ∩ ⋂ a ∈ g, Iio a}
h_basis : IsTopologicalBasis basis
a b : ι
hb_1 : b < a
f g : Set ι
hfc : f ⊆ c
hgc : g ⊆ c
f_fin : f.Finite
g_fin : g.Finite
hb : Membership.mem (γ := Set ι) ((⋂ a ∈ f, Ioi a) ∩ ⋂ a ∈ g, Iio a) b
hfg : (⋂ a ∈ f, Ioi a) ∩ ⋂ a ∈ g, Iio a ⊆ Iio a
⊢ Membership.mem (γ := Set (WithTop ι)) (((⋂ z ∈ f, Ioi (↑z : WithTop ι)) ∩ ⋂ z ∈ g, Iio (↑z : WithTop ι)) ∩ Iio ⊤)
    (↑b : WithTop ι)

Tactic:
simpa using hb
-- Module: Mathlib.Topology.Order.WithTop
Goal:
ι : Type u_1
inst : Preorder ι
ts : TopologicalSpace ι
ht : OrderTopology ι
inst_1 : SecondCountableTopology ι
x₀ : ι
c : Set ι
c_count : c.Countable
hc : ts = generateFrom {s : Set ι | ∃ a ∈ c, s = Ioi a ∨ s = Iio a}
c' : Set ι
c'_count : c'.Countable
hc' : Dense c'
x₁ : ι := if h : ∃ (x : ι), Ioi x = ∅ then h.choose (p := fun (x : ι) ↦ Ioi x = ∅) else x₀
d : Set (WithTop ι) := WithTop.some '' c ∪ WithTop.some '' c' ∪ {⊤} ∪ {(↑x₁ : WithTop ι)}
basis : Set (Set ι) :=
  {s : Set ι | ∃ (f : Set ι) (g : Set ι), f ⊆ c ∧ g ⊆ c ∧ f.Finite ∧ g.Finite ∧ s = (⋂ a ∈ f, Ioi a) ∩ ⋂ a ∈ g, Iio a}
h_basis : IsTopologicalBasis basis
a b : ι
hb_1 : b < a
f g : Set ι
hfc : f ⊆ c
hgc : g ⊆ c
f_fin : f.Finite
g_fin : g.Finite
hb : Membership.mem (γ := Set ι) ((⋂ a ∈ f, Ioi a) ∩ ⋂ a ∈ g, Iio a) b
hfg : (⋂ a ∈ f, Ioi a) ∩ ⋂ a ∈ g, Iio a ⊆ Iio a
inr : ((⋂ z ∈ f, Ioi (↑z : WithTop ι)) ∩ ⋂ z ∈ g, Iio (↑z : WithTop ι)) ∩ Iio ⊤ ⊆ Iio (↑a : WithTop ι)
inr₁ :
  IsOpen[generateFrom {s : Set (WithTop ι) | ∃ a ∈ d, s = Ioi a ∨ s = Iio a}]
    (((⋂ z ∈ f, Ioi (↑z : WithTop ι)) ∩ ⋂ z ∈ g, Iio (↑z : WithTop ι)) ∩ Iio ⊤)
⊢ ∃ t ⊆ Iio (↑a : WithTop ι),
    IsOpen[generateFrom {s : Set (WithTop ι) | ∃ a ∈ d, s = Ioi a ∨ s = Iio a}] t ∧ (↑b : WithTop ι) ∈ t

Tactic:
refine ⟨(⋂ z ∈ f, Ioi z) ∩ (⋂ z ∈ g, Iio z) ∩ Iio ⊤, ?_, ?_, by simpa using hb⟩
-- Module: Mathlib.Topology.Order.WithTop
Goal:
ι : Type u_1
inst : Preorder ι
ts : TopologicalSpace ι
ht : OrderTopology ι
inst_1 : SecondCountableTopology ι
x₀ : ι
c : Set ι
c_count : c.Countable
hc : ts = generateFrom {s : Set ι | ∃ a ∈ c, s = Ioi a ∨ s = Iio a}
c' : Set ι
c'_count : c'.Countable
hc' : Dense c'
x₁ : ι := if h : ∃ (x : ι), Ioi x = ∅ then h.choose (p := fun (x : ι) ↦ Ioi x = ∅) else x₀
d : Set (WithTop ι) := WithTop.some '' c ∪ WithTop.some '' c' ∪ {⊤} ∪ {(↑x₁ : WithTop ι)}
basis : Set (Set ι) :=
  {s : Set ι | ∃ (f : Set ι) (g : Set ι), f ⊆ c ∧ g ⊆ c ∧ f.Finite ∧ g.Finite ∧ s = (⋂ a ∈ f, Ioi a) ∩ ⋂ a ∈ g, Iio a}
h_basis : IsTopologicalBasis basis
a b : ι
hb_1 : b < a
f g : Set ι
hfc : f ⊆ c
hgc : g ⊆ c
f_fin : f.Finite
g_fin : g.Finite
hb : Membership.mem (γ := Set ι) ((⋂ a ∈ f, Ioi a) ∩ ⋂ a ∈ g, Iio a) b
hfg : (⋂ a ∈ f, Ioi a) ∩ ⋂ a ∈ g, Iio a ⊆ Iio a
hw : Membership.mem (γ := Set (WithTop ι)) (((⋂ z ∈ f, Ioi (↑z : WithTop ι)) ∩ ⋂ z ∈ g, Iio (↑z : WithTop ι)) ∩ Iio ⊤) ⊤
⊢ ⊤ ∈ Iio (↑a : WithTop ι)

Tactic:
simp at hw
-- Module: Mathlib.Topology.Order.WithTop
Goal:
ι : Type u_1
inst : Preorder ι
ts : TopologicalSpace ι
ht : OrderTopology ι
inst_1 : SecondCountableTopology ι
x₀ : ι
c : Set ι
c_count : c.Countable
hc : ts = generateFrom {s : Set ι | ∃ a ∈ c, s = Ioi a ∨ s = Iio a}
c' : Set ι
c'_count : c'.Countable
hc' : Dense c'
x₁ : ι := if h : ∃ (x : ι), Ioi x = ∅ then h.choose (p := fun (x : ι) ↦ Ioi x = ∅) else x₀
d : Set (WithTop ι) := WithTop.some '' c ∪ WithTop.some '' c' ∪ {⊤} ∪ {(↑x₁ : WithTop ι)}
basis : Set (Set ι) :=
  {s : Set ι | ∃ (f : Set ι) (g : Set ι), f ⊆ c ∧ g ⊆ c ∧ f.Finite ∧ g.Finite ∧ s = (⋂ a ∈ f, Ioi a) ∩ ⋂ a ∈ g, Iio a}
h_basis : IsTopologicalBasis basis
a b : ι
hb_1 : b < a
f g : Set ι
hfc : f ⊆ c
hgc : g ⊆ c
f_fin : f.Finite
g_fin : g.Finite
hb : Membership.mem (γ := Set ι) ((⋂ a ∈ f, Ioi a) ∩ ⋂ a ∈ g, Iio a) b
hfg : (⋂ a ∈ f, Ioi a) ∩ ⋂ a ∈ g, Iio a ⊆ Iio a
w : ι
hw :
  Membership.mem (γ := Set (WithTop ι)) (((⋂ z ∈ f, Ioi (↑z : WithTop ι)) ∩ ⋂ z ∈ g, Iio (↑z : WithTop ι)) ∩ Iio ⊤)
    (↑w : WithTop ι)
inr : w < a
⊢ (↑w : WithTop ι) ∈ Iio (↑a : WithTop ι)

Tactic:
simp only [mem_Iio, WithTop.coe_lt_coe]

Premises used: Set.mem_Iio, WithTop.coe_lt_coe
-- Module: Mathlib.Topology.Order.WithTop
Goal:
ι : Type u_1
inst : Preorder ι
ts : TopologicalSpace ι
ht : OrderTopology ι
inst_1 : SecondCountableTopology ι
x₀ : ι
c : Set ι
c_count : c.Countable
hc : ts = generateFrom {s : Set ι | ∃ a ∈ c, s = Ioi a ∨ s = Iio a}
c' : Set ι
c'_count : c'.Countable
hc' : Dense c'
x₁ : ι := if h : ∃ (x : ι), Ioi x = ∅ then h.choose (p := fun (x : ι) ↦ Ioi x = ∅) else x₀
d : Set (WithTop ι) := WithTop.some '' c ∪ WithTop.some '' c' ∪ {⊤} ∪ {(↑x₁ : WithTop ι)}
basis : Set (Set ι) :=
  {s : Set ι | ∃ (f : Set ι) (g : Set ι), f ⊆ c ∧ g ⊆ c ∧ f.Finite ∧ g.Finite ∧ s = (⋂ a ∈ f, Ioi a) ∩ ⋂ a ∈ g, Iio a}
h_basis : IsTopologicalBasis basis
a b : ι
hb_1 : b < a
f g : Set ι
hfc : f ⊆ c
hgc : g ⊆ c
f_fin : f.Finite
g_fin : g.Finite
hb : Membership.mem (γ := Set ι) ((⋂ a ∈ f, Ioi a) ∩ ⋂ a ∈ g, Iio a) b
hfg : (⋂ a ∈ f, Ioi a) ∩ ⋂ a ∈ g, Iio a ⊆ Iio a
w : ι
hw :
  Membership.mem (γ := Set (WithTop ι)) (((⋂ z ∈ f, Ioi (↑z : WithTop ι)) ∩ ⋂ z ∈ g, Iio (↑z : WithTop ι)) ∩ Iio ⊤)
    (↑w : WithTop ι)
inr : Membership.mem (γ := Set ι) ((⋂ a ∈ f, Ioi a) ∩ ⋂ a ∈ g, Iio a) w
⊢ w < a

Tactic:
apply hfg
-- Module: Mathlib.Topology.Order.WithTop
Goal:
ι : Type u_1
inst : Preorder ι
ts : TopologicalSpace ι
ht : OrderTopology ι
inst_1 : SecondCountableTopology ι
x₀ : ι
c : Set ι
c_count : c.Countable
hc : ts = generateFrom {s : Set ι | ∃ a ∈ c, s = Ioi a ∨ s = Iio a}
c' : Set ι
c'_count : c'.Countable
hc' : Dense c'
x₁ : ι := if h : ∃ (x : ι), Ioi x = ∅ then h.choose (p := fun (x : ι) ↦ Ioi x = ∅) else x₀
d : Set (WithTop ι) := WithTop.some '' c ∪ WithTop.some '' c' ∪ {⊤} ∪ {(↑x₁ : WithTop ι)}
basis : Set (Set ι) :=
  {s : Set ι | ∃ (f : Set ι) (g : Set ι), f ⊆ c ∧ g ⊆ c ∧ f.Finite ∧ g.Finite ∧ s = (⋂ a ∈ f, Ioi a) ∩ ⋂ a ∈ g, Iio a}
h_basis : IsTopologicalBasis basis
a b : ι
hb_1 : b < a
f g : Set ι
hfc : f ⊆ c
hgc : g ⊆ c
f_fin : f.Finite
g_fin : g.Finite
hb : Membership.mem (γ := Set ι) ((⋂ a ∈ f, Ioi a) ∩ ⋂ a ∈ g, Iio a) b
hfg : (⋂ a ∈ f, Ioi a) ∩ ⋂ a ∈ g, Iio a ⊆ Iio a
w : ι
hw :
  Membership.mem (γ := Set (WithTop ι)) (((⋂ z ∈ f, Ioi (↑z : WithTop ι)) ∩ ⋂ z ∈ g, Iio (↑z : WithTop ι)) ∩ Iio ⊤)
    (↑w : WithTop ι)
⊢ Membership.mem (γ := Set ι) ((⋂ a ∈ f, Ioi a) ∩ ⋂ a ∈ g, Iio a) w

Tactic:
simpa using hw
-- Module: Mathlib.Topology.Order.WithTop
Goal:
ι : Type u_1
inst : Preorder ι
ts : TopologicalSpace ι
ht : OrderTopology ι
inst_1 : SecondCountableTopology ι
x₀ : ι
c : Set ι
c_count : c.Countable
hc : ts = generateFrom {s : Set ι | ∃ a ∈ c, s = Ioi a ∨ s = Iio a}
c' : Set ι
c'_count : c'.Countable
hc' : Dense c'
x₁ : ι := if h : ∃ (x : ι), Ioi x = ∅ then h.choose (p := fun (x : ι) ↦ Ioi x = ∅) else x₀
d : Set (WithTop ι) := WithTop.some '' c ∪ WithTop.some '' c' ∪ {⊤} ∪ {(↑x₁ : WithTop ι)}
basis : Set (Set ι) :=
  {s : Set ι | ∃ (f : Set ι) (g : Set ι), f ⊆ c ∧ g ⊆ c ∧ f.Finite ∧ g.Finite ∧ s = (⋂ a ∈ f, Ioi a) ∩ ⋂ a ∈ g, Iio a}
h_basis : IsTopologicalBasis basis
a b : ι
hb_1 : b < a
f g : Set ι
hfc : f ⊆ c
hgc : g ⊆ c
f_fin : f.Finite
g_fin : g.Finite
hb : Membership.mem (γ := Set ι) ((⋂ a ∈ f, Ioi a) ∩ ⋂ a ∈ g, Iio a) b
hfg : (⋂ a ∈ f, Ioi a) ∩ ⋂ a ∈ g, Iio a ⊆ Iio a
w : WithTop ι
hw : Membership.mem (γ := Set (WithTop ι)) (((⋂ z ∈ f, Ioi (↑z : WithTop ι)) ∩ ⋂ z ∈ g, Iio (↑z : WithTop ι)) ∩ Iio ⊤) w
inr :
  ∀
    (hw :
      Membership.mem (γ := Set (WithTop ι)) (((⋂ z ∈ f, Ioi (↑z : WithTop ι)) ∩ ⋂ z ∈ g, Iio (↑z : WithTop ι)) ∩ Iio ⊤)
        ⊤),
    ⊤ ∈ Iio (↑a : WithTop ι)
inr₁ :
  ∀ (w : ι)
    (hw :
      Membership.mem (γ := Set (WithTop ι)) (((⋂ z ∈ f, Ioi (↑z : WithTop ι)) ∩ ⋂ z ∈ g, Iio (↑z : WithTop ι)) ∩ Iio ⊤)
        (↑w : WithTop ι)),
    (↑w : WithTop ι) ∈ Iio (↑a : WithTop ι)
⊢ w ∈ Iio (↑a : WithTop ι)

Tactic:
induction w with
          | top => simp at hw
          | coe w =>
            simp only [mem_Iio, WithTop.coe_lt_coe]
            apply hfg
            simpa using hw

Premises used: Set.mem_Iio, WithTop.coe_lt_coe
-- Module: Mathlib.Topology.Order.WithTop
Goal:
ι : Type u_1
inst : Preorder ι
ts : TopologicalSpace ι
ht : OrderTopology ι
inst_1 : SecondCountableTopology ι
x₀ : ι
c : Set ι
c_count : c.Countable
hc : ts = generateFrom {s : Set ι | ∃ a ∈ c, s = Ioi a ∨ s = Iio a}
c' : Set ι
c'_count : c'.Countable
hc' : Dense c'
x₁ : ι := if h : ∃ (x : ι), Ioi x = ∅ then h.choose (p := fun (x : ι) ↦ Ioi x = ∅) else x₀
d : Set (WithTop ι) := WithTop.some '' c ∪ WithTop.some '' c' ∪ {⊤} ∪ {(↑x₁ : WithTop ι)}
basis : Set (Set ι) :=
  {s : Set ι | ∃ (f : Set ι) (g : Set ι), f ⊆ c ∧ g ⊆ c ∧ f.Finite ∧ g.Finite ∧ s = (⋂ a ∈ f, Ioi a) ∩ ⋂ a ∈ g, Iio a}
h_basis : IsTopologicalBasis basis
a b : ι
hb_1 : b < a
f g : Set ι
hfc : f ⊆ c
hgc : g ⊆ c
f_fin : f.Finite
g_fin : g.Finite
hb : Membership.mem (γ := Set ι) ((⋂ a ∈ f, Ioi a) ∩ ⋂ a ∈ g, Iio a) b
hfg : (⋂ a ∈ f, Ioi a) ∩ ⋂ a ∈ g, Iio a ⊆ Iio a
inr :
  IsOpen[generateFrom {s : Set (WithTop ι) | ∃ a ∈ d, s = Ioi a ∨ s = Iio a}]
    ((⋂ z ∈ f, Ioi (↑z : WithTop ι)) ∩ ⋂ z ∈ g, Iio (↑z : WithTop ι))
inr₁ : IsOpen[generateFrom {s : Set (WithTop ι) | ∃ a ∈ d, s = Ioi a ∨ s = Iio a}] (Iio ⊤)
⊢ IsOpen[generateFrom {s : Set (WithTop ι) | ∃ a ∈ d, s = Ioi a ∨ s = Iio a}]
    (((⋂ z ∈ f, Ioi (↑z : WithTop ι)) ∩ ⋂ z ∈ g, Iio (↑z : WithTop ι)) ∩ Iio ⊤)

Tactic:
apply @IsOpen.inter _ (generateFrom {s | ∃ a ∈ d, s = Ioi a ∨ s = Iio a})

Premises used: IsOpen.inter
-- Module: Mathlib.Topology.Order.WithTop
Goal:
ι : Type u_1
inst : Preorder ι
ts : TopologicalSpace ι
ht : OrderTopology ι
inst_1 : SecondCountableTopology ι
x₀ : ι
c : Set ι
c_count : c.Countable
hc : ts = generateFrom {s : Set ι | ∃ a ∈ c, s = Ioi a ∨ s = Iio a}
c' : Set ι
c'_count : c'.Countable
hc' : Dense c'
x₁ : ι := if h : ∃ (x : ι), Ioi x = ∅ then h.choose (p := fun (x : ι) ↦ Ioi x = ∅) else x₀
d : Set (WithTop ι) := WithTop.some '' c ∪ WithTop.some '' c' ∪ {⊤} ∪ {(↑x₁ : WithTop ι)}
basis : Set (Set ι) :=
  {s : Set ι | ∃ (f : Set ι) (g : Set ι), f ⊆ c ∧ g ⊆ c ∧ f.Finite ∧ g.Finite ∧ s = (⋂ a ∈ f, Ioi a) ∩ ⋂ a ∈ g, Iio a}
h_basis : IsTopologicalBasis basis
a b : ι
hb_1 : b < a
f g : Set ι
hfc : f ⊆ c
hgc : g ⊆ c
f_fin : f.Finite
g_fin : g.Finite
hb : Membership.mem (γ := Set ι) ((⋂ a ∈ f, Ioi a) ∩ ⋂ a ∈ g, Iio a) b
hfg : (⋂ a ∈ f, Ioi a) ∩ ⋂ a ∈ g, Iio a ⊆ Iio a
inr : Membership.mem (γ := Set (Set (WithTop ι))) {s : Set (WithTop ι) | ∃ a ∈ d, s = Ioi a ∨ s = Iio a} (Iio ⊤)
⊢ IsOpen[generateFrom {s : Set (WithTop ι) | ∃ a ∈ d, s = Ioi a ∨ s = Iio a}] (Iio ⊤)

Tactic:
apply isOpen_generateFrom_of_mem

Premises used: TopologicalSpace.isOpen_generateFrom_of_mem