-- Mathlib/Topology/UniformSpace/Cauchy.lean
theorem secondCountable_of_separable [SeparableSpace α] : SecondCountableTopology α

Proof state:
case intro.intro.intro.intro.refine_2.intro.intro.intro.intro.intro
α : Type u
uniformSpace : UniformSpace α
inst✝¹ : (𝓤 α).IsCountablyGenerated
inst✝ : SeparableSpace α
s : Set α
hsc : s.Countable
hsd : Dense s
t : ℕ → Set (α × α)
h_basis : (𝓤 α).HasAntitoneBasis t
ht_mem : ∀ (i : ℕ), t i ∈ (𝓤 α).sets
hto : ∀ (i : ℕ), IsOpen (t i)
hts : ∀ (i : ℕ), SymmetricRel (t i)
x : α
V : Set α
hxV : x ∈ V
hVo : IsOpen V
U : Set (α × α)
hU : U ∈ 𝓤 α
hUV : ball x U ⊆ V
U' : Set (α × α)
hU' : U' ∈ 𝓤 α
left✝ : ∀ {a b : α}, (a, b) ∈ U' → (b, a) ∈ U'
hUU' : U' ○ U' ⊆ U
⊢ ∃ v, (∃ i ∈ s, ∃ y, ball i (t y) = v) ∧ x ∈ v ∧ v ⊆ V

Tactic:
rcases h_basis.toHasBasis.mem_iff.1 hU' with ⟨k, -, hk⟩

Result:
case intro.intro.intro.intro.refine_2.intro.intro.intro.intro.intro.intro.intro
α : Type u
uniformSpace : UniformSpace α
inst✝¹ : (𝓤 α).IsCountablyGenerated
inst✝ : SeparableSpace α
s : Set α
hsc : s.Countable
hsd : Dense s
t : ℕ → Set (α × α)
h_basis : (𝓤 α).HasAntitoneBasis t
ht_mem : ∀ (i : ℕ), t i ∈ (𝓤 α).sets
hto : ∀ (i : ℕ), IsOpen (t i)
hts : ∀ (i : ℕ), SymmetricRel (t i)
x : α
V : Set α
hxV : x ∈ V
hVo : IsOpen V
U : Set (α × α)
hU : U ∈ 𝓤 α
hUV : ball x U ⊆ V
U' : Set (α × α)
hU' : U' ∈ 𝓤 α
left✝ : ∀ {a b : α}, (a, b) ∈ U' → (b, a) ∈ U'
hUU' : U' ○ U' ⊆ U
k : ℕ
hk : t k ⊆ U'
⊢ ∃ v, (∃ i ∈ s, ∃ y, ball i (t y) = v) ∧ x ∈ v ∧ v ⊆ V

Proof state:
case intro.intro.intro.intro.refine_2
α : Type u
uniformSpace : UniformSpace α
inst✝¹ : (𝓤 α).IsCountablyGenerated
inst✝ : SeparableSpace α
s : Set α
hsc : s.Countable
hsd : Dense s
t : ℕ → Set (α × α)
h_basis : (𝓤 α).HasAntitoneBasis t
ht_mem : ∀ (i : ℕ), t i ∈ (𝓤 α).sets
hto : ∀ (i : ℕ), IsOpen (t i)
hts : ∀ (i : ℕ), SymmetricRel (t i)
⊢ ∀ (a : α) (u : Set α), a ∈ u → IsOpen u → ∃ v ∈ ⋃ x ∈ s, range fun k => ball x (t k), a ∈ v ∧ v ⊆ u

Tactic:
intro x V hxV hVo

Result:
case intro.intro.intro.intro.refine_2
α : Type u
uniformSpace : UniformSpace α
inst✝¹ : (𝓤 α).IsCountablyGenerated
inst✝ : SeparableSpace α
s : Set α
hsc : s.Countable
hsd : Dense s
t : ℕ → Set (α × α)
h_basis : (𝓤 α).HasAntitoneBasis t
ht_mem : ∀ (i : ℕ), t i ∈ (𝓤 α).sets
hto : ∀ (i : ℕ), IsOpen (t i)
hts : ∀ (i : ℕ), SymmetricRel (t i)
x : α
V : Set α
hxV : x ∈ V
hVo : IsOpen V
⊢ ∃ v ∈ ⋃ x ∈ s, range fun k => ball x (t k), x ∈ v ∧ v ⊆ V

Proof state:
case intro.intro.intro.intro.refine_1.intro.intro.intro
α : Type u
uniformSpace : UniformSpace α
inst✝¹ : (𝓤 α).IsCountablyGenerated
inst✝ : SeparableSpace α
s : Set α
hsc : s.Countable
hsd : Dense s
t : ℕ → Set (α × α)
h_basis : (𝓤 α).HasAntitoneBasis t
ht_mem : ∀ (i : ℕ), t i ∈ (𝓤 α).sets
hto : ∀ (i : ℕ), IsOpen (t i)
hts : ∀ (i : ℕ), SymmetricRel (t i)
x : α
w✝ : x ∈ s
k : ℕ
⊢ IsOpen (ball x (t k))

Tactic:
exact isOpen_ball x (hto k)

Result:
no goals

Proof state:
α : Type u
uniformSpace : UniformSpace α
inst✝¹ : (𝓤 α).IsCountablyGenerated
inst✝ : SeparableSpace α
⊢ SecondCountableTopology α

Tactic:
rcases exists_countable_dense α with ⟨s, hsc, hsd⟩

Result:
case intro.intro
α : Type u
uniformSpace : UniformSpace α
inst✝¹ : (𝓤 α).IsCountablyGenerated
inst✝ : SeparableSpace α
s : Set α
hsc : s.Countable
hsd : Dense s
⊢ SecondCountableTopology α

Proof state:
case intro.intro.intro.intro.refine_1
α : Type u
uniformSpace : UniformSpace α
inst✝¹ : (𝓤 α).IsCountablyGenerated
inst✝ : SeparableSpace α
s : Set α
hsc : s.Countable
hsd : Dense s
t : ℕ → Set (α × α)
h_basis : (𝓤 α).HasAntitoneBasis t
ht_mem : ∀ (i : ℕ), t i ∈ (𝓤 α).sets
hto : ∀ (i : ℕ), IsOpen (t i)
hts : ∀ (i : ℕ), SymmetricRel (t i)
⊢ ∀ (u : Set α), (∃ i, ∃ (_ : i ∈ s), ∃ y, ball i (t y) = u) → IsOpen u

Tactic:
rintro _ ⟨x, _, k, rfl⟩

Result:
case intro.intro.intro.intro.refine_1.intro.intro.intro
α : Type u
uniformSpace : UniformSpace α
inst✝¹ : (𝓤 α).IsCountablyGenerated
inst✝ : SeparableSpace α
s : Set α
hsc : s.Countable
hsd : Dense s
t : ℕ → Set (α × α)
h_basis : (𝓤 α).HasAntitoneBasis t
ht_mem : ∀ (i : ℕ), t i ∈ (𝓤 α).sets
hto : ∀ (i : ℕ), IsOpen (t i)
hts : ∀ (i : ℕ), SymmetricRel (t i)
x : α
w✝ : x ∈ s
k : ℕ
⊢ IsOpen (ball x (t k))

Proof state:
case intro.intro.intro.intro
α : Type u
uniformSpace : UniformSpace α
inst✝¹ : (𝓤 α).IsCountablyGenerated
inst✝ : SeparableSpace α
s : Set α
hsc : s.Countable
hsd : Dense s
t : ℕ → Set (α × α)
h_basis : (𝓤 α).HasAntitoneBasis t
ht_mem : ∀ (i : ℕ), t i ∈ (𝓤 α).sets
hto : ∀ (i : ℕ), IsOpen (t i)
hts : ∀ (i : ℕ), SymmetricRel (t i)
⊢ toTopologicalSpace = generateFrom (⋃ x ∈ s, range fun k => ball x (t k))

Tactic:
refine (isTopologicalBasis_of_isOpen_of_nhds ?_ ?_).eq_generateFrom

Result:
case intro.intro.intro.intro.refine_1
α : Type u
uniformSpace : UniformSpace α
inst✝¹ : (𝓤 α).IsCountablyGenerated
inst✝ : SeparableSpace α
s : Set α
hsc : s.Countable
hsd : Dense s
t : ℕ → Set (α × α)
h_basis : (𝓤 α).HasAntitoneBasis t
ht_mem : ∀ (i : ℕ), t i ∈ (𝓤 α).sets
hto : ∀ (i : ℕ), IsOpen (t i)
hts : ∀ (i : ℕ), SymmetricRel (t i)
⊢ ∀ u ∈ ⋃ x ∈ s, range fun k => ball x (t k), IsOpen u

case intro.intro.intro.intro.refine_2
α : Type u
uniformSpace : UniformSpace α
inst✝¹ : (𝓤 α).IsCountablyGenerated
inst✝ : SeparableSpace α
s : Set α
hsc : s.Countable
hsd : Dense s
t : ℕ → Set (α × α)
h_basis : (𝓤 α).HasAntitoneBasis t
ht_mem : ∀ (i : ℕ), t i ∈ (𝓤 α).sets
hto : ∀ (i : ℕ), IsOpen (t i)
hts : ∀ (i : ℕ), SymmetricRel (t i)
⊢ ∀ (a : α) (u : Set α), a ∈ u → IsOpen u → ∃ v ∈ ⋃ x ∈ s, range fun k => ball x (t k), a ∈ v ∧ v ⊆ u

Proof state:
case intro.intro.intro.intro.refine_2
α : Type u
uniformSpace : UniformSpace α
inst✝¹ : (𝓤 α).IsCountablyGenerated
inst✝ : SeparableSpace α
s : Set α
hsc : s.Countable
hsd : Dense s
t : ℕ → Set (α × α)
h_basis : (𝓤 α).HasAntitoneBasis t
ht_mem : ∀ (i : ℕ), t i ∈ (𝓤 α).sets
hto : ∀ (i : ℕ), IsOpen (t i)
hts : ∀ (i : ℕ), SymmetricRel (t i)
x : α
V : Set α
hxV : x ∈ V
hVo : IsOpen V
⊢ ∃ v, (∃ i ∈ s, ∃ y, ball i (t y) = v) ∧ x ∈ v ∧ v ⊆ V

Tactic:
rcases UniformSpace.mem_nhds_iff.1 (IsOpen.mem_nhds hVo hxV) with ⟨U, hU, hUV⟩

Result:
case intro.intro.intro.intro.refine_2.intro.intro
α : Type u
uniformSpace : UniformSpace α
inst✝¹ : (𝓤 α).IsCountablyGenerated
inst✝ : SeparableSpace α
s : Set α
hsc : s.Countable
hsd : Dense s
t : ℕ → Set (α × α)
h_basis : (𝓤 α).HasAntitoneBasis t
ht_mem : ∀ (i : ℕ), t i ∈ (𝓤 α).sets
hto : ∀ (i : ℕ), IsOpen (t i)
hts : ∀ (i : ℕ), SymmetricRel (t i)
x : α
V : Set α
hxV : x ∈ V
hVo : IsOpen V
U : Set (α × α)
hU : U ∈ 𝓤 α
hUV : ball x U ⊆ V
⊢ ∃ v, (∃ i ∈ s, ∃ y, ball i (t y) = v) ∧ x ∈ v ∧ v ⊆ V

Proof state:
case intro.intro.intro.intro
α : Type u
uniformSpace : UniformSpace α
inst✝¹ : (𝓤 α).IsCountablyGenerated
inst✝ : SeparableSpace α
s : Set α
hsc : s.Countable
hsd : Dense s
t : ℕ → Set (α × α)
hto : ∀ (i : ℕ), t i ∈ (𝓤 α).sets ∧ IsOpen (t i) ∧ SymmetricRel (t i)
h_basis : (𝓤 α).HasAntitoneBasis t
⊢ SecondCountableTopology α

Tactic:
choose ht_mem hto hts using hto

Result:
case intro.intro.intro.intro
α : Type u
uniformSpace : UniformSpace α
inst✝¹ : (𝓤 α).IsCountablyGenerated
inst✝ : SeparableSpace α
s : Set α
hsc : s.Countable
hsd : Dense s
t : ℕ → Set (α × α)
h_basis : (𝓤 α).HasAntitoneBasis t
ht_mem : ∀ (i : ℕ), t i ∈ (𝓤 α).sets
hto : ∀ (i : ℕ), IsOpen (t i)
hts : ∀ (i : ℕ), SymmetricRel (t i)
⊢ SecondCountableTopology α