no goals
α : Type u_2
β : Type ?u.837525
γ : Type ?u.837528
δ : Type u_1
ι : Type ?u.837534
R : Type ?u.837537
R' : Type ?u.837540
m0 : MeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s s' t : Set α
inst✝ : PseudoMetricSpace δ
f : α → δ
x : δ
hμ : μ ≠ 0
⊢ (⋃ (i : ℕ), f ⁻¹' Metric.ball x ↑i) = univ
rw [← preimage_iUnion, Metric.iUnion_ball_nat, preimage_univ]