no goals
α : Type u_1
β : Type u_2
γ : Type ?u.798298
δ : Type ?u.798301
ι : Type ?u.798304
R : Type ?u.798307
R' : Type ?u.798310
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ✝ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s s' t : Set α
μ : Measure α
f : α → β
hf : AEMeasurable f
h : SigmaFinite (Measure.map f μ)
n : ℕ
⊢ ↑↑μ ((fun n => f ⁻¹' spanningSets (Measure.map f μ) n) n) < ⊤
simp only [← map_apply_of_aemeasurable hf, measurable_spanningSets,
  measure_spanningSets_lt_top]
no goals
α : Type u_1
β : Type u_2
γ : Type ?u.798298
δ : Type ?u.798301
ι : Type ?u.798304
R : Type ?u.798307
R' : Type ?u.798310
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ✝ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s s' t : Set α
μ : Measure α
f : α → β
hf : AEMeasurable f
h : SigmaFinite (Measure.map f μ)
⊢ (⋃ (i : ℕ), (fun n => f ⁻¹' spanningSets (Measure.map f μ) n) i) = univ
rw [← preimage_iUnion, iUnion_spanningSets, preimage_univ]