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_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 ι)
⊢ (↑w : WithTop ι) ∈ Iio (↑a : WithTop ι)
have inr : w < a
Tactic: simp only [mem_Iio, 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 : 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 ι)
⊢ w < a
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 : 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
⊢ w ∈ Iio (↑a : WithTop ι)
have inr : ∀
  (hw :
    Membership.mem (γ := Set (WithTop ι)) (((⋂ z ∈ f, Ioi (↑z : WithTop ι)) ∩ ⋂ z ∈ g, Iio (↑z : WithTop ι)) ∩ Iio ⊤)
      ⊤),
  ⊤ ∈ 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
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 : 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 ι)
⊢ w ∈ Iio (↑a : WithTop ι)
have 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 ι)
Tactic: induction w with
          | top => simp at hw
          | coe w =>
            simp only [mem_Iio, 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 : 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
⊢ IsOpen[generateFrom {s : Set (WithTop ι) | ∃ a ∈ d, s = Ioi a ∨ s = Iio a}]
    (((⋂ z ∈ f, Ioi (↑z : WithTop ι)) ∩ ⋂ z ∈ g, Iio (↑z : WithTop ι)) ∩ Iio ⊤)
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: 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 : 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 ι))
⊢ IsOpen[generateFrom {s : Set (WithTop ι) | ∃ a ∈ d, s = Ioi a ∨ s = Iio a}]
    (((⋂ z ∈ f, Ioi (↑z : WithTop ι)) ∩ ⋂ z ∈ g, Iio (↑z : WithTop ι)) ∩ Iio ⊤)
have inr₁ : IsOpen[generateFrom {s : Set (WithTop ι) | ∃ a ∈ d, s = Ioi a ∨ s = Iio a}] (Iio ⊤)
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 : 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
⊢ 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 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
⊢ 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 : 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 ι))
⊢ 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 : 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 : 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 : 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
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 : 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 : 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 : 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
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
a : ι
b : WithTop ι
hb : b ∈ Iio (↑a : WithTop ι)
⊢ ∃ t ⊆ Iio (↑a : WithTop ι), IsOpen[generateFrom {s : Set (WithTop ι) | ∃ a ∈ d, s = Ioi a ∨ s = Iio a}] t ∧ b ∈ t
have inr : ∀ (hb : ⊤ ∈ Iio (↑a : WithTop ι)),
  ∃ t ⊆ Iio (↑a : WithTop ι), IsOpen[generateFrom {s : Set (WithTop ι) | ∃ a ∈ d, s = Ioi a ∨ s = Iio a}] t ∧ ⊤ ∈ t
Tactic: induction b with
      | top => simp at hb
      | coe b =>
        -- `b` can not be equal to `⊤`, so it comes from `ι`. In `ι` we can find a finite
        -- intersection of our sets containing `b` and contained in `Iio a`. We lift it
        -- to `WithTop ι`, and intersect with `Iio ⊤` (which is also in our set) to exclude `⊤`.
        simp only [mem_Iio, WithTop.coe_lt_coe] at hb
        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
        refine ⟨(⋂ z ∈ f, Ioi z) ∩ (⋂ z ∈ g, Iio z) ∩ Iio ⊤, ?_, ?_, by simpa using hb⟩
        · intro w hw
          induction w with
          | top => simp at hw
          | coe w =>
            simp only [mem_Iio, WithTop.coe_lt_coe]
            apply hfg
            simpa using hw
        · apply @IsOpen.inter _ (generateFrom {s | ∃ a ∈ d, s = Ioi a ∨ s = Iio a}); swap
          · apply isOpen_generateFrom_of_mem
            simp [d]
          apply @IsOpen.inter _ (generateFrom {s | ∃ a ∈ d, s = Ioi a ∨ s = Iio a})
          · apply @Finite.isOpen_biInter _ _ (generateFrom {s | ∃ a ∈ d, s = Ioi a ∨ s = Iio a})
            · exact f_fin
            · intro i hi
              apply isOpen_generateFrom_of_mem
              grind
          · apply @Finite.isOpen_biInter _ _ (generateFrom {s | ∃ a ∈ d, s = Ioi a ∨ s = Iio a})
            · exact g_fin
            · intro i hi
              apply isOpen_generateFrom_of_mem
              grind
Cleared hypotheses: 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 : WithTop ι
hb : b ∈ Iio (↑a : WithTop ι)
inr :
  ∀ (hb : ⊤ ∈ Iio (↑a : WithTop ι)),
    ∃ t ⊆ Iio (↑a : WithTop ι), IsOpen[generateFrom {s : Set (WithTop ι) | ∃ a ∈ d, s = Ioi a ∨ s = Iio a}] t ∧ ⊤ ∈ t
⊢ ∃ t ⊆ Iio (↑a : WithTop ι), IsOpen[generateFrom {s : Set (WithTop ι) | ∃ a ∈ d, s = Ioi a ∨ s = Iio a}] t ∧ b ∈ t
have inr₁ : ∀ (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
Tactic: induction b with
      | top => simp at hb
      | coe b =>
        -- `b` can not be equal to `⊤`, so it comes from `ι`. In `ι` we can find a finite
        -- intersection of our sets containing `b` and contained in `Iio a`. We lift it
        -- to `WithTop ι`, and intersect with `Iio ⊤` (which is also in our set) to exclude `⊤`.
        simp only [mem_Iio, WithTop.coe_lt_coe] at hb
        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
        refine ⟨(⋂ z ∈ f, Ioi z) ∩ (⋂ z ∈ g, Iio z) ∩ Iio ⊤, ?_, ?_, by simpa using hb⟩
        · intro w hw
          induction w with
          | top => simp at hw
          | coe w =>
            simp only [mem_Iio, WithTop.coe_lt_coe]
            apply hfg
            simpa using hw
        · apply @IsOpen.inter _ (generateFrom {s | ∃ a ∈ d, s = Ioi a ∨ s = Iio a}); swap
          · apply isOpen_generateFrom_of_mem
            simp [d]
          apply @IsOpen.inter _ (generateFrom {s | ∃ a ∈ d, s = Ioi a ∨ s = Iio a})
          · apply @Finite.isOpen_biInter _ _ (generateFrom {s | ∃ a ∈ d, s = Ioi a ∨ s = Iio a})
            · exact f_fin
            · intro i hi
              apply isOpen_generateFrom_of_mem
              grind
          · apply @Finite.isOpen_biInter _ _ (generateFrom {s | ∃ a ∈ d, s = Ioi a ∨ s = Iio a})
            · exact g_fin
            · intro i hi
              apply isOpen_generateFrom_of_mem
              grind
Cleared hypotheses: b, hb