no goals
α : Type u_1
β : Type ?u.307127
γ : Type ?u.307130
δ : Type ?u.307133
ι : Type ?u.307136
R : Type ?u.307139
R' : Type ?u.307142
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s s' t✝ : Set α
hs : MeasurableSet s
H : restrict μ s = restrict ν s
t : Set α
hts : t ⊆ s
ht : MeasurableSet t
⊢ ↑↑μ t = ↑↑ν t
rw [← inter_eq_self_of_subset_left hts, ← restrict_apply ht, H, restrict_apply ht]
no goals
α : Type u_1
β : Type ?u.307127
γ : Type ?u.307130
δ : Type ?u.307133
ι : Type ?u.307136
R : Type ?u.307139
R' : Type ?u.307142
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s s' t✝ : Set α
hs : MeasurableSet s
H : ∀ (t : Set α), t ⊆ s → MeasurableSet t → ↑↑μ t = ↑↑ν t
t : Set α
ht : MeasurableSet t
⊢ ↑↑(restrict μ s) t = ↑↑(restrict ν s) t
rw [restrict_apply ht, restrict_apply ht, H _ (inter_subset_right _ _) (ht.inter hs)]