awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.Bases (goal)
Goal:
α : Type u
β : Type u_1
t : TopologicalSpace α
s : Set α
inst : TopologicalSpace β
B : Set (Set β)
hB : IsTopologicalBasis B
f : α → β
⊢ (∀ (t_1 : Set β), IsOpen[inst] t_1 → ∃ (u : Set α), IsOpen[t] u ∧ f ⁻¹' t_1 ∩ s = u ∩ s) ↔
    ∀ t_1 ∈ B, ∃ (u : Set α), IsOpen[t] u ∧ f ⁻¹' t_1 ∩ s = u ∩ s
have refine : ∀ (h : ∀ t_1 ∈ B, ∃ (u : Set α), IsOpen[t] u ∧ f ⁻¹' t_1 ∩ s = u ∩ s) (t_1 : Set β) (ht : IsOpen[inst] t_1),
  ∃ (u : Set α), IsOpen[t] u ∧ f ⁻¹' t_1 ∩ s = u ∩ s
Tactic: refine ⟨fun h t ht => h t (hB.isOpen ht), fun h t ht => ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Bases (goal)
Goal:
α : Type u
β : Type u_1
t_1 : TopologicalSpace α
s : Set α
inst : TopologicalSpace β
B : Set (Set β)
hB : IsTopologicalBasis B
f : α → β
h : ∀ t ∈ B, ∃ (u : Set α), IsOpen[t_1] u ∧ f ⁻¹' t ∩ s = u ∩ s
t : Set β
ht : IsOpen[inst] t
⊢ ∃ (u : Set α), IsOpen[t_1] u ∧ f ⁻¹' t ∩ s = u ∩ s
have obtain : ∀ (ι : Type u_1) (g : ι → Set β) (hg : ∀ (i : ι), g i ∈ B) (ht : IsOpen[inst] (⋃ (i : ι), g i)),
  ∃ (u : Set α), IsOpen[t_1] u ∧ (f ⁻¹' ⋃ (i : ι), g i) ∩ s = u ∩ s
Tactic: obtain ⟨ι, g, rfl, hg⟩ := hB.open_eq_iUnion ht
Cleared hypotheses: t, ht
-- Lean 4 proof step from Mathlib.Topology.Bases (goal)
Goal:
α : Type u
β : Type u_1
t : TopologicalSpace α
s : Set α
inst : TopologicalSpace β
B : Set (Set β)
hB : IsTopologicalBasis B
f : α → β
h : ∀ t_1 ∈ B, ∃ (u : Set α), IsOpen[t] u ∧ f ⁻¹' t_1 ∩ s = u ∩ s
ι : Type u_1
g : ι → Set β
hg : ∀ (i : ι), g i ∈ B
ht : IsOpen[inst] (⋃ (i : ι), g i)
⊢ ∃ (u : Set α), IsOpen[t] u ∧ (f ⁻¹' ⋃ (i : ι), g i) ∩ s = u ∩ s
have choose : ∀ (v : (i : ι) → Set α) (hv : ∀ (i : ι), IsOpen[t] (v i)) (he : ∀ (i : ι), f ⁻¹' g i ∩ s = v i ∩ s),
  ∃ (u : Set α), IsOpen[t] u ∧ (f ⁻¹' ⋃ (i : ι), g i) ∩ s = u ∩ s
Tactic: choose v hv he using (fun i => h (g i) (hg i))
-- Lean 4 proof step from Mathlib.Topology.Bases (goal)
Goal:
α : Type u
t : TopologicalSpace α
inst : SeparableSpace α
inst_1 : Nonempty α
⊢ ∃ (u : ℕ → α), DenseRange u
have obtain : ∀ (s : Set α) (hs : s.Countable) (s_dense : Dense s), ∃ (u : ℕ → α), DenseRange u
Tactic: obtain ⟨s : Set α, hs, s_dense⟩ := exists_countable_dense α
-- Lean 4 proof step from Mathlib.Topology.Bases (goal)
Goal:
α : Type u
t : TopologicalSpace α
inst : SeparableSpace α
inst_1 : Nonempty α
s : Set α
hs : s.Countable
s_dense : Dense s
⊢ ∃ (u : ℕ → α), DenseRange u
have obtain : ∀ (u : ℕ → α) (hu : s ⊆ range u), ∃ (u : ℕ → α), DenseRange u
Tactic: obtain ⟨u, hu⟩ := Set.countable_iff_exists_subset_range.mp hs
-- Lean 4 proof step from Mathlib.Topology.Bases (goal)
Goal:
α : Type u
β : Type u_1
t : TopologicalSpace α
inst : TopologicalSpace β
inst_1 : SeparableSpace β
f : α → β
h : IsOpenMap f
h' : IsInducing f
⊢ SeparableSpace α
have inl : IsEmpty α → SeparableSpace α
Tactic: cases isEmpty_or_nonempty α
-- Lean 4 proof step from Mathlib.Topology.Bases (goal)
Goal:
α : Type u
β : Type u_1
t : TopologicalSpace α
inst : TopologicalSpace β
inst_1 : SeparableSpace β
f : α → β
h : IsOpenMap f
h' : IsInducing f
inl : IsEmpty α → SeparableSpace α
⊢ SeparableSpace α
have inr : Nonempty α → SeparableSpace α
Tactic: cases isEmpty_or_nonempty α
-- Lean 4 proof step from Mathlib.Topology.Bases (goal)
Goal:
α : Type u
β : Type u_1
t : TopologicalSpace α
inst : TopologicalSpace β
inst_1 : SeparableSpace β
f : α → β
h : IsOpenMap f
h' : IsInducing f
h_1 : Nonempty α
⊢ SeparableSpace α
have inr : ∀ (s : Set β) (s_cnt : s.Countable) (s_dense : Dense s), SeparableSpace α
Tactic: obtain ⟨s, s_cnt, s_dense⟩ := exists_countable_dense β
-- Lean 4 proof step from Mathlib.Topology.Bases (goal)
Goal:
α : Type u
β : Type u_1
t : TopologicalSpace α
inst : TopologicalSpace β
inst_1 : SeparableSpace β
f : α → β
h : IsOpenMap f
h' : IsInducing f
h_1 : Nonempty α
s : Set β
s_cnt : s.Countable
s_dense : Dense s
⊢ SeparableSpace α
have inr : Dense (invFun f '' s)
Tactic: refine ⟨f.invFun '' s, s_cnt.image _, ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Bases (goal)
Goal:
α : Type u
β : Type u_1
t : TopologicalSpace α
inst : TopologicalSpace β
inst_1 : SeparableSpace β
f : α → β
h : IsOpenMap f
h' : IsInducing f
h_1 : Nonempty α
s : Set β
s_cnt : s.Countable
s_dense : Dense s
⊢ Dense (invFun f '' s)
have inr : ∀ (x : α) (o : Set β), IsOpen[inst] o → f x ∈ o → (o ∩ f '' invFun f '' s).Nonempty
Tactic: simp_rw [h'.dense_iff, mem_closure_iff]
-- Lean 4 proof step from Mathlib.Topology.Bases (goal)
Goal:
α : Type u
β : Type u_1
t : TopologicalSpace α
inst : TopologicalSpace β
inst_1 : SeparableSpace β
f : α → β
h : IsOpenMap f
h' : IsInducing f
h_1 : Nonempty α
s : Set β
s_cnt : s.Countable
s_dense : Dense s
x : α
U : Set β
hU : IsOpen[inst] U
hx : f x ∈ U
⊢ (U ∩ f '' invFun f '' s).Nonempty
have inr : ∀ (x' : α) (hx's : f x' ∈ s) (hx'U : f x' ∈ U), (U ∩ f '' invFun f '' s).Nonempty
Tactic: obtain ⟨-, ⟨hx'U, x', rfl⟩, hx's⟩ :=
    s_dense.inter_open_nonempty (U ∩ range f) (hU.inter h.isOpen_range) ⟨f x, hx, mem_range_self _⟩
-- Lean 4 proof step from Mathlib.Topology.Bases (goal)
Goal:
α : Type u
β : Type u_1
t : TopologicalSpace α
inst : TopologicalSpace β
inst_1 : SeparableSpace β
f : α → β
h : IsOpenMap f
h' : IsInducing f
h_1 : Nonempty α
s : Set β
s_cnt : s.Countable
s_dense : Dense s
x : α
U : Set β
hU : IsOpen[inst] U
hx : f x ∈ U
x' : α
hx's : f x' ∈ s
hx'U : f x' ∈ U
⊢ (U ∩ f '' invFun f '' s).Nonempty
have inr : f (invFun f (f x')) ∈ U
Tactic: refine ⟨f <| f.invFun <| f x', ?_, mem_image_of_mem _ <| mem_image_of_mem _ hx's⟩
-- Lean 4 proof step from Mathlib.Topology.Bases (goal)
Goal:
α : Type u
β : Type u_1
t : TopologicalSpace α
B : Set (Set α)
s : Set α
inst : TopologicalSpace β
inst_1 : SeparableSpace α
inst_2 : SeparableSpace β
⊢ SeparableSpace (α × β)
have rcases : ∀ (s : Set α) (hsc : s.Countable) (hsd : Dense s), SeparableSpace (α × β)
Tactic: rcases exists_countable_dense α with ⟨s, hsc, hsd⟩
-- Lean 4 proof step from Mathlib.Topology.Bases (goal)
Goal:
α : Type u
β : Type u_1
t : TopologicalSpace α
B : Set (Set α)
s_1 : Set α
inst : TopologicalSpace β
inst_1 : SeparableSpace α
inst_2 : SeparableSpace β
s : Set α
hsc : s.Countable
hsd : Dense s
⊢ SeparableSpace (α × β)
have rcases : ∀ (t_1 : Set β) (htc : t_1.Countable) (htd : Dense t_1), SeparableSpace (α × β)
Tactic: rcases exists_countable_dense β with ⟨t, htc, htd⟩
-- Lean 4 proof step from Mathlib.Topology.Bases (goal)
Goal:
α : Type u
β : Type u_1
t : TopologicalSpace α
B : Set (Set α)
s : Set α
ι : Type u_2
X : ι → Type u_3
inst : (i : ι) → TopologicalSpace (X i)
inst_1 : ∀ (i : ι), SeparableSpace.{u_3} (X i)
inst_2 : Countable ι
⊢ SeparableSpace ((i : ι) → X i)
have choose : ∀ (t : (x : ι) → Set (X x)) (htc : ∀ (x : ι), (t x).Countable) (htd : ∀ (x : ι), Dense (t x)),
  SeparableSpace ((i : ι) → X i)
Tactic: choose t htc htd using (exists_countable_dense <| X ·)
-- Lean 4 proof step from Mathlib.Topology.Bases (hypothesis)
Goal:
α : Type u
β : Type u_1
t_1 : TopologicalSpace α
B : Set (Set α)
s : Set α
ι : Type u_2
X : ι → Type u_3
inst : (i : ι) → TopologicalSpace (X i)
inst_1 : ∀ (i : ι), SeparableSpace.{u_3} (X i)
inst_2 : Countable ι
t : (x : ι) → Set (X x)
htc : ∀ (x : ι), (t x).Countable
htd : ∀ (x : ι), Dense (t x)
⊢ SeparableSpace ((i : ι) → X i)
have this : ∀ (i : ι), Countable.{u_3 + 1} (↑(t i) : Type u_3)
Tactic: haveI := fun i ↦ (htc i).to_subtype
-- Lean 4 proof step from Mathlib.Topology.Bases (hypothesis)
Goal:
α : Type u
β : Type u_1
t_1 : TopologicalSpace α
B : Set (Set α)
s : Set α
ι : Type u_2
X : ι → Type u_3
inst : (i : ι) → TopologicalSpace (X i)
inst_1 : ∀ (i : ι), SeparableSpace.{u_3} (X i)
inst_2 : Countable ι
t : (x : ι) → Set (X x)
htc : ∀ (x : ι), (t x).Countable
htd : ∀ (x : ι), Dense (t x)
this : ∀ (i : ι), Countable.{u_3 + 1} (↑(t i) : Type u_3)
⊢ SeparableSpace ((i : ι) → X i)
have a : Nontrivial ((i : ι) → X i)
Tactic: nontriviality ∀ i, X i
-- Lean 4 proof step from Mathlib.Topology.Bases (goal)
Goal:
α : Type u
β : Type u_1
t_1 : TopologicalSpace α
B : Set (Set α)
s : Set α
ι : Type u_2
X : ι → Type u_3
inst : (i : ι) → TopologicalSpace (X i)
inst_1 : ∀ (i : ι), SeparableSpace.{u_3} (X i)
inst_2 : Countable ι
t : (x : ι) → Set (X x)
htc : ∀ (x : ι), (t x).Countable
htd : ∀ (x : ι), Dense (t x)
this : ∀ (i : ι), Countable.{u_3 + 1} (↑(t i) : Type u_3)
h : Nontrivial ((i : ι) → X i)
⊢ SeparableSpace ((i : ι) → X i)
have inhabit : ∀ (inhabited_h : Inhabited ((i : ι) → X i)), SeparableSpace ((i : ι) → X i)
Tactic: inhabit ∀ i, X i
-- Lean 4 proof step from Mathlib.Topology.Bases (goal)
Goal:
α : Type u
β : Type u_1
t_1 : TopologicalSpace α
B : Set (Set α)
s : Set α
ι : Type u_2
X : ι → Type u_3
inst : (i : ι) → TopologicalSpace (X i)
inst_1 : ∀ (i : ι), SeparableSpace.{u_3} (X i)
inst_2 : Countable ι
t : (x : ι) → Set (X x)
htc : ∀ (x : ι), (t x).Countable
htd : ∀ (x : ι), Dense (t x)
this : ∀ (i : ι), Countable.{u_3 + 1} (↑(t i) : Type u_3)
h : Nontrivial ((i : ι) → X i)
inhabited_h : Inhabited ((i : ι) → X i)
f : (I : Finset ι) × ((i : ↥I) → (↑(t (↑i : ι)) : Type u_3)) → (i : ι) → X i :=
  fun (x : (I : Finset ι) × ((i : ↥I) → (↑(t (↑i : ι)) : Type u_3))) (i : ι) ↦
    match (motive := (I : Finset ι) × ((i : ↥I) → (↑(t (↑i : ι)) : Type u_3)) → X i) x with
    | ⟨I, g⟩ => if hi : i ∈ I then (↑(g (Subtype.mk (p := fun (x : ι) ↦ x ∈ I) i hi)) : X (↑⟨i, hi⟩ : ι)) else default i
⊢ SeparableSpace ((i : ι) → X i)
have refine : ∀ (U : Set ((i : ι) → X i)) (hU : IsOpen[Pi.topologicalSpace] U),
  U.Nonempty → ∀ (g : (i : ι) → X i) (hg : g ∈ U), (U ∩ range f).Nonempty
Tactic: refine ⟨⟨range f, countable_range f, dense_iff_inter_open.2 fun U hU ⟨g, hg⟩ ↦ ?_⟩⟩
-- Lean 4 proof step from Mathlib.Topology.Bases (goal)
Goal:
α : Type u
β : Type u_1
t_1 : TopologicalSpace α
B : Set (Set α)
s : Set α
ι : Type u_2
X : ι → Type u_3
inst : (i : ι) → TopologicalSpace (X i)
inst_1 : ∀ (i : ι), SeparableSpace.{u_3} (X i)
inst_2 : Countable ι
t : (x : ι) → Set (X x)
htc : ∀ (x : ι), (t x).Countable
htd : ∀ (x : ι), Dense (t x)
this : ∀ (i : ι), Countable.{u_3 + 1} (↑(t i) : Type u_3)
h : Nontrivial ((i : ι) → X i)
inhabited_h : Inhabited ((i : ι) → X i)
f : (I : Finset ι) × ((i : ↥I) → (↑(t (↑i : ι)) : Type u_3)) → (i : ι) → X i :=
  fun (x : (I : Finset ι) × ((i : ↥I) → (↑(t (↑i : ι)) : Type u_3))) (i : ι) ↦
    match (motive := (I : Finset ι) × ((i : ↥I) → (↑(t (↑i : ι)) : Type u_3)) → X i) x with
    | ⟨I, g⟩ => if hi : i ∈ I then (↑(g (Subtype.mk (p := fun (x : ι) ↦ x ∈ I) i hi)) : X (↑⟨i, hi⟩ : ι)) else default i
U : Set ((i : ι) → X i)
hU : IsOpen[Pi.topologicalSpace] U
h_1 : U.Nonempty
g : (i : ι) → X i
hg : g ∈ U
⊢ (U ∩ range f).Nonempty
have rcases : ∀ (I : Finset ι) (u : (a : ι) → Set (X a)) (huo : ∀ a ∈ I, IsOpen[inst a] (u a) ∧ g a ∈ u a)
  (huU : (↑I : Set ι).pi (α := X) u ⊆ U), (U ∩ range f).Nonempty
Tactic: rcases isOpen_pi_iff.1 hU g hg with ⟨I, u, huo, huU⟩
-- Lean 4 proof step from Mathlib.Topology.Bases (hypothesis)
Goal:
α : Type u
β : Type u_1
t_1 : TopologicalSpace α
B : Set (Set α)
s : Set α
ι : Type u_2
X : ι → Type u_3
inst : (i : ι) → TopologicalSpace (X i)
inst_1 : ∀ (i : ι), SeparableSpace.{u_3} (X i)
inst_2 : Countable ι
t : (x : ι) → Set (X x)
htc : ∀ (x : ι), (t x).Countable
htd : ∀ (x : ι), Dense (t x)
this : ∀ (i : ι), Countable.{u_3 + 1} (↑(t i) : Type u_3)
h : Nontrivial ((i : ι) → X i)
inhabited_h : Inhabited ((i : ι) → X i)
f : (I : Finset ι) × ((i : ↥I) → (↑(t (↑i : ι)) : Type u_3)) → (i : ι) → X i :=
  fun (x : (I : Finset ι) × ((i : ↥I) → (↑(t (↑i : ι)) : Type u_3))) (i : ι) ↦
    match (motive := (I : Finset ι) × ((i : ↥I) → (↑(t (↑i : ι)) : Type u_3)) → X i) x with
    | ⟨I, g⟩ => if hi : i ∈ I then (↑(g (Subtype.mk (p := fun (x : ι) ↦ x ∈ I) i hi)) : X (↑⟨i, hi⟩ : ι)) else default i
U : Set ((i : ι) → X i)
hU : IsOpen[Pi.topologicalSpace] U
h_1 : U.Nonempty
g : (i : ι) → X i
hg : g ∈ U
I : Finset ι
u : (a : ι) → Set (X a)
huo : ∀ a ∈ I, IsOpen[inst a] (u a) ∧ g a ∈ u a
huU : (↑I : Set ι).pi (α := X) u ⊆ U
⊢ (U ∩ range f).Nonempty
have this₁ : ∀ (i : ↥I),
  ∃ (y : X (↑i : ι)),
    Membership.mem (γ := Set (X (↑i : ι))) (t (↑i : ι)) y ∧ Membership.mem (γ := Set (X (↑i : ι))) (u (↑i : ι)) y
Tactic: have : ∀ i : I, ∃ y ∈ t i, y ∈ u i := fun i ↦
      (htd i).exists_mem_open (huo i i.2).1 ⟨_, (huo i i.2).2⟩
-- Lean 4 proof step from Mathlib.Topology.Bases (goal)
Goal:
α : Type u
β : Type u_1
t_1 : TopologicalSpace α
B : Set (Set α)
s : Set α
ι : Type u_2
X : ι → Type u_3
inst : (i : ι) → TopologicalSpace (X i)
inst_1 : ∀ (i : ι), SeparableSpace.{u_3} (X i)
inst_2 : Countable ι
t : (x : ι) → Set (X x)
htc : ∀ (x : ι), (t x).Countable
htd : ∀ (x : ι), Dense (t x)
this_1 : ∀ (i : ι), Countable.{u_3 + 1} (↑(t i) : Type u_3)
h : Nontrivial ((i : ι) → X i)
inhabited_h : Inhabited ((i : ι) → X i)
f : (I : Finset ι) × ((i : ↥I) → (↑(t (↑i : ι)) : Type u_3)) → (i : ι) → X i :=
  fun (x : (I : Finset ι) × ((i : ↥I) → (↑(t (↑i : ι)) : Type u_3))) (i : ι) ↦
    match (motive := (I : Finset ι) × ((i : ↥I) → (↑(t (↑i : ι)) : Type u_3)) → X i) x with
    | ⟨I, g⟩ => if hi : i ∈ I then (↑(g (Subtype.mk (p := fun (x : ι) ↦ x ∈ I) i hi)) : X (↑⟨i, hi⟩ : ι)) else default i
U : Set ((i : ι) → X i)
hU : IsOpen[Pi.topologicalSpace] U
h_1 : U.Nonempty
g : (i : ι) → X i
hg : g ∈ U
I : Finset ι
u : (a : ι) → Set (X a)
huo : ∀ a ∈ I, IsOpen[inst a] (u a) ∧ g a ∈ u a
huU : (↑I : Set ι).pi (α := X) u ⊆ U
this :
  ∀ (i : ↥I),
    ∃ (y : X (↑i : ι)),
      Membership.mem (γ := Set (X (↑i : ι))) (t (↑i : ι)) y ∧ Membership.mem (γ := Set (X (↑i : ι))) (u (↑i : ι)) y
⊢ (U ∩ range f).Nonempty
have choose : ∀ (y : (i : ↥I) → X (↑i : ι)) (hyt : ∀ (i : ↥I), Membership.mem (γ := Set (X (↑i : ι))) (t (↑i : ι)) (y i))
  (hyu : ∀ (i : ↥I), Membership.mem (γ := Set (X (↑i : ι))) (u (↑i : ι)) (y i)), (U ∩ range f).Nonempty
Tactic: choose y hyt hyu using this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Topology.Bases (goal)
Goal:
α : Type u
β : Type u_1
t_1 : TopologicalSpace α
B : Set (Set α)
s : Set α
ι : Type u_2
X : ι → Type u_3
inst : (i : ι) → TopologicalSpace (X i)
inst_1 : ∀ (i : ι), SeparableSpace.{u_3} (X i)
inst_2 : Countable ι
t : (x : ι) → Set (X x)
htc : ∀ (x : ι), (t x).Countable
htd : ∀ (x : ι), Dense (t x)
this : ∀ (i : ι), Countable.{u_3 + 1} (↑(t i) : Type u_3)
h : Nontrivial ((i : ι) → X i)
inhabited_h : Inhabited ((i : ι) → X i)
f : (I : Finset ι) × ((i : ↥I) → (↑(t (↑i : ι)) : Type u_3)) → (i : ι) → X i :=
  fun (x : (I : Finset ι) × ((i : ↥I) → (↑(t (↑i : ι)) : Type u_3))) (i : ι) ↦
    match (motive := (I : Finset ι) × ((i : ↥I) → (↑(t (↑i : ι)) : Type u_3)) → X i) x with
    | ⟨I, g⟩ => if hi : i ∈ I then (↑(g (Subtype.mk (p := fun (x : ι) ↦ x ∈ I) i hi)) : X (↑⟨i, hi⟩ : ι)) else default i
U : Set ((i : ι) → X i)
hU : IsOpen[Pi.topologicalSpace] U
h_1 : U.Nonempty
g : (i : ι) → X i
hg : g ∈ U
I : Finset ι
u : (a : ι) → Set (X a)
huo : ∀ a ∈ I, IsOpen[inst a] (u a) ∧ g a ∈ u a
huU : (↑I : Set ι).pi (α := X) u ⊆ U
y : (i : ↥I) → X (↑i : ι)
hyt : ∀ (i : ↥I), Membership.mem (γ := Set (X (↑i : ι))) (t (↑i : ι)) (y i)
hyu : ∀ (i : ↥I), Membership.mem (γ := Set (X (↑i : ι))) (u (↑i : ι)) (y i)
⊢ (U ∩ range f).Nonempty
have lift : ∀ (y : (i : ↥I) → (↑(t (↑i : ι)) : Type u_3))
  (hyu : ∀ (i : ↥I), Membership.mem (γ := Set (X (↑i : ι))) (u (↑i : ι)) ((fun (i : ↥I) ↦ (↑(y i) : X (↑i : ι))) i)),
  (U ∩ range f).Nonempty
Tactic: lift y to ∀ i : I, t i using hyt
Cleared hypotheses: y, hyt, hyu
-- Lean 4 proof step from Mathlib.Topology.Bases (goal)
Goal:
α : Type u
β : Type u_1
t_1 : TopologicalSpace α
B : Set (Set α)
s : Set α
ι : Type u_2
X : ι → Type u_3
inst : (i : ι) → TopologicalSpace (X i)
inst_1 : ∀ (i : ι), SeparableSpace.{u_3} (X i)
inst_2 : Countable ι
t : (x : ι) → Set (X x)
htc : ∀ (x : ι), (t x).Countable
htd : ∀ (x : ι), Dense (t x)
this : ∀ (i : ι), Countable.{u_3 + 1} (↑(t i) : Type u_3)
h : Nontrivial ((i : ι) → X i)
inhabited_h : Inhabited ((i : ι) → X i)
f : (I : Finset ι) × ((i : ↥I) → (↑(t (↑i : ι)) : Type u_3)) → (i : ι) → X i :=
  fun (x : (I : Finset ι) × ((i : ↥I) → (↑(t (↑i : ι)) : Type u_3))) (i : ι) ↦
    match (motive := (I : Finset ι) × ((i : ↥I) → (↑(t (↑i : ι)) : Type u_3)) → X i) x with
    | ⟨I, g⟩ => if hi : i ∈ I then (↑(g (Subtype.mk (p := fun (x : ι) ↦ x ∈ I) i hi)) : X (↑⟨i, hi⟩ : ι)) else default i
U : Set ((i : ι) → X i)
hU : IsOpen[Pi.topologicalSpace] U
h_1 : U.Nonempty
g : (i : ι) → X i
hg : g ∈ U
I : Finset ι
u : (a : ι) → Set (X a)
huo : ∀ a ∈ I, IsOpen[inst a] (u a) ∧ g a ∈ u a
huU : (↑I : Set ι).pi (α := X) u ⊆ U
y : (i : ↥I) → (↑(t (↑i : ι)) : Type u_3)
hyu : ∀ (i : ↥I), Membership.mem (γ := Set (X (↑i : ι))) (u (↑i : ι)) ((fun (i : ↥I) ↦ (↑(y i) : X (↑i : ι))) i)
⊢ (U ∩ range f).Nonempty
have refine : ∀ (i : ι) (hi : i ∈ I), f (Sigma.mk (β := fun (I : Finset ι) ↦ (i : ↥I) → (↑(t (↑i : ι)) : Type u_3)) I y) i ∈ u i
Tactic: refine ⟨f ⟨I, y⟩, huU fun i (hi : i ∈ I) ↦ ?_, mem_range_self (f := f) ⟨I, y⟩⟩
-- Lean 4 proof step from Mathlib.Topology.Bases (goal)
Goal:
α : Type u
β : Type u_1
t_1 : TopologicalSpace α
B : Set (Set α)
s : Set α
ι : Type u_2
X : ι → Type u_3
inst : (i : ι) → TopologicalSpace (X i)
inst_1 : ∀ (i : ι), SeparableSpace.{u_3} (X i)
inst_2 : Countable ι
t : (x : ι) → Set (X x)
htc : ∀ (x : ι), (t x).Countable
htd : ∀ (x : ι), Dense (t x)
this : ∀ (i : ι), Countable.{u_3 + 1} (↑(t i) : Type u_3)
h : Nontrivial ((i : ι) → X i)
inhabited_h : Inhabited ((i : ι) → X i)
f : (I : Finset ι) × ((i : ↥I) → (↑(t (↑i : ι)) : Type u_3)) → (i : ι) → X i :=
  fun (x : (I : Finset ι) × ((i : ↥I) → (↑(t (↑i : ι)) : Type u_3))) (i : ι) ↦
    match (motive := (I : Finset ι) × ((i : ↥I) → (↑(t (↑i : ι)) : Type u_3)) → X i) x with
    | ⟨I, g⟩ => if hi : i ∈ I then (↑(g (Subtype.mk (p := fun (x : ι) ↦ x ∈ I) i hi)) : X (↑⟨i, hi⟩ : ι)) else default i
U : Set ((i : ι) → X i)
hU : IsOpen[Pi.topologicalSpace] U
h_1 : U.Nonempty
g : (i : ι) → X i
hg : g ∈ U
I : Finset ι
u : (a : ι) → Set (X a)
huo : ∀ a ∈ I, IsOpen[inst a] (u a) ∧ g a ∈ u a
huU : (↑I : Set ι).pi (α := X) u ⊆ U
y : (i : ↥I) → (↑(t (↑i : ι)) : Type u_3)
hyu : ∀ (i : ↥I), Membership.mem (γ := Set (X (↑i : ι))) (u (↑i : ι)) ((fun (i : ↥I) ↦ (↑(y i) : X (↑i : ι))) i)
i : ι
hi : i ∈ I
⊢ f (Sigma.mk (β := fun (I : Finset ι) ↦ (i : ↥I) → (↑(t (↑i : ι)) : Type u_3)) I y) i ∈ u i
have simp : Membership.mem (α := X i) (u i) ((↑(y (Subtype.mk (p := fun (x : ι) ↦ x ∈ I) i sorry)) : X i) : X i)
Tactic: simp only [f, dif_pos hi]
-- Lean 4 proof step from Mathlib.Topology.Bases (goal)
Goal:
α : Type u
β : Type u_1
t_1 : TopologicalSpace α
B : Set (Set α)
s : Set α
ι : Type u_2
X : ι → Type u_3
inst : (i : ι) → TopologicalSpace (X i)
inst_1 : ∀ (i : ι), SeparableSpace.{u_3} (X i)
inst_2 : Countable ι
t : (x : ι) → Set (X x)
htc : ∀ (x : ι), (t x).Countable
htd : ∀ (x : ι), Dense (t x)
this : ∀ (i : ι), Countable.{u_3 + 1} (↑(t i) : Type u_3)
h : Nontrivial ((i : ι) → X i)
inhabited_h : Inhabited ((i : ι) → X i)
set set₁ : SeparableSpace ((i : ι) → X i)
⊢ SeparableSpace ((i : ι) → X i)
have set₂ : let f : (I : Finset ι) × ((i : ↥I) → (↑(t (↑i : ι)) : Type u_3)) → (i : ι) → X i :=
  fun (x : (I : Finset ι) × ((i : ↥I) → (↑(t (↑i : ι)) : Type u_3))) (i : ι) ↦
  match (motive := (I : Finset ι) × ((i : ↥I) → (↑(t (↑i : ι)) : Type u_3)) → X i) x with
  | ⟨I, g⟩ => if hi : i ∈ I then (↑(g (Subtype.mk (p := fun (x : ι) ↦ x ∈ I) i hi)) : X (↑⟨i, hi⟩ : ι)) else default i;
∀ (U : Set ((i : ι) → X i)) (hU : IsOpen[Pi.topologicalSpace] U),
  U.Nonempty → ∀ (g : (i : ι) → X i) (hg : g ∈ U), (U ∩ range f).Nonempty
Tactic: classical
    set f : (Σ I : Finset ι, ∀ i : I, t i) → ∀ i, X i := fun ⟨I, g⟩ i ↦
      if hi : i ∈ I then g ⟨i, hi⟩ else (default : ∀ i, X i) i
    refine ⟨⟨range f, countable_range f, dense_iff_inter_open.2 fun U hU ⟨g, hg⟩ ↦ ?_⟩⟩
    rcases isOpen_pi_iff.1 hU g hg with ⟨I, u, huo, huU⟩
    have : ∀ i : I, ∃ y ∈ t i, y ∈ u i := fun i ↦
      (htd i).exists_mem_open (huo i i.2).1 ⟨_, (huo i i.2).2⟩
    choose y hyt hyu using this
    lift y to ∀ i : I, t i using hyt
    refine ⟨f ⟨I, y⟩, huU fun i (hi : i ∈ I) ↦ ?_, mem_range_self (f := f) ⟨I, y⟩⟩
    simp only [f, dif_pos hi]
    exact hyu ⟨i, _⟩
-- Lean 4 proof step from Mathlib.Topology.Bases (goal)
Goal:
α : Type u
β : Type u_1
t_1 : TopologicalSpace α
B : Set (Set α)
s : Set α
ι : Type u_2
X : ι → Type u_3
inst : (i : ι) → TopologicalSpace (X i)
inst_1 : ∀ (i : ι), SeparableSpace.{u_3} (X i)
inst_2 : Countable ι
t : (x : ι) → Set (X x)
htc : ∀ (x : ι), (t x).Countable
htd : ∀ (x : ι), Dense (t x)
this : ∀ (i : ι), Countable.{u_3 + 1} (↑(t i) : Type u_3)
h : Nontrivial ((i : ι) → X i)
inhabited_h : Inhabited ((i : ι) → X i)
set set₁ : SeparableSpace ((i : ι) → X i)
set₂ :
  let f : (I : Finset ι) × ((i : ↥I) → (↑(t (↑i : ι)) : Type u_3)) → (i : ι) → X i :=
    fun (x : (I : Finset ι) × ((i : ↥I) → (↑(t (↑i : ι)) : Type u_3))) (i : ι) ↦
    match (motive := (I : Finset ι) × ((i : ↥I) → (↑(t (↑i : ι)) : Type u_3)) → X i) x with
    | ⟨I, g⟩ =>
      if hi : i ∈ I then (↑(g (Subtype.mk (p := fun (x : ι) ↦ x ∈ I) i hi)) : X (↑⟨i, hi⟩ : ι)) else default i;
  ∀ (U : Set ((i : ι) → X i)) (hU : IsOpen[Pi.topologicalSpace] U),
    U.Nonempty → ∀ (g : (i : ι) → X i) (hg : g ∈ U), (U ∩ range f).Nonempty
⊢ SeparableSpace ((i : ι) → X i)
have set₃ : let f : (I : Finset ι) × ((i : ↥I) → (↑(t (↑i : ι)) : Type u_3)) → (i : ι) → X i :=
  fun (x : (I : Finset ι) × ((i : ↥I) → (↑(t (↑i : ι)) : Type u_3))) (i : ι) ↦
  match (motive := (I : Finset ι) × ((i : ↥I) → (↑(t (↑i : ι)) : Type u_3)) → X i) x with
  | ⟨I, g⟩ => if hi : i ∈ I then (↑(g (Subtype.mk (p := fun (x : ι) ↦ x ∈ I) i hi)) : X (↑⟨i, hi⟩ : ι)) else default i;
∀ (U : Set ((i : ι) → X i)) (hU : IsOpen[Pi.topologicalSpace] U),
  U.Nonempty →
    ∀ (g : (i : ι) → X i) (hg : g ∈ U) (I : Finset ι) (u : (a : ι) → Set (X a))
      (huo : ∀ a ∈ I, IsOpen[inst a] (u a) ∧ g a ∈ u a) (huU : (↑I : Set ι).pi (α := X) u ⊆ U), (U ∩ range f).Nonempty
Tactic: classical
    set f : (Σ I : Finset ι, ∀ i : I, t i) → ∀ i, X i := fun ⟨I, g⟩ i ↦
      if hi : i ∈ I then g ⟨i, hi⟩ else (default : ∀ i, X i) i
    refine ⟨⟨range f, countable_range f, dense_iff_inter_open.2 fun U hU ⟨g, hg⟩ ↦ ?_⟩⟩
    rcases isOpen_pi_iff.1 hU g hg with ⟨I, u, huo, huU⟩
    have : ∀ i : I, ∃ y ∈ t i, y ∈ u i := fun i ↦
      (htd i).exists_mem_open (huo i i.2).1 ⟨_, (huo i i.2).2⟩
    choose y hyt hyu using this
    lift y to ∀ i : I, t i using hyt
    refine ⟨f ⟨I, y⟩, huU fun i (hi : i ∈ I) ↦ ?_, mem_range_self (f := f) ⟨I, y⟩⟩
    simp only [f, dif_pos hi]
    exact hyu ⟨i, _⟩
-- Lean 4 proof step from Mathlib.Topology.Bases (goal)
Goal:
α : Type u
β : Type u_1
t : TopologicalSpace α
B : Set (Set α)
s : Set α
inst : TopologicalSpace β
inst_1 : SeparableSpace α
inst_2 : SeparableSpace β
⊢ SeparableSpace (α ⊕ β)
have obtain : ∀ (s : Set α) (hsc : s.Countable) (hsd : Dense s), SeparableSpace (α ⊕ β)
Tactic: obtain ⟨s, hsc, hsd⟩ := exists_countable_dense α
-- Lean 4 proof step from Mathlib.Topology.Bases (goal)
Goal:
α : Type u
β : Type u_1
t : TopologicalSpace α
B : Set (Set α)
s_1 : Set α
inst : TopologicalSpace β
inst_1 : SeparableSpace α
inst_2 : SeparableSpace β
s : Set α
hsc : s.Countable
hsd : Dense s
⊢ SeparableSpace (α ⊕ β)
have obtain : ∀ (t_1 : Set β) (htc : t_1.Countable) (htd : Dense t_1), SeparableSpace (α ⊕ β)
Tactic: obtain ⟨t, htc, htd⟩ := exists_countable_dense β
-- 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
⊢ SeparableSpace (α ⊕ β)
have refine : Dense (Sum.inl '' s ∪ Sum.inr '' t)
Tactic: refine ⟨Sum.inl '' s ∪ Sum.inr '' t, (hsc.image _).union (htc.image _), ?_⟩
-- 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
⊢ Dense (Sum.inl '' s ∪ Sum.inr '' t)
have simp_rw : closure[instTopologicalSpaceSum] (Sum.inl '' s ∪ 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]