-- Mathlib/Topology/Bases.lean
theorem _root_.Pairwise.countable_of_isOpen_disjoint [SeparableSpace α] {ι : Type*}
    {s : ι → Set α} (hd : Pairwise (Disjoint on s)) (ho : ∀ i, IsOpen (s i))
    (hne : ∀ i, (s i).Nonempty) : Countable ι

Proof state:
case intro.intro
α : Type u
t : TopologicalSpace α
inst✝ : SeparableSpace α
ι : Type u_2
s : ι → Set α
hd : Pairwise (Disjoint on s)
ho : ∀ (i : ι), IsOpen (s i)
hne : ∀ (i : ι), (s i).Nonempty
u : Set α
u_countable : u.Countable
u_dense : Dense u
f : ι → α
hfu : ∀ (i : ι), f i ∈ u
hfs : ∀ (i : ι), f i ∈ s i
f_inj : Injective f
this : Countable ↑u
⊢ Countable ι

Tactic:
exact (f_inj.codRestrict hfu).countable

Result:
no goals

Proof state:
case intro.intro
α : Type u
t : TopologicalSpace α
inst✝ : SeparableSpace α
ι : Type u_2
s : ι → Set α
hd : Pairwise (Disjoint on s)
ho : ∀ (i : ι), IsOpen (s i)
hne : ∀ (i : ι), (s i).Nonempty
u : Set α
u_countable : u.Countable
u_dense : Dense u
f : ι → α
hfu : ∀ (i : ι), f i ∈ u
hfs : ∀ (i : ι), f i ∈ s i
⊢ Countable ι

Tactic:
have f_inj : Injective f := fun i j hij ↦
  hd.eq <| not_disjoint_iff.2 ⟨f i, hfs i, hij.symm ▸ hfs j⟩

Result:
case intro.intro
α : Type u
t : TopologicalSpace α
inst✝ : SeparableSpace α
ι : Type u_2
s : ι → Set α
hd : Pairwise (Disjoint on s)
ho : ∀ (i : ι), IsOpen (s i)
hne : ∀ (i : ι), (s i).Nonempty
u : Set α
u_countable : u.Countable
u_dense : Dense u
f : ι → α
hfu : ∀ (i : ι), f i ∈ u
hfs : ∀ (i : ι), f i ∈ s i
f_inj : Injective f
⊢ Countable ι

Proof state:
case intro.intro
α : Type u
t : TopologicalSpace α
inst✝ : SeparableSpace α
ι : Type u_2
s : ι → Set α
hd : Pairwise (Disjoint on s)
ho : ∀ (i : ι), IsOpen (s i)
hne : ∀ (i : ι), (s i).Nonempty
u : Set α
u_countable : u.Countable
u_dense : Dense u
⊢ Countable ι

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

Result:
case intro.intro
α : Type u
t : TopologicalSpace α
inst✝ : SeparableSpace α
ι : Type u_2
s : ι → Set α
hd : Pairwise (Disjoint on s)
ho : ∀ (i : ι), IsOpen (s i)
hne : ∀ (i : ι), (s i).Nonempty
u : Set α
u_countable : u.Countable
u_dense : Dense u
f : ι → α
hfu : ∀ (i : ι), f i ∈ u
hfs : ∀ (i : ι), f i ∈ s i
⊢ Countable ι

Proof state:
case intro.intro
α : Type u
t : TopologicalSpace α
inst✝ : SeparableSpace α
ι : Type u_2
s : ι → Set α
hd : Pairwise (Disjoint on s)
ho : ∀ (i : ι), IsOpen (s i)
hne : ∀ (i : ι), (s i).Nonempty
u : Set α
u_countable : u.Countable
u_dense : Dense u
f : ι → α
hfu : ∀ (i : ι), f i ∈ u
hfs : ∀ (i : ι), f i ∈ s i
f_inj : Injective f
⊢ Countable ι

Tactic:
have := u_countable.to_subtype

Result:
case intro.intro
α : Type u
t : TopologicalSpace α
inst✝ : SeparableSpace α
ι : Type u_2
s : ι → Set α
hd : Pairwise (Disjoint on s)
ho : ∀ (i : ι), IsOpen (s i)
hne : ∀ (i : ι), (s i).Nonempty
u : Set α
u_countable : u.Countable
u_dense : Dense u
f : ι → α
hfu : ∀ (i : ι), f i ∈ u
hfs : ∀ (i : ι), f i ∈ s i
f_inj : Injective f
this : Countable ↑u
⊢ Countable ι

Proof state:
α : Type u
t : TopologicalSpace α
inst✝ : SeparableSpace α
ι : Type u_2
s : ι → Set α
hd : Pairwise (Disjoint on s)
ho : ∀ (i : ι), IsOpen (s i)
hne : ∀ (i : ι), (s i).Nonempty
⊢ Countable ι

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

Result:
case intro.intro
α : Type u
t : TopologicalSpace α
inst✝ : SeparableSpace α
ι : Type u_2
s : ι → Set α
hd : Pairwise (Disjoint on s)
ho : ∀ (i : ι), IsOpen (s i)
hne : ∀ (i : ι), (s i).Nonempty
u : Set α
u_countable : u.Countable
u_dense : Dense u
⊢ Countable ι