awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.Order.WithTop (goal)
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 ⊆ Ioi (↑a : WithTop ι),
    IsOpen[generateFrom {s : Set (WithTop ι) | ∃ a ∈ d, s = Ioi a ∨ s = Iio a}] t ∧ (↑b : WithTop ι) ∈ t
have 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
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
-- Lean 4 proof step from Mathlib.Topology.Order.WithTop (goal)
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
⊢ ∃ t ⊆ Ioi (↑a : WithTop ι),
    IsOpen[generateFrom {s : Set (WithTop ι) | ∃ a ∈ d, s = Ioi a ∨ s = Iio a}] t ∧ (↑b : WithTop ι) ∈ t
have inr : (⋂ z ∈ f, Ioi (↑z : WithTop ι)) ∩ ⋂ z ∈ g, Iio (↑z : WithTop ι) ⊆ Ioi (↑a : WithTop ι)
Tactic: refine ⟨(⋂ z ∈ f, Ioi z) ∩ ⋂ z ∈ g, Iio z, ?_, ?_, by simpa using hb⟩
-- Lean 4 proof step from Mathlib.Topology.Order.WithTop (goal)
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 ι)
⊢ ∃ t ⊆ Ioi (↑a : WithTop ι),
    IsOpen[generateFrom {s : Set (WithTop ι) | ∃ a ∈ d, s = Ioi a ∨ s = Iio a}] t ∧ (↑b : WithTop ι) ∈ t
have inr₁ : IsOpen[generateFrom {s : Set (WithTop ι) | ∃ a ∈ d, s = Ioi a ∨ s = Iio a}]
  ((⋂ z ∈ f, Ioi (↑z : WithTop ι)) ∩ ⋂ z ∈ g, Iio (↑z : WithTop ι))
Tactic: refine ⟨(⋂ z ∈ f, Ioi z) ∩ ⋂ z ∈ g, Iio z, ?_, ?_, by simpa using hb⟩
-- Lean 4 proof step from Mathlib.Topology.Order.WithTop (goal)
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 ι)
⊢ (↑w : WithTop ι) ∈ Ioi (↑a : WithTop ι)
have inr : a < w
Tactic: simp only [mem_Ioi, WithTop.coe_lt_coe]
-- Lean 4 proof step from Mathlib.Topology.Order.WithTop (goal)
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 ι)
⊢ a < w
have inr : Membership.mem (γ := Set ι) ((⋂ a ∈ f, Ioi a) ∩ ⋂ a ∈ g, Iio a) w
Tactic: apply hfg
-- Lean 4 proof step from Mathlib.Topology.Order.WithTop (goal)
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
⊢ w ∈ Ioi (↑a : WithTop ι)
have inr : ∀ (hw : Membership.mem (γ := Set (WithTop ι)) ((⋂ z ∈ f, Ioi (↑z : WithTop ι)) ∩ ⋂ z ∈ g, Iio (↑z : WithTop ι)) ⊤),
  ⊤ ∈ Ioi (↑a : WithTop ι)
Tactic: induction w with
          | top => simp
          | coe w =>
            simp only [mem_Ioi, WithTop.coe_lt_coe]
            apply hfg
            simpa using hw
Cleared hypotheses: w, hw
-- Lean 4 proof step from Mathlib.Topology.Order.WithTop (goal)
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 ι)
⊢ w ∈ Ioi (↑a : WithTop ι)
have inr₁ : ∀ (w : ι)
  (hw :
    Membership.mem (γ := Set (WithTop ι)) ((⋂ z ∈ f, Ioi (↑z : WithTop ι)) ∩ ⋂ z ∈ g, Iio (↑z : WithTop ι))
      (↑w : WithTop ι)),
  (↑w : WithTop ι) ∈ Ioi (↑a : WithTop ι)
Tactic: induction w with
          | top => simp
          | coe w =>
            simp only [mem_Ioi, WithTop.coe_lt_coe]
            apply hfg
            simpa using hw
Cleared hypotheses: w, hw
-- Lean 4 proof step from Mathlib.Topology.Order.WithTop (goal)
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
⊢ IsOpen[generateFrom {s : Set (WithTop ι) | ∃ a ∈ d, s = Ioi a ∨ s = Iio a}]
    ((⋂ z ∈ f, Ioi (↑z : WithTop ι)) ∩ ⋂ z ∈ g, Iio (↑z : WithTop ι))
have inr : IsOpen[generateFrom {s : Set (WithTop ι) | ∃ a ∈ d, s = Ioi a ∨ s = Iio a}] (⋂ z ∈ f, Ioi (↑z : WithTop ι))
Tactic: apply @IsOpen.inter _ (generateFrom {s | ∃ a ∈ d, s = Ioi a ∨ s = Iio a})
-- Lean 4 proof step from Mathlib.Topology.Order.WithTop (goal)
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 ι))
⊢ IsOpen[generateFrom {s : Set (WithTop ι) | ∃ a ∈ d, s = Ioi a ∨ s = Iio a}]
    ((⋂ z ∈ f, Ioi (↑z : WithTop ι)) ∩ ⋂ z ∈ g, Iio (↑z : WithTop ι))
have inr₁ : IsOpen[generateFrom {s : Set (WithTop ι) | ∃ a ∈ d, s = Ioi a ∨ s = Iio a}] (⋂ z ∈ g, Iio (↑z : WithTop ι))
Tactic: apply @IsOpen.inter _ (generateFrom {s | ∃ a ∈ d, s = Ioi a ∨ s = Iio a})
-- Lean 4 proof step from Mathlib.Topology.Order.WithTop (goal)
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
⊢ IsOpen[generateFrom {s : Set (WithTop ι) | ∃ a ∈ d, s = Ioi a ∨ s = Iio a}] (⋂ z ∈ f, Ioi (↑z : WithTop ι))
have inr₁ : ∀ i ∈ f, IsOpen[generateFrom {s : Set (WithTop ι) | ∃ a ∈ d, s = Ioi a ∨ s = Iio a}] (Ioi (↑i : WithTop ι))
Tactic: apply @Finite.isOpen_biInter _ _ (generateFrom {s | ∃ a ∈ d, s = Ioi a ∨ s = Iio a})
-- Lean 4 proof step from Mathlib.Topology.Order.WithTop (goal)
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
⊢ IsOpen[generateFrom {s : Set (WithTop ι) | ∃ a ∈ d, s = Ioi a ∨ s = Iio a}] (Ioi (↑i : WithTop ι))
have inr : Membership.mem (γ := Set (Set (WithTop ι))) {s : Set (WithTop ι) | ∃ a ∈ d, s = Ioi a ∨ s = Iio a}
  (Ioi (↑i : WithTop ι))
Tactic: apply isOpen_generateFrom_of_mem
-- Lean 4 proof step from Mathlib.Topology.Order.WithTop (goal)
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
⊢ IsOpen[generateFrom {s : Set (WithTop ι) | ∃ a ∈ d, s = Ioi a ∨ s = Iio a}] (⋂ z ∈ g, Iio (↑z : WithTop ι))
have inr₁ : ∀ i ∈ g, IsOpen[generateFrom {s : Set (WithTop ι) | ∃ a ∈ d, s = Ioi a ∨ s = Iio a}] (Iio (↑i : WithTop ι))
Tactic: apply @Finite.isOpen_biInter _ _ (generateFrom {s | ∃ a ∈ d, s = Ioi a ∨ s = Iio a})
-- Lean 4 proof step from Mathlib.Topology.Order.WithTop (goal)
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
⊢ IsOpen[generateFrom {s : Set (WithTop ι) | ∃ a ∈ d, s = Ioi a ∨ s = Iio a}] (Iio (↑i : WithTop ι))
have inr : Membership.mem (γ := Set (Set (WithTop ι))) {s : Set (WithTop ι) | ∃ a ∈ d, s = Ioi a ∨ s = Iio a}
  (Iio (↑i : WithTop ι))
Tactic: apply isOpen_generateFrom_of_mem
-- Lean 4 proof step from Mathlib.Topology.Order.WithTop (goal)
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
⊢ IsOpen[generateFrom {s : Set (WithTop ι) | ∃ a ∈ d, s = Ioi a ∨ s = Iio a}] (Iio ⊤)
have inr : Membership.mem (γ := Set (Set (WithTop ι))) {s : Set (WithTop ι) | ∃ a ∈ d, s = Ioi a ∨ s = Iio a} (Iio ⊤)
Tactic: apply isOpen_generateFrom_of_mem
-- Lean 4 proof step from Mathlib.Topology.Order.WithTop (goal)
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 : ι
⊢ IsOpen[generateFrom {s : Set (WithTop ι) | ∃ a ∈ d, s = Ioi a ∨ s = Iio a}] (Iio (↑a : WithTop ι))
have 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
Tactic: rw [@isOpen_iff_forall_mem_open]
-- Lean 4 proof step from Mathlib.Topology.Order.WithTop (hypothesis)
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 ι)
⊢ ∃ t ⊆ Iio (↑a : WithTop ι),
    IsOpen[generateFrom {s : Set (WithTop ι) | ∃ a ∈ d, s = Ioi a ∨ s = Iio a}] t ∧ (↑b : WithTop ι) ∈ t
have hb₁ : b < a
Tactic: simp only [mem_Iio, WithTop.coe_lt_coe] at hb
Cleared hypotheses: hb
-- Lean 4 proof step from Mathlib.Topology.Order.WithTop (goal)
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 ⊆ Iio (↑a : WithTop ι),
    IsOpen[generateFrom {s : Set (WithTop ι) | ∃ a ∈ d, s = Ioi a ∨ s = Iio a}] t ∧ (↑b : WithTop ι) ∈ t
have 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
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
-- Lean 4 proof step from Mathlib.Topology.Order.WithTop (goal)
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
⊢ ∃ t ⊆ Iio (↑a : WithTop ι),
    IsOpen[generateFrom {s : Set (WithTop ι) | ∃ a ∈ d, s = Ioi a ∨ s = Iio a}] t ∧ (↑b : WithTop ι) ∈ t
have inr : ((⋂ z ∈ f, Ioi (↑z : WithTop ι)) ∩ ⋂ z ∈ g, Iio (↑z : WithTop ι)) ∩ Iio ⊤ ⊆ Iio (↑a : WithTop ι)
Tactic: refine ⟨(⋂ z ∈ f, Ioi z) ∩ (⋂ z ∈ g, Iio z) ∩ Iio ⊤, ?_, ?_, by simpa using hb⟩
-- Lean 4 proof step from Mathlib.Topology.Order.WithTop (goal)
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 ι)
⊢ ∃ t ⊆ Iio (↑a : WithTop ι),
    IsOpen[generateFrom {s : Set (WithTop ι) | ∃ a ∈ d, s = Ioi a ∨ s = Iio a}] t ∧ (↑b : WithTop ι) ∈ t
have 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 ⊤)
Tactic: refine ⟨(⋂ z ∈ f, Ioi z) ∩ (⋂ z ∈ g, Iio z) ∩ Iio ⊤, ?_, ?_, by simpa using hb⟩