α : Type u_1
β : Type u_2
γ : Type ?u.93120
δ : Type ?u.93123
δ' : Type ?u.93126
ι : Sort uι
s✝ t✝ u : Set α
m : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝ : Countable ι
t : ι → Set α
htm : ∀ (i : ι), MeasurableSet (t i)
f : (i : ι) → ↑(t i) → β
hfm : ∀ (i : ι), Measurable (f i)
hf :
  ∀ (i j : ι) (x : α) (hxi : x ∈ t i) (hxj : x ∈ t j),
    f i { val := x, property := hxi } = f j { val := x, property := hxj }
htU : (⋃ (i : ι), t i) = univ
s : Set β
hs : MeasurableSet s
⊢ MeasurableSet (⋃ (i : ι), Subtype.val '' (f i ⁻¹' s))
α : Type u_1
β : Type u_2
γ : Type ?u.93120
δ : Type ?u.93123
δ' : Type ?u.93126
ι : Sort uι
s✝ t✝ u : Set α
m : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝ : Countable ι
t : ι → Set α
htm : ∀ (i : ι), MeasurableSet (t i)
f : (i : ι) → ↑(t i) → β
hfm : ∀ (i : ι), Measurable (f i)
hf :
  ∀ (i j : ι) (x : α) (hxi : x ∈ t i) (hxj : x ∈ t j),
    f i { val := x, property := hxi } = f j { val := x, property := hxj }
htU : (⋃ (i : ι), t i) = univ
s : Set β
hs : MeasurableSet s
⊢ MeasurableSet (liftCover t f hf htU ⁻¹' s)
rw [preimage_liftCover]
no goals
α : Type u_1
β : Type u_2
γ : Type ?u.93120
δ : Type ?u.93123
δ' : Type ?u.93126
ι : Sort uι
s✝ t✝ u : Set α
m : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝ : Countable ι
t : ι → Set α
htm : ∀ (i : ι), MeasurableSet (t i)
f : (i : ι) → ↑(t i) → β
hfm : ∀ (i : ι), Measurable (f i)
hf :
  ∀ (i j : ι) (x : α) (hxi : x ∈ t i) (hxj : x ∈ t j),
    f i { val := x, property := hxi } = f j { val := x, property := hxj }
htU : (⋃ (i : ι), t i) = univ
s : Set β
hs : MeasurableSet s
⊢ MeasurableSet (⋃ (i : ι), Subtype.val '' (f i ⁻¹' s))
exact .iUnion fun i => .subtype_image (htm i) <| hfm i hs