awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Order.UpperLowerSetTopology
Goal:
α : Type u_1
inst : Preorder α
inst_1 : TopologicalSpace α
inst_2 : Topology.IsLowerSet α
a : α
rw : (↑(lowerClosure {a}) : Set α) = Iic a
rw₁ : (↑(LowerSet.Iic a) : Set α) = Iic a
rw₂ rw₃ : Iic a = Iic a
⊢ nhdsKer {a} = Iic a

Tactic:
rw [nhdsKer_eq_lowerClosure, lowerClosure_singleton, LowerSet.coe_Iic]

Premises used: Topology.IsLowerSet.nhdsKer_eq_lowerClosure, lowerClosure_singleton, LowerSet.coe_Iic
-- Module: Mathlib.Topology.Order.UpperLowerSetTopology
Goal:
α : Type u_1
inst : Preorder α
inst_1 : TopologicalSpace α
inst_2 : Topology.IsLowerSet α
a : α
rw : 𝓟 (nhdsKer {a}) = 𝓟 (Iic a)
rw₁ rw₂ : 𝓟 (Iic a) = 𝓟 (Iic a)
⊢ 𝓝 a = 𝓟 (Iic a)

Tactic:
rw [← principal_nhdsKer_singleton, nhdsKer_singleton]

Premises used: principal_nhdsKer_singleton, Topology.IsLowerSet.nhdsKer_singleton
-- Module: Mathlib.Topology.Order.UpperLowerSetTopology
Goal:
α : Type u_1
inst : Preorder α
inst_1 : TopologicalSpace α
inst_2 : Topology.IsLowerSet α
s : Set α
rw : 𝓟 (nhdsKer s) = 𝓟 (↑(lowerClosure s) : Set α)
rw₁ rw₂ : 𝓟 (↑(lowerClosure s) : Set α) = 𝓟 (↑(lowerClosure s) : Set α)
⊢ 𝓝ˢ s = 𝓟 (↑(lowerClosure s) : Set α)

Tactic:
rw [← principal_nhdsKer, nhdsKer_eq_lowerClosure]

Premises used: Topology.IsLowerSet.nhdsKer_eq_lowerClosure, principal_nhdsKer
-- Module: Mathlib.Topology.Order.UpperLowerSetTopology
Goal:
α : Type u_4
inst : TopologicalSpace α
inst_1 : Preorder α
hα : ∀ (a : α), 𝓝 a = 𝓟 (Iic a)
⊢ inst = lowerSet α

Tactic:
simp [TopologicalSpace.ext_iff_nhds, hα, nhds_eq_principal_Iic]

Premises used: TopologicalSpace.ext_iff_nhds, Topology.IsLowerSet.nhds_eq_principal_Iic
-- Module: Mathlib.Topology.Order.UpperLowerSetTopology
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
inst_2 : TopologicalSpace α
inst_3 : TopologicalSpace β
inst_4 : Topology.IsLowerSet α
inst_5 : Topology.IsLowerSet β
f : α → β
rw :
  Monotone (α := αᵒᵈ) (β := βᵒᵈ) ((⇑toDual : (a : β) → βᵒᵈ) ∘ f ∘ (⇑ofDual : (a : αᵒᵈ) → α)) ↔
    Continuous[inst_2, inst_3] f
⊢ Monotone f ↔ Continuous[inst_2, inst_3] f

Tactic:
rw [← monotone_dual_iff]

Premises used: monotone_dual_iff
-- Module: Mathlib.Topology.Order.UpperLowerSetTopology
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
inst_2 : TopologicalSpace α
inst_3 : TopologicalSpace β
inst_4 : Topology.IsLowerSet α
inst_5 : Topology.IsLowerSet β
f : α → β
⊢ Monotone (α := αᵒᵈ) (β := βᵒᵈ) ((⇑toDual : (a : β) → βᵒᵈ) ∘ f ∘ (⇑ofDual : (a : αᵒᵈ) → α)) ↔
    Continuous[inst_2, inst_3] f

Tactic:
IsUpperSet.monotone_iff_continuous (α := αᵒᵈ) (β := βᵒᵈ)
    (f := (toDual ∘ f ∘ ofDual : αᵒᵈ → βᵒᵈ))

Premises used: Topology.IsUpperSet.monotone_iff_continuous, OrderDual
-- Module: Mathlib.Topology.Order.UpperLowerSetTopology
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
inst_2 : TopologicalSpace α
inst_3 : TopologicalSpace β
inst_4 : Topology.IsLowerSet α
inst_5 : Topology.IsLowerSet β
f : α → β
⊢ Monotone (α := αᵒᵈ) (β := βᵒᵈ) ((⇑toDual : (a : β) → βᵒᵈ) ∘ f ∘ (⇑ofDual : (a : αᵒᵈ) → α)) ↔
    Continuous[inst_2, inst_3] f

Tactic:
exact IsUpperSet.monotone_iff_continuous (α := αᵒᵈ) (β := βᵒᵈ)
    (f := (toDual ∘ f ∘ ofDual : αᵒᵈ → βᵒᵈ))

Premises used: Topology.IsUpperSet.monotone_iff_continuous
-- Module: Mathlib.Topology.Order.UpperLowerSetTopology
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
inst_2 : TopologicalSpace α
inst_3 : TopologicalSpace β
inst_4 : Topology.IsLowerSet α
inst_5 : IsLower β
f : α → β
hf : Monotone f
⊢ Continuous[inst_2, inst_3] f

Tactic:
IsUpperSet.monotone_to_upperTopology_continuous (α := αᵒᵈ) (β := βᵒᵈ) hf.dual

Premises used: Monotone.dual, Topology.IsUpperSet.monotone_to_upperTopology_continuous, OrderDual
-- Module: Mathlib.Topology.Order.UpperLowerSetTopology
Goal:
α : Type u_1
inst : Preorder α
t₁ t₂ : TopologicalSpace α
inst_1 : Topology.IsLowerSet α
inst_2 : IsLower α
s : Set α
hs : IsOpen[t₂] s
rw : IsLowerSet s
⊢ IsOpen[t₁] s

Tactic:
rw [@isOpen_iff_isLowerSet α _ t₁]

Premises used: Topology.IsLowerSet.isOpen_iff_isLowerSet
-- Module: Mathlib.Topology.Order.UpperLowerSetTopology
Goal:
α : Type u_1
inst : Preorder α
t₁ t₂ : TopologicalSpace α
inst_1 : Topology.IsLowerSet α
inst_2 : IsLower α
s : Set α
hs : IsOpen[t₂] s
⊢ IsLowerSet s

Tactic:
IsLower.isLowerSet_of_isOpen hs

Premises used: Topology.IsLower.isLowerSet_of_isOpen
-- Module: Mathlib.Topology.Order.UpperLowerSetTopology
Goal:
α : Type u_1
inst : Preorder α
t₁ t₂ : TopologicalSpace α
inst_1 : Topology.IsLowerSet α
inst_2 : IsLower α
s : Set α
hs : IsOpen[t₂] s
⊢ IsLowerSet s

Tactic:
exact IsLower.isLowerSet_of_isOpen hs

Premises used: Topology.IsLower.isLowerSet_of_isOpen
-- Module: Mathlib.Topology.Order.UpperLowerSetTopology
Goal:
α : Type u_1
inst : Preorder α
inst_1 : TopologicalSpace α
mp : Topology.IsUpperSet.{u_1} αᵒᵈ → Topology.IsLowerSet α
mpr : Topology.IsLowerSet α → Topology.IsUpperSet.{u_1} αᵒᵈ
⊢ Topology.IsUpperSet.{u_1} αᵒᵈ ↔ Topology.IsLowerSet α

Tactic:
constructor
-- Module: Mathlib.Topology.Order.UpperLowerSetTopology
Goal:
α : Type u_1
inst : Preorder α
inst_1 : TopologicalSpace α
⊢ Topology.IsUpperSet.{u_1} αᵒᵈ → Topology.IsLowerSet α

Tactic:
apply OrderDual.instIsLowerSet

Premises used: OrderDual.instIsLowerSet
-- Module: Mathlib.Topology.Order.UpperLowerSetTopology
Goal:
α : Type u_1
inst : Preorder α
inst_1 : TopologicalSpace α
⊢ Topology.IsLowerSet α → Topology.IsUpperSet.{u_1} αᵒᵈ

Tactic:
apply OrderDual.instIsUpperSet

Premises used: OrderDual.instIsUpperSet
-- Module: Mathlib.Topology.Order.UpperLowerSetTopology
Goal:
α : Type u_1
inst : Preorder α
inst_1 : TopologicalSpace α
⊢ Topology.IsLowerSet.{u_1} αᵒᵈ ↔ Topology.IsUpperSet α

Tactic:
isUpperSet_orderDual.symm

Premises used: Topology.isUpperSet_orderDual, OrderDual, Iff.symm
-- Module: Mathlib.Topology.Order.UpperLowerSetTopology
Goal:
α : Type u_1
inst : Preorder α
⊢ Eq.{u_1 + 1} (α := C(WithUpperSet α, WithUpperSet α)) (map OrderHom.id) (ContinuousMap.id (WithUpperSet α))

Tactic:
rfl

Premises used: ContinuousMap.id, Topology.WithUpperSet.map, rfl
-- Module: Mathlib.Topology.Order.UpperLowerSetTopology
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : Preorder α
inst_1 : Preorder β
inst_2 : Preorder γ
g : β →o γ
f : α →o β
⊢ map (g.comp f) = (map g).comp (map f)

Tactic:
rfl

Premises used: ContinuousMap.comp, Topology.WithUpperSet.map, rfl
-- Module: Mathlib.Topology.Order.UpperLowerSetTopology
Goal:
α : Type u_1
inst : Preorder α
a b : α
simp_rw :
  Subset (α := Set (WithUpperSet α))
      (closure[instTopologicalSpace]
        (singleton (α := WithUpperSet α) ((toUpperSet : (a : α) → WithUpperSet α) b : WithUpperSet α)))
      (closure[instTopologicalSpace]
        (singleton (α := WithUpperSet α) ((toUpperSet : (a : α) → WithUpperSet α) a : WithUpperSet α))) ↔
    b ≤ a
simp_rw₁ :
  Subset (α := Set (WithUpperSet α)) (Iic ((toUpperSet : (a : α) → WithUpperSet α) b) : Set (WithUpperSet α))
      (Iic ((toUpperSet : (a : α) → WithUpperSet α) a) : Set (WithUpperSet α)) ↔
    b ≤ a
simp_rw₂ :
  LE.le (α := WithUpperSet α) ((toUpperSet : (a : α) → WithUpperSet α) b : WithUpperSet α)
      ((toUpperSet : (a : α) → WithUpperSet α) a : WithUpperSet α) ↔
    b ≤ a
⊢ Specializes (X := WithUpperSet α) ((toUpperSet : (a : α) → WithUpperSet α) a : WithUpperSet α)
      ((toUpperSet : (a : α) → WithUpperSet α) b : WithUpperSet α) ↔
    b ≤ a

Tactic:
simp_rw [specializes_iff_closure_subset, IsUpperSet.closure_singleton, Iic_subset_Iic,
    toUpperSet_le_iff]

Premises used: Set.Iic_subset_Iic, Topology.WithUpperSet.toUpperSet_le_iff, Topology.IsUpperSet.closure_singleton, specializes_iff_closure_subset
-- Module: Mathlib.Topology.Order.UpperLowerSetTopology
Goal:
α : Type u_1
inst : Preorder α
a b : WithUpperSet α
⊢ LE.le (α := α) ((ofUpperSet : (a : WithUpperSet α) → α) a : α) ((ofUpperSet : (a : WithUpperSet α) → α) b : α) ↔ b ⤳ a

Tactic:
toUpperSet_specializes_toUpperSet.symm

Premises used: Topology.WithUpperSet.toUpperSet_specializes_toUpperSet, Iff.symm
-- Module: Mathlib.Topology.Order.UpperLowerSetTopology
Goal:
α : Type u_1
inst : Preorder α
s : Set (WithUpperSet α)
⊢ IsUpperSet (α := α) ((⇑toUpperSet : (a : α) → WithUpperSet α) ⁻¹' s) ↔ IsOpen[instTopologicalSpace] s

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf, IsUpperSet, Set.preimage, IsOpen
-- Module: Mathlib.Topology.Order.UpperLowerSetTopology
Goal:
α : Type u_1
inst : Preorder α
s : Set α
⊢ IsOpen[instTopologicalSpace] ((⇑ofUpperSet : (a : WithUpperSet α) → α) ⁻¹' s) ↔ IsUpperSet s

Tactic:
isUpperSet_toUpperSet_preimage.symm

Premises used: Set.Mem, setOf, Topology.WithUpperSet.isUpperSet_toUpperSet_preimage, Set.preimage, Iff.symm
-- Module: Mathlib.Topology.Order.UpperLowerSetTopology
Goal:
α : Type u_1
inst : Preorder α
⊢ Eq.{u_1 + 1} (α := C(WithLowerSet α, WithLowerSet α)) (map OrderHom.id) (ContinuousMap.id (WithLowerSet α))

Tactic:
rfl

Premises used: ContinuousMap.id, Topology.WithLowerSet.map, rfl
-- Module: Mathlib.Topology.Order.UpperLowerSetTopology
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : Preorder α
inst_1 : Preorder β
inst_2 : Preorder γ
g : β →o γ
f : α →o β
⊢ map (g.comp f) = (map g).comp (map f)

Tactic:
rfl

Premises used: ContinuousMap.comp, Topology.WithLowerSet.map, rfl
-- Module: Mathlib.Topology.Order.UpperLowerSetTopology
Goal:
α : Type u_1
inst : Preorder α
a b : α
simp_rw :
  Subset (α := Set (WithLowerSet α))
      (closure[instTopologicalSpace]
        (singleton (α := WithLowerSet α) ((toLowerSet : (a : α) → WithLowerSet α) b : WithLowerSet α)))
      (closure[instTopologicalSpace]
        (singleton (α := WithLowerSet α) ((toLowerSet : (a : α) → WithLowerSet α) a : WithLowerSet α))) ↔
    a ≤ b
simp_rw₁ :
  Subset (α := Set (WithLowerSet α)) (Ici ((toLowerSet : (a : α) → WithLowerSet α) b) : Set (WithLowerSet α))
      (Ici ((toLowerSet : (a : α) → WithLowerSet α) a) : Set (WithLowerSet α)) ↔
    a ≤ b
simp_rw₂ :
  LE.le (α := WithLowerSet α) ((toLowerSet : (a : α) → WithLowerSet α) a : WithLowerSet α)
      ((toLowerSet : (a : α) → WithLowerSet α) b : WithLowerSet α) ↔
    a ≤ b
⊢ Specializes (X := WithLowerSet α) ((toLowerSet : (a : α) → WithLowerSet α) a : WithLowerSet α)
      ((toLowerSet : (a : α) → WithLowerSet α) b : WithLowerSet α) ↔
    a ≤ b

Tactic:
simp_rw [specializes_iff_closure_subset, IsLowerSet.closure_singleton, Ici_subset_Ici,
    toLowerSet_le_iff]

Premises used: Topology.IsLowerSet.closure_singleton, Set.Ici_subset_Ici, Topology.WithLowerSet.toLowerSet_le_iff, specializes_iff_closure_subset
-- Module: Mathlib.Topology.Order.UpperLowerSetTopology
Goal:
α : Type u_1
inst : Preorder α
a b : WithLowerSet α
⊢ LE.le (α := α) ((ofLowerSet : (a : WithLowerSet α) → α) a : α) ((ofLowerSet : (a : WithLowerSet α) → α) b : α) ↔ a ⤳ b

Tactic:
toLowerSet_specializes_toLowerSet.symm

Premises used: Iff.symm, Topology.WithLowerSet.toLowerSet_specializes_toLowerSet
-- Module: Mathlib.Topology.Order.UpperLowerSetTopology
Goal:
α : Type u_1
inst : Preorder α
s : Set (WithLowerSet α)
⊢ IsLowerSet (α := α) ((⇑toLowerSet : (a : α) → WithLowerSet α) ⁻¹' s) ↔ IsOpen[instTopologicalSpace] s

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf, Set.preimage, IsLowerSet, IsOpen
-- Module: Mathlib.Topology.Order.UpperLowerSetTopology
Goal:
α : Type u_1
inst : Preorder α
s : Set α
⊢ IsOpen[instTopologicalSpace] ((⇑ofLowerSet : (a : WithLowerSet α) → α) ⁻¹' s) ↔ IsLowerSet s

Tactic:
isLowerSet_toLowerSet_preimage.symm

Premises used: Set.Mem, setOf, Topology.WithLowerSet.isLowerSet_toLowerSet_preimage, Set.preimage, Iff.symm
-- Module: Mathlib.Topology.Order.WithTop
Goal:
ι : Type u_1
inst : Preorder ι
inst_1 : TopologicalSpace ι
inst_2 : OrderTopology ι
⊢ OrderTopology.{u_1} (WithTop ι)

Tactic:
⟨rfl⟩

Premises used: OrderTopology.mk, rfl
-- Module: Mathlib.Topology.Order.WithTop
Goal:
ι : Type u_1
inst : Preorder ι
ts : TopologicalSpace ι
ht : OrderTopology ι
inst_1 : SecondCountableTopology ι
inl : ∀ (hι : IsEmpty ι), SecondCountableTopology.{u_1} (WithTop ι)
inr : ∀ (x₀ : ι), SecondCountableTopology.{u_1} (WithTop ι)
⊢ SecondCountableTopology.{u_1} (WithTop ι)

Tactic:
rcases isEmpty_or_nonempty ι with hι | ⟨⟨x₀⟩⟩

Premises used: isEmpty_or_nonempty
-- Module: Mathlib.Topology.Order.WithTop
Goal:
ι : Type u_1
inst : Preorder ι
ts : TopologicalSpace ι
ht : OrderTopology ι
inst_1 : SecondCountableTopology ι
hι : IsEmpty ι
⊢ SecondCountableTopology.{u_1} (WithTop ι)

Tactic:
infer_instance
-- Module: Mathlib.Topology.Order.WithTop
Goal:
ι : Type u_1
inst : Preorder ι
ts : TopologicalSpace ι
ht : OrderTopology ι
inst_1 : SecondCountableTopology ι
x₀ : ι
⊢ ∃ (c : Set ι), c.Countable ∧ ts = generateFrom {s : Set ι | ∃ a ∈ c, s = Ioi a ∨ s = Iio a}

Tactic:
exists_countable_generateFrom_Ioi_Iio ι

Premises used: exists_countable_generateFrom_Ioi_Iio
-- Module: Mathlib.Topology.Order.WithTop
Goal:
ι : Type u_1
inst : Preorder ι
ts : TopologicalSpace ι
ht : OrderTopology ι
inst_1 : SecondCountableTopology ι
x₀ : ι
inr :
  ∀ (c : Set ι) (c_count : c.Countable) (hc : ts = generateFrom {s : Set ι | ∃ a ∈ c, s = Ioi a ∨ s = Iio a}),
    SecondCountableTopology.{u_1} (WithTop ι)
⊢ SecondCountableTopology.{u_1} (WithTop ι)

Tactic:
obtain ⟨c, c_count, hc⟩ : ∃ (c : Set ι), c.Countable ∧
      ts = generateFrom { s | ∃ a ∈ c, s = Ioi a ∨ s = Iio a } :=
    exists_countable_generateFrom_Ioi_Iio ι

Premises used: exists_countable_generateFrom_Ioi_Iio, Set
-- 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'.Countable ∧ Dense c'

Tactic:
SeparableSpace.exists_countable_dense

Premises used: TopologicalSpace.SeparableSpace.exists_countable_dense
-- 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}
inr : ∀ (c' : Set ι) (c'_count : c'.Countable) (hc' : Dense c'), SecondCountableTopology.{u_1} (WithTop ι)
⊢ SecondCountableTopology.{u_1} (WithTop ι)

Tactic:
obtain ⟨c', c'_count, hc'⟩ : ∃ c' : Set ι, c'.Countable ∧ Dense c' :=
    SeparableSpace.exists_countable_dense

Premises used: TopologicalSpace.SeparableSpace.exists_countable_dense, Set
-- 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 ι)}
H :
  Eq.{u_1 + 1} (α := TopologicalSpace (WithTop ι)) instWithTopOfOrderTopology
    (generateFrom {s : Set (WithTop ι) | ∃ a ∈ d, s = Ioi a ∨ s = Iio a})
rw rw₁ : Eq.{u_1 + 1} (α := TopologicalSpace (WithTop ι)) instWithTopOfOrderTopology instWithTopOfOrderTopology
⊢ Eq.{u_1 + 1} (α := TopologicalSpace (WithTop ι)) instWithTopOfOrderTopology
    (generateFrom {s : Set (WithTop ι) | ∃ a ∈ d, s = Ioi a ∨ s = Iio a})

Tactic:
rw [← H]
-- 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 ι)}
H :
  Eq.{u_1 + 1} (α := TopologicalSpace (WithTop ι)) instWithTopOfOrderTopology
    (generateFrom {s : Set (WithTop ι) | ∃ a ∈ d, s = Ioi a ∨ s = Iio a})
refine : Set.Countable.{u_1} (α := Set (WithTop ι)) {s : Set (WithTop ι) | ∃ a ∈ d, s = Ioi a ∨ s = Iio a}
⊢ SecondCountableTopology.{u_1} (WithTop ι)

Tactic:
refine ⟨{s | ∃ a ∈ d, s = Ioi a ∨ s = Iio a}, ?_, by rw [← H]⟩
-- 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 ι)}
H :
  Eq.{u_1 + 1} (α := TopologicalSpace (WithTop ι)) instWithTopOfOrderTopology
    (generateFrom {s : Set (WithTop ι) | ∃ a ∈ d, s = Ioi a ∨ s = Iio a})
⊢ Set.Countable (α := 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 ι)}
H :
  Eq.{u_1 + 1} (α := TopologicalSpace (WithTop ι)) instWithTopOfOrderTopology
    (generateFrom {s : Set (WithTop ι) | ∃ a ∈ d, s = Ioi a ∨ s = Iio a})
⊢ Set.Countable (α := WithTop ι) {(↑x₁ : 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 ι)}
H :
  Eq.{u_1 + 1} (α := TopologicalSpace (WithTop ι)) instWithTopOfOrderTopology
    (generateFrom {s : Set (WithTop ι) | ∃ a ∈ d, s = Ioi a ∨ s = Iio a})
⊢ d.Countable

Tactic:
have d_count : d.Countable :=
      (((c_count.image _).union (c'_count.image _)).union (by simp)).union (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 ι)}
H :
  Eq.{u_1 + 1} (α := TopologicalSpace (WithTop ι)) instWithTopOfOrderTopology
    (generateFrom {s : Set (WithTop ι) | ∃ a ∈ d, s = Ioi a ∨ s = Iio a})
d_count : d.Countable
⊢ {s : Set (WithTop ι) | ∃ a ∈ d, s = Ioi a ∨ s = Iio a} = Ioi '' d ∪ Iio '' d

Tactic:
grind (splits := 12)
-- 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 ι)}
H :
  Eq.{u_1 + 1} (α := TopologicalSpace (WithTop ι)) instWithTopOfOrderTopology
    (generateFrom {s : Set (WithTop ι) | ∃ a ∈ d, s = Ioi a ∨ s = Iio a})
d_count : d.Countable
⊢ {s : Set (WithTop ι) | ∃ a ∈ d, s = Ioi a ∨ s = Iio a} = Ioi '' d ∪ Iio '' d

Tactic:
have : {s | ∃ a ∈ d, s = Ioi a ∨ s = Iio a} = Ioi '' d ∪ Iio '' d := by
      #adaptation_note /-- Before leanprover/lean4#13166, this was just `grind`.
      The new canonicalizer using `isDefEq` less,
      and so does not unify as many of the conditions that `grind` wants to case split on.
      Alternatively `ext; simp; grind` work here. -/
      grind (splits := 12)
-- 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 ι)}
H :
  Eq.{u_1 + 1} (α := TopologicalSpace (WithTop ι)) instWithTopOfOrderTopology
    (generateFrom {s : Set (WithTop ι) | ∃ a ∈ d, s = Ioi a ∨ s = Iio a})
d_count : d.Countable
this : {s : Set (WithTop ι) | ∃ a ∈ d, s = Ioi a ∨ s = Iio a} = Ioi '' d ∪ Iio '' d
rw : (Ioi '' d ∪ Iio '' d).Countable
⊢ Set.Countable.{u_1} (α := Set (WithTop ι)) {s : Set (WithTop ι) | ∃ a ∈ d, s = Ioi a ∨ s = Iio a}

Tactic:
rw [this]
-- 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 ι)}
H :
  Eq.{u_1 + 1} (α := TopologicalSpace (WithTop ι)) instWithTopOfOrderTopology
    (generateFrom {s : Set (WithTop ι) | ∃ a ∈ d, s = Ioi a ∨ s = Iio a})
d_count : d.Countable
this : {s : Set (WithTop ι) | ∃ a ∈ d, s = Ioi a ∨ s = Iio a} = Ioi '' d ∪ Iio '' d
⊢ (Ioi '' d ∪ Iio '' d).Countable

Tactic:
(d_count.image _).union (d_count.image _)

Premises used: Set.Countable.image, Set.Countable.union
-- 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 ι)}
H :
  Eq.{u_1 + 1} (α := TopologicalSpace (WithTop ι)) instWithTopOfOrderTopology
    (generateFrom {s : Set (WithTop ι) | ∃ a ∈ d, s = Ioi a ∨ s = Iio a})
d_count : d.Countable
this : {s : Set (WithTop ι) | ∃ a ∈ d, s = Ioi a ∨ s = Iio a} = Ioi '' d ∪ Iio '' d
⊢ (Ioi '' d ∪ Iio '' d).Countable

Tactic:
exact (d_count.image _).union (d_count.image _)

Premises used: Set.Countable.image, Set.Countable.union