case intro.intro
α : Type u_1
β : Type ?u.62091
γ : Type ?u.62094
δ : Type ?u.62097
δ' : Type ?u.62100
ι : Sort uι
s✝ t✝ u✝ : Set α
m : MeasurableSpace α
mβ : MeasurableSpace β
s t : Set α
h : s ⊆ t
hs : MeasurableSet (Subtype.val ⁻¹' s)
u : Set α
hu : MeasurableSet u
⊢ MeasurableSet (inclusion h '' (Subtype.val ⁻¹' u))
α : Type u_1
β : Type ?u.62091
γ : Type ?u.62094
δ : Type ?u.62097
δ' : Type ?u.62100
ι : Sort uι
s✝ t✝ u✝ : Set α
m : MeasurableSpace α
mβ : MeasurableSpace β
s t : Set α
h : s ⊆ t
u : Set ↑s
hs : MeasurableSet (Subtype.val ⁻¹' s)
hu : MeasurableSet u
⊢ MeasurableSet (inclusion h '' u)
rcases hu with ⟨u, hu, rfl⟩
case h.e'_3
α : Type u_1
β : Type ?u.62091
γ : Type ?u.62094
δ : Type ?u.62097
δ' : Type ?u.62100
ι : Sort uι
s✝ t✝ u✝ : Set α
m : MeasurableSpace α
mβ : MeasurableSpace β
s t : Set α
h : s ⊆ t
hs : MeasurableSet (Subtype.val ⁻¹' s)
u : Set α
hu : MeasurableSet u
⊢ inclusion h '' (Subtype.val ⁻¹' u) = Subtype.val ⁻¹' u ∩ Subtype.val ⁻¹' s
case intro.intro
α : Type u_1
β : Type ?u.62091
γ : Type ?u.62094
δ : Type ?u.62097
δ' : Type ?u.62100
ι : Sort uι
s✝ t✝ u✝ : Set α
m : MeasurableSpace α
mβ : MeasurableSpace β
s t : Set α
h : s ⊆ t
hs : MeasurableSet (Subtype.val ⁻¹' s)
u : Set α
hu : MeasurableSet u
⊢ MeasurableSet (inclusion h '' (Subtype.val ⁻¹' u))
convert (measurable_subtype_coe hu).inter hs
case h.e'_3.h.mk
α : Type u_1
β : Type ?u.62091
γ : Type ?u.62094
δ : Type ?u.62097
δ' : Type ?u.62100
ι : Sort uι
s✝ t✝ u✝ : Set α
m : MeasurableSpace α
mβ : MeasurableSpace β
s t : Set α
h : s ⊆ t
hs : MeasurableSet (Subtype.val ⁻¹' s)
u : Set α
hu : MeasurableSet u
x : α
hx : x ∈ t
⊢ { val := x, property := hx } ∈ inclusion h '' (Subtype.val ⁻¹' u) ↔
    { val := x, property := hx } ∈ Subtype.val ⁻¹' u ∩ Subtype.val ⁻¹' s
case h.e'_3
α : Type u_1
β : Type ?u.62091
γ : Type ?u.62094
δ : Type ?u.62097
δ' : Type ?u.62100
ι : Sort uι
s✝ t✝ u✝ : Set α
m : MeasurableSpace α
mβ : MeasurableSpace β
s t : Set α
h : s ⊆ t
hs : MeasurableSet (Subtype.val ⁻¹' s)
u : Set α
hu : MeasurableSet u
⊢ inclusion h '' (Subtype.val ⁻¹' u) = Subtype.val ⁻¹' u ∩ Subtype.val ⁻¹' s
ext ⟨x, hx⟩
no goals
case h.e'_3.h.mk
α : Type u_1
β : Type ?u.62091
γ : Type ?u.62094
δ : Type ?u.62097
δ' : Type ?u.62100
ι : Sort uι
s✝ t✝ u✝ : Set α
m : MeasurableSpace α
mβ : MeasurableSpace β
s t : Set α
h : s ⊆ t
hs : MeasurableSet (Subtype.val ⁻¹' s)
u : Set α
hu : MeasurableSet u
x : α
hx : x ∈ t
⊢ { val := x, property := hx } ∈ inclusion h '' (Subtype.val ⁻¹' u) ↔
    { val := x, property := hx } ∈ Subtype.val ⁻¹' u ∩ Subtype.val ⁻¹' s
simpa [@and_comm _ (_ = x)] using and_comm