-- Mathlib/Topology/EMetricSpace/Defs.lean
theorem subset_countable_closure_of_almost_dense_set (s : Set α)
    (hs : ∀ ε > 0, ∃ t : Set α, t.Countable ∧ s ⊆ ⋃ x ∈ t, closedBall x ε) :
    ∃ t, t ⊆ s ∧ t.Countable ∧ s ⊆ closure t

Proof state:
case inl
α : Type u
inst✝ : PseudoEMetricSpace α
s : Set α
hs : ∀ ε > 0, ∃ t, t.Countable ∧ s ⊆ ⋃ x ∈ t, closedBall x ε
x₀ : α
hx₀ : x₀ ∈ s
T : ℕ → Set α
hTc : ∀ (n : ℕ), (T n).Countable
hsT : ∀ (n : ℕ), s ⊆ ⋃ x ∈ T n, closedBall x (↑n)⁻¹
r : ℝ≥0∞
x : α
he : closedBall x r ∩ s = ∅
⊢ closedBall x r ∩ s ⊆ closedBall x₀ (r * 2)

Tactic:
rw [he]

Result:
case inl
α : Type u
inst✝ : PseudoEMetricSpace α
s : Set α
hs : ∀ ε > 0, ∃ t, t.Countable ∧ s ⊆ ⋃ x ∈ t, closedBall x ε
x₀ : α
hx₀ : x₀ ∈ s
T : ℕ → Set α
hTc : ∀ (n : ℕ), (T n).Countable
hsT : ∀ (n : ℕ), s ⊆ ⋃ x ∈ T n, closedBall x (↑n)⁻¹
r : ℝ≥0∞
x : α
he : closedBall x r ∩ s = ∅
⊢ ∅ ⊆ closedBall x₀ (r * 2)

Proof state:
case inr.intro
α : Type u
inst✝ : PseudoEMetricSpace α
s : Set α
hs : ∀ ε > 0, ∃ t, t.Countable ∧ s ⊆ ⋃ x ∈ t, closedBall x ε
x₀ : α
hx₀ : x₀ ∈ s
⊢ ∃ t ⊆ s, t.Countable ∧ s ⊆ closure t

Tactic:
choose! T hTc hsT using fun n : ℕ => hs n⁻¹ (by simp)

Result:
case inr.intro
α : Type u
inst✝ : PseudoEMetricSpace α
s : Set α
hs : ∀ ε > 0, ∃ t, t.Countable ∧ s ⊆ ⋃ x ∈ t, closedBall x ε
x₀ : α
hx₀ : x₀ ∈ s
T : ℕ → Set α
hTc : ∀ (n : ℕ), (T n).Countable
hsT : ∀ (n : ℕ), s ⊆ ⋃ x ∈ T n, closedBall x (↑n)⁻¹
⊢ ∃ t ⊆ s, t.Countable ∧ s ⊆ closure t

Proof state:
case inr.intro.intro.intro.intro
α : Type u
inst✝ : PseudoEMetricSpace α
s : Set α
hs : ∀ ε > 0, ∃ t, t.Countable ∧ s ⊆ ⋃ x ∈ t, closedBall x ε
x₀ : α
hx₀ : x₀ ∈ s
T : ℕ → Set α
hTc : ∀ (n : ℕ), (T n).Countable
hsT : ∀ (n : ℕ), s ⊆ ⋃ x ∈ T n, closedBall x (↑n)⁻¹
f : ℝ≥0∞ → α → α
hfs : ∀ (r : ℝ≥0∞) (x : α), f r x ∈ s
hf : ∀ (r : ℝ≥0∞) (x : α), closedBall x r ∩ s ⊆ closedBall (f r x) (r * 2)
x : α
hx : x ∈ s
ε : ℝ≥0∞
ε0 : ε > 0
n : ℕ
hn : (↑n)⁻¹ < ε / 2
y : α
hyn : y ∈ T n
hyx : x ∈ closedBall y (↑n)⁻¹
⊢ ∃ y ∈ ⋃ n, f (↑n)⁻¹ '' T n, edist x y < ε

Tactic:
refine ⟨f n⁻¹ y, mem_iUnion.2 ⟨n, mem_image_of_mem _ hyn⟩, ?_⟩

Result:
case inr.intro.intro.intro.intro
α : Type u
inst✝ : PseudoEMetricSpace α
s : Set α
hs : ∀ ε > 0, ∃ t, t.Countable ∧ s ⊆ ⋃ x ∈ t, closedBall x ε
x₀ : α
hx₀ : x₀ ∈ s
T : ℕ → Set α
hTc : ∀ (n : ℕ), (T n).Countable
hsT : ∀ (n : ℕ), s ⊆ ⋃ x ∈ T n, closedBall x (↑n)⁻¹
f : ℝ≥0∞ → α → α
hfs : ∀ (r : ℝ≥0∞) (x : α), f r x ∈ s
hf : ∀ (r : ℝ≥0∞) (x : α), closedBall x r ∩ s ⊆ closedBall (f r x) (r * 2)
x : α
hx : x ∈ s
ε : ℝ≥0∞
ε0 : ε > 0
n : ℕ
hn : (↑n)⁻¹ < ε / 2
y : α
hyn : y ∈ T n
hyx : x ∈ closedBall y (↑n)⁻¹
⊢ edist x (f (↑n)⁻¹ y) < ε

Proof state:
case inl
α : Type u
inst✝ : PseudoEMetricSpace α
s : Set α
hs : ∀ ε > 0, ∃ t, t.Countable ∧ s ⊆ ⋃ x ∈ t, closedBall x ε
x₀ : α
hx₀ : x₀ ∈ s
T : ℕ → Set α
hTc : ∀ (n : ℕ), (T n).Countable
hsT : ∀ (n : ℕ), s ⊆ ⋃ x ∈ T n, closedBall x (↑n)⁻¹
r : ℝ≥0∞
x : α
he : closedBall x r ∩ s = ∅
⊢ ∃ y ∈ s, closedBall x r ∩ s ⊆ closedBall y (r * 2)

Tactic:
refine ⟨x₀, hx₀, ?_⟩

Result:
case inl
α : Type u
inst✝ : PseudoEMetricSpace α
s : Set α
hs : ∀ ε > 0, ∃ t, t.Countable ∧ s ⊆ ⋃ x ∈ t, closedBall x ε
x₀ : α
hx₀ : x₀ ∈ s
T : ℕ → Set α
hTc : ∀ (n : ℕ), (T n).Countable
hsT : ∀ (n : ℕ), s ⊆ ⋃ x ∈ T n, closedBall x (↑n)⁻¹
r : ℝ≥0∞
x : α
he : closedBall x r ∩ s = ∅
⊢ closedBall x r ∩ s ⊆ closedBall x₀ (r * 2)

Proof state:
case inr.intro.intro.intro.intro
α : Type u
inst✝ : PseudoEMetricSpace α
s : Set α
hs : ∀ ε > 0, ∃ t, t.Countable ∧ s ⊆ ⋃ x ∈ t, closedBall x ε
x₀ : α
hx₀ : x₀ ∈ s
T : ℕ → Set α
hTc : ∀ (n : ℕ), (T n).Countable
hsT : ∀ (n : ℕ), s ⊆ ⋃ x ∈ T n, closedBall x (↑n)⁻¹
f : ℝ≥0∞ → α → α
hfs : ∀ (r : ℝ≥0∞) (x : α), f r x ∈ s
hf : ∀ (r : ℝ≥0∞) (x : α), closedBall x r ∩ s ⊆ closedBall (f r x) (r * 2)
x : α
hx : x ∈ s
ε : ℝ≥0∞
ε0 : ε > 0
n : ℕ
hn : (↑n)⁻¹ < ε / 2
y : α
hyn : y ∈ T n
hyx : x ∈ closedBall y (↑n)⁻¹
⊢ edist x (f (↑n)⁻¹ y) < ε

Tactic:
calc
  edist x (f n⁻¹ y) ≤ (n : ℝ≥0∞)⁻¹ * 2 := hf _ _ ⟨hyx, hx⟩
  _ < ε := ENNReal.mul_lt_of_lt_div hn

Result:
no goals

Proof state:
case inl
α : Type u
inst✝ : PseudoEMetricSpace α
s : Set α
hs : ∀ ε > 0, ∃ t, t.Countable ∧ s ⊆ ⋃ x ∈ t, closedBall x ε
x₀ : α
hx₀ : x₀ ∈ s
T : ℕ → Set α
hTc : ∀ (n : ℕ), (T n).Countable
hsT : ∀ (n : ℕ), s ⊆ ⋃ x ∈ T n, closedBall x (↑n)⁻¹
r : ℝ≥0∞
x : α
he : closedBall x r ∩ s = ∅
⊢ ∅ ⊆ closedBall x₀ (r * 2)

Tactic:
exact empty_subset _

Result:
no goals

Proof state:
α : Type u
inst✝ : PseudoEMetricSpace α
s : Set α
hs : ∀ ε > 0, ∃ t, t.Countable ∧ s ⊆ ⋃ x ∈ t, closedBall x ε
⊢ ∃ t ⊆ s, t.Countable ∧ s ⊆ closure t

Tactic:
rcases s.eq_empty_or_nonempty with (rfl | ⟨x₀, hx₀⟩)

Result:
case inl
α : Type u
inst✝ : PseudoEMetricSpace α
hs : ∀ ε > 0, ∃ t, t.Countable ∧ ∅ ⊆ ⋃ x ∈ t, closedBall x ε
⊢ ∃ t ⊆ ∅, t.Countable ∧ ∅ ⊆ closure t

case inr.intro
α : Type u
inst✝ : PseudoEMetricSpace α
s : Set α
hs : ∀ ε > 0, ∃ t, t.Countable ∧ s ⊆ ⋃ x ∈ t, closedBall x ε
x₀ : α
hx₀ : x₀ ∈ s
⊢ ∃ t ⊆ s, t.Countable ∧ s ⊆ closure t

Proof state:
case inr.intro
α : Type u
inst✝ : PseudoEMetricSpace α
s : Set α
hs : ∀ ε > 0, ∃ t, t.Countable ∧ s ⊆ ⋃ x ∈ t, closedBall x ε
x₀ : α
hx₀ : x₀ ∈ s
T : ℕ → Set α
hTc : ∀ (n : ℕ), (T n).Countable
hsT : ∀ (n : ℕ), s ⊆ ⋃ x ∈ T n, closedBall x (↑n)⁻¹
this : ∀ (r : ℝ≥0∞) (x : α), ∃ y ∈ s, closedBall x r ∩ s ⊆ closedBall y (r * 2)
⊢ ∃ t ⊆ s, t.Countable ∧ s ⊆ closure t

Tactic:
choose f hfs hf using this

Result:
case inr.intro
α : Type u
inst✝ : PseudoEMetricSpace α
s : Set α
hs : ∀ ε > 0, ∃ t, t.Countable ∧ s ⊆ ⋃ x ∈ t, closedBall x ε
x₀ : α
hx₀ : x₀ ∈ s
T : ℕ → Set α
hTc : ∀ (n : ℕ), (T n).Countable
hsT : ∀ (n : ℕ), s ⊆ ⋃ x ∈ T n, closedBall x (↑n)⁻¹
f : ℝ≥0∞ → α → α
hfs : ∀ (r : ℝ≥0∞) (x : α), f r x ∈ s
hf : ∀ (r : ℝ≥0∞) (x : α), closedBall x r ∩ s ⊆ closedBall (f r x) (r * 2)
⊢ ∃ t ⊆ s, t.Countable ∧ s ⊆ closure t

Proof state:
case inr.intro.intro
α : Type u
inst✝ : PseudoEMetricSpace α
s : Set α
hs : ∀ ε > 0, ∃ t, t.Countable ∧ s ⊆ ⋃ x ∈ t, closedBall x ε
x₀ : α
hx₀ : x₀ ∈ s
T : ℕ → Set α
hTc : ∀ (n : ℕ), (T n).Countable
hsT : ∀ (n : ℕ), s ⊆ ⋃ x ∈ T n, closedBall x (↑n)⁻¹
f : ℝ≥0∞ → α → α
hfs : ∀ (r : ℝ≥0∞) (x : α), f r x ∈ s
hf : ∀ (r : ℝ≥0∞) (x : α), closedBall x r ∩ s ⊆ closedBall (f r x) (r * 2)
x : α
hx : x ∈ s
ε : ℝ≥0∞
ε0 : ε > 0
n : ℕ
hn : (↑n)⁻¹ < ε / 2
⊢ ∃ y ∈ ⋃ n, f (↑n)⁻¹ '' T n, edist x y < ε

Tactic:
rcases mem_iUnion₂.1 (hsT n hx) with ⟨y, hyn, hyx⟩

Result:
case inr.intro.intro.intro.intro
α : Type u
inst✝ : PseudoEMetricSpace α
s : Set α
hs : ∀ ε > 0, ∃ t, t.Countable ∧ s ⊆ ⋃ x ∈ t, closedBall x ε
x₀ : α
hx₀ : x₀ ∈ s
T : ℕ → Set α
hTc : ∀ (n : ℕ), (T n).Countable
hsT : ∀ (n : ℕ), s ⊆ ⋃ x ∈ T n, closedBall x (↑n)⁻¹
f : ℝ≥0∞ → α → α
hfs : ∀ (r : ℝ≥0∞) (x : α), f r x ∈ s
hf : ∀ (r : ℝ≥0∞) (x : α), closedBall x r ∩ s ⊆ closedBall (f r x) (r * 2)
x : α
hx : x ∈ s
ε : ℝ≥0∞
ε0 : ε > 0
n : ℕ
hn : (↑n)⁻¹ < ε / 2
y : α
hyn : y ∈ T n
hyx : x ∈ closedBall y (↑n)⁻¹
⊢ ∃ y ∈ ⋃ n, f (↑n)⁻¹ '' T n, edist x y < ε

Proof state:
case inr.intro.intro
α : Type u
inst✝ : PseudoEMetricSpace α
s : Set α
hs : ∀ ε > 0, ∃ t, t.Countable ∧ s ⊆ ⋃ x ∈ t, closedBall x ε
x₀ : α
hx₀ : x₀ ∈ s
T : ℕ → Set α
hTc : ∀ (n : ℕ), (T n).Countable
hsT : ∀ (n : ℕ), s ⊆ ⋃ x ∈ T n, closedBall x (↑n)⁻¹
r : ℝ≥0∞
x y : α
hxy : y ∈ closedBall x r
hys : y ∈ s
z : α
hz : z ∈ closedBall x r ∩ s
⊢ z ∈ closedBall y (r * 2)

Tactic:
calc
  edist z y ≤ edist z x + edist y x := edist_triangle_right _ _ _
  _ ≤ r + r := add_le_add hz.1 hxy
  _ = r * 2 := (mul_two r).symm

Result:
no goals