awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.Bases (goal)
Goal:
α : Type u
t : TopologicalSpace α
inst : SecondCountableTopology α
f : α → Set α
s : Set α
hf : ∀ x ∈ s, f x ∈ 𝓝[s] x
this : ∀ (x : (↑s : Type u)), Subtype.val (p := fun (x : α) ↦ x ∈ s) ⁻¹' f (↑x : α) ∈ 𝓝 x
⊢ ∃ t ⊆ s, t.Countable ∧ s ⊆ ⋃ x ∈ t, f x
have rcases : ∀ (t : Set (↑s : Type u)) (htc : t.Countable)
  (htU : Eq.{u + 1} (α := Set (↑s : Type u)) (⋃ x ∈ t, Subtype.val (p := fun (x : α) ↦ x ∈ s) ⁻¹' f (↑x : α)) univ),
  ∃ t ⊆ s, t.Countable ∧ s ⊆ ⋃ x ∈ t, f x
Tactic: rcases countable_cover_nhds this with ⟨t, htc, htU⟩
-- Lean 4 proof step from Mathlib.Topology.Bases (goal)
Goal:
α : Type u
t_1 : TopologicalSpace α
inst : SecondCountableTopology α
f : α → Set α
s : Set α
hf : ∀ x ∈ s, f x ∈ 𝓝[s] x
this : ∀ (x : (↑s : Type u)), Subtype.val (p := fun (x : α) ↦ x ∈ s) ⁻¹' f (↑x : α) ∈ 𝓝 x
t : Set (↑s : Type u)
htc : t.Countable
htU : Eq.{u + 1} (α := Set (↑s : Type u)) (⋃ x ∈ t, Subtype.val (p := fun (x : α) ↦ x ∈ s) ⁻¹' f (↑x : α)) univ
⊢ ∃ t ⊆ s, t.Countable ∧ s ⊆ ⋃ x ∈ t, f x
have refine : ∀ (x : α) (hx : x ∈ s), Membership.mem (γ := Set α) (⋃ x ∈ Subtype.val (p := fun (x : α) ↦ x ∈ s) '' t, f x) x
Tactic: refine ⟨(↑) '' t, Subtype.coe_image_subset _ _, htc.image _, fun x hx => ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Bases (goal)
Goal:
α : Type u
t_1 : TopologicalSpace α
inst : SecondCountableTopology α
f : α → Set α
s : Set α
hf : ∀ x ∈ s, f x ∈ 𝓝[s] x
this : ∀ (x : (↑s : Type u)), Subtype.val (p := fun (x : α) ↦ x ∈ s) ⁻¹' f (↑x : α) ∈ 𝓝 x
t : Set (↑s : Type u)
htc : t.Countable
htU : Eq.{u + 1} (α := Set (↑s : Type u)) (⋃ x ∈ t, Subtype.val (p := fun (x : α) ↦ x ∈ s) ⁻¹' f (↑x : α)) univ
x : α
hx : x ∈ s
⊢ Membership.mem (γ := Set α) (⋃ x ∈ Subtype.val (p := fun (x : α) ↦ x ∈ s) '' t, f x) x
have simp : ∀ (htU : ∀ (x : (↑s : Type u)), Membership.mem (γ := Set α) (⋃ i ∈ t, f (↑i : α)) (↑x : α)),
  Membership.mem (γ := Set α) (⋃ y ∈ t, f (↑y : α)) x
Tactic: simp only [biUnion_image, eq_univ_iff_forall, ← preimage_iUnion, mem_preimage] at htU ⊢
Cleared hypotheses: htU
-- Lean 4 proof step from Mathlib.Topology.Bases (hypothesis)
Goal:
α : Type u
t_1 : TopologicalSpace α
inst : SecondCountableTopology α
t : Set (Set α)
ht : IsTopologicalBasis t
u : Set α
hu : IsOpen[t_1] u
⊢ ∃ s ⊆ t, s.Countable ∧ u = ⋃ a ∈ s, a
have A : ∀ x ∈ u, ∃ a ∈ t, x ∈ a ∧ a ⊆ u
Tactic: have A : ∀ x ∈ u, ∃ a ∈ t, x ∈ a ∧ a ⊆ u :=
    fun x hx ↦ ht.exists_subset_of_mem_open hx hu
-- Lean 4 proof step from Mathlib.Topology.Bases (goal)
Goal:
α : Type u
t_1 : TopologicalSpace α
inst : SecondCountableTopology α
t : Set (Set α)
ht : IsTopologicalBasis t
u : Set α
hu : IsOpen[t_1] u
A : ∀ x ∈ u, ∃ a ∈ t, x ∈ a ∧ a ⊆ u
⊢ ∃ s ⊆ t, s.Countable ∧ u = ⋃ a ∈ s, a
have choose! : ∀ (a : (x : α) → Set α) (hat : ∀ x ∈ u, a x ∈ t) (xa : ∀ x ∈ u, x ∈ a x) (au : ∀ x ∈ u, a x ⊆ u),
  ∃ s ⊆ t, s.Countable ∧ u = ⋃ a ∈ s, a
Tactic: choose! a hat xa au using A
Cleared hypotheses: A
-- Lean 4 proof step from Mathlib.Topology.Bases (goal)
Goal:
α : Type u
t_1 : TopologicalSpace α
inst : SecondCountableTopology α
t : Set (Set α)
ht : IsTopologicalBasis t
u : Set α
hu : IsOpen[t_1] u
a : (x : α) → Set α
hat : ∀ x ∈ u, a x ∈ t
xa : ∀ x ∈ u, x ∈ a x
au : ∀ x ∈ u, a x ⊆ u
⊢ ∃ (T : Set (↑u : Type u)),
    T.Countable ∧ Eq.{u + 1} (α := Set α) (⋃ i ∈ T, a (↑i : α)) (⋃ (i : (↑u : Type u)), a (↑i : α))
have apply : ∀ (i : (↑u : Type u)), IsOpen[t_1] (a (↑i : α))
Tactic: apply isOpen_iUnion_countable _
-- Lean 4 proof step from Mathlib.Topology.Bases (goal)
Goal:
α : Type u
t_1 : TopologicalSpace α
inst : SecondCountableTopology α
t : Set (Set α)
ht : IsTopologicalBasis t
u : Set α
hu : IsOpen[t_1] u
a : (x : α) → Set α
hat : ∀ x ∈ u, a x ∈ t
xa : ∀ x ∈ u, x ∈ a x
au : ∀ x ∈ u, a x ⊆ u
⊢ ∃ s ⊆ t, s.Countable ∧ u = ⋃ a ∈ s, a
have obtain : ∀ (T : Set (↑u : Type u)) (T_count : T.Countable)
  (hT : Eq.{u + 1} (α := Set α) (⋃ i ∈ T, a (↑i : α)) (⋃ (i : (↑u : Type u)), a (↑i : α))),
  ∃ s ⊆ t, s.Countable ∧ u = ⋃ a ∈ s, a
Tactic: obtain ⟨T, T_count, hT⟩ : ∃ T : Set u, T.Countable ∧ ⋃ i ∈ T, a i = ⋃ (i : u), a i := by
    apply isOpen_iUnion_countable _
    rintro ⟨x, hx⟩
    exact ht.isOpen (hat x hx)
-- Lean 4 proof step from Mathlib.Topology.Bases (goal)
Goal:
α : Type u
t_1 : TopologicalSpace α
inst : SecondCountableTopology α
t : Set (Set α)
ht : IsTopologicalBasis t
u : Set α
hu : IsOpen[t_1] u
a : (x : α) → Set α
hat : ∀ x ∈ u, a x ∈ t
xa : ∀ x ∈ u, x ∈ a x
au : ∀ x ∈ u, a x ⊆ u
T : Set (↑u : Type u)
T_count : T.Countable
hT : Eq.{u + 1} (α := Set α) (⋃ i ∈ T, a (↑i : α)) (⋃ (i : (↑u : Type u)), a (↑i : α))
⊢ ∃ s ⊆ t, s.Countable ∧ u = ⋃ a ∈ s, a
have refine_1 : (fun (x : (↑u : Type u)) ↦ a (↑x : α)) '' T ⊆ t
Tactic: refine ⟨(fun (x : u) ↦ a x) '' T, ?_, T_count.image _, ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Bases (goal)
Goal:
α : Type u
t_1 : TopologicalSpace α
inst : SecondCountableTopology α
t : Set (Set α)
ht : IsTopologicalBasis t
u : Set α
hu : IsOpen[t_1] u
a : (x : α) → Set α
hat : ∀ x ∈ u, a x ∈ t
xa : ∀ x ∈ u, x ∈ a x
au : ∀ x ∈ u, a x ⊆ u
T : Set (↑u : Type u)
T_count : T.Countable
hT : Eq.{u + 1} (α := Set α) (⋃ i ∈ T, a (↑i : α)) (⋃ (i : (↑u : Type u)), a (↑i : α))
refine_1 : (fun (x : (↑u : Type u)) ↦ a (↑x : α)) '' T ⊆ t
⊢ ∃ s ⊆ t, s.Countable ∧ u = ⋃ a ∈ s, a
have refine_2 : u = ⋃ (a_1 : Set α), ⋃ (_ : Membership.mem (γ := Set (Set α)) ((fun (x : (↑u : Type u)) ↦ a (↑x : α)) '' T) a_1), a_1
Tactic: refine ⟨(fun (x : u) ↦ a x) '' T, ?_, T_count.image _, ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Bases (goal)
Goal:
α : Type u
t_1 : TopologicalSpace α
inst : SecondCountableTopology α
t : Set (Set α)
ht : IsTopologicalBasis t
u : Set α
hu : IsOpen[t_1] u
a : (x : α) → Set α
hat : ∀ x ∈ u, a x ∈ t
xa : ∀ x ∈ u, x ∈ a x
au : ∀ x ∈ u, a x ⊆ u
T : Set (↑u : Type u)
T_count : T.Countable
hT : Eq.{u + 1} (α := Set α) (⋃ i ∈ T, a (↑i : α)) (⋃ (i : (↑u : Type u)), a (↑i : α))
⊢ (fun (x : (↑u : Type u)) ↦ a (↑x : α)) '' T ⊆ t
have refine_1 : T ⊆ (fun (x : (↑u : Type u)) ↦ a (↑x : α)) ⁻¹' t
Tactic: simp only [image_subset_iff]
-- Lean 4 proof step from Mathlib.Topology.Bases (goal)
Goal:
α : Type u
t_1 : TopologicalSpace α
inst : SecondCountableTopology α
t : Set (Set α)
ht : IsTopologicalBasis t
u : Set α
hu : IsOpen[t_1] u
a : (x : α) → Set α
hat : ∀ x ∈ u, a x ∈ t
xa : ∀ x ∈ u, x ∈ a x
au : ∀ x ∈ u, a x ⊆ u
T : Set (↑u : Type u)
T_count : T.Countable
hT : Eq.{u + 1} (α := Set α) (⋃ i ∈ T, a (↑i : α)) (⋃ (i : (↑u : Type u)), a (↑i : α))
⊢ u = ⋃ (a_1 : Set α), ⋃ (_ : Membership.mem (γ := Set (Set α)) ((fun (x : (↑u : Type u)) ↦ a (↑x : α)) '' T) a_1), a_1
have refine_2 : u = ⋃ (i : (↑u : Type u)), a (↑i : α)
Tactic: rw [biUnion_image, hT]
-- Lean 4 proof step from Mathlib.Topology.Bases (goal)
Goal:
α : Type u
t_1 : TopologicalSpace α
inst : SecondCountableTopology α
t : Set (Set α)
ht : IsTopologicalBasis t
u : Set α
hu : IsOpen[t_1] u
a : (x : α) → Set α
hat : ∀ x ∈ u, a x ∈ t
xa : ∀ x ∈ u, x ∈ a x
au : ∀ x ∈ u, a x ⊆ u
T : Set (↑u : Type u)
T_count : T.Countable
hT : Eq.{u + 1} (α := Set α) (⋃ i ∈ T, a (↑i : α)) (⋃ (i : (↑u : Type u)), a (↑i : α))
⊢ u = ⋃ (i : (↑u : Type u)), a (↑i : α)
have refine_2 : u ⊆ ⋃ (i : (↑u : Type u)), a (↑i : α)
Tactic: apply Subset.antisymm
-- Lean 4 proof step from Mathlib.Topology.Bases (goal)
Goal:
α : Type u
t_1 : TopologicalSpace α
inst : SecondCountableTopology α
t : Set (Set α)
ht : IsTopologicalBasis t
u : Set α
hu : IsOpen[t_1] u
a : (x : α) → Set α
hat : ∀ x ∈ u, a x ∈ t
xa : ∀ x ∈ u, x ∈ a x
au : ∀ x ∈ u, a x ⊆ u
T : Set (↑u : Type u)
T_count : T.Countable
hT : Eq.{u + 1} (α := Set α) (⋃ i ∈ T, a (↑i : α)) (⋃ (i : (↑u : Type u)), a (↑i : α))
refine_2 : u ⊆ ⋃ (i : (↑u : Type u)), a (↑i : α)
⊢ u = ⋃ (i : (↑u : Type u)), a (↑i : α)
have refine_2₁ : ⋃ (i : (↑u : Type u)), a (↑i : α) ⊆ u
Tactic: apply Subset.antisymm
-- Lean 4 proof step from Mathlib.Topology.Bases (goal)
Goal:
α : Type u
t_1 : TopologicalSpace α
inst : SecondCountableTopology α
t : Set (Set α)
ht : IsTopologicalBasis t
u : Set α
hu : IsOpen[t_1] u
a : (x : α) → Set α
hat : ∀ x ∈ u, a x ∈ t
xa : ∀ x ∈ u, x ∈ a x
au : ∀ x ∈ u, a x ⊆ u
T : Set (↑u : Type u)
T_count : T.Countable
hT : Eq.{u + 1} (α := Set α) (⋃ i ∈ T, a (↑i : α)) (⋃ (i : (↑u : Type u)), a (↑i : α))
x : α
hx : x ∈ u
⊢ Membership.mem (γ := Set α) (⋃ (i : (↑u : Type u)), a (↑i : α)) x
have refine_2 : ∃ i ∈ u, x ∈ a i
Tactic: simp
-- Lean 4 proof step from Mathlib.Topology.Bases (hypothesis)
Goal:
α : Type u
t_1 : TopologicalSpace α
inst : SecondCountableTopology α
t : Set (Set α)
ht : IsTopologicalBasis t
⊢ ∃ s ⊆ t, s.Countable ∧ IsTopologicalBasis s
have A : ∀ u ∈ countableBasis α, ∃ s ⊆ t, s.Countable ∧ u = ⋃ a ∈ s, a
Tactic: have A : ∀ u ∈ countableBasis α, ∃ s ⊆ t, s.Countable ∧ u = ⋃ a ∈ s, a :=
    fun u hu ↦ ht.exists_countable_biUnion_of_isOpen ((isBasis_countableBasis α).isOpen hu)
-- Lean 4 proof step from Mathlib.Topology.Bases (goal)
Goal:
α : Type u
t_1 : TopologicalSpace α
inst : SecondCountableTopology α
t : Set (Set α)
ht : IsTopologicalBasis t
A : ∀ u ∈ countableBasis α, ∃ s ⊆ t, s.Countable ∧ u = ⋃ a ∈ s, a
⊢ ∃ s ⊆ t, s.Countable ∧ IsTopologicalBasis s
have choose! : ∀ (s : (u : Set α) → Set (Set α)) (hst : ∀ u ∈ countableBasis α, s u ⊆ t)
  (s_count : ∀ u ∈ countableBasis α, (s u).Countable) (hs : ∀ u ∈ countableBasis α, u = ⋃ a ∈ s u, a),
  ∃ s ⊆ t, s.Countable ∧ IsTopologicalBasis s
Tactic: choose! s hst s_count hs using A
Cleared hypotheses: A
-- Lean 4 proof step from Mathlib.Topology.Bases (goal)
Goal:
α : Type u
t_1 : TopologicalSpace α
inst : SecondCountableTopology α
t : Set (Set α)
ht : IsTopologicalBasis t
s : (u : Set α) → Set (Set α)
hst : ∀ u ∈ countableBasis α, s u ⊆ t
s_count : ∀ u ∈ countableBasis α, (s u).Countable
hs : ∀ u ∈ countableBasis α, u = ⋃ a ∈ s u, a
⊢ ∃ s ⊆ t, s.Countable ∧ IsTopologicalBasis s
have refine : IsTopologicalBasis.{u} (α := α) (⋃ u ∈ countableBasis α, s u)
Tactic: refine ⟨⋃ u ∈ countableBasis α, s u, by simpa using hst,
    (countable_countableBasis α).biUnion s_count, ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Bases (goal)
Goal:
α : Type u
t_1 : TopologicalSpace α
inst : SecondCountableTopology α
t : Set (Set α)
ht : IsTopologicalBasis t
s : (u : Set α) → Set (Set α)
hst : ∀ u ∈ countableBasis α, s u ⊆ t
s_count : ∀ u ∈ countableBasis α, (s u).Countable
hs : ∀ u ∈ countableBasis α, u = ⋃ a ∈ s u, a
⊢ IsTopologicalBasis.{u} (α := α) (⋃ u ∈ countableBasis α, s u)
have h_open : ∀ (u : Set α), Membership.mem (γ := Set (Set α)) (⋃ u ∈ countableBasis α, s u) u → IsOpen[t_1] u
Tactic: apply isTopologicalBasis_of_isOpen_of_nhds
-- Lean 4 proof step from Mathlib.Topology.Bases (goal)
Goal:
α : Type u
t_1 : TopologicalSpace α
inst : SecondCountableTopology α
t : Set (Set α)
ht : IsTopologicalBasis t
s : (u : Set α) → Set (Set α)
hst : ∀ u ∈ countableBasis α, s u ⊆ t
s_count : ∀ u ∈ countableBasis α, (s u).Countable
hs : ∀ u ∈ countableBasis α, u = ⋃ a ∈ s u, a
h_open : ∀ (u : Set α), Membership.mem (γ := Set (Set α)) (⋃ u ∈ countableBasis α, s u) u → IsOpen[t_1] u
⊢ IsTopologicalBasis.{u} (α := α) (⋃ u ∈ countableBasis α, s u)
have h_nhds : ∀ (a : α) (u : Set α),
  a ∈ u →
    IsOpen[t_1] u → ∃ (v : Set α), Membership.mem (γ := Set (Set α)) (⋃ u ∈ countableBasis α, s u) v ∧ a ∈ v ∧ v ⊆ u
Tactic: apply isTopologicalBasis_of_isOpen_of_nhds
-- Lean 4 proof step from Mathlib.Topology.Bases (goal)
Goal:
α : Type u
t_1 : TopologicalSpace α
inst : SecondCountableTopology α
t : Set (Set α)
ht : IsTopologicalBasis t
s : (u : Set α) → Set (Set α)
hst : ∀ u ∈ countableBasis α, s u ⊆ t
s_count : ∀ u ∈ countableBasis α, (s u).Countable
hs : ∀ u ∈ countableBasis α, u = ⋃ a ∈ s u, a
⊢ ∀ (u : Set α), Membership.mem (γ := Set (Set α)) (⋃ u ∈ countableBasis α, s u) u → IsOpen[t_1] u
have h_open : ∀ (u x : Set α), x ∈ countableBasis α → u ∈ s x → IsOpen[t_1] u
Tactic: simp only [mem_iUnion, exists_prop, forall_exists_index, and_imp]
-- Lean 4 proof step from Mathlib.Topology.Bases (hypothesis)
Goal:
α : Type u
t_1 : TopologicalSpace α
inst : SecondCountableTopology α
t : Set (Set α)
ht : IsTopologicalBasis t
s : (u : Set α) → Set (Set α)
hst : ∀ u ∈ countableBasis α, s u ⊆ t
s_count : ∀ u ∈ countableBasis α, (s u).Countable
hs : ∀ u ∈ countableBasis α, u = ⋃ a ∈ s u, a
⊢ ∀ (u x : Set α), x ∈ countableBasis α → u ∈ s x → IsOpen[t_1] u
have this : ∀ (s : Set α) (hs : s ∈ t), IsOpen[t_1] s
Tactic: have := @ht.isOpen
-- Lean 4 proof step from Mathlib.Topology.Bases (goal)
Goal:
α : Type u
t_1 : TopologicalSpace α
inst : SecondCountableTopology α
t : Set (Set α)
ht : IsTopologicalBasis t
s : (u : Set α) → Set (Set α)
hst : ∀ u ∈ countableBasis α, s u ⊆ t
s_count : ∀ u ∈ countableBasis α, (s u).Countable
hs : ∀ u ∈ countableBasis α, u = ⋃ a ∈ s u, a
x : α
v : Set α
hx : x ∈ v
hv : IsOpen[t_1] v
⊢ ∃ (v_1 : Set α), Membership.mem (γ := Set (Set α)) (⋃ u ∈ countableBasis α, s u) v_1 ∧ x ∈ v_1 ∧ v_1 ⊆ v
have h_nhds : ∃ (v_1 : Set α), (∃ i ∈ countableBasis α, v_1 ∈ s i) ∧ x ∈ v_1 ∧ v_1 ⊆ v
Tactic: simp only [mem_iUnion, exists_prop]
-- Lean 4 proof step from Mathlib.Topology.Bases (goal)
Goal:
α : Type u
t_1 : TopologicalSpace α
inst : SecondCountableTopology α
t : Set (Set α)
ht : IsTopologicalBasis t
s : (u : Set α) → Set (Set α)
hst : ∀ u ∈ countableBasis α, s u ⊆ t
s_count : ∀ u ∈ countableBasis α, (s u).Countable
hs : ∀ u ∈ countableBasis α, u = ⋃ a ∈ s u, a
x : α
v : Set α
hx : x ∈ v
hv : IsOpen[t_1] v
⊢ ∃ (v_1 : Set α), (∃ i ∈ countableBasis α, v_1 ∈ s i) ∧ x ∈ v_1 ∧ v_1 ⊆ v
have h_nhds : ∀ (u : Set α) (u_mem : u ∈ countableBasis α) (xu : x ∈ u) (uv : u ⊆ v),
  ∃ (v_1 : Set α), (∃ i ∈ countableBasis α, v_1 ∈ s i) ∧ x ∈ v_1 ∧ v_1 ⊆ v
Tactic: obtain ⟨u, u_mem, xu, uv⟩ : ∃ u ∈ countableBasis α, x ∈ u ∧ u ⊆ v :=
      (isBasis_countableBasis α).isOpen_iff.1 hv _ hx
-- Lean 4 proof step from Mathlib.Topology.Bases (goal)
Goal:
α : Type u
t_1 : TopologicalSpace α
inst : SecondCountableTopology α
t : Set (Set α)
ht : IsTopologicalBasis t
s : (u : Set α) → Set (Set α)
hst : ∀ u ∈ countableBasis α, s u ⊆ t
s_count : ∀ u ∈ countableBasis α, (s u).Countable
hs : ∀ u ∈ countableBasis α, u = ⋃ a ∈ s u, a
x : α
v : Set α
hx : x ∈ v
hv : IsOpen[t_1] v
u : Set α
u_mem : u ∈ countableBasis α
xu : x ∈ u
uv : u ⊆ v
⊢ Membership.mem (γ := Set α) (⋃ a ∈ s u, a) x
have h : ⋃ a ∈ s u, a = u
Tactic: convert! xu
-- Lean 4 proof step from Mathlib.Topology.Bases (hypothesis)
Goal:
α : Type u
t_1 : TopologicalSpace α
inst : SecondCountableTopology α
t : Set (Set α)
ht : IsTopologicalBasis t
s : (u : Set α) → Set (Set α)
hst : ∀ u ∈ countableBasis α, s u ⊆ t
s_count : ∀ u ∈ countableBasis α, (s u).Countable
hs : ∀ u ∈ countableBasis α, u = ⋃ a ∈ s u, a
x : α
v : Set α
hx : x ∈ v
hv : IsOpen[t_1] v
u : Set α
u_mem : u ∈ countableBasis α
xu : x ∈ u
uv : u ⊆ v
⊢ ∃ (v_1 : Set α), (∃ i ∈ countableBasis α, v_1 ∈ s i) ∧ x ∈ v_1 ∧ v_1 ⊆ v
have this : Membership.mem (γ := Set α) (⋃ a ∈ s u, a) x
Tactic: have : x ∈ ⋃ a ∈ s u, a := by
      convert! xu
      exact (hs u u_mem).symm
-- Lean 4 proof step from Mathlib.Topology.Bases (goal)
Goal:
α : Type u
t_1 : TopologicalSpace α
inst : SecondCountableTopology α
t : Set (Set α)
ht : IsTopologicalBasis t
s : (u : Set α) → Set (Set α)
hst : ∀ u ∈ countableBasis α, s u ⊆ t
s_count : ∀ u ∈ countableBasis α, (s u).Countable
hs : ∀ u ∈ countableBasis α, u = ⋃ a ∈ s u, a
x : α
v : Set α
hx : x ∈ v
hv : IsOpen[t_1] v
u : Set α
u_mem : u ∈ countableBasis α
xu : x ∈ u
uv : u ⊆ v
this : Membership.mem (γ := Set α) (⋃ a ∈ s u, a) x
⊢ ∃ (v_1 : Set α), (∃ i ∈ countableBasis α, v_1 ∈ s i) ∧ x ∈ v_1 ∧ v_1 ⊆ v
have h_nhds : ∀ (w : Set α) (ws : w ∈ s u) (xw : x ∈ w), ∃ (v_1 : Set α), (∃ i ∈ countableBasis α, v_1 ∈ s i) ∧ x ∈ v_1 ∧ v_1 ⊆ v
Tactic: obtain ⟨w, ws, xw⟩ : ∃ w ∈ s u, x ∈ w := by simpa using this
-- Lean 4 proof step from Mathlib.Topology.Bases (goal)
Goal:
α : Type u
t_1 : TopologicalSpace α
inst : SecondCountableTopology α
t : Set (Set α)
ht : IsTopologicalBasis t
s : (u : Set α) → Set (Set α)
hst : ∀ u ∈ countableBasis α, s u ⊆ t
s_count : ∀ u ∈ countableBasis α, (s u).Countable
hs : ∀ u ∈ countableBasis α, u = ⋃ a ∈ s u, a
x : α
v : Set α
hx : x ∈ v
hv : IsOpen[t_1] v
u : Set α
u_mem : u ∈ countableBasis α
xu : x ∈ u
uv : u ⊆ v
this : Membership.mem (γ := Set α) (⋃ a ∈ s u, a) x
w : Set α
ws : w ∈ s u
xw : x ∈ w
⊢ ∃ (v_1 : Set α), (∃ i ∈ countableBasis α, v_1 ∈ s i) ∧ x ∈ v_1 ∧ v_1 ⊆ v
have h_nhds : w ⊆ v
Tactic: refine ⟨w, ⟨u, u_mem, ws⟩, xw, ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Bases (goal)
Goal:
α : Type u
t_1 : TopologicalSpace α
inst : SecondCountableTopology α
t : Set (Set α)
ht : IsTopologicalBasis t
s : (u : Set α) → Set (Set α)
hst : ∀ u ∈ countableBasis α, s u ⊆ t
s_count : ∀ u ∈ countableBasis α, (s u).Countable
hs : ∀ u ∈ countableBasis α, u = ⋃ a ∈ s u, a
x : α
v : Set α
hx : x ∈ v
hv : IsOpen[t_1] v
u : Set α
u_mem : u ∈ countableBasis α
xu : x ∈ u
uv : u ⊆ v
this : Membership.mem (γ := Set α) (⋃ a ∈ s u, a) x
w : Set α
ws : w ∈ s u
xw : x ∈ w
⊢ w ⊆ v
have apply : w ⊆ ⋃ a ∈ s u, a
Tactic: apply Subset.trans (Subset.trans _ (hs u u_mem).symm.subset) uv
-- Lean 4 proof step from Mathlib.Topology.Bases (hypothesis)
Goal:
α : Type u_1
ts : TopologicalSpace α
inst : SecondCountableTopology α
t : Set (Set α)
ht : ts = generateFrom t
t' : Set (Set α) := (fun (f : Set (Set α)) ↦ ⋂₀ f) '' {f : Set (Set α) | f.Finite ∧ f ⊆ t}
⊢ ∃ s ⊆ t, s.Countable ∧ ts = generateFrom s
have this : IsTopologicalBasis t'
Tactic: have : IsTopologicalBasis t' := TopologicalSpace.isTopologicalBasis_of_subbasis ht
-- Lean 4 proof step from Mathlib.Topology.Bases (goal)
Goal:
α : Type u_1
ts : TopologicalSpace α
inst : SecondCountableTopology α
t : Set (Set α)
ht : ts = generateFrom t
t' : Set (Set α) := (fun (f : Set (Set α)) ↦ ⋂₀ f) '' {f : Set (Set α) | f.Finite ∧ f ⊆ t}
this : IsTopologicalBasis t'
⊢ ∃ s ⊆ t, s.Countable ∧ ts = generateFrom s
have obtain : ∀ (s' : Set (Set α)) (s't' : s' ⊆ t') (s'_count : s'.Countable) (hs' : IsTopologicalBasis s'),
  ∃ s ⊆ t, s.Countable ∧ ts = generateFrom s
Tactic: obtain ⟨s', s't', s'_count, hs'⟩ : ∃ s' ⊆ t', s'.Countable ∧ IsTopologicalBasis s' :=
    this.exists_countable
-- Lean 4 proof step from Mathlib.Topology.Bases (hypothesis)
Goal:
α : Type u_1
ts : TopologicalSpace α
inst : SecondCountableTopology α
t : Set (Set α)
ht : ts = generateFrom t
t' : Set (Set α) := (fun (f : Set (Set α)) ↦ ⋂₀ f) '' {f : Set (Set α) | f.Finite ∧ f ⊆ t}
this : IsTopologicalBasis t'
s' : Set (Set α)
s't' : s' ⊆ t'
s'_count : s'.Countable
hs' : IsTopologicalBasis s'
⊢ ∃ s ⊆ t, s.Countable ∧ ts = generateFrom s
have A : ∀ u ∈ s', ∃ (f : Set (Set α)), f.Finite ∧ f ⊆ t ∧ ⋂₀ f = u
Tactic: have A : ∀ u ∈ s', ∃ (f : Set (Set α)), f.Finite ∧ f ⊆ t ∧ ⋂₀ f = u :=
    fun u hu ↦ by simpa [t', and_assoc] using s't' hu
-- Lean 4 proof step from Mathlib.Topology.Bases (goal)
Goal:
α : Type u_1
ts : TopologicalSpace α
inst : SecondCountableTopology α
t : Set (Set α)
ht : ts = generateFrom t
t' : Set (Set α) := (fun (f : Set (Set α)) ↦ ⋂₀ f) '' {f : Set (Set α) | f.Finite ∧ f ⊆ t}
this : IsTopologicalBasis t'
s' : Set (Set α)
s't' : s' ⊆ t'
s'_count : s'.Countable
hs' : IsTopologicalBasis s'
A : ∀ u ∈ s', ∃ (f : Set (Set α)), f.Finite ∧ f ⊆ t ∧ ⋂₀ f = u
⊢ ∃ s ⊆ t, s.Countable ∧ ts = generateFrom s
have choose! : ∀ (f : (u : Set α) → Set (Set α)) (f_fin : ∀ u ∈ s', (f u).Finite) (ft : ∀ u ∈ s', f u ⊆ t) (hf : ∀ u ∈ s', ⋂₀ f u = u),
  ∃ s ⊆ t, s.Countable ∧ ts = generateFrom s
Tactic: choose! f f_fin ft hf using A
Cleared hypotheses: A
-- Lean 4 proof step from Mathlib.Topology.Bases (goal)
Goal:
α : Type u_1
ts : TopologicalSpace α
inst : SecondCountableTopology α
t : Set (Set α)
ht : ts = generateFrom t
t' : Set (Set α) := (fun (f : Set (Set α)) ↦ ⋂₀ f) '' {f : Set (Set α) | f.Finite ∧ f ⊆ t}
this : IsTopologicalBasis t'
s' : Set (Set α)
s't' : s' ⊆ t'
s'_count : s'.Countable
hs' : IsTopologicalBasis s'
f : (u : Set α) → Set (Set α)
f_fin : ∀ u ∈ s', (f u).Finite
ft : ∀ u ∈ s', f u ⊆ t
hf : ∀ u ∈ s', ⋂₀ f u = u
⊢ ∃ s ⊆ t, s.Countable ∧ ts = generateFrom s
have refine_1 : Set.Countable.{u_1} (α := Set α) (⋃ u ∈ s', f u)
Tactic: refine ⟨⋃ u ∈ s', f u, by simpa using ft, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Bases (goal)
Goal:
α : Type u_1
ts : TopologicalSpace α
inst : SecondCountableTopology α
t : Set (Set α)
ht : ts = generateFrom t
t' : Set (Set α) := (fun (f : Set (Set α)) ↦ ⋂₀ f) '' {f : Set (Set α) | f.Finite ∧ f ⊆ t}
this : IsTopologicalBasis t'
s' : Set (Set α)
s't' : s' ⊆ t'
s'_count : s'.Countable
hs' : IsTopologicalBasis s'
f : (u : Set α) → Set (Set α)
f_fin : ∀ u ∈ s', (f u).Finite
ft : ∀ u ∈ s', f u ⊆ t
hf : ∀ u ∈ s', ⋂₀ f u = u
refine_1 : Set.Countable.{u_1} (α := Set α) (⋃ u ∈ s', f u)
⊢ ∃ s ⊆ t, s.Countable ∧ ts = generateFrom s
have refine_2 : ts = generateFrom (⋃ u ∈ s', f u)
Tactic: refine ⟨⋃ u ∈ s', f u, by simpa using ft, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Bases (goal)
Goal:
α : Type u_1
ts : TopologicalSpace α
inst : SecondCountableTopology α
t : Set (Set α)
ht : ts = generateFrom t
t' : Set (Set α) := (fun (f : Set (Set α)) ↦ ⋂₀ f) '' {f : Set (Set α) | f.Finite ∧ f ⊆ t}
this : IsTopologicalBasis t'
s' : Set (Set α)
s't' : s' ⊆ t'
s'_count : s'.Countable
hs' : IsTopologicalBasis s'
f : (u : Set α) → Set (Set α)
f_fin : ∀ u ∈ s', (f u).Finite
ft : ∀ u ∈ s', f u ⊆ t
hf : ∀ u ∈ s', ⋂₀ f u = u
⊢ Set.Countable.{u_1} (α := Set α) (⋃ u ∈ s', f u)
have refine_1 : ∀ (a : Set α) (ha : a ∈ s'), (f a).Countable
Tactic: apply s'_count.biUnion
-- Lean 4 proof step from Mathlib.Topology.Bases (goal)
Goal:
α : Type u_1
ts : TopologicalSpace α
inst : SecondCountableTopology α
t : Set (Set α)
ht : ts = generateFrom t
t' : Set (Set α) := (fun (f : Set (Set α)) ↦ ⋂₀ f) '' {f : Set (Set α) | f.Finite ∧ f ⊆ t}
this : IsTopologicalBasis t'
s' : Set (Set α)
s't' : s' ⊆ t'
s'_count : s'.Countable
hs' : IsTopologicalBasis s'
f : (u : Set α) → Set (Set α)
f_fin : ∀ u ∈ s', (f u).Finite
ft : ∀ u ∈ s', f u ⊆ t
hf : ∀ u ∈ s', ⋂₀ f u = u
⊢ ts = generateFrom (⋃ u ∈ s', f u)
have refine_2 : ts ≤ generateFrom (⋃ u ∈ s', f u)
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.Topology.Bases (goal)
Goal:
α : Type u_1
ts : TopologicalSpace α
inst : SecondCountableTopology α
t : Set (Set α)
ht : ts = generateFrom t
t' : Set (Set α) := (fun (f : Set (Set α)) ↦ ⋂₀ f) '' {f : Set (Set α) | f.Finite ∧ f ⊆ t}
this : IsTopologicalBasis t'
s' : Set (Set α)
s't' : s' ⊆ t'
s'_count : s'.Countable
hs' : IsTopologicalBasis s'
f : (u : Set α) → Set (Set α)
f_fin : ∀ u ∈ s', (f u).Finite
ft : ∀ u ∈ s', f u ⊆ t
hf : ∀ u ∈ s', ⋂₀ f u = u
refine_2 : ts ≤ generateFrom (⋃ u ∈ s', f u)
⊢ ts = generateFrom (⋃ u ∈ s', f u)
have refine_2₁ : generateFrom (⋃ u ∈ s', f u) ≤ ts
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.Topology.Bases (goal)
Goal:
α : Type u_1
ts : TopologicalSpace α
inst : SecondCountableTopology α
t : Set (Set α)
ht : ts = generateFrom t
t' : Set (Set α) := (fun (f : Set (Set α)) ↦ ⋂₀ f) '' {f : Set (Set α) | f.Finite ∧ f ⊆ t}
this : IsTopologicalBasis t'
s' : Set (Set α)
s't' : s' ⊆ t'
s'_count : s'.Countable
hs' : IsTopologicalBasis s'
f : (u : Set α) → Set (Set α)
f_fin : ∀ u ∈ s', (f u).Finite
ft : ∀ u ∈ s', f u ⊆ t
hf : ∀ u ∈ s', ⋂₀ f u = u
⊢ ts ≤ generateFrom (⋃ u ∈ s', f u)
have refine_2 : Subset.{u_1} (α := Set (Set α)) (⋃ u ∈ s', f u) {s : Set α | IsOpen[ts] s}
Tactic: apply le_generateFrom_iff_subset_isOpen.2
-- Lean 4 proof step from Mathlib.Topology.Bases (goal)
Goal:
α : Type u_1
ts : TopologicalSpace α
inst : SecondCountableTopology α
t : Set (Set α)
ht : ts = generateFrom t
t' : Set (Set α) := (fun (f : Set (Set α)) ↦ ⋂₀ f) '' {f : Set (Set α) | f.Finite ∧ f ⊆ t}
this : IsTopologicalBasis t'
s' : Set (Set α)
s't' : s' ⊆ t'
s'_count : s'.Countable
hs' : IsTopologicalBasis s'
f : (u : Set α) → Set (Set α)
f_fin : ∀ u ∈ s', (f u).Finite
ft : ∀ u ∈ s', f u ⊆ t
hf : ∀ u ∈ s', ⋂₀ f u = u
⊢ Subset.{u_1} (α := Set (Set α)) (⋃ u ∈ s', f u) {s : Set α | IsOpen[ts] s}
have refine_2 : ∀ (i : Set α) (i_1 : i ∈ s'), f i ⊆ {s : Set α | IsOpen[ts] s}
Tactic: simp only [iUnion_subset_iff]