case h
α : Type u_1
β : Type ?u.290160
γ : Type ?u.290163
δ : Type ?u.290166
ι : Type ?u.290169
R : Type ?u.290172
R' : Type ?u.290175
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s s' t : Set α
h : s ⊆ t
u : Set α
hu : MeasurableSet u
⊢ ↑↑(restrict (restrict μ t) s) u = ↑↑(restrict μ s) u
α : Type u_1
β : Type ?u.290160
γ : Type ?u.290163
δ : Type ?u.290166
ι : Type ?u.290169
R : Type ?u.290172
R' : Type ?u.290175
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s s' t : Set α
h : s ⊆ t
⊢ restrict (restrict μ t) s = restrict μ s
ext1 u hu
case h.h
α : Type u_1
β : Type ?u.290160
γ : Type ?u.290163
δ : Type ?u.290166
ι : Type ?u.290169
R : Type ?u.290172
R' : Type ?u.290175
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s s' t : Set α
h : s ⊆ t
u : Set α
hu : MeasurableSet u
⊢ u ∩ s ⊆ t
case h
α : Type u_1
β : Type ?u.290160
γ : Type ?u.290163
δ : Type ?u.290166
ι : Type ?u.290169
R : Type ?u.290172
R' : Type ?u.290175
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s s' t : Set α
h : s ⊆ t
u : Set α
hu : MeasurableSet u
⊢ ↑↑(restrict (restrict μ t) s) u = ↑↑(restrict μ s) u
rw [restrict_apply hu, restrict_apply hu, restrict_eq_self]
no goals
case h.h
α : Type u_1
β : Type ?u.290160
γ : Type ?u.290163
δ : Type ?u.290166
ι : Type ?u.290169
R : Type ?u.290172
R' : Type ?u.290175
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s s' t : Set α
h : s ⊆ t
u : Set α
hu : MeasurableSet u
⊢ u ∩ s ⊆ t
exact (inter_subset_right _ _).trans h