no goals
α : Type u_1
β : Type ?u.307608
γ : Type ?u.307611
δ : Type ?u.307614
ι : Type ?u.307617
R : Type ?u.307620
R' : Type ?u.307623
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s s' t : Set α
hs : s ⊆ t
h : restrict μ t = restrict ν t
⊢ restrict μ s = restrict ν s
rw [← restrict_restrict_of_subset hs, h, restrict_restrict_of_subset hs]