awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Bases
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
⊢ ∀ (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⟩
-- Module: Mathlib.Topology.Bases
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
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
⊢ (U ∩ range f).Nonempty

Tactic:
choose y hyt hyu using this
-- Module: Mathlib.Topology.Bases
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)
⊢ ∀ (i : ↥I), Membership.mem (γ := Set (X (↑i : ι))) (t (↑i : ι)) (y i)

Tactic:
hyt
-- Module: Mathlib.Topology.Bases
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)
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
⊢ (U ∩ range f).Nonempty

Tactic:
lift y to ∀ i : I, t i using hyt
-- Module: Mathlib.Topology.Bases
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

Tactic:
⟨f ⟨I, y⟩, huU fun i (hi : i ∈ I) ↦ ?_, mem_range_self (f := f) ⟨I, y⟩⟩

Premises used: Set.mem_range_self, Set.Nonempty, And.intro, Exists.intro, Sigma.mk
-- Module: Mathlib.Topology.Bases
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)
refine :
  ∀ (i : ι) (hi : i ∈ I), f (Sigma.mk (β := fun (I : Finset ι) ↦ (i : ↥I) → (↑(t (↑i : ι)) : Type u_3)) I y) i ∈ u i
⊢ (U ∩ range f).Nonempty

Tactic:
refine ⟨f ⟨I, y⟩, huU fun i (hi : i ∈ I) ↦ ?_, mem_range_self (f := f) ⟨I, y⟩⟩
-- Module: Mathlib.Topology.Bases
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
simp : Membership.mem (α := X i) (u i) ((↑(y (Subtype.mk (p := fun (x : ι) ↦ x ∈ I) i ⋯)) : X i) : X i)
⊢ f (Sigma.mk (β := fun (I : Finset ι) ↦ (i : ↥I) → (↑(t (↑i : ι)) : Type u_3)) I y) i ∈ u i

Tactic:
simp only [f, dif_pos hi]

Premises used: dif_pos
-- Module: Mathlib.Topology.Bases
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
⊢ Membership.mem (α := X i) (u i) ((↑(y (Subtype.mk (p := fun (x : ι) ↦ x ∈ I) i ⋯)) : X i) : X i)

Tactic:
hyu ⟨i, _⟩

Premises used: Set.Mem, Subtype.mk
-- Module: Mathlib.Topology.Bases
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
⊢ Membership.mem (α := X i) (u i) ((↑(y (Subtype.mk (p := fun (x : ι) ↦ x ∈ I) i ⋯)) : X i) : X i)

Tactic:
exact hyu ⟨i, _⟩

Premises used: Subtype.mk
-- Module: Mathlib.Topology.Bases
Goal:
α : Type u
β : Type u_1
t : TopologicalSpace α
B : Set (Set α)
s : Set α
inst : SeparableSpace α
r : α → α → Prop
⊢ SeparableSpace.{u} (Quot r)

Tactic:
isQuotientMap_quot_mk.separableSpace

Premises used: Topology.IsQuotientMap.separableSpace, isQuotientMap_quot_mk
-- Module: Mathlib.Topology.Bases
Goal:
α : Type u
β : Type u_1
t : TopologicalSpace α
B : Set (Set α)
s_1 : Set α
inst : SeparableSpace α
s : Setoid α
⊢ SeparableSpace.{u} (Quotient s)

Tactic:
isQuotientMap_quot_mk.separableSpace

Premises used: Topology.IsQuotientMap.separableSpace, Quotient, Quotient.mk', isQuotientMap_quot_mk
-- Module: Mathlib.Topology.Bases
Goal:
α : Type u
β : Type u_1
t : TopologicalSpace α
B : Set (Set α)
s : Set α
inst : TopologicalSpace β
inst_1 : SeparableSpace α
inst_2 : SeparableSpace β
obtain : ∀ (s : Set α) (hsc : s.Countable) (hsd : Dense s), SeparableSpace (α ⊕ β)
⊢ SeparableSpace (α ⊕ β)

Tactic:
obtain ⟨s, hsc, hsd⟩ := exists_countable_dense α

Premises used: TopologicalSpace.exists_countable_dense
-- Module: Mathlib.Topology.Bases
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
obtain : ∀ (t_1 : Set β) (htc : t_1.Countable) (htd : Dense t_1), SeparableSpace (α ⊕ β)
⊢ SeparableSpace (α ⊕ β)

Tactic:
obtain ⟨t, htc, htd⟩ := exists_countable_dense β

Premises used: TopologicalSpace.exists_countable_dense
-- Module: Mathlib.Topology.Bases
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 (α ⊕ β)

Tactic:
⟨Sum.inl '' s ∪ Sum.inr '' t, (hsc.image _).union (htc.image _), ?_⟩

Premises used: Sum.inl, Set.Countable.image, Set.Countable.union, Sum.inr, And.intro, Exists.intro, Set.image, TopologicalSpace.SeparableSpace.mk, Union.union
-- Module: Mathlib.Topology.Bases
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
refine : Dense (Sum.inl '' s ∪ Sum.inr '' t)
⊢ SeparableSpace (α ⊕ β)

Tactic:
refine ⟨Sum.inl '' s ∪ Sum.inr '' t, (hsc.image _).union (htc.image _), ?_⟩
-- Module: Mathlib.Topology.Bases
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
simp_rw₆ : Eq (α := Set (α ⊕ β)) (range Sum.inl ∪ range Sum.inr) univ
⊢ Dense (Sum.inl '' s ∪ Sum.inr '' t)

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]

Premises used: Set.image_univ, Set.range_inl_union_range_inr, dense_iff_closure_eq, closure_union, Dense.closure_eq, Topology.IsClosedEmbedding.inr, Topology.IsClosedEmbedding.inl, Topology.IsClosedEmbedding.closure_image_eq
-- Module: Mathlib.Topology.Bases
Goal:
α : Type u
β : Type u_1
t : TopologicalSpace α
inst : TopologicalSpace β
⊢ SeparableSpace (α ⊕ β) ↔ SeparableSpace α ∧ SeparableSpace β

Tactic:
⟨fun _ => ⟨(IsOpenEmbedding.inl (Y := β)).separableSpace,
    (IsOpenEmbedding.inr (X := α)).separableSpace⟩, fun ⟨_, _⟩ => inferInstance⟩

Premises used: _private.0.TopologicalSpace.separableSpace_sum_iff.match_1, inferInstance, Sum, Topology.IsOpenEmbedding.inr, And.intro, Topology.IsOpenEmbedding.inl, Iff.intro, Topology.IsOpenEmbedding.separableSpace, TopologicalSpace.SeparableSpace
-- Module: Mathlib.Topology.Bases
Goal:
α : Type u
t : TopologicalSpace α
inst : DiscreteTopology α
⊢ SeparableSpace α ↔ Countable α

Tactic:
simp [separableSpace_iff, countable_univ_iff]

Premises used: Set.countable_univ_iff, TopologicalSpace.separableSpace_iff
-- Module: Mathlib.Topology.Bases
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
rcases : ∀ (u : Set α) (u_countable : u.Countable) (u_dense : Dense u), Countable ι
⊢ Countable ι

Tactic:
rcases exists_countable_dense α with ⟨u, u_countable, u_dense⟩

Premises used: TopologicalSpace.exists_countable_dense
-- Module: Mathlib.Topology.Bases
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
choose : ∀ (f : (i : ι) → α) (hfu : ∀ (i : ι), f i ∈ u) (hfs : ∀ (i : ι), f i ∈ s i), Countable ι
⊢ Countable ι

Tactic:
choose f hfu hfs using fun i ↦ u_dense.exists_mem_open (ho i) (hne i)

Premises used: Dense.exists_mem_open
-- Module: Mathlib.Topology.Bases
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
⊢ 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⟩
-- Module: Mathlib.Topology.Bases
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.{u + 1} (↑u : Type u)

Tactic:
have := u_countable.to_subtype
-- Module: Mathlib.Topology.Bases
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
this : Countable.{u + 1} (↑u : Type u)
⊢ Countable ι

Tactic:
(f_inj.codRestrict hfu).countable

Premises used: Function.Injective.countable, Function.Injective.codRestrict
-- Module: Mathlib.Topology.Bases
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
this : Countable.{u + 1} (↑u : Type u)
⊢ Countable ι

Tactic:
exact (f_inj.codRestrict hfu).countable

Premises used: Function.Injective.countable, Function.Injective.codRestrict
-- Module: Mathlib.Topology.Bases
Goal:
α : Type u
t : TopologicalSpace α
inst : SeparableSpace α
ι : Type u_2
s : ι → Set α
a : Set ι
h : a.PairwiseDisjoint s
ho : ∀ i ∈ a, IsOpen[t] (s i)
hne : ∀ i ∈ a, (s i).Nonempty
⊢ a.Countable

Tactic:
(h.subtype _ _).countable_of_isOpen_disjoint (Subtype.forall.2 ho) (Subtype.forall.2 hne)

Premises used: Iff.mpr, Pairwise.countable_of_isOpen_disjoint, Subtype.forall, Set.Pairwise.subtype, Set.Countable
-- Module: Mathlib.Topology.Bases
Goal:
α : Type u
t : TopologicalSpace α
inst : SeparableSpace α
ι : Type u_2
s : ι → Set α
a : Set ι
h : a.PairwiseDisjoint s
ha : ∀ i ∈ a, (interior (s i)).Nonempty
⊢ a.Countable

Tactic:
(h.mono fun _ => interior_subset).countable_of_isOpen (fun _ _ => isOpen_interior) ha

Premises used: Set.PairwiseDisjoint.mono, interior_subset, isOpen_interior, Set.PairwiseDisjoint.countable_of_isOpen
-- Module: Mathlib.Topology.Bases
Goal:
α : Type u
t : TopologicalSpace α
s u : Set α
hs : IsSeparable s
hu : u ⊆ s
rcases : ∀ (c : Set α) (c_count : c.Countable) (hs : s ⊆ closure[t] c), IsSeparable u
⊢ IsSeparable u

Tactic:
rcases hs with ⟨c, c_count, hs⟩
-- Module: Mathlib.Topology.Bases
Goal:
α : Type u
t : TopologicalSpace α
s u : Set α
hu : u ⊆ s
c : Set α
c_count : c.Countable
hs : s ⊆ closure[t] c
⊢ IsSeparable u

Tactic:
⟨c, c_count, hu.trans hs⟩

Premises used: TopologicalSpace.IsSeparable, HasSubset.Subset.trans, And.intro, Exists.intro
-- Module: Mathlib.Topology.Bases
Goal:
α : Type u
t : TopologicalSpace α
s u : Set α
hu : u ⊆ s
c : Set α
c_count : c.Countable
hs : s ⊆ closure[t] c
⊢ IsSeparable u

Tactic:
exact ⟨c, c_count, hu.trans hs⟩
-- Module: Mathlib.Topology.Bases
Goal:
α : Type u
t : TopologicalSpace α
ι : Sort u_2
inst : Countable ι
s : ι → Set α
hs : ∀ (i : ι), IsSeparable (s i)
choose :
  ∀ (c : (i : ι) → Set α) (hc : ∀ (i : ι), (c i).Countable) (h'c : ∀ (i : ι), s i ⊆ closure[t] (c i)),
    IsSeparable.{u} (α := α) (⋃ (i : ι), s i)
⊢ IsSeparable.{u} (α := α) (⋃ (i : ι), s i)

Tactic:
choose c hc h'c using hs
-- Module: Mathlib.Topology.Bases
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)

Tactic:
⟨⋃ i, c i, countable_iUnion hc, iUnion_subset_iff.2 fun i => ?_⟩

Premises used: Iff.mpr, Set.iUnion_subset_iff, TopologicalSpace.IsSeparable, Set.countable_iUnion, And.intro, Exists.intro, Set.iUnion
-- Module: Mathlib.Topology.Bases
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)
refine : ∀ (i : ι), s i ⊆ closure[t] (⋃ (i : ι), c i)
⊢ IsSeparable.{u} (α := α) (⋃ (i : ι), s i)

Tactic:
refine ⟨⋃ i, c i, countable_iUnion hc, iUnion_subset_iff.2 fun i => ?_⟩
-- Module: Mathlib.Topology.Bases
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)
i : ι
⊢ s i ⊆ closure[t] (⋃ (i : ι), c i)

Tactic:
(h'c i).trans (closure_mono (subset_iUnion _ i))

Premises used: HasSubset.Subset.trans, closure_mono, Set.subset_iUnion
-- Module: Mathlib.Topology.Bases
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)
i : ι
⊢ s i ⊆ closure[t] (⋃ (i : ι), c i)

Tactic:
exact (h'c i).trans (closure_mono (subset_iUnion _ i))

Premises used: HasSubset.Subset.trans, closure_mono, Set.subset_iUnion