-- Mathlib/Topology/MetricSpace/Basic.lean
theorem secondCountable_of_countable_discretization {α : Type u} [MetricSpace α]
    (H : ∀ ε > (0 : ℝ), ∃ (β : Type*) (_ : Encodable β) (F : α → β),
      ∀ x y, F x = F y → dist x y ≤ ε) :
    SecondCountableTopology α

Proof state:
α : Type u
inst✝ : MetricSpace α
H : ∀ ε > 0, ∃ β x F, ∀ (x y : α), F x = F y → dist x y ≤ ε
⊢ SecondCountableTopology α

Tactic:
refine secondCountable_of_almost_dense_set fun ε ε0 => ?_

Result:
α : Type u
inst✝ : MetricSpace α
H : ∀ ε > 0, ∃ β x F, ∀ (x y : α), F x = F y → dist x y ≤ ε
ε : ℝ
ε0 : ε > 0
⊢ ∃ s, s.Countable ∧ ∀ (x : α), ∃ y ∈ s, dist x y ≤ ε

Proof state:
case intro.intro.intro
α : Type u
inst✝ : MetricSpace α
H : ∀ ε > 0, ∃ β x F, ∀ (x y : α), F x = F y → dist x y ≤ ε
ε : ℝ
ε0 : ε > 0
β : Type u_2
fβ : Encodable β
F : α → β
hF : ∀ (x y : α), F x = F y → dist x y ≤ ε
⊢ ∃ s, s.Countable ∧ ∀ (x : α), ∃ y ∈ s, dist x y ≤ ε

Tactic:
let Finv := rangeSplitting F

Result:
case intro.intro.intro
α : Type u
inst✝ : MetricSpace α
H : ∀ ε > 0, ∃ β x F, ∀ (x y : α), F x = F y → dist x y ≤ ε
ε : ℝ
ε0 : ε > 0
β : Type u_2
fβ : Encodable β
F : α → β
hF : ∀ (x y : α), F x = F y → dist x y ≤ ε
Finv : ↑(range F) → α := rangeSplitting F
⊢ ∃ s, s.Countable ∧ ∀ (x : α), ∃ y ∈ s, dist x y ≤ ε

Proof state:
case intro.intro.intro
α : Type u
inst✝ : MetricSpace α
H : ∀ ε > 0, ∃ β x F, ∀ (x y : α), F x = F y → dist x y ≤ ε
ε : ℝ
ε0 : ε > 0
β : Type u_2
fβ : Encodable β
F : α → β
hF : ∀ (x y : α), F x = F y → dist x y ≤ ε
Finv : ↑(range F) → α := rangeSplitting F
x : α
⊢ ∃ y ∈ range Finv, dist x y ≤ ε

Tactic:
let x' := Finv ⟨F x, mem_range_self _⟩

Result:
case intro.intro.intro
α : Type u
inst✝ : MetricSpace α
H : ∀ ε > 0, ∃ β x F, ∀ (x y : α), F x = F y → dist x y ≤ ε
ε : ℝ
ε0 : ε > 0
β : Type u_2
fβ : Encodable β
F : α → β
hF : ∀ (x y : α), F x = F y → dist x y ≤ ε
Finv : ↑(range F) → α := rangeSplitting F
x : α
x' : α := Finv ⟨F x, ⋯⟩
⊢ ∃ y ∈ range Finv, dist x y ≤ ε

Proof state:
case intro.intro.intro
α : Type u
inst✝ : MetricSpace α
H : ∀ ε > 0, ∃ β x F, ∀ (x y : α), F x = F y → dist x y ≤ ε
ε : ℝ
ε0 : ε > 0
β : Type u_2
fβ : Encodable β
F : α → β
hF : ∀ (x y : α), F x = F y → dist x y ≤ ε
Finv : ↑(range F) → α := rangeSplitting F
⊢ ∃ s, s.Countable ∧ ∀ (x : α), ∃ y ∈ s, dist x y ≤ ε

Tactic:
refine ⟨range Finv, ⟨countable_range _, fun x => ?_⟩⟩

Result:
case intro.intro.intro
α : Type u
inst✝ : MetricSpace α
H : ∀ ε > 0, ∃ β x F, ∀ (x y : α), F x = F y → dist x y ≤ ε
ε : ℝ
ε0 : ε > 0
β : Type u_2
fβ : Encodable β
F : α → β
hF : ∀ (x y : α), F x = F y → dist x y ≤ ε
Finv : ↑(range F) → α := rangeSplitting F
x : α
⊢ ∃ y ∈ range Finv, dist x y ≤ ε

Proof state:
α : Type u
inst✝ : MetricSpace α
H : ∀ ε > 0, ∃ β x F, ∀ (x y : α), F x = F y → dist x y ≤ ε
ε : ℝ
ε0 : ε > 0
⊢ ∃ s, s.Countable ∧ ∀ (x : α), ∃ y ∈ s, dist x y ≤ ε

Tactic:
rcases H ε ε0 with ⟨β, fβ, F, hF⟩

Result:
case intro.intro.intro
α : Type u
inst✝ : MetricSpace α
H : ∀ ε > 0, ∃ β x F, ∀ (x y : α), F x = F y → dist x y ≤ ε
ε : ℝ
ε0 : ε > 0
β : Type u_2
fβ : Encodable β
F : α → β
hF : ∀ (x y : α), F x = F y → dist x y ≤ ε
⊢ ∃ s, s.Countable ∧ ∀ (x : α), ∃ y ∈ s, dist x y ≤ ε

Proof state:
case intro.intro.intro
α : Type u
inst✝ : MetricSpace α
H : ∀ ε > 0, ∃ β x F, ∀ (x y : α), F x = F y → dist x y ≤ ε
ε : ℝ
ε0 : ε > 0
β : Type u_2
fβ : Encodable β
F : α → β
hF : ∀ (x y : α), F x = F y → dist x y ≤ ε
Finv : ↑(range F) → α := rangeSplitting F
x : α
x' : α := Finv ⟨F x, ⋯⟩
⊢ ∃ y ∈ range Finv, dist x y ≤ ε

Tactic:
have : F x' = F x := apply_rangeSplitting F _

Result:
case intro.intro.intro
α : Type u
inst✝ : MetricSpace α
H : ∀ ε > 0, ∃ β x F, ∀ (x y : α), F x = F y → dist x y ≤ ε
ε : ℝ
ε0 : ε > 0
β : Type u_2
fβ : Encodable β
F : α → β
hF : ∀ (x y : α), F x = F y → dist x y ≤ ε
Finv : ↑(range F) → α := rangeSplitting F
x : α
x' : α := Finv ⟨F x, ⋯⟩
this : F x' = F x
⊢ ∃ y ∈ range Finv, dist x y ≤ ε

Proof state:
case intro.intro.intro
α : Type u
inst✝ : MetricSpace α
H : ∀ ε > 0, ∃ β x F, ∀ (x y : α), F x = F y → dist x y ≤ ε
ε : ℝ
ε0 : ε > 0
β : Type u_2
fβ : Encodable β
F : α → β
hF : ∀ (x y : α), F x = F y → dist x y ≤ ε
Finv : ↑(range F) → α := rangeSplitting F
x : α
x' : α := Finv ⟨F x, ⋯⟩
this : F x' = F x
⊢ ∃ y ∈ range Finv, dist x y ≤ ε

Tactic:
exact ⟨x', mem_range_self _, hF _ _ this.symm⟩

Result:
no goals