no goals
α : Type u_2
β : Type ?u.319831
γ : Type ?u.319834
δ : Type ?u.319837
ι : Type u_1
R : Type ?u.319843
R' : Type ?u.319846
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s✝ s' t : Set α
S : Set ι
s : ι → Set α
hc : Set.Countable S
hs : (⋃ (i : ι) (_ : i ∈ S), s i) = univ
⊢ μ = ν ↔ ∀ (i : ι), i ∈ S → restrict μ (s i) = restrict ν (s i)
rw [← restrict_biUnion_congr hc, hs, restrict_univ, restrict_univ]