α : Type u_2
β : Type ?u.316219
γ : Type ?u.316222
δ : Type ?u.316225
ι : Type u_1
R : Type ?u.316231
R' : Type ?u.316234
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s✝ s' t✝ : Set α
s : Set ι
t : ι → Set α
hc : Set.Countable s
this : Encodable ↑s
⊢ restrict μ (⋃ (i : ι) (_ : i ∈ s), t i) = restrict ν (⋃ (i : ι) (_ : i ∈ s), t i) ↔
    ∀ (i : ι), i ∈ s → restrict μ (t i) = restrict ν (t i)
α : Type u_2
β : Type ?u.316219
γ : Type ?u.316222
δ : Type ?u.316225
ι : Type u_1
R : Type ?u.316231
R' : Type ?u.316234
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s✝ s' t✝ : Set α
s : Set ι
t : ι → Set α
hc : Set.Countable s
⊢ restrict μ (⋃ (i : ι) (_ : i ∈ s), t i) = restrict ν (⋃ (i : ι) (_ : i ∈ s), t i) ↔
    ∀ (i : ι), i ∈ s → restrict μ (t i) = restrict ν (t i)
haveI := hc.toEncodable
no goals
α : Type u_2
β : Type ?u.316219
γ : Type ?u.316222
δ : Type ?u.316225
ι : Type u_1
R : Type ?u.316231
R' : Type ?u.316234
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s✝ s' t✝ : Set α
s : Set ι
t : ι → Set α
hc : Set.Countable s
this : Encodable ↑s
⊢ restrict μ (⋃ (i : ι) (_ : i ∈ s), t i) = restrict ν (⋃ (i : ι) (_ : i ∈ s), t i) ↔
    ∀ (i : ι), i ∈ s → restrict μ (t i) = restrict ν (t i)
simp only [biUnion_eq_iUnion, SetCoe.forall', restrict_iUnion_congr]