α : Type u_2
β : Type ?u.314892
γ : Type ?u.314895
δ : Type ?u.314898
ι : Type u_1
R : Type ?u.314904
R' : Type ?u.314907
m0 : MeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s✝ s' t : Set α
inst✝ : Countable ι
s : ι → Set α
h : ∀ (i : ι), restrict μ (s i) = restrict ν (s i)
⊢ restrict μ (⋃ (i : ι), s i) = restrict ν (⋃ (i : ι), s i)
α : Type u_2
β : Type ?u.314892
γ : Type ?u.314895
δ : Type ?u.314898
ι : Type u_1
R : Type ?u.314904
R' : Type ?u.314907
m0 : MeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s✝ s' t : Set α
inst✝ : Countable ι
s : ι → Set α
⊢ restrict μ (⋃ (i : ι), s i) = restrict ν (⋃ (i : ι), s i) ↔ ∀ (i : ι), restrict μ (s i) = restrict ν (s i)
refine' ⟨fun h i => restrict_congr_mono (subset_iUnion _ _) h, fun h => _⟩
case h
α : Type u_2
β : Type ?u.314892
γ : Type ?u.314895
δ : Type ?u.314898
ι : Type u_1
R : Type ?u.314904
R' : Type ?u.314907
m0 : MeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s✝ s' t✝ : Set α
inst✝ : Countable ι
s : ι → Set α
h : ∀ (i : ι), restrict μ (s i) = restrict ν (s i)
t : Set α
ht : MeasurableSet t
⊢ ↑↑(restrict μ (⋃ (i : ι), s i)) t = ↑↑(restrict ν (⋃ (i : ι), s i)) t
α : Type u_2
β : Type ?u.314892
γ : Type ?u.314895
δ : Type ?u.314898
ι : Type u_1
R : Type ?u.314904
R' : Type ?u.314907
m0 : MeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s✝ s' t : Set α
inst✝ : Countable ι
s : ι → Set α
h : ∀ (i : ι), restrict μ (s i) = restrict ν (s i)
⊢ restrict μ (⋃ (i : ι), s i) = restrict ν (⋃ (i : ι), s i)
ext1 t ht
case h
α : Type u_2
β : Type ?u.314892
γ : Type ?u.314895
δ : Type ?u.314898
ι : Type u_1
R : Type ?u.314904
R' : Type ?u.314907
m0 : MeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s✝ s' t✝ : Set α
inst✝ : Countable ι
s : ι → Set α
h : ∀ (i : ι), restrict μ (s i) = restrict ν (s i)
t : Set α
ht : MeasurableSet t
D : Directed (fun x x_1 => x ⊆ x_1) fun t => ⋃ (i : ι) (_ : i ∈ t), s i
⊢ ↑↑(restrict μ (⋃ (t : Finset ι) (i : ι) (_ : i ∈ t), s i)) t =
    ↑↑(restrict ν (⋃ (t : Finset ι) (i : ι) (_ : i ∈ t), s i)) t
case h
α : Type u_2
β : Type ?u.314892
γ : Type ?u.314895
δ : Type ?u.314898
ι : Type u_1
R : Type ?u.314904
R' : Type ?u.314907
m0 : MeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s✝ s' t✝ : Set α
inst✝ : Countable ι
s : ι → Set α
h : ∀ (i : ι), restrict μ (s i) = restrict ν (s i)
t : Set α
ht : MeasurableSet t
D : Directed (fun x x_1 => x ⊆ x_1) fun t => ⋃ (i : ι) (_ : i ∈ t), s i
⊢ ↑↑(restrict μ (⋃ (i : ι), s i)) t = ↑↑(restrict ν (⋃ (i : ι), s i)) t
rw [iUnion_eq_iUnion_finset]
no goals
case h
α : Type u_2
β : Type ?u.314892
γ : Type ?u.314895
δ : Type ?u.314898
ι : Type u_1
R : Type ?u.314904
R' : Type ?u.314907
m0 : MeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s✝ s' t✝ : Set α
inst✝ : Countable ι
s : ι → Set α
h : ∀ (i : ι), restrict μ (s i) = restrict ν (s i)
t : Set α
ht : MeasurableSet t
D : Directed (fun x x_1 => x ⊆ x_1) fun t => ⋃ (i : ι) (_ : i ∈ t), s i
⊢ ↑↑(restrict μ (⋃ (t : Finset ι) (i : ι) (_ : i ∈ t), s i)) t =
    ↑↑(restrict ν (⋃ (t : Finset ι) (i : ι) (_ : i ∈ t), s i)) t
simp only [restrict_iUnion_apply_eq_iSup D ht, restrict_finset_biUnion_congr.2 fun i _ => h i]