awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.Bases (goal)
Goal:
α : Type u
β : Type u_1
t_1 : TopologicalSpace α
B : Set (Set α)
s_1 : Set α
inst : TopologicalSpace β
inst_1 : SeparableSpace α
inst_2 : SeparableSpace β
s : Set α
hsc : s.Countable
hsd : Dense s
t : Set β
htc : t.Countable
htd : Dense t
simp_rw : closure[instTopologicalSpaceSum] (Sum.inl '' s ∪ Sum.inr '' t) = univ
⊢ Dense (Sum.inl '' s ∪ Sum.inr '' t)
have simp_rw₁ : closure[instTopologicalSpaceSum] (Sum.inl '' s) ∪ closure[instTopologicalSpaceSum] (Sum.inr '' t) = univ
Tactic: simp_rw [dense_iff_closure_eq, closure_union, IsClosedEmbedding.inl.closure_image_eq,
    hsd.closure_eq, IsClosedEmbedding.inr.closure_image_eq, htd.closure_eq, image_univ,
    range_inl_union_range_inr]
-- Lean 4 proof step from Mathlib.Topology.Bases (goal)
Goal:
α : Type u
β : Type u_1
t_1 : TopologicalSpace α
B : Set (Set α)
s_1 : Set α
inst : TopologicalSpace β
inst_1 : SeparableSpace α
inst_2 : SeparableSpace β
s : Set α
hsc : s.Countable
hsd : Dense s
t : Set β
htc : t.Countable
htd : Dense t
simp_rw : closure[instTopologicalSpaceSum] (Sum.inl '' s ∪ Sum.inr '' t) = univ
simp_rw₁ : closure[instTopologicalSpaceSum] (Sum.inl '' s) ∪ closure[instTopologicalSpaceSum] (Sum.inr '' t) = univ
⊢ Dense (Sum.inl '' s ∪ Sum.inr '' t)
have simp_rw₂ : Sum.inl '' closure[t_1] s ∪ closure[instTopologicalSpaceSum] (Sum.inr '' t) = univ
Tactic: simp_rw [dense_iff_closure_eq, closure_union, IsClosedEmbedding.inl.closure_image_eq,
    hsd.closure_eq, IsClosedEmbedding.inr.closure_image_eq, htd.closure_eq, image_univ,
    range_inl_union_range_inr]
-- Lean 4 proof step from Mathlib.Topology.Bases (goal)
Goal:
α : Type u
β : Type u_1
t_1 : TopologicalSpace α
B : Set (Set α)
s_1 : Set α
inst : TopologicalSpace β
inst_1 : SeparableSpace α
inst_2 : SeparableSpace β
s : Set α
hsc : s.Countable
hsd : Dense s
t : Set β
htc : t.Countable
htd : Dense t
simp_rw : closure[instTopologicalSpaceSum] (Sum.inl '' s ∪ Sum.inr '' t) = univ
simp_rw₁ : closure[instTopologicalSpaceSum] (Sum.inl '' s) ∪ closure[instTopologicalSpaceSum] (Sum.inr '' t) = univ
simp_rw₂ : Sum.inl '' closure[t_1] s ∪ closure[instTopologicalSpaceSum] (Sum.inr '' t) = univ
⊢ Dense (Sum.inl '' s ∪ Sum.inr '' t)
have simp_rw₃ : Eq (α := Set (α ⊕ β)) (Sum.inl '' univ ∪ closure[instTopologicalSpaceSum] (Sum.inr '' t)) univ
Tactic: simp_rw [dense_iff_closure_eq, closure_union, IsClosedEmbedding.inl.closure_image_eq,
    hsd.closure_eq, IsClosedEmbedding.inr.closure_image_eq, htd.closure_eq, image_univ,
    range_inl_union_range_inr]
-- Lean 4 proof step from Mathlib.Topology.Bases (goal)
Goal:
α : Type u
β : Type u_1
t_1 : TopologicalSpace α
B : Set (Set α)
s_1 : Set α
inst : TopologicalSpace β
inst_1 : SeparableSpace α
inst_2 : SeparableSpace β
s : Set α
hsc : s.Countable
hsd : Dense s
t : Set β
htc : t.Countable
htd : Dense t
simp_rw : closure[instTopologicalSpaceSum] (Sum.inl '' s ∪ Sum.inr '' t) = univ
simp_rw₁ : closure[instTopologicalSpaceSum] (Sum.inl '' s) ∪ closure[instTopologicalSpaceSum] (Sum.inr '' t) = univ
simp_rw₂ : Sum.inl '' closure[t_1] s ∪ closure[instTopologicalSpaceSum] (Sum.inr '' t) = univ
simp_rw₃ : Eq (α := Set (α ⊕ β)) (Sum.inl '' univ ∪ closure[instTopologicalSpaceSum] (Sum.inr '' t)) univ
⊢ Dense (Sum.inl '' s ∪ Sum.inr '' t)
have simp_rw₄ : Eq (α := Set (α ⊕ β)) (Sum.inl '' univ ∪ Sum.inr '' closure[inst] t) univ
Tactic: simp_rw [dense_iff_closure_eq, closure_union, IsClosedEmbedding.inl.closure_image_eq,
    hsd.closure_eq, IsClosedEmbedding.inr.closure_image_eq, htd.closure_eq, image_univ,
    range_inl_union_range_inr]
-- Lean 4 proof step from Mathlib.Topology.Bases (goal)
Goal:
α : Type u
β : Type u_1
t_1 : TopologicalSpace α
B : Set (Set α)
s_1 : Set α
inst : TopologicalSpace β
inst_1 : SeparableSpace α
inst_2 : SeparableSpace β
s : Set α
hsc : s.Countable
hsd : Dense s
t : Set β
htc : t.Countable
htd : Dense t
simp_rw : closure[instTopologicalSpaceSum] (Sum.inl '' s ∪ Sum.inr '' t) = univ
simp_rw₁ : closure[instTopologicalSpaceSum] (Sum.inl '' s) ∪ closure[instTopologicalSpaceSum] (Sum.inr '' t) = univ
simp_rw₂ : Sum.inl '' closure[t_1] s ∪ closure[instTopologicalSpaceSum] (Sum.inr '' t) = univ
simp_rw₃ : Eq (α := Set (α ⊕ β)) (Sum.inl '' univ ∪ closure[instTopologicalSpaceSum] (Sum.inr '' t)) univ
simp_rw₄ : Eq (α := Set (α ⊕ β)) (Sum.inl '' univ ∪ Sum.inr '' closure[inst] t) univ
⊢ Dense (Sum.inl '' s ∪ Sum.inr '' t)
have simp_rw₅ : Eq (α := Set (α ⊕ β)) (Sum.inl '' univ ∪ Sum.inr '' univ) univ
Tactic: simp_rw [dense_iff_closure_eq, closure_union, IsClosedEmbedding.inl.closure_image_eq,
    hsd.closure_eq, IsClosedEmbedding.inr.closure_image_eq, htd.closure_eq, image_univ,
    range_inl_union_range_inr]
-- Lean 4 proof step from Mathlib.Topology.Bases (goal)
Goal:
α : Type u
β : Type u_1
t_1 : TopologicalSpace α
B : Set (Set α)
s_1 : Set α
inst : TopologicalSpace β
inst_1 : SeparableSpace α
inst_2 : SeparableSpace β
s : Set α
hsc : s.Countable
hsd : Dense s
t : Set β
htc : t.Countable
htd : Dense t
simp_rw : closure[instTopologicalSpaceSum] (Sum.inl '' s ∪ Sum.inr '' t) = univ
simp_rw₁ : closure[instTopologicalSpaceSum] (Sum.inl '' s) ∪ closure[instTopologicalSpaceSum] (Sum.inr '' t) = univ
simp_rw₂ : Sum.inl '' closure[t_1] s ∪ closure[instTopologicalSpaceSum] (Sum.inr '' t) = univ
simp_rw₃ : Eq (α := Set (α ⊕ β)) (Sum.inl '' univ ∪ closure[instTopologicalSpaceSum] (Sum.inr '' t)) univ
simp_rw₄ : Eq (α := Set (α ⊕ β)) (Sum.inl '' univ ∪ Sum.inr '' closure[inst] t) univ
simp_rw₅ : Eq (α := Set (α ⊕ β)) (Sum.inl '' univ ∪ Sum.inr '' univ) univ
⊢ Dense (Sum.inl '' s ∪ Sum.inr '' t)
have simp_rw₆ : Eq (α := Set (α ⊕ β)) (range Sum.inl ∪ range Sum.inr) univ
Tactic: simp_rw [dense_iff_closure_eq, closure_union, IsClosedEmbedding.inl.closure_image_eq,
    hsd.closure_eq, IsClosedEmbedding.inr.closure_image_eq, htd.closure_eq, image_univ,
    range_inl_union_range_inr]
-- Lean 4 proof step from Mathlib.Topology.Bases (goal)
Goal:
α : Type u
t : TopologicalSpace α
inst : SeparableSpace α
ι : Type u_2
s : ι → Set α
hd : Pairwise (Disjoint on s)
ho : ∀ (i : ι), IsOpen[t] (s i)
hne : ∀ (i : ι), (s i).Nonempty
⊢ Countable ι
have rcases : ∀ (u : Set α) (u_countable : u.Countable) (u_dense : Dense u), Countable ι
Tactic: rcases exists_countable_dense α with ⟨u, u_countable, u_dense⟩
-- Lean 4 proof step from Mathlib.Topology.Bases (goal)
Goal:
α : Type u
t : TopologicalSpace α
inst : SeparableSpace α
ι : Type u_2
s : ι → Set α
hd : Pairwise (Disjoint on s)
ho : ∀ (i : ι), IsOpen[t] (s i)
hne : ∀ (i : ι), (s i).Nonempty
u : Set α
u_countable : u.Countable
u_dense : Dense u
⊢ Countable ι
have choose : ∀ (f : (i : ι) → α) (hfu : ∀ (i : ι), f i ∈ u) (hfs : ∀ (i : ι), f i ∈ s i), Countable ι
Tactic: choose f hfu hfs using fun i ↦ u_dense.exists_mem_open (ho i) (hne i)
-- Lean 4 proof step from Mathlib.Topology.Bases (hypothesis)
Goal:
α : Type u
t : TopologicalSpace α
inst : SeparableSpace α
ι : Type u_2
s : ι → Set α
hd : Pairwise (Disjoint on s)
ho : ∀ (i : ι), IsOpen[t] (s i)
hne : ∀ (i : ι), (s i).Nonempty
u : Set α
u_countable : u.Countable
u_dense : Dense u
f : (i : ι) → α
hfu : ∀ (i : ι), f i ∈ u
hfs : ∀ (i : ι), f i ∈ s i
⊢ Countable ι
have f_inj : Injective f
Tactic: have f_inj : Injective f := fun i j hij ↦
    hd.eq <| not_disjoint_iff.2 ⟨f i, hfs i, hij.symm ▸ hfs j⟩
-- Lean 4 proof step from Mathlib.Topology.Bases (hypothesis)
Goal:
α : Type u
t : TopologicalSpace α
inst : SeparableSpace α
ι : Type u_2
s : ι → Set α
hd : Pairwise (Disjoint on s)
ho : ∀ (i : ι), IsOpen[t] (s i)
hne : ∀ (i : ι), (s i).Nonempty
u : Set α
u_countable : u.Countable
u_dense : Dense u
f : (i : ι) → α
hfu : ∀ (i : ι), f i ∈ u
hfs : ∀ (i : ι), f i ∈ s i
f_inj : Injective f
⊢ Countable ι
have this : Countable.{u + 1} (↑u : Type u)
Tactic: have := u_countable.to_subtype
-- Lean 4 proof step from Mathlib.Topology.Bases (goal)
Goal:
α : Type u
t : TopologicalSpace α
s u : Set α
hs : IsSeparable s
hu : u ⊆ s
⊢ IsSeparable u
have rcases : ∀ (c : Set α) (c_count : c.Countable) (hs : s ⊆ closure[t] c), IsSeparable u
Tactic: rcases hs with ⟨c, c_count, hs⟩
Cleared hypotheses: hs
-- Lean 4 proof step from Mathlib.Topology.Bases (goal)
Goal:
α : Type u
t : TopologicalSpace α
ι : Sort u_2
inst : Countable ι
s : ι → Set α
hs : ∀ (i : ι), IsSeparable (s i)
⊢ IsSeparable.{u} (α := α) (⋃ (i : ι), s i)
have choose : ∀ (c : (i : ι) → Set α) (hc : ∀ (i : ι), (c i).Countable) (h'c : ∀ (i : ι), s i ⊆ closure[t] (c i)),
  IsSeparable.{u} (α := α) (⋃ (i : ι), s i)
Tactic: choose c hc h'c using hs
Cleared hypotheses: hs
-- Lean 4 proof step from Mathlib.Topology.Bases (goal)
Goal:
α : Type u
t : TopologicalSpace α
ι : Sort u_2
inst : Countable ι
s c : (i : ι) → Set α
hc : ∀ (i : ι), (c i).Countable
h'c : ∀ (i : ι), s i ⊆ closure[t] (c i)
⊢ IsSeparable.{u} (α := α) (⋃ (i : ι), s i)
have refine : ∀ (i : ι), s i ⊆ closure[t] (⋃ (i : ι), c i)
Tactic: refine ⟨⋃ i, c i, countable_iUnion hc, iUnion_subset_iff.2 fun i => ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Bases (goal)
Goal:
ι : Type u_2
inst : Countable ι
X : ι → Type u_3
s : (i : ι) → Set (X i)
inst_1 : (i : ι) → TopologicalSpace (X i)
h : ∀ (i : ι), IsSeparable (s i)
⊢ IsSeparable (Set.pi (α := X) univ s)
have inl : ∀ (he : Set.pi (α := X) univ s = ∅), IsSeparable (Set.pi (α := X) univ s)
Tactic: rcases eq_empty_or_nonempty (univ.pi s) with he | ⟨f₀, -⟩
-- Lean 4 proof step from Mathlib.Topology.Bases (goal)
Goal:
ι : Type u_2
inst : Countable ι
X : ι → Type u_3
s : (i : ι) → Set (X i)
inst_1 : (i : ι) → TopologicalSpace (X i)
h : ∀ (i : ι), IsSeparable (s i)
inl : ∀ (he : Set.pi (α := X) univ s = ∅), IsSeparable (Set.pi (α := X) univ s)
⊢ IsSeparable (Set.pi (α := X) univ s)
have inr : ∀ (f₀ : (i : ι) → X i), IsSeparable (Set.pi (α := X) univ s)
Tactic: rcases eq_empty_or_nonempty (univ.pi s) with he | ⟨f₀, -⟩
-- Lean 4 proof step from Mathlib.Topology.Bases (goal)
Goal:
ι : Type u_2
inst : Countable ι
X : ι → Type u_3
s : (i : ι) → Set (X i)
inst_1 : (i : ι) → TopologicalSpace (X i)
h : ∀ (i : ι), IsSeparable (s i)
he : Set.pi (α := X) univ s = ∅
⊢ IsSeparable (Set.pi (α := X) univ s)
have inl : IsSeparable (α := (i : ι) → X i) ∅
Tactic: rw [he]
-- Lean 4 proof step from Mathlib.Topology.Bases (goal)
Goal:
ι : Type u_2
inst : Countable ι
X : ι → Type u_3
s : (i : ι) → Set (X i)
inst_1 : (i : ι) → TopologicalSpace (X i)
h : ∀ (i : ι), IsSeparable (s i)
f₀ : (i : ι) → X i
⊢ IsSeparable (Set.pi (α := X) univ s)
have inr : ∀ (c : (i : ι) → Set (X i)) (c_count : ∀ (i : ι), (c i).Countable) (hc : ∀ (i : ι), s i ⊆ closure[inst_1 i] (c i)),
  IsSeparable (Set.pi (α := X) univ s)
Tactic: choose c c_count hc using h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Topology.Bases (hypothesis)
Goal:
ι : Type u_2
inst : Countable ι
X : ι → Type u_3
s : (i : ι) → Set (X i)
inst_1 : (i : ι) → TopologicalSpace (X i)
f₀ : (i : ι) → X i
c : (i : ι) → Set (X i)
c_count : ∀ (i : ι), (c i).Countable
hc : ∀ (i : ι), s i ⊆ closure[inst_1 i] (c i)
⊢ IsSeparable (Set.pi (α := X) univ s)
have this : ∀ (i : ι), Countable.{u_3 + 1} (↑(c i) : Type u_3)
Tactic: haveI := fun i ↦ (c_count i).to_subtype
-- Lean 4 proof step from Mathlib.Topology.Bases (goal)
Goal:
ι : Type u_2
inst : Countable ι
X : ι → Type u_3
s : (i : ι) → Set (X i)
inst_1 : (i : ι) → TopologicalSpace (X i)
f₀ : (i : ι) → X i
c : (i : ι) → Set (X i)
c_count : ∀ (i : ι), (c i).Countable
hc : ∀ (i : ι), s i ⊆ closure[inst_1 i] (c i)
this : ∀ (i : ι), Countable.{u_3 + 1} (↑(c i) : Type u_3)
g : (I : Finset ι) × ((i : ↥I) → (↑(c (↑i : ι)) : Type u_3)) → (i : ι) → X i :=
  fun (x : (I : Finset ι) × ((i : ↥I) → (↑(c (↑i : ι)) : Type u_3))) (i : ι) ↦
    match (motive := (I : Finset ι) × ((i : ↥I) → (↑(c (↑i : ι)) : Type u_3)) → X i) x with
    | ⟨I, f⟩ => if hi : i ∈ I then (↑(f (Subtype.mk (p := fun (x : ι) ↦ x ∈ I) i hi)) : X (↑⟨i, hi⟩ : ι)) else f₀ i
⊢ IsSeparable (Set.pi (α := X) univ s)
have inr : ∀ (f : (i : ι) → X i) (hf : f ∈ Set.pi (α := X) univ s) (o : Set ((i : ι) → X i)) (ho : IsOpen[Pi.topologicalSpace] o)
  (hfo : f ∈ o), (o ∩ range g).Nonempty
Tactic: refine ⟨range g, countable_range g, fun f hf ↦ mem_closure_iff.2 fun o ho hfo ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Bases (goal)
Goal:
ι : Type u_2
inst : Countable ι
X : ι → Type u_3
s : (i : ι) → Set (X i)
inst_1 : (i : ι) → TopologicalSpace (X i)
f₀ : (i : ι) → X i
c : (i : ι) → Set (X i)
c_count : ∀ (i : ι), (c i).Countable
hc : ∀ (i : ι), s i ⊆ closure[inst_1 i] (c i)
this : ∀ (i : ι), Countable.{u_3 + 1} (↑(c i) : Type u_3)
g : (I : Finset ι) × ((i : ↥I) → (↑(c (↑i : ι)) : Type u_3)) → (i : ι) → X i :=
  fun (x : (I : Finset ι) × ((i : ↥I) → (↑(c (↑i : ι)) : Type u_3))) (i : ι) ↦
    match (motive := (I : Finset ι) × ((i : ↥I) → (↑(c (↑i : ι)) : Type u_3)) → X i) x with
    | ⟨I, f⟩ => if hi : i ∈ I then (↑(f (Subtype.mk (p := fun (x : ι) ↦ x ∈ I) i hi)) : X (↑⟨i, hi⟩ : ι)) else f₀ i
f : (i : ι) → X i
hf : f ∈ Set.pi (α := X) univ s
o : Set ((i : ι) → X i)
ho : IsOpen[Pi.topologicalSpace] o
hfo : f ∈ o
⊢ (o ∩ range g).Nonempty
have inr : ∀ (I : Finset ι) (u : (a : ι) → Set (X a)) (huo : ∀ a ∈ I, IsOpen[inst_1 a] (u a) ∧ f a ∈ u a)
  (hI : (↑I : Set ι).pi (α := X) u ⊆ o), (o ∩ range g).Nonempty
Tactic: rcases isOpen_pi_iff.1 ho f hfo with ⟨I, u, huo, hI⟩
-- Lean 4 proof step from Mathlib.Topology.Bases (goal)
Goal:
ι : Type u_2
inst : Countable ι
X : ι → Type u_3
s : (i : ι) → Set (X i)
inst_1 : (i : ι) → TopologicalSpace (X i)
f₀ : (i : ι) → X i
c : (i : ι) → Set (X i)
c_count : ∀ (i : ι), (c i).Countable
hc : ∀ (i : ι), s i ⊆ closure[inst_1 i] (c i)
this : ∀ (i : ι), Countable.{u_3 + 1} (↑(c i) : Type u_3)
g : (I : Finset ι) × ((i : ↥I) → (↑(c (↑i : ι)) : Type u_3)) → (i : ι) → X i :=
  fun (x : (I : Finset ι) × ((i : ↥I) → (↑(c (↑i : ι)) : Type u_3))) (i : ι) ↦
    match (motive := (I : Finset ι) × ((i : ↥I) → (↑(c (↑i : ι)) : Type u_3)) → X i) x with
    | ⟨I, f⟩ => if hi : i ∈ I then (↑(f (Subtype.mk (p := fun (x : ι) ↦ x ∈ I) i hi)) : X (↑⟨i, hi⟩ : ι)) else f₀ i
f : (i : ι) → X i
hf : f ∈ Set.pi (α := X) univ s
o : Set ((i : ι) → X i)
ho : IsOpen[Pi.topologicalSpace] o
hfo : f ∈ o
I : Finset ι
u : (a : ι) → Set (X a)
huo : ∀ a ∈ I, IsOpen[inst_1 a] (u a) ∧ f a ∈ u a
hI : (↑I : Set ι).pi (α := X) u ⊆ o
⊢ (o ∩ range g).Nonempty
have inr : ∀ (f : (i : ↥I) → (↑(c (↑i : ι)) : Type u_3))
  (hf :
    g (Sigma.mk (β := fun (I : Finset ι) ↦ (i : ↥I) → (↑(c (↑i : ι)) : Type u_3)) I f) ∈ (↑I : Set ι).pi (α := X) u),
  (o ∩ range g).Nonempty
Tactic: rsuffices ⟨f, hf⟩ : ∃ f : (i : I) → c i, g ⟨I, f⟩ ∈ Set.pi I u
-- Lean 4 proof step from Mathlib.Topology.Bases (goal)
Goal:
ι : Type u_2
inst : Countable ι
X : ι → Type u_3
s : (i : ι) → Set (X i)
inst_1 : (i : ι) → TopologicalSpace (X i)
f₀ : (i : ι) → X i
c : (i : ι) → Set (X i)
c_count : ∀ (i : ι), (c i).Countable
hc : ∀ (i : ι), s i ⊆ closure[inst_1 i] (c i)
this : ∀ (i : ι), Countable.{u_3 + 1} (↑(c i) : Type u_3)
g : (I : Finset ι) × ((i : ↥I) → (↑(c (↑i : ι)) : Type u_3)) → (i : ι) → X i :=
  fun (x : (I : Finset ι) × ((i : ↥I) → (↑(c (↑i : ι)) : Type u_3))) (i : ι) ↦
    match (motive := (I : Finset ι) × ((i : ↥I) → (↑(c (↑i : ι)) : Type u_3)) → X i) x with
    | ⟨I, f⟩ => if hi : i ∈ I then (↑(f (Subtype.mk (p := fun (x : ι) ↦ x ∈ I) i hi)) : X (↑⟨i, hi⟩ : ι)) else f₀ i
f : (i : ι) → X i
hf : f ∈ Set.pi (α := X) univ s
o : Set ((i : ι) → X i)
ho : IsOpen[Pi.topologicalSpace] o
hfo : f ∈ o
I : Finset ι
u : (a : ι) → Set (X a)
huo : ∀ a ∈ I, IsOpen[inst_1 a] (u a) ∧ f a ∈ u a
hI : (↑I : Set ι).pi (α := X) u ⊆ o
inr :
  ∀ (f : (i : ↥I) → (↑(c (↑i : ι)) : Type u_3))
    (hf :
      g (Sigma.mk (β := fun (I : Finset ι) ↦ (i : ↥I) → (↑(c (↑i : ι)) : Type u_3)) I f) ∈ (↑I : Set ι).pi (α := X) u),
    (o ∩ range g).Nonempty
⊢ (o ∩ range g).Nonempty
have rsuffices : ∃ (f : (i : ↥I) → (↑(c (↑i : ι)) : Type u_3)),
  g (Sigma.mk (β := fun (I : Finset ι) ↦ (i : ↥I) → (↑(c (↑i : ι)) : Type u_3)) I f) ∈ (↑I : Set ι).pi (α := X) u
Tactic: rsuffices ⟨f, hf⟩ : ∃ f : (i : I) → c i, g ⟨I, f⟩ ∈ Set.pi I u
-- Lean 4 proof step from Mathlib.Topology.Bases (goal)
Goal:
ι : Type u_2
inst : Countable ι
X : ι → Type u_3
s : (i : ι) → Set (X i)
inst_1 : (i : ι) → TopologicalSpace (X i)
f₀ : (i : ι) → X i
c : (i : ι) → Set (X i)
c_count : ∀ (i : ι), (c i).Countable
hc : ∀ (i : ι), s i ⊆ closure[inst_1 i] (c i)
this : ∀ (i : ι), Countable.{u_3 + 1} (↑(c i) : Type u_3)
g : (I : Finset ι) × ((i : ↥I) → (↑(c (↑i : ι)) : Type u_3)) → (i : ι) → X i :=
  fun (x : (I : Finset ι) × ((i : ↥I) → (↑(c (↑i : ι)) : Type u_3))) (i : ι) ↦
    match (motive := (I : Finset ι) × ((i : ↥I) → (↑(c (↑i : ι)) : Type u_3)) → X i) x with
    | ⟨I, f⟩ => if hi : i ∈ I then (↑(f (Subtype.mk (p := fun (x : ι) ↦ x ∈ I) i hi)) : X (↑⟨i, hi⟩ : ι)) else f₀ i
f : (i : ι) → X i
hf : f ∈ Set.pi (α := X) univ s
o : Set ((i : ι) → X i)
ho : IsOpen[Pi.topologicalSpace] o
hfo : f ∈ o
I : Finset ι
u : (a : ι) → Set (X a)
huo : ∀ a ∈ I, IsOpen[inst_1 a] (u a) ∧ f a ∈ u a
hI : (↑I : Set ι).pi (α := X) u ⊆ o
H : ∀ i ∈ I, (u i ∩ c i).Nonempty
⊢ ∃ (f : (i : ↥I) → (↑(c (↑i : ι)) : Type u_3)),
    g (Sigma.mk (β := fun (I : Finset ι) ↦ (i : ↥I) → (↑(c (↑i : ι)) : Type u_3)) I f) ∈ (↑I : Set ι).pi (α := X) u
have choose : ∀ (f : (i : ι) → i ∈ I → X i) (hfu : ∀ (i : ι) (a : i ∈ I), f i a ∈ u i) (hfc : ∀ (i : ι) (a : i ∈ I), f i a ∈ c i),
  ∃ (f : (i : ↥I) → (↑(c (↑i : ι)) : Type u_3)),
    g (Sigma.mk (β := fun (I : Finset ι) ↦ (i : ↥I) → (↑(c (↑i : ι)) : Type u_3)) I f) ∈ (↑I : Set ι).pi (α := X) u
Tactic: choose f hfu hfc using H
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.Topology.Bases (goal)
Goal:
ι : Type u_2
inst : Countable ι
X : ι → Type u_3
s : (i : ι) → Set (X i)
inst_1 : (i : ι) → TopologicalSpace (X i)
f₀ : (i : ι) → X i
c : (i : ι) → Set (X i)
c_count : ∀ (i : ι), (c i).Countable
hc : ∀ (i : ι), s i ⊆ closure[inst_1 i] (c i)
this : ∀ (i : ι), Countable.{u_3 + 1} (↑(c i) : Type u_3)
g : (I : Finset ι) × ((i : ↥I) → (↑(c (↑i : ι)) : Type u_3)) → (i : ι) → X i :=
  fun (x : (I : Finset ι) × ((i : ↥I) → (↑(c (↑i : ι)) : Type u_3))) (i : ι) ↦
    match (motive := (I : Finset ι) × ((i : ↥I) → (↑(c (↑i : ι)) : Type u_3)) → X i) x with
    | ⟨I, f⟩ => if hi : i ∈ I then (↑(f (Subtype.mk (p := fun (x : ι) ↦ x ∈ I) i hi)) : X (↑⟨i, hi⟩ : ι)) else f₀ i
f_1 : (i : ι) → X i
hf : f_1 ∈ Set.pi (α := X) univ s
o : Set ((i : ι) → X i)
ho : IsOpen[Pi.topologicalSpace] o
hfo : f_1 ∈ o
I : Finset ι
u : (a : ι) → Set (X a)
huo : ∀ a ∈ I, IsOpen[inst_1 a] (u a) ∧ f_1 a ∈ u a
hI : (↑I : Set ι).pi (α := X) u ⊆ o
f : (i : ι) → i ∈ I → X i
hfu : ∀ (i : ι) (a : i ∈ I), f i a ∈ u i
hfc : ∀ (i : ι) (a : i ∈ I), f i a ∈ c i
⊢ ∃ (f : (i : ↥I) → (↑(c (↑i : ι)) : Type u_3)),
    g (Sigma.mk (β := fun (I : Finset ι) ↦ (i : ↥I) → (↑(c (↑i : ι)) : Type u_3)) I f) ∈ (↑I : Set ι).pi (α := X) u
have refine : ∀ (i : ι) (hi : i ∈ I),
  g
      (Sigma.mk (β := fun (I : Finset ι) ↦ (i : ↥I) → (↑(c (↑i : ι)) : Type u_3)) I fun (i : ↥I) ↦
        Subtype.mk (p := fun (x : X (↑i : ι)) ↦ Membership.mem (γ := Set (X (↑i : ι))) (c (↑i : ι)) x) (f (↑i : ι) sorry) sorry)
      i ∈
    u i
Tactic: refine ⟨fun i ↦ ⟨f i i.2, hfc i i.2⟩, fun i (hi : i ∈ I) ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Bases (goal)
Goal:
ι : Type u_2
inst : Countable ι
X : ι → Type u_3
s : (i : ι) → Set (X i)
inst_1 : (i : ι) → TopologicalSpace (X i)
f₀ : (i : ι) → X i
c : (i : ι) → Set (X i)
c_count : ∀ (i : ι), (c i).Countable
hc : ∀ (i : ι), s i ⊆ closure[inst_1 i] (c i)
this : ∀ (i : ι), Countable.{u_3 + 1} (↑(c i) : Type u_3)
g : (I : Finset ι) × ((i : ↥I) → (↑(c (↑i : ι)) : Type u_3)) → (i : ι) → X i :=
  fun (x : (I : Finset ι) × ((i : ↥I) → (↑(c (↑i : ι)) : Type u_3))) (i : ι) ↦
    match (motive := (I : Finset ι) × ((i : ↥I) → (↑(c (↑i : ι)) : Type u_3)) → X i) x with
    | ⟨I, f⟩ => if hi : i ∈ I then (↑(f (Subtype.mk (p := fun (x : ι) ↦ x ∈ I) i hi)) : X (↑⟨i, hi⟩ : ι)) else f₀ i
f : (i : ι) → X i
hf : f ∈ Set.pi (α := X) univ s
o : Set ((i : ι) → X i)
ho : IsOpen[Pi.topologicalSpace] o
hfo : f ∈ o
I : Finset ι
u : (a : ι) → Set (X a)
huo : ∀ a ∈ I, IsOpen[inst_1 a] (u a) ∧ f a ∈ u a
hI : (↑I : Set ι).pi (α := X) u ⊆ o
⊢ ∃ (f : (i : ↥I) → (↑(c (↑i : ι)) : Type u_3)),
    g (Sigma.mk (β := fun (I : Finset ι) ↦ (i : ↥I) → (↑(c (↑i : ι)) : Type u_3)) I f) ∈ (↑I : Set ι).pi (α := X) u
have suffices : ∀ i ∈ I, (u i ∩ c i).Nonempty
Tactic: suffices H : ∀ i ∈ I, (u i ∩ c i).Nonempty by
      choose f hfu hfc using H
      refine ⟨fun i ↦ ⟨f i i.2, hfc i i.2⟩, fun i (hi : i ∈ I) ↦ ?_⟩
      simpa only [g, dif_pos hi] using hfu i hi
-- Lean 4 proof step from Mathlib.Topology.Bases (goal)
Goal:
ι : Type u_2
inst : Countable ι
X : ι → Type u_3
s : (i : ι) → Set (X i)
inst_1 : (i : ι) → TopologicalSpace (X i)
h : ∀ (i : ι), IsSeparable (s i)
⊢ IsSeparable (Set.pi (α := X) univ s)
have inl : ∀ (he : Set.pi (α := X) univ s = ∅), IsSeparable (Set.pi (α := X) univ s)
Tactic: classical
  rcases eq_empty_or_nonempty (univ.pi s) with he | ⟨f₀, -⟩
  · rw [he]
    exact countable_empty.isSeparable
  · choose c c_count hc using h
    haveI := fun i ↦ (c_count i).to_subtype
    set g : (I : Finset ι) × ((i : I) → c i) → (i : ι) → X i := fun ⟨I, f⟩ i ↦
      if hi : i ∈ I then f ⟨i, hi⟩ else f₀ i
    refine ⟨range g, countable_range g, fun f hf ↦ mem_closure_iff.2 fun o ho hfo ↦ ?_⟩
    rcases isOpen_pi_iff.1 ho f hfo with ⟨I, u, huo, hI⟩
    rsuffices ⟨f, hf⟩ : ∃ f : (i : I) → c i, g ⟨I, f⟩ ∈ Set.pi I u
    · exact ⟨g ⟨I, f⟩, hI hf, mem_range_self (f := g) ⟨I, f⟩⟩
    suffices H : ∀ i ∈ I, (u i ∩ c i).Nonempty by
      choose f hfu hfc using H
      refine ⟨fun i ↦ ⟨f i i.2, hfc i i.2⟩, fun i (hi : i ∈ I) ↦ ?_⟩
      simpa only [g, dif_pos hi] using hfu i hi
    intro i hi
    exact mem_closure_iff.1 (hc i <| hf _ trivial) _ (huo i hi).1 (huo i hi).2
-- Lean 4 proof step from Mathlib.Topology.Bases (goal)
Goal:
ι : Type u_2
inst : Countable ι
X : ι → Type u_3
s : (i : ι) → Set (X i)
inst_1 : (i : ι) → TopologicalSpace (X i)
h : ∀ (i : ι), IsSeparable (s i)
inl : ∀ (he : Set.pi (α := X) univ s = ∅), IsSeparable (Set.pi (α := X) univ s)
⊢ IsSeparable (Set.pi (α := X) univ s)
have inr : ∀ (f₀ : (i : ι) → X i), IsSeparable (Set.pi (α := X) univ s)
Tactic: classical
  rcases eq_empty_or_nonempty (univ.pi s) with he | ⟨f₀, -⟩
  · rw [he]
    exact countable_empty.isSeparable
  · choose c c_count hc using h
    haveI := fun i ↦ (c_count i).to_subtype
    set g : (I : Finset ι) × ((i : I) → c i) → (i : ι) → X i := fun ⟨I, f⟩ i ↦
      if hi : i ∈ I then f ⟨i, hi⟩ else f₀ i
    refine ⟨range g, countable_range g, fun f hf ↦ mem_closure_iff.2 fun o ho hfo ↦ ?_⟩
    rcases isOpen_pi_iff.1 ho f hfo with ⟨I, u, huo, hI⟩
    rsuffices ⟨f, hf⟩ : ∃ f : (i : I) → c i, g ⟨I, f⟩ ∈ Set.pi I u
    · exact ⟨g ⟨I, f⟩, hI hf, mem_range_self (f := g) ⟨I, f⟩⟩
    suffices H : ∀ i ∈ I, (u i ∩ c i).Nonempty by
      choose f hfu hfc using H
      refine ⟨fun i ↦ ⟨f i i.2, hfc i i.2⟩, fun i (hi : i ∈ I) ↦ ?_⟩
      simpa only [g, dif_pos hi] using hfu i hi
    intro i hi
    exact mem_closure_iff.1 (hc i <| hf _ trivial) _ (huo i hi).1 (huo i hi).2
-- Lean 4 proof step from Mathlib.Topology.Bases (goal)
Goal:
α : Type u
t_1 : TopologicalSpace α
β : Type u_2
inst : TopologicalSpace β
s : Set α
t : Set β
hs : IsSeparable s
ht : IsSeparable t
⊢ IsSeparable (s ×ˢ t)
have rcases : ∀ (cs : Set α) (cs_count : cs.Countable) (hcs : s ⊆ closure[t_1] cs), IsSeparable (s ×ˢ t)
Tactic: rcases hs with ⟨cs, cs_count, hcs⟩
Cleared hypotheses: hs
-- Lean 4 proof step from Mathlib.Topology.Bases (goal)
Goal:
α : Type u
t_1 : TopologicalSpace α
β : Type u_2
inst : TopologicalSpace β
s : Set α
t : Set β
ht : IsSeparable t
cs : Set α
cs_count : cs.Countable
hcs : s ⊆ closure[t_1] cs
⊢ IsSeparable (s ×ˢ t)
have rcases : ∀ (ct : Set β) (ct_count : ct.Countable) (hct : t ⊆ closure[inst] ct), IsSeparable (s ×ˢ t)
Tactic: rcases ht with ⟨ct, ct_count, hct⟩
Cleared hypotheses: ht
-- Lean 4 proof step from Mathlib.Topology.Bases (goal)
Goal:
α : Type u
t_1 : TopologicalSpace α
β : Type u_2
inst : TopologicalSpace β
s : Set α
t : Set β
cs : Set α
cs_count : cs.Countable
hcs : s ⊆ closure[t_1] cs
ct : Set β
ct_count : ct.Countable
hct : t ⊆ closure[inst] ct
⊢ IsSeparable (s ×ˢ t)
have refine : s ×ˢ t ⊆ closure[instTopologicalSpaceProd] (cs ×ˢ ct)
Tactic: refine ⟨cs ×ˢ ct, cs_count.prod ct_count, ?_⟩