awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.Bases (goal)
Goal:
ι : Type u_1
X : ι → Type u_2
inst : (i : ι) → TopologicalSpace (X i)
i : ι
refine :
  ∀ (s : Set ((i : ι) → X i)),
    Membership.mem (γ := Set (Set ((i : ι) → X i)))
        {S : Set ((i : ι) → X i) |
          ∃ (U : (i : ι) → Set (X i)) (F : Finset ι),
            (∀ i ∈ F, Membership.mem (γ := Set (Set (X i))) {U : Set (X i) | IsOpen[inst i] U} (U i)) ∧
              S = (↑F : Set ι).pi (α := X) U}
        s →
      IsOpen[inst i] (eval (β := X) i '' s)
refine₁ :
  ∀ (U : (i : ι) → Set (X i)) (s : Finset ι)
    (hU : ∀ i ∈ s, Membership.mem (γ := Set (Set (X i))) {U : Set (X i) | IsOpen[inst i] U} (U i)),
    IsOpen[inst i] (eval (β := X) i '' (↑s : Set ι).pi (α := X) U)
inl :
  ∀ (U : (i : ι) → Set (X i)) (s : Finset ι)
    (hU : ∀ i ∈ s, Membership.mem (γ := Set (Set (X i))) {U : Set (X i) | IsOpen[inst i] U} (U i))
    (h : (↑s : Set ι).pi (α := X) U = ∅), IsOpen[inst i] (eval (β := X) i '' (↑s : Set ι).pi (α := X) U)
inr inr₁ :
  ∀ (U : (i : ι) → Set (X i)) (s : Finset ι)
    (hU : ∀ i ∈ s, Membership.mem (γ := Set (Set (X i))) {U : Set (X i) | IsOpen[inst i] U} (U i))
    (h : ((↑s : Set ι).pi (α := X) U).Nonempty), IsOpen[inst i] (eval (β := X) i '' (↑s : Set ι).pi (α := X) U)
⊢ IsOpenMap (X := (x : ι) → X x) (eval (β := X) i)
have pos : ∀ (U : (i : ι) → Set (X i)) (s : Finset ι)
  (hU : ∀ i ∈ s, Membership.mem (γ := Set (Set (X i))) {U : Set (X i) | IsOpen[inst i] U} (U i))
  (h : ((↑s : Set ι).pi (α := X) U).Nonempty) (hi : i ∈ s),
  IsOpen[inst i] (eval (β := X) i '' (↑s : Set ι).pi (α := X) U)
Tactic: classical
  refine (isTopologicalBasis_pi fun _ ↦ isTopologicalBasis_opens).isOpenMap_iff.2 ?_
  rintro _ ⟨U, s, hU, rfl⟩
  obtain h | h := ((s : Set ι).pi U).eq_empty_or_nonempty
  · simp [h]
  by_cases hi : i ∈ s
  · rw [eval_image_pi (mod_cast hi) h]
    exact hU _ hi
  · rw [eval_image_pi_of_notMem (mod_cast hi), if_pos h]
    exact isOpen_univ
-- Lean 4 proof step from Mathlib.Topology.Bases (goal)
Goal:
ι : Type u_1
X : ι → Type u_2
inst : (i : ι) → TopologicalSpace (X i)
i : ι
refine :
  ∀ (s : Set ((i : ι) → X i)),
    Membership.mem (γ := Set (Set ((i : ι) → X i)))
        {S : Set ((i : ι) → X i) |
          ∃ (U : (i : ι) → Set (X i)) (F : Finset ι),
            (∀ i ∈ F, Membership.mem (γ := Set (Set (X i))) {U : Set (X i) | IsOpen[inst i] U} (U i)) ∧
              S = (↑F : Set ι).pi (α := X) U}
        s →
      IsOpen[inst i] (eval (β := X) i '' s)
refine₁ :
  ∀ (U : (i : ι) → Set (X i)) (s : Finset ι)
    (hU : ∀ i ∈ s, Membership.mem (γ := Set (Set (X i))) {U : Set (X i) | IsOpen[inst i] U} (U i)),
    IsOpen[inst i] (eval (β := X) i '' (↑s : Set ι).pi (α := X) U)
inl :
  ∀ (U : (i : ι) → Set (X i)) (s : Finset ι)
    (hU : ∀ i ∈ s, Membership.mem (γ := Set (Set (X i))) {U : Set (X i) | IsOpen[inst i] U} (U i))
    (h : (↑s : Set ι).pi (α := X) U = ∅), IsOpen[inst i] (eval (β := X) i '' (↑s : Set ι).pi (α := X) U)
inr inr₁ :
  ∀ (U : (i : ι) → Set (X i)) (s : Finset ι)
    (hU : ∀ i ∈ s, Membership.mem (γ := Set (Set (X i))) {U : Set (X i) | IsOpen[inst i] U} (U i))
    (h : ((↑s : Set ι).pi (α := X) U).Nonempty), IsOpen[inst i] (eval (β := X) i '' (↑s : Set ι).pi (α := X) U)
pos :
  ∀ (U : (i : ι) → Set (X i)) (s : Finset ι)
    (hU : ∀ i ∈ s, Membership.mem (γ := Set (Set (X i))) {U : Set (X i) | IsOpen[inst i] U} (U i))
    (h : ((↑s : Set ι).pi (α := X) U).Nonempty) (hi : i ∈ s),
    IsOpen[inst i] (eval (β := X) i '' (↑s : Set ι).pi (α := X) U)
⊢ IsOpenMap (X := (x : ι) → X x) (eval (β := X) i)
have neg : ∀ (U : (i : ι) → Set (X i)) (s : Finset ι)
  (hU : ∀ i ∈ s, Membership.mem (γ := Set (Set (X i))) {U : Set (X i) | IsOpen[inst i] U} (U i))
  (h : ((↑s : Set ι).pi (α := X) U).Nonempty) (hi : i ∉ s),
  IsOpen[inst i] (eval (β := X) i '' (↑s : Set ι).pi (α := X) U)
Tactic: classical
  refine (isTopologicalBasis_pi fun _ ↦ isTopologicalBasis_opens).isOpenMap_iff.2 ?_
  rintro _ ⟨U, s, hU, rfl⟩
  obtain h | h := ((s : Set ι).pi U).eq_empty_or_nonempty
  · simp [h]
  by_cases hi : i ∈ s
  · rw [eval_image_pi (mod_cast hi) h]
    exact hU _ hi
  · rw [eval_image_pi_of_notMem (mod_cast hi), if_pos h]
    exact isOpen_univ
-- Lean 4 proof step from Mathlib.Topology.Bases (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : PartialOrder α
s : Set α
inst_2 : SeparableSpace.{u_1} (↑s : Type u_1)
hs : Dense s
⊢ ∃ t ⊆ s, t.Countable ∧ Dense t ∧ (∀ (x : α), IsBot x → x ∈ s → x ∈ t) ∧ ∀ (x : α), IsTop x → x ∈ s → x ∈ t
have rcases : ∀ (t : Set α) (hts : t ⊆ s) (htc : t.Countable) (htd : Dense t),
  ∃ t ⊆ s, t.Countable ∧ Dense t ∧ (∀ (x : α), IsBot x → x ∈ s → x ∈ t) ∧ ∀ (x : α), IsTop x → x ∈ s → x ∈ t
Tactic: rcases hs.exists_countable_dense_subset with ⟨t, hts, htc, htd⟩
-- Lean 4 proof step from Mathlib.Topology.Bases (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : PartialOrder α
s : Set α
inst_2 : SeparableSpace.{u_1} (↑s : Type u_1)
hs : Dense s
t : Set α
hts : t ⊆ s
htc : t.Countable
htd : Dense t
⊢ ∃ t ⊆ s, t.Countable ∧ Dense t ∧ (∀ (x : α), IsBot x → x ∈ s → x ∈ t) ∧ ∀ (x : α), IsTop x → x ∈ s → x ∈ t
have refine_1 : (t ∪ ({x : α | IsBot x} ∪ {x : α | IsTop x})) ∩ s ⊆ s
Tactic: refine ⟨(t ∪ ({ x | IsBot x } ∪ { x | IsTop x })) ∩ s, ?_, ?_, ?_, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Bases (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : PartialOrder α
s : Set α
inst_2 : SeparableSpace.{u_1} (↑s : Type u_1)
hs : Dense s
t : Set α
hts : t ⊆ s
htc : t.Countable
htd : Dense t
refine_1 : (t ∪ ({x : α | IsBot x} ∪ {x : α | IsTop x})) ∩ s ⊆ s
⊢ ∃ t ⊆ s, t.Countable ∧ Dense t ∧ (∀ (x : α), IsBot x → x ∈ s → x ∈ t) ∧ ∀ (x : α), IsTop x → x ∈ s → x ∈ t
have refine_2 : ((t ∪ ({x : α | IsBot x} ∪ {x : α | IsTop x})) ∩ s).Countable
Tactic: refine ⟨(t ∪ ({ x | IsBot x } ∪ { x | IsTop x })) ∩ s, ?_, ?_, ?_, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Bases (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : PartialOrder α
s : Set α
inst_2 : SeparableSpace.{u_1} (↑s : Type u_1)
hs : Dense s
t : Set α
hts : t ⊆ s
htc : t.Countable
htd : Dense t
refine_1 : (t ∪ ({x : α | IsBot x} ∪ {x : α | IsTop x})) ∩ s ⊆ s
refine_2 : ((t ∪ ({x : α | IsBot x} ∪ {x : α | IsTop x})) ∩ s).Countable
⊢ ∃ t ⊆ s, t.Countable ∧ Dense t ∧ (∀ (x : α), IsBot x → x ∈ s → x ∈ t) ∧ ∀ (x : α), IsTop x → x ∈ s → x ∈ t
have refine_3 : Dense ((t ∪ ({x : α | IsBot x} ∪ {x : α | IsTop x})) ∩ s)
Tactic: refine ⟨(t ∪ ({ x | IsBot x } ∪ { x | IsTop x })) ∩ s, ?_, ?_, ?_, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Bases (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : PartialOrder α
s : Set α
inst_2 : SeparableSpace.{u_1} (↑s : Type u_1)
hs : Dense s
t : Set α
hts : t ⊆ s
htc : t.Countable
htd : Dense t
refine_1 : (t ∪ ({x : α | IsBot x} ∪ {x : α | IsTop x})) ∩ s ⊆ s
refine_2 : ((t ∪ ({x : α | IsBot x} ∪ {x : α | IsTop x})) ∩ s).Countable
refine_3 : Dense ((t ∪ ({x : α | IsBot x} ∪ {x : α | IsTop x})) ∩ s)
⊢ ∃ t ⊆ s, t.Countable ∧ Dense t ∧ (∀ (x : α), IsBot x → x ∈ s → x ∈ t) ∧ ∀ (x : α), IsTop x → x ∈ s → x ∈ t
have refine_4 : ∀ (x : α), IsBot x → x ∈ s → x ∈ (t ∪ ({x : α | IsBot x} ∪ {x : α | IsTop x})) ∩ s
Tactic: refine ⟨(t ∪ ({ x | IsBot x } ∪ { x | IsTop x })) ∩ s, ?_, ?_, ?_, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Bases (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : PartialOrder α
s : Set α
inst_2 : SeparableSpace.{u_1} (↑s : Type u_1)
hs : Dense s
t : Set α
hts : t ⊆ s
htc : t.Countable
htd : Dense t
refine_1 : (t ∪ ({x : α | IsBot x} ∪ {x : α | IsTop x})) ∩ s ⊆ s
refine_2 : ((t ∪ ({x : α | IsBot x} ∪ {x : α | IsTop x})) ∩ s).Countable
refine_3 : Dense ((t ∪ ({x : α | IsBot x} ∪ {x : α | IsTop x})) ∩ s)
refine_4 : ∀ (x : α), IsBot x → x ∈ s → x ∈ (t ∪ ({x : α | IsBot x} ∪ {x : α | IsTop x})) ∩ s
⊢ ∃ t ⊆ s, t.Countable ∧ Dense t ∧ (∀ (x : α), IsBot x → x ∈ s → x ∈ t) ∧ ∀ (x : α), IsTop x → x ∈ s → x ∈ t
have refine_5 : ∀ (x : α), IsTop x → x ∈ s → x ∈ (t ∪ ({x : α | IsBot x} ∪ {x : α | IsTop x})) ∩ s
Tactic: refine ⟨(t ∪ ({ x | IsBot x } ∪ { x | IsTop x })) ∩ s, ?_, ?_, ?_, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Bases (goal)
Goal:
α : Type u
t : TopologicalSpace α
β : Type u_1
inst : TopologicalSpace β
inst_1 : FirstCountableTopology β
f : α → β
hf : IsInducing f
⊢ FirstCountableTopology α
have rw : FirstCountableTopology α
Tactic: rw [hf.1]
-- Lean 4 proof step from Mathlib.Topology.Bases (goal)
Goal:
α : Type u
t : TopologicalSpace α
inst : FirstCountableTopology α
x : α
f : Filter α
inst_1 : f.IsCountablyGenerated
hx : (𝓝 x ⊓ f).NeBot
⊢ ∃ (ψ : ℕ → α), Tendsto ψ atTop (𝓝 x) ∧ Tendsto ψ atTop f
have obtain : ∀ (g : ℕ → α) (hg : Tendsto g atTop (𝓝 x ⊓ f)), ∃ (ψ : ℕ → α), Tendsto ψ atTop (𝓝 x) ∧ Tendsto ψ atTop f
Tactic: obtain ⟨g, hg⟩ := Filter.exists_seq_tendsto (𝓝 x ⊓ f)
-- Lean 4 proof step from Mathlib.Topology.Bases (goal)
Goal:
α : Type u
t : TopologicalSpace α
β : Type u_1
inst : TopologicalSpace β
inst_1 : FirstCountableTopology α
inst_2 : FirstCountableTopology β
x_1 : α × β
x : α
y : β
⊢ (𝓝 (x, y)).IsCountablyGenerated
have rw : (𝓝 x ×ˢ 𝓝 y).IsCountablyGenerated
Tactic: rw [nhds_prod_eq]
-- Lean 4 proof step from Mathlib.Topology.Bases (goal)
Goal:
α : Type u
t : TopologicalSpace α
ι : Type u_1
X : ι → Type u_2
inst : Countable ι
inst_1 : (i : ι) → TopologicalSpace (X i)
inst_2 : ∀ (i : ι), FirstCountableTopology.{u_2} (X i)
f : (i : ι) → X i
⊢ (𝓝 f).IsCountablyGenerated
have rw : IsCountablyGenerated (α := (i : ι) → X i) (Filter.pi (α := X) fun (i : ι) ↦ 𝓝 (f i))
Tactic: rw [nhds_pi]
-- Lean 4 proof step from Mathlib.Topology.Bases (goal)
Goal:
α : Type u
t : TopologicalSpace α
inst : SecondCountableTopology α
⊢ ∃ (b : Set (Set α)), b.Countable ∧ ∅ ∉ b ∧ IsTopologicalBasis b
have obtain : ∀ (b : Set (Set α)) (hb₁ : b.Countable) (hb₂ : t = generateFrom b),
  ∃ (b : Set (Set α)), b.Countable ∧ ∅ ∉ b ∧ IsTopologicalBasis b
Tactic: obtain ⟨b, hb₁, hb₂⟩ := @SecondCountableTopology.is_open_generated_countable α _ _
-- Lean 4 proof step from Mathlib.Topology.Bases (goal)
Goal:
α : Type u
t : TopologicalSpace α
inst : SecondCountableTopology α
b : Set (Set α)
hb₁ : b.Countable
hb₂ : t = generateFrom b
⊢ ∃ (b : Set (Set α)), b.Countable ∧ ∅ ∉ b ∧ IsTopologicalBasis b
have refine_1 : Set.Countable (α := Set α) ((fun (f : Set (Set α)) ↦ ⋂₀ f) '' {f : Set (Set α) | f.Finite ∧ f ⊆ b} \ {∅})
Tactic: refine ⟨_, ?_, notMem_diff_of_mem ?_, (isTopologicalBasis_of_subbasis hb₂).diff_empty⟩
-- Lean 4 proof step from Mathlib.Topology.Bases (goal)
Goal:
α : Type u
t : TopologicalSpace α
inst : SecondCountableTopology α
b : Set (Set α)
hb₁ : b.Countable
hb₂ : t = generateFrom b
refine_1 : Set.Countable (α := Set α) ((fun (f : Set (Set α)) ↦ ⋂₀ f) '' {f : Set (Set α) | f.Finite ∧ f ⊆ b} \ {∅})
⊢ ∃ (b : Set (Set α)), b.Countable ∧ ∅ ∉ b ∧ IsTopologicalBasis b
have refine_2 : Membership.mem (γ := Set (Set α)) {∅} ∅
Tactic: refine ⟨_, ?_, notMem_diff_of_mem ?_, (isTopologicalBasis_of_subbasis hb₂).diff_empty⟩
-- Lean 4 proof step from Mathlib.Topology.Bases (goal)
Goal:
α : Type u
t : TopologicalSpace α
inst : SecondCountableTopology α
⊢ ∃ (b : ℕ → Set α), IsTopologicalBasis (range b)
have obtain : ∀ (t_1 : Set (Set α)) (ht : t_1.Countable ∧ ∅ ∉ t_1 ∧ IsTopologicalBasis t_1),
  ∃ (b : ℕ → Set α), IsTopologicalBasis (range b)
Tactic: obtain ⟨t, ht⟩ := TopologicalSpace.exists_countable_basis α
-- Lean 4 proof step from Mathlib.Topology.Bases (goal)
Goal:
α : Type u
t_1 : TopologicalSpace α
inst : SecondCountableTopology α
t : Set (Set α)
ht : t.Countable ∧ ∅ ∉ t ∧ IsTopologicalBasis t
⊢ ∃ (b : ℕ → Set α), IsTopologicalBasis (range b)
have pos : ∀ (hn : t.Nonempty), ∃ (b : ℕ → Set α), IsTopologicalBasis (range b)
Tactic: by_cases! hn : t.Nonempty
-- Lean 4 proof step from Mathlib.Topology.Bases (goal)
Goal:
α : Type u
t_1 : TopologicalSpace α
inst : SecondCountableTopology α
t : Set (Set α)
ht : t.Countable ∧ ∅ ∉ t ∧ IsTopologicalBasis t
pos : ∀ (hn : t.Nonempty), ∃ (b : ℕ → Set α), IsTopologicalBasis (range b)
⊢ ∃ (b : ℕ → Set α), IsTopologicalBasis (range b)
have neg : ∀ (hn : t = ∅), ∃ (b : ℕ → Set α), IsTopologicalBasis (range b)
Tactic: by_cases! hn : t.Nonempty
-- Lean 4 proof step from Mathlib.Topology.Bases (goal)
Goal:
α : Type u
t_1 : TopologicalSpace α
inst : SecondCountableTopology α
t : Set (Set α)
ht : t.Countable ∧ ∅ ∉ t ∧ IsTopologicalBasis t
hn : t.Nonempty
⊢ ∃ (b : ℕ → Set α), IsTopologicalBasis (range b)
have pos : ∀ (b : ℕ → Set α) (ht : (range b).Countable ∧ ∅ ∉ range b ∧ IsTopologicalBasis (range b)) (hn : (range b).Nonempty),
  ∃ (b : ℕ → Set α), IsTopologicalBasis (range b)
Tactic: obtain ⟨b, rfl⟩ := ht.1.exists_eq_range hn
Cleared hypotheses: t, ht, hn
-- Lean 4 proof step from Mathlib.Topology.Bases (goal)
Goal:
α : Type u
t : TopologicalSpace α
inst : Countable α
inst_1 : FirstCountableTopology α
⊢ ∃ (b : Set (Set α)), b.Countable ∧ t = generateFrom b
have choose : ∀ (b : (x : α) → ℕ → Set α) (hxb : ∀ (x : α) (i : ℕ), x ∈ b x i ∧ IsOpen[t] (b x i))
  (hbb : ∀ (x : α), (𝓝 x).HasAntitoneBasis fun (i : ℕ) ↦ b x i), ∃ (b : Set (Set α)), b.Countable ∧ t = generateFrom b
Tactic: choose b hxb hbb using fun x : α => (nhds_basis_opens x).exists_antitone_subbasis
-- Lean 4 proof step from Mathlib.Topology.Bases (goal)
Goal:
α : Type u
t : TopologicalSpace α
inst : Countable α
inst_1 : FirstCountableTopology α
b : (x : α) → ℕ → Set α
hxb : ∀ (x : α) (i : ℕ), x ∈ b x i ∧ IsOpen[t] (b x i)
hbb : ∀ (x : α), (𝓝 x).HasAntitoneBasis fun (i : ℕ) ↦ b x i
⊢ ∃ (b : Set (Set α)), b.Countable ∧ t = generateFrom b
have right : t = generateFrom (range (uncurry b))
Tactic: use range b.uncurry, countable_range b.uncurry
-- Lean 4 proof step from Mathlib.Topology.Bases (goal)
Goal:
α : Type u
t : TopologicalSpace α
inst : Countable α
inst_1 : FirstCountableTopology α
b : (x : α) → ℕ → Set α
hxb : ∀ (x : α) (i : ℕ), x ∈ b x i ∧ IsOpen[t] (b x i)
hbb : ∀ (x : α), (𝓝 x).HasAntitoneBasis fun (i : ℕ) ↦ b x i
⊢ t = generateFrom (range (uncurry b))
have right : t ≤ generateFrom (range (uncurry b))
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.Topology.Bases (goal)
Goal:
α : Type u
t : TopologicalSpace α
inst : Countable α
inst_1 : FirstCountableTopology α
b : (x : α) → ℕ → Set α
hxb : ∀ (x : α) (i : ℕ), x ∈ b x i ∧ IsOpen[t] (b x i)
hbb : ∀ (x : α), (𝓝 x).HasAntitoneBasis fun (i : ℕ) ↦ b x i
right : t ≤ generateFrom (range (uncurry b))
⊢ t = generateFrom (range (uncurry b))
have right₁ : generateFrom (range (uncurry b)) ≤ t
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.Topology.Bases (goal)
Goal:
α : Type u
t : TopologicalSpace α
inst : Countable α
inst_1 : FirstCountableTopology α
b : (x : α) → ℕ → Set α
hxb : ∀ (x : α) (i : ℕ), x ∈ b x i ∧ IsOpen[t] (b x i)
hbb : ∀ (x : α), (𝓝 x).HasAntitoneBasis fun (i : ℕ) ↦ b x i
⊢ t ≤ generateFrom (range (uncurry b))
have right : range (uncurry b) ⊆ {s : Set α | IsOpen[t] s}
Tactic: rw [le_generateFrom_iff_subset_isOpen]
-- Lean 4 proof step from Mathlib.Topology.Bases (goal)
Goal:
α : Type u
t : TopologicalSpace α
inst : Countable α
inst_1 : FirstCountableTopology α
b : (x : α) → ℕ → Set α
hxb : ∀ (x : α) (i : ℕ), x ∈ b x i ∧ IsOpen[t] (b x i)
hbb : ∀ (x : α), (𝓝 x).HasAntitoneBasis fun (i : ℕ) ↦ b x i
⊢ generateFrom (range (uncurry b)) ≤ t
have right : ∀ (x : α), 𝓝 x ≤ 𝓝 x
Tactic: rw [le_iff_nhds]
-- Lean 4 proof step from Mathlib.Topology.Bases (goal)
Goal:
α : Type u
t : TopologicalSpace α
inst : Countable α
inst_1 : FirstCountableTopology α
b : (x : α) → ℕ → Set α
hxb : ∀ (x : α) (i : ℕ), x ∈ b x i ∧ IsOpen[t] (b x i)
hbb : ∀ (x : α), (𝓝 x).HasAntitoneBasis fun (i : ℕ) ↦ b x i
x : α
⊢ 𝓝 x ≤ 𝓝 x
have right : ∀ (i' : ℕ), True → b x i' ∈ 𝓝 x
Tactic: rw [(hbb x).ge_iff]
-- Lean 4 proof step from Mathlib.Topology.Bases (goal)
Goal:
α : Type u
t : TopologicalSpace α
inst : Countable α
inst_1 : FirstCountableTopology α
b : (x : α) → ℕ → Set α
hxb : ∀ (x : α) (i : ℕ), x ∈ b x i ∧ IsOpen[t] (b x i)
hbb : ∀ (x : α), (𝓝 x).HasAntitoneBasis fun (i : ℕ) ↦ b x i
x : α
n : ℕ
h : True
⊢ b x n ∈ 𝓝 x
have right : IsOpen[generateFrom (range (uncurry b))] (b x n)
Tactic: refine @IsOpen.mem_nhds α (generateFrom (range b.uncurry)) x (b x n) ?_ (hxb x n).left
-- Lean 4 proof step from Mathlib.Topology.Bases (goal)
Goal:
α : Type u_1
β : Type u_2
t : TopologicalSpace β
inst : SecondCountableTopology β
f : α → β
⊢ SecondCountableTopology α
have rcases : ∀ (b : Set (Set β)) (hb : b.Countable) (eq : t = generateFrom b), SecondCountableTopology α
Tactic: rcases @SecondCountableTopology.is_open_generated_countable β _ _ with ⟨b, hb, eq⟩
-- Lean 4 proof step from Mathlib.Topology.Bases (goal)
Goal:
α : Type u_1
β : Type u_2
t : TopologicalSpace β
inst : SecondCountableTopology β
f : α → β
b : Set (Set β)
hb : b.Countable
eq : t = generateFrom b
this : TopologicalSpace α := induced f t
⊢ SecondCountableTopology α
have refine : induced f t = generateFrom (preimage f '' b)
Tactic: refine { is_open_generated_countable := ⟨preimage f '' b, hb.image _, ?_⟩ }
-- Lean 4 proof step from Mathlib.Topology.Bases (goal)
Goal:
α : Type u_1
β : Type u_2
t : TopologicalSpace β
inst : SecondCountableTopology β
f : α → β
b : Set (Set β)
hb : b.Countable
eq : t = generateFrom b
this : TopologicalSpace α := induced f t
⊢ induced f t = generateFrom (preimage f '' b)
have rw : induced f (generateFrom b) = generateFrom (preimage f '' b)
Tactic: rw [eq, induced_generateFrom_eq]
-- Lean 4 proof step from Mathlib.Topology.Bases (goal)
Goal:
α : Type u_1
β : Type u_2
t : TopologicalSpace β
inst : SecondCountableTopology β
f : α → β
b : Set (Set β)
hb : b.Countable
eq : t = generateFrom b
this : TopologicalSpace α := induced f t
rw : induced f (generateFrom b) = generateFrom (preimage f '' b)
⊢ induced f t = generateFrom (preimage f '' b)
have rw₁ : generateFrom (preimage f '' b) = generateFrom (preimage f '' b)
Tactic: rw [eq, induced_generateFrom_eq]
-- Lean 4 proof step from Mathlib.Topology.Bases (goal)
Goal:
α : Type u_1
ι : Sort u_2
inst : Countable ι
t : ι → TopologicalSpace α
ht : ∀ (i : ι), SecondCountableTopology α
⊢ SecondCountableTopology α
have rw : SecondCountableTopology α
Tactic: rw [funext fun i => @eq_generateFrom_countableBasis α (t i) (ht i), ← generateFrom_iUnion]
-- Lean 4 proof step from Mathlib.Topology.Bases (goal)
Goal:
α : Type u
t : TopologicalSpace α
inst : SecondCountableTopology α
⊢ SeparableSpace α
have choose : ∀ (p : (s : (↑(countableBasis α) : Type u)) → α) (hp : ∀ (s : (↑(countableBasis α) : Type u)), p s ∈ (↑s : Set α)),
  SeparableSpace α
Tactic: choose p hp using fun s : countableBasis α => nonempty_of_mem_countableBasis s.2
-- Lean 4 proof step from Mathlib.Topology.Bases (goal)
Goal:
α : Type u
t : TopologicalSpace α
inst : SecondCountableTopology α
ι : Type u_1
s : ι → Set α
H : ∀ (i : ι), IsOpen[t] (s i)
B : Set (Set α) := {b : Set α | b ∈ countableBasis α ∧ ∃ (i : ι), b ⊆ s i}
⊢ ∃ (T : Set ι), T.Countable ∧ Eq.{u + 1} (α := Set α) (⋃ i ∈ T, s i) (⋃ (i : ι), s i)
have choose : ∀ (f : (b : (↑B : Type u)) → ι) (hf : ∀ (b : (↑B : Type u)), (↑b : Set α) ⊆ s (f b)),
  ∃ (T : Set ι), T.Countable ∧ Eq.{u + 1} (α := Set α) (⋃ i ∈ T, s i) (⋃ (i : ι), s i)
Tactic: choose f hf using fun b : B => b.2.2
-- Lean 4 proof step from Mathlib.Topology.Bases (hypothesis)
Goal:
α : Type u
t : TopologicalSpace α
inst : SecondCountableTopology α
ι : Type u_1
s : ι → Set α
H : ∀ (i : ι), IsOpen[t] (s i)
B : Set (Set α) := {b : Set α | b ∈ countableBasis α ∧ ∃ (i : ι), b ⊆ s i}
f : (b : (↑B : Type u)) → ι
hf : ∀ (b : (↑B : Type u)), (↑b : Set α) ⊆ s (f b)
⊢ ∃ (T : Set ι), T.Countable ∧ Eq.{u + 1} (α := Set α) (⋃ i ∈ T, s i) (⋃ (i : ι), s i)
have this : Countable.{u + 1} (↑B : Type u)
Tactic: haveI : Countable B := ((countable_countableBasis α).mono (sep_subset _ _)).to_subtype
-- Lean 4 proof step from Mathlib.Topology.Bases (goal)
Goal:
α : Type u
t : TopologicalSpace α
inst : SecondCountableTopology α
ι : Type u_1
s : ι → Set α
H : ∀ (i : ι), IsOpen[t] (s i)
B : Set (Set α) := {b : Set α | b ∈ countableBasis α ∧ ∃ (i : ι), b ⊆ s i}
f : (b : (↑B : Type u)) → ι
hf : ∀ (b : (↑B : Type u)), (↑b : Set α) ⊆ s (f b)
this : Countable.{u + 1} (↑B : Type u)
⊢ ∃ (T : Set ι), T.Countable ∧ Eq.{u + 1} (α := Set α) (⋃ i ∈ T, s i) (⋃ (i : ι), s i)
have refine : ∀ (t' : Set α), Membership.mem (γ := Set (Set α)) (range fun (i : ι) ↦ s i) t' → t' ⊆ ⋃ i ∈ range f, s i
Tactic: refine ⟨_, countable_range f, (iUnion₂_subset_iUnion _ _).antisymm (sUnion_subset ?_)⟩
-- Lean 4 proof step from Mathlib.Topology.Bases (goal)
Goal:
α : Type u
t : TopologicalSpace α
inst : SecondCountableTopology α
ι : Type u_1
s : ι → Set α
H : ∀ (i : ι), IsOpen[t] (s i)
B : Set (Set α) := {b : Set α | b ∈ countableBasis α ∧ ∃ (i : ι), b ⊆ s i}
f : (b : (↑B : Type u)) → ι
hf : ∀ (b : (↑B : Type u)), (↑b : Set α) ⊆ s (f b)
this : Countable.{u + 1} (↑B : Type u)
i : ι
x : α
xs : Membership.mem (γ := Set α) ((fun (i : ι) ↦ s i) i) x
⊢ Membership.mem (γ := Set α) (⋃ i ∈ range f, s i) x
have rcases : ∀ (b : Set α) (hb : b ∈ countableBasis α) (xb : x ∈ b) (bs : b ⊆ (fun (i : ι) ↦ s i) i),
  Membership.mem (γ := Set α) (⋃ i ∈ range f, s i) x
Tactic: rcases (isBasis_countableBasis α).exists_subset_of_mem_open xs (H _) with ⟨b, hb, xb, bs⟩
-- Lean 4 proof step from Mathlib.Topology.Bases (goal)
Goal:
α : Type u
t : TopologicalSpace α
inst : SecondCountableTopology α
ι : Type u_1
I : Set ι
s : ι → Set α
H : ∀ i ∈ I, IsOpen[t] (s i)
⊢ ∃ T ⊆ I, T.Countable ∧ Eq.{u + 1} (α := Set α) (⋃ i ∈ T, s i) (⋃ i ∈ I, s i)
have simp_rw : ∃ (s_1 : Set (↑I : Type u_1)),
  (Subtype.val (p := fun (x : ι) ↦ x ∈ I) '' s_1).Countable ∧
    Eq.{u + 1} (α := Set α) (⋃ y ∈ s_1, s (↑y : ι)) (⋃ i ∈ I, s i)
Tactic: simp_rw [← Subtype.exists_set_subtype, biUnion_image]
-- Lean 4 proof step from Mathlib.Topology.Bases (goal)
Goal:
α : Type u
t : TopologicalSpace α
inst : SecondCountableTopology α
ι : Type u_1
I : Set ι
s : ι → Set α
H : ∀ i ∈ I, IsOpen[t] (s i)
⊢ ∃ (s_1 : Set (↑I : Type u_1)),
    (Subtype.val (p := fun (x : ι) ↦ x ∈ I) '' s_1).Countable ∧
      Eq.{u + 1} (α := Set α) (⋃ y ∈ s_1, s (↑y : ι)) (⋃ i ∈ I, s i)
have rcases : ∀ (T : Set (↑I : Type u_1)) (hTc : T.Countable)
  (hU : Eq.{u + 1} (α := Set α) (⋃ i ∈ T, s (↑i : ι)) (⋃ (i : (↑I : Type u_1)), s (↑i : ι))),
  ∃ (s_1 : Set (↑I : Type u_1)),
    (Subtype.val (p := fun (x : ι) ↦ x ∈ I) '' s_1).Countable ∧
      Eq.{u + 1} (α := Set α) (⋃ y ∈ s_1, s (↑y : ι)) (⋃ i ∈ I, s i)
Tactic: rcases isOpen_iUnion_countable (fun i : I ↦ s i) fun i ↦ H i i.2 with ⟨T, hTc, hU⟩
-- Lean 4 proof step from Mathlib.Topology.Bases (goal)
Goal:
α : Type u
t : TopologicalSpace α
inst : SecondCountableTopology α
f : α → Set α
hf : ∀ (x : α), f x ∈ 𝓝 x
⊢ ∃ (s : Set α), s.Countable ∧ Eq.{u + 1} (α := Set α) (⋃ x ∈ s, f x) univ
have rcases : ∀ (s : Set α) (hsc : s.Countable) (hsU : Eq.{u + 1} (α := Set α) (⋃ i ∈ s, interior (f i)) (⋃ (i : α), interior (f i))),
  ∃ (s : Set α), s.Countable ∧ Eq.{u + 1} (α := Set α) (⋃ x ∈ s, f x) univ
Tactic: rcases isOpen_iUnion_countable (fun x => interior (f x)) fun x => isOpen_interior with
    ⟨s, hsc, hsU⟩
-- Lean 4 proof step from Mathlib.Topology.Bases (goal)
Goal:
α : Type u
t : TopologicalSpace α
inst : SecondCountableTopology α
f : α → Set α
hf : ∀ (x : α), f x ∈ 𝓝 x
s : Set α
hsc : s.Countable
hsU : Eq.{u + 1} (α := Set α) (⋃ i ∈ s, interior (f i)) (⋃ (i : α), interior (f i))
⊢ ∃ (s : Set α), s.Countable ∧ Eq.{u + 1} (α := Set α) (⋃ x ∈ s, f x) univ
have suffices : Eq.{u + 1} (α := Set α) (⋃ x ∈ s, interior (f x)) univ
Tactic: suffices ⋃ x ∈ s, interior (f x) = univ from
    ⟨s, hsc, flip eq_univ_of_subset this <| iUnion₂_mono fun _ _ => interior_subset⟩
-- Lean 4 proof step from Mathlib.Topology.Bases (goal)
Goal:
α : Type u
t : TopologicalSpace α
inst : SecondCountableTopology α
f : α → Set α
hf : ∀ (x : α), f x ∈ 𝓝 x
s : Set α
hsc : s.Countable
hsU : Eq.{u + 1} (α := Set α) (⋃ i ∈ s, interior (f i)) (⋃ (i : α), interior (f i))
⊢ Eq.{u + 1} (α := Set α) (⋃ x ∈ s, interior (f x)) univ
have simp : ∀ (x : α), ∃ (i : α), x ∈ interior (f i)
Tactic: simp only [hsU, eq_univ_iff_forall, mem_iUnion]
-- Lean 4 proof step from Mathlib.Topology.Bases (hypothesis)
Goal:
α : Type u
t : TopologicalSpace α
inst : SecondCountableTopology α
f : α → Set α
s : Set α
hf : ∀ x ∈ s, f x ∈ 𝓝[s] x
⊢ ∃ t ⊆ s, t.Countable ∧ s ⊆ ⋃ x ∈ t, f x
have this : ∀ (x : (↑s : Type u)), Subtype.val (p := fun (x : α) ↦ x ∈ s) ⁻¹' f (↑x : α) ∈ 𝓝 x
Tactic: have : ∀ x : s, (↑) ⁻¹' f x ∈ 𝓝 x := fun x => preimage_coe_mem_nhds_subtype.2 (hf x x.2)