-- Mathlib/MeasureTheory/Function/StronglyMeasurable/Basic.lean
theorem isSeparable_range {m : MeasurableSpace α} [TopologicalSpace β]
    (hf : StronglyMeasurable f) : TopologicalSpace.IsSeparable (range f)

Proof state:
case intro.h
α : Type u_1
β : Type u_2
f : α → β
m : MeasurableSpace α
inst✝ : TopologicalSpace β
hf : StronglyMeasurable f
this : IsSeparable (closure (⋃ n, range ⇑(hf.approx n)))
x : α
n : ℕ
⊢ (hf.approx n) x ∈ ⋃ n, range ⇑(hf.approx n)

Tactic:
apply mem_iUnion_of_mem n

Result:
case intro.h
α : Type u_1
β : Type u_2
f : α → β
m : MeasurableSpace α
inst✝ : TopologicalSpace β
hf : StronglyMeasurable f
this : IsSeparable (closure (⋃ n, range ⇑(hf.approx n)))
x : α
n : ℕ
⊢ (hf.approx n) x ∈ range ⇑(hf.approx n)

Proof state:
α : Type u_1
β : Type u_2
f : α → β
m : MeasurableSpace α
inst✝ : TopologicalSpace β
hf : StronglyMeasurable f
⊢ IsSeparable (range f)

Tactic:
have : IsSeparable (closure (⋃ n, range (hf.approx n))) :=
  .closure <| .iUnion fun n => (hf.approx n).finite_range.isSeparable

Result:
α : Type u_1
β : Type u_2
f : α → β
m : MeasurableSpace α
inst✝ : TopologicalSpace β
hf : StronglyMeasurable f
this : IsSeparable (closure (⋃ n, range ⇑(hf.approx n)))
⊢ IsSeparable (range f)

Proof state:
α : Type u_1
β : Type u_2
f : α → β
m : MeasurableSpace α
inst✝ : TopologicalSpace β
hf : StronglyMeasurable f
this : IsSeparable (closure (⋃ n, range ⇑(hf.approx n)))
⊢ IsSeparable (range f)

Tactic:
apply this.mono

Result:
α : Type u_1
β : Type u_2
f : α → β
m : MeasurableSpace α
inst✝ : TopologicalSpace β
hf : StronglyMeasurable f
this : IsSeparable (closure (⋃ n, range ⇑(hf.approx n)))
⊢ range f ⊆ closure (⋃ n, range ⇑(hf.approx n))

Proof state:
case intro.h
α : Type u_1
β : Type u_2
f : α → β
m : MeasurableSpace α
inst✝ : TopologicalSpace β
hf : StronglyMeasurable f
this : IsSeparable (closure (⋃ n, range ⇑(hf.approx n)))
x : α
n : ℕ
⊢ (hf.approx n) x ∈ range ⇑(hf.approx n)

Tactic:
exact mem_range_self _

Result:
no goals

Proof state:
case intro
α : Type u_1
β : Type u_2
f : α → β
m : MeasurableSpace α
inst✝ : TopologicalSpace β
hf : StronglyMeasurable f
this : IsSeparable (closure (⋃ n, range ⇑(hf.approx n)))
x : α
⊢ f x ∈ closure (⋃ n, range ⇑(hf.approx n))

Tactic:
apply mem_closure_of_tendsto (hf.tendsto_approx x)

Result:
case intro
α : Type u_1
β : Type u_2
f : α → β
m : MeasurableSpace α
inst✝ : TopologicalSpace β
hf : StronglyMeasurable f
this : IsSeparable (closure (⋃ n, range ⇑(hf.approx n)))
x : α
⊢ ∀ᶠ (x_1 : ℕ) in atTop, (hf.approx x_1) x ∈ ⋃ n, range ⇑(hf.approx n)

Proof state:
case intro
α : Type u_1
β : Type u_2
f : α → β
m : MeasurableSpace α
inst✝ : TopologicalSpace β
hf : StronglyMeasurable f
this : IsSeparable (closure (⋃ n, range ⇑(hf.approx n)))
x : α
⊢ ∀ᶠ (x_1 : ℕ) in atTop, (hf.approx x_1) x ∈ ⋃ n, range ⇑(hf.approx n)

Tactic:
filter_upwards with n

Result:
case intro.h
α : Type u_1
β : Type u_2
f : α → β
m : MeasurableSpace α
inst✝ : TopologicalSpace β
hf : StronglyMeasurable f
this : IsSeparable (closure (⋃ n, range ⇑(hf.approx n)))
x : α
n : ℕ
⊢ (hf.approx n) x ∈ ⋃ n, range ⇑(hf.approx n)

Proof state:
α : Type u_1
β : Type u_2
f : α → β
m : MeasurableSpace α
inst✝ : TopologicalSpace β
hf : StronglyMeasurable f
this : IsSeparable (closure (⋃ n, range ⇑(hf.approx n)))
⊢ range f ⊆ closure (⋃ n, range ⇑(hf.approx n))

Tactic:
rintro _ ⟨x, rfl⟩

Result:
case intro
α : Type u_1
β : Type u_2
f : α → β
m : MeasurableSpace α
inst✝ : TopologicalSpace β
hf : StronglyMeasurable f
this : IsSeparable (closure (⋃ n, range ⇑(hf.approx n)))
x : α
⊢ f x ∈ closure (⋃ n, range ⇑(hf.approx n))