no goals
α : Type u_1
β : Type ?u.317105
γ : Type ?u.317108
δ : Type ?u.317111
ι : Type ?u.317114
R : Type ?u.317117
R' : Type ?u.317120
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s s' t : Set α
S : Set (Set α)
hc : Set.Countable S
⊢ restrict μ (⋃₀ S) = restrict ν (⋃₀ S) ↔ ∀ (s : Set α), s ∈ S → restrict μ s = restrict ν s
rw [sUnion_eq_biUnion, restrict_biUnion_congr hc]