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 : ι
hb_1 : ⊤ ∈ Ioi (↑a : WithTop ι)
ha : (Ioi a).Nonempty
b : ι
bc' : b ∈ c'
hb : b ∈ Ioi a
inr : Ioi (↑b : WithTop ι) ⊆ Ioi (↑a : WithTop ι)
inr₁ : IsOpen[generateFrom {s : Set (WithTop ι) | ∃ a ∈ d, s = Ioi a ∨ s = Iio a}] (Ioi (↑b : WithTop ι))
⊢ ∃ t ⊆ Ioi (↑a : WithTop ι), IsOpen[generateFrom {s : Set (WithTop ι) | ∃ a ∈ d, s = Ioi a ∨ s = Iio a}] t ∧ ⊤ ∈ t

Tactic:
refine ⟨Ioi b, ?_, ?_, by simp⟩
-- 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_1 : ⊤ ∈ Ioi (↑a : WithTop ι)
ha : (Ioi a).Nonempty
b : ι
bc' : b ∈ c'
hb : b ∈ Ioi a
inr : (↑a : WithTop ι) ≤ (↑b : WithTop ι)
⊢ Ioi (↑b : WithTop ι) ⊆ Ioi (↑a : WithTop ι)

Tactic:
apply Ioi_subset_Ioi

Premises used: Set.Ioi_subset_Ioi
-- 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_1 : ⊤ ∈ Ioi (↑a : WithTop ι)
ha : (Ioi a).Nonempty
b : ι
bc' : b ∈ c'
hb : b ∈ Ioi a
⊢ (↑a : WithTop ι) ≤ (↑b : WithTop ι)

Tactic:
simpa using hb.le

Premises used: LT.lt.le
-- 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_1 : ⊤ ∈ Ioi (↑a : WithTop ι)
ha : (Ioi a).Nonempty
b : ι
bc' : b ∈ c'
hb : b ∈ Ioi a
inr :
  Membership.mem (γ := Set (Set (WithTop ι))) {s : Set (WithTop ι) | ∃ a ∈ d, s = Ioi a ∨ s = Iio a}
    (Ioi (↑b : WithTop ι))
⊢ IsOpen[generateFrom {s : Set (WithTop ι) | ∃ a ∈ d, s = Ioi a ∨ s = Iio a}] (Ioi (↑b : 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 : ι
hb_1 : ⊤ ∈ Ioi (↑a : WithTop ι)
ha : (Ioi a).Nonempty
b : ι
bc' : b ∈ c'
hb : b ∈ Ioi a
⊢ (↑b : WithTop ι) ∈ d

Tactic:
simp [d, bc']
-- 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_1 : ⊤ ∈ Ioi (↑a : WithTop ι)
ha : (Ioi a).Nonempty
b : ι
bc' : b ∈ c'
hb : b ∈ Ioi a
⊢ Membership.mem (γ := Set (Set (WithTop ι))) {s : Set (WithTop ι) | ∃ a ∈ d, s = Ioi a ∨ s = Iio a}
    (Ioi (↑b : WithTop ι))

Tactic:
exact ⟨b, by simp [d, bc'], Or.inl 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 : (↑b : WithTop ι) ∈ Ioi (↑a : WithTop ι)
⊢ a < b

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

Premises used: Set.mem_Ioi, 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 : a < b
⊢ ∃ t ∈ basis, b ∈ t ∧ t ⊆ Ioi a

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

Premises used: TopologicalSpace.IsTopologicalBasis.isOpen_iff, Iff.mp, isOpen_Ioi'
-- 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 : a < b
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 ⊆ Ioi a),
    ∃ t ⊆ Ioi (↑a : WithTop ι),
      IsOpen[generateFrom {s : Set (WithTop ι) | ∃ a ∈ d, s = Ioi a ∨ s = Iio a}] t ∧ (↑b : WithTop ι) ∈ t
⊢ ∃ t ⊆ Ioi (↑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 ⊆ Ioi a := h_basis.isOpen_iff.1 (isOpen_Ioi' a) b hb

Premises used: TopologicalSpace.IsTopologicalBasis.isOpen_iff, Set.Ioi, Iff.mp, isOpen_Ioi', 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 : 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
⊢ Membership.mem (γ := Set (WithTop ι)) ((⋂ z ∈ f, Ioi (↑z : WithTop ι)) ∩ ⋂ z ∈ g, Iio (↑z : WithTop ι))
    (↑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 : 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 : (⋂ z ∈ f, Ioi (↑z : WithTop ι)) ∩ ⋂ z ∈ g, Iio (↑z : WithTop ι) ⊆ Ioi (↑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 ι))
⊢ ∃ t ⊆ Ioi (↑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, ?_, ?_, 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 : 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
hw : Membership.mem (γ := Set (WithTop ι)) ((⋂ z ∈ f, Ioi (↑z : WithTop ι)) ∩ ⋂ z ∈ g, Iio (↑z : WithTop ι)) ⊤
⊢ ⊤ ∈ Ioi (↑a : WithTop ι)

Tactic:
simp
-- 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
w : ι
hw :
  Membership.mem (γ := Set (WithTop ι)) ((⋂ z ∈ f, Ioi (↑z : WithTop ι)) ∩ ⋂ z ∈ g, Iio (↑z : WithTop ι))
    (↑w : WithTop ι)
inr : a < w
⊢ (↑w : WithTop ι) ∈ Ioi (↑a : WithTop ι)

Tactic:
simp only [mem_Ioi, WithTop.coe_lt_coe]

Premises used: Set.mem_Ioi, 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 : 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
w : ι
hw :
  Membership.mem (γ := Set (WithTop ι)) ((⋂ z ∈ f, Ioi (↑z : WithTop ι)) ∩ ⋂ z ∈ g, Iio (↑z : WithTop ι))
    (↑w : WithTop ι)
inr : Membership.mem (γ := Set ι) ((⋂ a ∈ f, Ioi a) ∩ ⋂ a ∈ g, Iio a) w
⊢ a < w

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 : 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
w : ι
hw :
  Membership.mem (γ := Set (WithTop ι)) ((⋂ z ∈ f, Ioi (↑z : WithTop ι)) ∩ ⋂ z ∈ g, Iio (↑z : WithTop ι))
    (↑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 : 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
w : WithTop ι
hw : Membership.mem (γ := Set (WithTop ι)) ((⋂ z ∈ f, Ioi (↑z : WithTop ι)) ∩ ⋂ z ∈ g, Iio (↑z : WithTop ι)) w
inr :
  ∀ (hw : Membership.mem (γ := Set (WithTop ι)) ((⋂ z ∈ f, Ioi (↑z : WithTop ι)) ∩ ⋂ z ∈ g, Iio (↑z : WithTop ι)) ⊤),
    ⊤ ∈ Ioi (↑a : WithTop ι)
inr₁ :
  ∀ (w : ι)
    (hw :
      Membership.mem (γ := Set (WithTop ι)) ((⋂ z ∈ f, Ioi (↑z : WithTop ι)) ∩ ⋂ z ∈ g, Iio (↑z : WithTop ι))
        (↑w : WithTop ι)),
    (↑w : WithTop ι) ∈ Ioi (↑a : WithTop ι)
⊢ w ∈ Ioi (↑a : WithTop ι)

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

Premises used: Set.mem_Ioi, 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 : 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 : IsOpen[generateFrom {s : Set (WithTop ι) | ∃ a ∈ d, s = Ioi a ∨ s = Iio a}] (⋂ z ∈ f, Ioi (↑z : WithTop ι))
inr₁ : IsOpen[generateFrom {s : Set (WithTop ι) | ∃ a ∈ d, s = Ioi a ∨ s = Iio a}] (⋂ z ∈ g, Iio (↑z : WithTop ι))
⊢ IsOpen[generateFrom {s : Set (WithTop ι) | ∃ a ∈ d, s = Ioi a ∨ s = Iio a}]
    ((⋂ z ∈ f, Ioi (↑z : WithTop ι)) ∩ ⋂ z ∈ g, Iio (↑z : WithTop ι))

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 : 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 : f.Finite
inr₁ : ∀ i ∈ f, IsOpen[generateFrom {s : Set (WithTop ι) | ∃ a ∈ d, s = Ioi a ∨ s = Iio a}] (Ioi (↑i : WithTop ι))
⊢ IsOpen[generateFrom {s : Set (WithTop ι) | ∃ a ∈ d, s = Ioi a ∨ s = Iio a}] (⋂ z ∈ f, Ioi (↑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
⊢ f.Finite

Tactic:
f_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
⊢ f.Finite

Tactic:
exact f_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 ∈ f
inr :
  Membership.mem (γ := Set (Set (WithTop ι))) {s : Set (WithTop ι) | ∃ a ∈ d, s = Ioi a ∨ s = Iio a}
    (Ioi (↑i : WithTop ι))
⊢ IsOpen[generateFrom {s : Set (WithTop ι) | ∃ a ∈ d, s = Ioi a ∨ s = Iio a}] (Ioi (↑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 ∈ f
⊢ Membership.mem (γ := Set (Set (WithTop ι))) {s : Set (WithTop ι) | ∃ a ∈ d, s = Ioi a ∨ s = Iio a}
    (Ioi (↑i : WithTop ι))

Tactic:
grind