awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.Order.UpperLowerSetTopology (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
inst_2 : TopologicalSpace α
inst_3 : TopologicalSpace β
inst_4 : Topology.IsUpperSet α
inst_5 : Topology.IsUpperSet β
f : α → β
hf : Continuous[inst_2, inst_3] f
a b : α
hab : Membership.mem (γ := Set α) (closure[inst_2] {b}) a
⊢ a ∈ closure[inst_2] (f ⁻¹' {f b})
have mpr : closure[inst_2] {b} ⊆ closure[inst_2] (f ⁻¹' {f b})
Tactic: apply mem_of_mem_of_subset hab
-- Lean 4 proof step from Mathlib.Topology.Order.UpperLowerSetTopology (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
inst_2 : TopologicalSpace α
inst_3 : TopologicalSpace β
inst_4 : Topology.IsUpperSet α
inst_5 : Topology.IsUpperSet β
f : α → β
hf : Continuous[inst_2, inst_3] f
a b : α
hab : Membership.mem (γ := Set α) (closure[inst_2] {b}) a
⊢ closure[inst_2] {b} ⊆ closure[inst_2] (f ⁻¹' {f b})
have mpr : {b} ⊆ f ⁻¹' {f b}
Tactic: apply closure_mono
-- Lean 4 proof step from Mathlib.Topology.Order.UpperLowerSetTopology (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
inst_2 : TopologicalSpace α
inst_3 : TopologicalSpace β
inst_4 : Topology.IsUpperSet α
inst_5 : Topology.IsUpperSet β
f : α → β
hf : Continuous[inst_2, inst_3] f
a b : α
hab : Membership.mem (γ := Set α) (closure[inst_2] {b}) a
⊢ {b} ⊆ f ⁻¹' {f b}
have mpr : b ∈ f ⁻¹' {f b}
Tactic: rw [singleton_subset_iff, mem_preimage, mem_singleton_iff]
-- Lean 4 proof step from Mathlib.Topology.Order.UpperLowerSetTopology (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
inst_2 : TopologicalSpace α
inst_3 : TopologicalSpace β
inst_4 : Topology.IsUpperSet α
inst_5 : Topology.IsUpperSet β
f : α → β
hf : Continuous[inst_2, inst_3] f
a b : α
hab : Membership.mem (γ := Set α) (closure[inst_2] {b}) a
mpr : b ∈ f ⁻¹' {f b}
⊢ {b} ⊆ f ⁻¹' {f b}
have mpr₁ : Membership.mem (γ := Set β) {f b} (f b)
Tactic: rw [singleton_subset_iff, mem_preimage, mem_singleton_iff]
-- Lean 4 proof step from Mathlib.Topology.Order.UpperLowerSetTopology (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
inst_2 : TopologicalSpace α
inst_3 : TopologicalSpace β
inst_4 : Topology.IsUpperSet α
inst_5 : Topology.IsUpperSet β
f : α → β
hf : Continuous[inst_2, inst_3] f
a b : α
hab : Membership.mem (γ := Set α) (closure[inst_2] {b}) a
mpr : b ∈ f ⁻¹' {f b}
mpr₁ : Membership.mem (γ := Set β) {f b} (f b)
⊢ {b} ⊆ f ⁻¹' {f b}
have mpr₂ : f b = f b
Tactic: rw [singleton_subset_iff, mem_preimage, mem_singleton_iff]
-- Lean 4 proof step from Mathlib.Topology.Order.UpperLowerSetTopology (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
inst_2 : TopologicalSpace α
inst_3 : TopologicalSpace β
inst_4 : Topology.IsUpperSet α
inst_5 : IsUpper β
f : α → β
hf : Monotone f
⊢ Continuous[inst_2, inst_3] f
have simp_rw : ∀ (s : Set β), IsOpen[inst_3] s → IsUpperSet (f ⁻¹' s)
Tactic: simp_rw [continuous_def, isOpen_iff_isUpperSet]
-- Lean 4 proof step from Mathlib.Topology.Order.UpperLowerSetTopology (goal)
Goal:
α : Type u_1
inst : Preorder α
t₁ t₂ : TopologicalSpace α
inst_1 : Topology.IsUpperSet α
inst_2 : IsUpper α
s : Set α
hs : IsOpen[t₂] s
⊢ IsOpen[t₁] s
have rw : IsUpperSet s
Tactic: rw [@isOpen_iff_isUpperSet α _ t₁]
-- Lean 4 proof step from Mathlib.Topology.Order.UpperLowerSetTopology (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : Preorder α
inst_1 : TopologicalSpace α
inst_2 : Topology.IsLowerSet α
s : Set α
⊢ Eq.{u_1 + 1} (α := TopologicalSpace αᵒᵈ) OrderDual.instTopologicalSpace (upperSet αᵒᵈ)
have a : ∀ (x : Set αᵒᵈ), IsOpen[OrderDual.instTopologicalSpace] x ↔ IsOpen[upperSet αᵒᵈ] x
Tactic: ext
-- Lean 4 proof step from Mathlib.Topology.Order.UpperLowerSetTopology (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : Preorder α
inst_1 : TopologicalSpace α
inst_2 : Topology.IsLowerSet α
s : Set α
x : Set αᵒᵈ
⊢ IsOpen[OrderDual.instTopologicalSpace] x ↔ IsOpen[upperSet αᵒᵈ] x
have a : IsOpen[OrderDual.instTopologicalSpace] x ↔ IsOpen[upperSet αᵒᵈ] x
Tactic: rw [IsLowerSet.topology_eq α]
-- Lean 4 proof step from Mathlib.Topology.Order.UpperLowerSetTopology (goal)
Goal:
α : Type u_1
inst : Preorder α
inst_1 : TopologicalSpace α
inst_2 : Topology.IsLowerSet α
s : Set α
⊢ IsOpen[inst_1] s ↔ IsLowerSet s
have rw : IsOpen[lowerSet α] s ↔ IsLowerSet s
Tactic: rw [topology_eq α]
-- Lean 4 proof step from Mathlib.Topology.Order.UpperLowerSetTopology (goal)
Goal:
α : Type u_1
inst : Preorder α
inst_1 : TopologicalSpace α
inst_2 : Topology.IsLowerSet α
s : Set α
⊢ IsClosed[inst_1] s ↔ IsUpperSet s
have rw : IsOpen[inst_1] sᶜ ↔ IsUpperSet s
Tactic: rw [← isOpen_compl_iff, isOpen_iff_isLowerSet, isUpperSet_compl.symm, compl_compl]
-- Lean 4 proof step from Mathlib.Topology.Order.UpperLowerSetTopology (goal)
Goal:
α : Type u_1
inst : Preorder α
inst_1 : TopologicalSpace α
inst_2 : Topology.IsLowerSet α
s : Set α
rw : IsOpen[inst_1] sᶜ ↔ IsUpperSet s
⊢ IsClosed[inst_1] s ↔ IsUpperSet s
have rw₁ : IsLowerSet sᶜ ↔ IsUpperSet s
Tactic: rw [← isOpen_compl_iff, isOpen_iff_isLowerSet, isUpperSet_compl.symm, compl_compl]
-- Lean 4 proof step from Mathlib.Topology.Order.UpperLowerSetTopology (goal)
Goal:
α : Type u_1
inst : Preorder α
inst_1 : TopologicalSpace α
inst_2 : Topology.IsLowerSet α
s : Set α
rw : IsOpen[inst_1] sᶜ ↔ IsUpperSet s
rw₁ : IsLowerSet sᶜ ↔ IsUpperSet s
⊢ IsClosed[inst_1] s ↔ IsUpperSet s
have rw₂ : IsUpperSet sᶜᶜ ↔ IsUpperSet s
Tactic: rw [← isOpen_compl_iff, isOpen_iff_isLowerSet, isUpperSet_compl.symm, compl_compl]
-- Lean 4 proof step from Mathlib.Topology.Order.UpperLowerSetTopology (goal)
Goal:
α : Type u_1
inst : Preorder α
inst_1 : TopologicalSpace α
inst_2 : Topology.IsLowerSet α
s : Set α
rw : IsOpen[inst_1] sᶜ ↔ IsUpperSet s
rw₁ : IsLowerSet sᶜ ↔ IsUpperSet s
rw₂ : IsUpperSet sᶜᶜ ↔ IsUpperSet s
⊢ IsClosed[inst_1] s ↔ IsUpperSet s
have rw₃ : IsUpperSet s ↔ IsUpperSet s
Tactic: rw [← isOpen_compl_iff, isOpen_iff_isLowerSet, isUpperSet_compl.symm, compl_compl]
-- Lean 4 proof step from Mathlib.Topology.Order.UpperLowerSetTopology (goal)
Goal:
α : Type u_1
inst : Preorder α
inst_1 : TopologicalSpace α
inst_2 : Topology.IsLowerSet α
a : α
⊢ closure[inst_1] {a} = Ici a
have rw : (↑(UpperSet.Ici a) : Set α) = Ici a
Tactic: rw [closure_eq_upperClosure, upperClosure_singleton]
-- Lean 4 proof step from Mathlib.Topology.Order.UpperLowerSetTopology (goal)
Goal:
α : Type u_1
inst : Preorder α
inst_1 : TopologicalSpace α
inst_2 : Topology.IsLowerSet α
s : Set α
⊢ nhdsKer s = (↑(lowerClosure s) : Set α)
have h : ∀ (x : α), x ∈ nhdsKer s ↔ x ∈ (↑(lowerClosure s) : Set α)
Tactic: ext
-- Lean 4 proof step from Mathlib.Topology.Order.UpperLowerSetTopology (goal)
Goal:
α : Type u_1
inst : Preorder α
inst_1 : TopologicalSpace α
inst_2 : Topology.IsLowerSet α
a : α
⊢ nhdsKer {a} = Iic a
have rw : (↑(lowerClosure {a}) : Set α) = Iic a
Tactic: rw [nhdsKer_eq_lowerClosure, lowerClosure_singleton, LowerSet.coe_Iic]
-- Lean 4 proof step from Mathlib.Topology.Order.UpperLowerSetTopology (goal)
Goal:
α : Type u_1
inst : Preorder α
inst_1 : TopologicalSpace α
inst_2 : Topology.IsLowerSet α
a : α
rw : (↑(lowerClosure {a}) : Set α) = Iic a
⊢ nhdsKer {a} = Iic a
have rw₁ : (↑(LowerSet.Iic a) : Set α) = Iic a
Tactic: rw [nhdsKer_eq_lowerClosure, lowerClosure_singleton, LowerSet.coe_Iic]
-- Lean 4 proof step from Mathlib.Topology.Order.UpperLowerSetTopology (goal)
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
⊢ nhdsKer {a} = Iic a
have rw₂ : Iic a = Iic a
Tactic: rw [nhdsKer_eq_lowerClosure, lowerClosure_singleton, LowerSet.coe_Iic]
-- Lean 4 proof step from Mathlib.Topology.Order.UpperLowerSetTopology (goal)
Goal:
α : Type u_1
inst : Preorder α
inst_1 : TopologicalSpace α
inst_2 : Topology.IsLowerSet α
a : α
⊢ 𝓝 a = 𝓟 (Iic a)
have rw : 𝓟 (nhdsKer {a}) = 𝓟 (Iic a)
Tactic: rw [← principal_nhdsKer_singleton, nhdsKer_singleton]
-- Lean 4 proof step from Mathlib.Topology.Order.UpperLowerSetTopology (goal)
Goal:
α : Type u_1
inst : Preorder α
inst_1 : TopologicalSpace α
inst_2 : Topology.IsLowerSet α
a : α
rw : 𝓟 (nhdsKer {a}) = 𝓟 (Iic a)
⊢ 𝓝 a = 𝓟 (Iic a)
have rw₁ : 𝓟 (Iic a) = 𝓟 (Iic a)
Tactic: rw [← principal_nhdsKer_singleton, nhdsKer_singleton]
-- Lean 4 proof step from Mathlib.Topology.Order.UpperLowerSetTopology (goal)
Goal:
α : Type u_1
inst : Preorder α
inst_1 : TopologicalSpace α
inst_2 : Topology.IsLowerSet α
s : Set α
⊢ 𝓝ˢ s = 𝓟 (↑(lowerClosure s) : Set α)
have rw : 𝓟 (nhdsKer s) = 𝓟 (↑(lowerClosure s) : Set α)
Tactic: rw [← principal_nhdsKer, nhdsKer_eq_lowerClosure]
-- Lean 4 proof step from Mathlib.Topology.Order.UpperLowerSetTopology (goal)
Goal:
α : Type u_1
inst : Preorder α
inst_1 : TopologicalSpace α
inst_2 : Topology.IsLowerSet α
s : Set α
rw : 𝓟 (nhdsKer s) = 𝓟 (↑(lowerClosure s) : Set α)
⊢ 𝓝ˢ s = 𝓟 (↑(lowerClosure s) : Set α)
have rw₁ : 𝓟 (↑(lowerClosure s) : Set α) = 𝓟 (↑(lowerClosure s) : Set α)
Tactic: rw [← principal_nhdsKer, nhdsKer_eq_lowerClosure]
-- Lean 4 proof step from Mathlib.Topology.Order.UpperLowerSetTopology (goal)
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 f ↔ Continuous[inst_2, inst_3] f
have rw : Monotone (α := αᵒᵈ) (β := βᵒᵈ) ((⇑toDual : (a : β) → βᵒᵈ) ∘ f ∘ (⇑ofDual : (a : αᵒᵈ) → α)) ↔
  Continuous[inst_2, inst_3] f
Tactic: rw [← monotone_dual_iff]
-- Lean 4 proof step from Mathlib.Topology.Order.UpperLowerSetTopology (goal)
Goal:
α : Type u_1
inst : Preorder α
t₁ t₂ : TopologicalSpace α
inst_1 : Topology.IsLowerSet α
inst_2 : IsLower α
s : Set α
hs : IsOpen[t₂] s
⊢ IsOpen[t₁] s
have rw : IsLowerSet s
Tactic: rw [@isOpen_iff_isLowerSet α _ t₁]
-- Lean 4 proof step from Mathlib.Topology.Order.UpperLowerSetTopology (goal)
Goal:
α : Type u_1
inst : Preorder α
inst_1 : TopologicalSpace α
⊢ Topology.IsUpperSet.{u_1} αᵒᵈ ↔ Topology.IsLowerSet α
have mp : Topology.IsUpperSet.{u_1} αᵒᵈ → Topology.IsLowerSet α
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.Order.UpperLowerSetTopology (goal)
Goal:
α : Type u_1
inst : Preorder α
inst_1 : TopologicalSpace α
mp : Topology.IsUpperSet.{u_1} αᵒᵈ → Topology.IsLowerSet α
⊢ Topology.IsUpperSet.{u_1} αᵒᵈ ↔ Topology.IsLowerSet α
have mpr : Topology.IsLowerSet α → Topology.IsUpperSet.{u_1} αᵒᵈ
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.Order.UpperLowerSetTopology (goal)
Goal:
α : Type u_1
inst : Preorder α
a b : α
⊢ Specializes (X := WithUpperSet α) ((toUpperSet : (a : α) → WithUpperSet α) a : WithUpperSet α)
      ((toUpperSet : (a : α) → WithUpperSet α) b : WithUpperSet α) ↔
    b ≤ a
have 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
Tactic: simp_rw [specializes_iff_closure_subset, IsUpperSet.closure_singleton, Iic_subset_Iic,
    toUpperSet_le_iff]
-- Lean 4 proof step from Mathlib.Topology.Order.UpperLowerSetTopology (goal)
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
⊢ Specializes (X := WithUpperSet α) ((toUpperSet : (a : α) → WithUpperSet α) a : WithUpperSet α)
      ((toUpperSet : (a : α) → WithUpperSet α) b : WithUpperSet α) ↔
    b ≤ a
have simp_rw₁ : Subset (α := Set (WithUpperSet α)) (Iic ((toUpperSet : (a : α) → WithUpperSet α) b) : Set (WithUpperSet α))
    (Iic ((toUpperSet : (a : α) → WithUpperSet α) a) : Set (WithUpperSet α)) ↔
  b ≤ a
Tactic: simp_rw [specializes_iff_closure_subset, IsUpperSet.closure_singleton, Iic_subset_Iic,
    toUpperSet_le_iff]
-- Lean 4 proof step from Mathlib.Topology.Order.UpperLowerSetTopology (goal)
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
⊢ Specializes (X := WithUpperSet α) ((toUpperSet : (a : α) → WithUpperSet α) a : WithUpperSet α)
      ((toUpperSet : (a : α) → WithUpperSet α) b : WithUpperSet α) ↔
    b ≤ a
have simp_rw₂ : LE.le (α := WithUpperSet α) ((toUpperSet : (a : α) → WithUpperSet α) b : WithUpperSet α)
    ((toUpperSet : (a : α) → WithUpperSet α) a : WithUpperSet α) ↔
  b ≤ a
Tactic: simp_rw [specializes_iff_closure_subset, IsUpperSet.closure_singleton, Iic_subset_Iic,
    toUpperSet_le_iff]
-- Lean 4 proof step from Mathlib.Topology.Order.UpperLowerSetTopology (goal)
Goal:
α : Type u_1
inst : Preorder α
a b : α
⊢ Specializes (X := WithLowerSet α) ((toLowerSet : (a : α) → WithLowerSet α) a : WithLowerSet α)
      ((toLowerSet : (a : α) → WithLowerSet α) b : WithLowerSet α) ↔
    a ≤ b
have 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
Tactic: simp_rw [specializes_iff_closure_subset, IsLowerSet.closure_singleton, Ici_subset_Ici,
    toLowerSet_le_iff]
-- Lean 4 proof step from Mathlib.Topology.Order.UpperLowerSetTopology (goal)
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
⊢ Specializes (X := WithLowerSet α) ((toLowerSet : (a : α) → WithLowerSet α) a : WithLowerSet α)
      ((toLowerSet : (a : α) → WithLowerSet α) b : WithLowerSet α) ↔
    a ≤ b
have simp_rw₁ : Subset (α := Set (WithLowerSet α)) (Ici ((toLowerSet : (a : α) → WithLowerSet α) b) : Set (WithLowerSet α))
    (Ici ((toLowerSet : (a : α) → WithLowerSet α) a) : Set (WithLowerSet α)) ↔
  a ≤ b
Tactic: simp_rw [specializes_iff_closure_subset, IsLowerSet.closure_singleton, Ici_subset_Ici,
    toLowerSet_le_iff]
-- Lean 4 proof step from Mathlib.Topology.Order.UpperLowerSetTopology (goal)
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
⊢ Specializes (X := WithLowerSet α) ((toLowerSet : (a : α) → WithLowerSet α) a : WithLowerSet α)
      ((toLowerSet : (a : α) → WithLowerSet α) b : WithLowerSet α) ↔
    a ≤ b
have simp_rw₂ : LE.le (α := 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]
-- Lean 4 proof step from Mathlib.Topology.Order.WithTop (goal)
Goal:
ι : Type u_1
inst : Preorder ι
ts : TopologicalSpace ι
ht : OrderTopology ι
inst_1 : SecondCountableTopology ι
⊢ SecondCountableTopology.{u_1} (WithTop ι)
have inl : ∀ (hι : IsEmpty ι), SecondCountableTopology.{u_1} (WithTop ι)
Tactic: rcases isEmpty_or_nonempty ι with hι | ⟨⟨x₀⟩⟩
-- Lean 4 proof step from Mathlib.Topology.Order.WithTop (goal)
Goal:
ι : Type u_1
inst : Preorder ι
ts : TopologicalSpace ι
ht : OrderTopology ι
inst_1 : SecondCountableTopology ι
inl : ∀ (hι : IsEmpty ι), SecondCountableTopology.{u_1} (WithTop ι)
⊢ SecondCountableTopology.{u_1} (WithTop ι)
have inr : ∀ (x₀ : ι), SecondCountableTopology.{u_1} (WithTop ι)
Tactic: rcases isEmpty_or_nonempty ι with hι | ⟨⟨x₀⟩⟩
-- Lean 4 proof step from Mathlib.Topology.Order.WithTop (goal)
Goal:
ι : Type u_1
inst : Preorder ι
ts : TopologicalSpace ι
ht : OrderTopology ι
inst_1 : SecondCountableTopology ι
x₀ : ι
⊢ SecondCountableTopology.{u_1} (WithTop ι)
have inr : ∀ (c : Set ι) (c_count : c.Countable) (hc : ts = generateFrom {s : Set ι | ∃ a ∈ c, s = Ioi a ∨ s = Iio a}),
  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 ι
-- 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}
⊢ SecondCountableTopology.{u_1} (WithTop ι)
have inr : ∀ (c' : Set ι) (c'_count : c'.Countable) (hc' : Dense c'), SecondCountableTopology.{u_1} (WithTop ι)
Tactic: obtain ⟨c', c'_count, hc'⟩ : ∃ c' : Set ι, c'.Countable ∧ Dense c' :=
    SeparableSpace.exists_countable_dense
-- 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 ι)}
H :
  Eq.{u_1 + 1} (α := TopologicalSpace (WithTop ι)) instWithTopOfOrderTopology
    (generateFrom {s : Set (WithTop ι) | ∃ a ∈ d, s = Ioi a ∨ s = Iio a})
⊢ Eq.{u_1 + 1} (α := TopologicalSpace (WithTop ι)) instWithTopOfOrderTopology
    (generateFrom {s : Set (WithTop ι) | ∃ a ∈ d, s = Ioi a ∨ s = Iio a})
have rw : Eq.{u_1 + 1} (α := TopologicalSpace (WithTop ι)) instWithTopOfOrderTopology instWithTopOfOrderTopology
Tactic: rw [← H]
-- 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 ι)}
H :
  Eq.{u_1 + 1} (α := TopologicalSpace (WithTop ι)) instWithTopOfOrderTopology
    (generateFrom {s : Set (WithTop ι) | ∃ a ∈ d, s = Ioi a ∨ s = Iio a})
⊢ SecondCountableTopology.{u_1} (WithTop ι)
have refine : Set.Countable.{u_1} (α := Set (WithTop ι)) {s : Set (WithTop ι) | ∃ a ∈ d, s = Ioi a ∨ s = Iio a}
Tactic: refine ⟨{s | ∃ a ∈ d, s = Ioi a ∨ s = Iio a}, ?_, by rw [← H]⟩
-- 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 ι)}
H :
  Eq.{u_1 + 1} (α := TopologicalSpace (WithTop ι)) instWithTopOfOrderTopology
    (generateFrom {s : Set (WithTop ι) | ∃ a ∈ d, s = Ioi a ∨ s = Iio a})
⊢ Set.Countable.{u_1} (α := Set (WithTop ι)) {s : Set (WithTop ι) | ∃ a ∈ d, s = Ioi a ∨ s = Iio a}
have d_count : d.Countable
Tactic: have d_count : d.Countable :=
      (((c_count.image _).union (c'_count.image _)).union (by simp)).union (by simp)
-- 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 ι)}
H :
  Eq.{u_1 + 1} (α := TopologicalSpace (WithTop ι)) instWithTopOfOrderTopology
    (generateFrom {s : Set (WithTop ι) | ∃ a ∈ d, s = Ioi a ∨ s = Iio a})
d_count : d.Countable
⊢ Set.Countable.{u_1} (α := Set (WithTop ι)) {s : Set (WithTop ι) | ∃ a ∈ d, s = Ioi a ∨ s = Iio a}
have this : {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)
-- 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 ι)}
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
⊢ Set.Countable.{u_1} (α := Set (WithTop ι)) {s : Set (WithTop ι) | ∃ a ∈ d, s = Ioi a ∨ s = Iio a}
have rw : (Ioi '' d ∪ Iio '' d).Countable
Tactic: rw [this]