α✝ : Type ?u.846775
β : Type ?u.846778
γ : Type ?u.846781
δ : Type ?u.846784
ι : Type ?u.846787
R : Type ?u.846790
R' : Type ?u.846793
m0 : MeasurableSpace α✝
inst✝² : MeasurableSpace β
inst✝¹ : MeasurableSpace γ
μ✝ μ₁ μ₂ μ₃ ν✝ ν' ν₁ ν₂ : Measure α✝
s✝ s' t : Set α✝
α : Type u_1
m₀ : MeasurableSpace α
μ ν : Measure α
inst✝ : IsFiniteMeasure μ
C : Set (Set α)
hμν : ∀ (s : Set α), s ∈ C → ↑↑μ s = ↑↑ν s
m : MeasurableSpace α
h : m ≤ m₀
hA : m = generateFrom C
hC : IsPiSystem C
h_univ : ↑↑μ univ = ↑↑ν univ
s : Set α
hs : MeasurableSet s
this : IsFiniteMeasure ν
⊢ ↑↑μ s = ↑↑ν s
α✝ : Type ?u.846775
β : Type ?u.846778
γ : Type ?u.846781
δ : Type ?u.846784
ι : Type ?u.846787
R : Type ?u.846790
R' : Type ?u.846793
m0 : MeasurableSpace α✝
inst✝² : MeasurableSpace β
inst✝¹ : MeasurableSpace γ
μ✝ μ₁ μ₂ μ₃ ν✝ ν' ν₁ ν₂ : Measure α✝
s✝ s' t : Set α✝
α : Type u_1
m₀ : MeasurableSpace α
μ ν : Measure α
inst✝ : IsFiniteMeasure μ
C : Set (Set α)
hμν : ∀ (s : Set α), s ∈ C → ↑↑μ s = ↑↑ν s
m : MeasurableSpace α
h : m ≤ m₀
hA : m = generateFrom C
hC : IsPiSystem C
h_univ : ↑↑μ univ = ↑↑ν univ
s : Set α
hs : MeasurableSet s
⊢ ↑↑μ s = ↑↑ν s
haveI : IsFiniteMeasure ν := by
  constructor
  rw [← h_univ]
  apply IsFiniteMeasure.measure_univ_lt_top
case refine'_1
α✝ : Type ?u.846775
β : Type ?u.846778
γ : Type ?u.846781
δ : Type ?u.846784
ι : Type ?u.846787
R : Type ?u.846790
R' : Type ?u.846793
m0 : MeasurableSpace α✝
inst✝² : MeasurableSpace β
inst✝¹ : MeasurableSpace γ
μ✝ μ₁ μ₂ μ₃ ν✝ ν' ν₁ ν₂ : Measure α✝
s✝ s' t : Set α✝
α : Type u_1
m₀ : MeasurableSpace α
μ ν : Measure α
inst✝ : IsFiniteMeasure μ
C : Set (Set α)
hμν : ∀ (s : Set α), s ∈ C → ↑↑μ s = ↑↑ν s
m : MeasurableSpace α
h : m ≤ m₀
hA : m = generateFrom C
hC : IsPiSystem C
h_univ : ↑↑μ univ = ↑↑ν univ
s : Set α
hs : MeasurableSet s
this : IsFiniteMeasure ν
⊢ ∀ (t : Set α), MeasurableSet t → ↑↑μ t = ↑↑ν t → ↑↑μ (tᶜ) = ↑↑ν (tᶜ)

case refine'_2
α✝ : Type ?u.846775
β : Type ?u.846778
γ : Type ?u.846781
δ : Type ?u.846784
ι : Type ?u.846787
R : Type ?u.846790
R' : Type ?u.846793
m0 : MeasurableSpace α✝
inst✝² : MeasurableSpace β
inst✝¹ : MeasurableSpace γ
μ✝ μ₁ μ₂ μ₃ ν✝ ν' ν₁ ν₂ : Measure α✝
s✝ s' t : Set α✝
α : Type u_1
m₀ : MeasurableSpace α
μ ν : Measure α
inst✝ : IsFiniteMeasure μ
C : Set (Set α)
hμν : ∀ (s : Set α), s ∈ C → ↑↑μ s = ↑↑ν s
m : MeasurableSpace α
h : m ≤ m₀
hA : m = generateFrom C
hC : IsPiSystem C
h_univ : ↑↑μ univ = ↑↑ν univ
s : Set α
hs : MeasurableSet s
this : IsFiniteMeasure ν
⊢ ∀ (f : ℕ → Set α),
    Pairwise (Disjoint on f) →
      (∀ (i : ℕ), MeasurableSet (f i)) →
        (∀ (i : ℕ), ↑↑μ (f i) = ↑↑ν (f i)) → ↑↑μ (⋃ (i : ℕ), f i) = ↑↑ν (⋃ (i : ℕ), f i)
α✝ : Type ?u.846775
β : Type ?u.846778
γ : Type ?u.846781
δ : Type ?u.846784
ι : Type ?u.846787
R : Type ?u.846790
R' : Type ?u.846793
m0 : MeasurableSpace α✝
inst✝² : MeasurableSpace β
inst✝¹ : MeasurableSpace γ
μ✝ μ₁ μ₂ μ₃ ν✝ ν' ν₁ ν₂ : Measure α✝
s✝ s' t : Set α✝
α : Type u_1
m₀ : MeasurableSpace α
μ ν : Measure α
inst✝ : IsFiniteMeasure μ
C : Set (Set α)
hμν : ∀ (s : Set α), s ∈ C → ↑↑μ s = ↑↑ν s
m : MeasurableSpace α
h : m ≤ m₀
hA : m = generateFrom C
hC : IsPiSystem C
h_univ : ↑↑μ univ = ↑↑ν univ
s : Set α
hs : MeasurableSet s
this : IsFiniteMeasure ν
⊢ ↑↑μ s = ↑↑ν s
refine' induction_on_inter hA hC (by simp) hμν _ _ hs
case measure_univ_lt_top
α✝ : Type ?u.846775
β : Type ?u.846778
γ : Type ?u.846781
δ : Type ?u.846784
ι : Type ?u.846787
R : Type ?u.846790
R' : Type ?u.846793
m0 : MeasurableSpace α✝
inst✝² : MeasurableSpace β
inst✝¹ : MeasurableSpace γ
μ✝ μ₁ μ₂ μ₃ ν✝ ν' ν₁ ν₂ : Measure α✝
s✝ s' t : Set α✝
α : Type u_1
m₀ : MeasurableSpace α
μ ν : Measure α
inst✝ : IsFiniteMeasure μ
C : Set (Set α)
hμν : ∀ (s : Set α), s ∈ C → ↑↑μ s = ↑↑ν s
m : MeasurableSpace α
h : m ≤ m₀
hA : m = generateFrom C
hC : IsPiSystem C
h_univ : ↑↑μ univ = ↑↑ν univ
s : Set α
hs : MeasurableSet s
⊢ ↑↑ν univ < ⊤
α✝ : Type ?u.846775
β : Type ?u.846778
γ : Type ?u.846781
δ : Type ?u.846784
ι : Type ?u.846787
R : Type ?u.846790
R' : Type ?u.846793
m0 : MeasurableSpace α✝
inst✝² : MeasurableSpace β
inst✝¹ : MeasurableSpace γ
μ✝ μ₁ μ₂ μ₃ ν✝ ν' ν₁ ν₂ : Measure α✝
s✝ s' t : Set α✝
α : Type u_1
m₀ : MeasurableSpace α
μ ν : Measure α
inst✝ : IsFiniteMeasure μ
C : Set (Set α)
hμν : ∀ (s : Set α), s ∈ C → ↑↑μ s = ↑↑ν s
m : MeasurableSpace α
h : m ≤ m₀
hA : m = generateFrom C
hC : IsPiSystem C
h_univ : ↑↑μ univ = ↑↑ν univ
s : Set α
hs : MeasurableSet s
⊢ IsFiniteMeasure ν
constructor
case measure_univ_lt_top
α✝ : Type ?u.846775
β : Type ?u.846778
γ : Type ?u.846781
δ : Type ?u.846784
ι : Type ?u.846787
R : Type ?u.846790
R' : Type ?u.846793
m0 : MeasurableSpace α✝
inst✝² : MeasurableSpace β
inst✝¹ : MeasurableSpace γ
μ✝ μ₁ μ₂ μ₃ ν✝ ν' ν₁ ν₂ : Measure α✝
s✝ s' t : Set α✝
α : Type u_1
m₀ : MeasurableSpace α
μ ν : Measure α
inst✝ : IsFiniteMeasure μ
C : Set (Set α)
hμν : ∀ (s : Set α), s ∈ C → ↑↑μ s = ↑↑ν s
m : MeasurableSpace α
h : m ≤ m₀
hA : m = generateFrom C
hC : IsPiSystem C
h_univ : ↑↑μ univ = ↑↑ν univ
s : Set α
hs : MeasurableSet s
⊢ ↑↑μ univ < ⊤
case measure_univ_lt_top
α✝ : Type ?u.846775
β : Type ?u.846778
γ : Type ?u.846781
δ : Type ?u.846784
ι : Type ?u.846787
R : Type ?u.846790
R' : Type ?u.846793
m0 : MeasurableSpace α✝
inst✝² : MeasurableSpace β
inst✝¹ : MeasurableSpace γ
μ✝ μ₁ μ₂ μ₃ ν✝ ν' ν₁ ν₂ : Measure α✝
s✝ s' t : Set α✝
α : Type u_1
m₀ : MeasurableSpace α
μ ν : Measure α
inst✝ : IsFiniteMeasure μ
C : Set (Set α)
hμν : ∀ (s : Set α), s ∈ C → ↑↑μ s = ↑↑ν s
m : MeasurableSpace α
h : m ≤ m₀
hA : m = generateFrom C
hC : IsPiSystem C
h_univ : ↑↑μ univ = ↑↑ν univ
s : Set α
hs : MeasurableSet s
⊢ ↑↑ν univ < ⊤
rw [← h_univ]
no goals
case measure_univ_lt_top
α✝ : Type ?u.846775
β : Type ?u.846778
γ : Type ?u.846781
δ : Type ?u.846784
ι : Type ?u.846787
R : Type ?u.846790
R' : Type ?u.846793
m0 : MeasurableSpace α✝
inst✝² : MeasurableSpace β
inst✝¹ : MeasurableSpace γ
μ✝ μ₁ μ₂ μ₃ ν✝ ν' ν₁ ν₂ : Measure α✝
s✝ s' t : Set α✝
α : Type u_1
m₀ : MeasurableSpace α
μ ν : Measure α
inst✝ : IsFiniteMeasure μ
C : Set (Set α)
hμν : ∀ (s : Set α), s ∈ C → ↑↑μ s = ↑↑ν s
m : MeasurableSpace α
h : m ≤ m₀
hA : m = generateFrom C
hC : IsPiSystem C
h_univ : ↑↑μ univ = ↑↑ν univ
s : Set α
hs : MeasurableSet s
⊢ ↑↑μ univ < ⊤
apply IsFiniteMeasure.measure_univ_lt_top
no goals
α✝ : Type ?u.846775
β : Type ?u.846778
γ : Type ?u.846781
δ : Type ?u.846784
ι : Type ?u.846787
R : Type ?u.846790
R' : Type ?u.846793
m0 : MeasurableSpace α✝
inst✝² : MeasurableSpace β
inst✝¹ : MeasurableSpace γ
μ✝ μ₁ μ₂ μ₃ ν✝ ν' ν₁ ν₂ : Measure α✝
s✝ s' t : Set α✝
α : Type u_1
m₀ : MeasurableSpace α
μ ν : Measure α
inst✝ : IsFiniteMeasure μ
C : Set (Set α)
hμν : ∀ (s : Set α), s ∈ C → ↑↑μ s = ↑↑ν s
m : MeasurableSpace α
h : m ≤ m₀
hA : m = generateFrom C
hC : IsPiSystem C
h_univ : ↑↑μ univ = ↑↑ν univ
s : Set α
hs : MeasurableSet s
this : IsFiniteMeasure ν
⊢ ↑↑μ ∅ = ↑↑ν ∅
simp
case refine'_1
α✝ : Type ?u.846775
β : Type ?u.846778
γ : Type ?u.846781
δ : Type ?u.846784
ι : Type ?u.846787
R : Type ?u.846790
R' : Type ?u.846793
m0 : MeasurableSpace α✝
inst✝² : MeasurableSpace β
inst✝¹ : MeasurableSpace γ
μ✝ μ₁ μ₂ μ₃ ν✝ ν' ν₁ ν₂ : Measure α✝
s✝ s' t✝ : Set α✝
α : Type u_1
m₀ : MeasurableSpace α
μ ν : Measure α
inst✝ : IsFiniteMeasure μ
C : Set (Set α)
hμν : ∀ (s : Set α), s ∈ C → ↑↑μ s = ↑↑ν s
m : MeasurableSpace α
h : m ≤ m₀
hA : m = generateFrom C
hC : IsPiSystem C
h_univ : ↑↑μ univ = ↑↑ν univ
s : Set α
hs : MeasurableSet s
this : IsFiniteMeasure ν
t : Set α
h1t : MeasurableSet t
h2t : ↑↑μ t = ↑↑ν t
⊢ ↑↑μ (tᶜ) = ↑↑ν (tᶜ)
case refine'_1
α✝ : Type ?u.846775
β : Type ?u.846778
γ : Type ?u.846781
δ : Type ?u.846784
ι : Type ?u.846787
R : Type ?u.846790
R' : Type ?u.846793
m0 : MeasurableSpace α✝
inst✝² : MeasurableSpace β
inst✝¹ : MeasurableSpace γ
μ✝ μ₁ μ₂ μ₃ ν✝ ν' ν₁ ν₂ : Measure α✝
s✝ s' t : Set α✝
α : Type u_1
m₀ : MeasurableSpace α
μ ν : Measure α
inst✝ : IsFiniteMeasure μ
C : Set (Set α)
hμν : ∀ (s : Set α), s ∈ C → ↑↑μ s = ↑↑ν s
m : MeasurableSpace α
h : m ≤ m₀
hA : m = generateFrom C
hC : IsPiSystem C
h_univ : ↑↑μ univ = ↑↑ν univ
s : Set α
hs : MeasurableSet s
this : IsFiniteMeasure ν
⊢ ∀ (t : Set α), MeasurableSet t → ↑↑μ t = ↑↑ν t → ↑↑μ (tᶜ) = ↑↑ν (tᶜ)
intro t h1t h2t
case refine'_1
α✝ : Type ?u.846775
β : Type ?u.846778
γ : Type ?u.846781
δ : Type ?u.846784
ι : Type ?u.846787
R : Type ?u.846790
R' : Type ?u.846793
m0 : MeasurableSpace α✝
inst✝² : MeasurableSpace β
inst✝¹ : MeasurableSpace γ
μ✝ μ₁ μ₂ μ₃ ν✝ ν' ν₁ ν₂ : Measure α✝
s✝ s' t✝ : Set α✝
α : Type u_1
m₀ : MeasurableSpace α
μ ν : Measure α
inst✝ : IsFiniteMeasure μ
C : Set (Set α)
hμν : ∀ (s : Set α), s ∈ C → ↑↑μ s = ↑↑ν s
m : MeasurableSpace α
h : m ≤ m₀
hA : m = generateFrom C
hC : IsPiSystem C
h_univ : ↑↑μ univ = ↑↑ν univ
s : Set α
hs : MeasurableSet s
this : IsFiniteMeasure ν
t : Set α
h1t : MeasurableSet t
h2t : ↑↑μ t = ↑↑ν t
h1t_ : MeasurableSet t
⊢ ↑↑μ (tᶜ) = ↑↑ν (tᶜ)
case refine'_1
α✝ : Type ?u.846775
β : Type ?u.846778
γ : Type ?u.846781
δ : Type ?u.846784
ι : Type ?u.846787
R : Type ?u.846790
R' : Type ?u.846793
m0 : MeasurableSpace α✝
inst✝² : MeasurableSpace β
inst✝¹ : MeasurableSpace γ
μ✝ μ₁ μ₂ μ₃ ν✝ ν' ν₁ ν₂ : Measure α✝
s✝ s' t✝ : Set α✝
α : Type u_1
m₀ : MeasurableSpace α
μ ν : Measure α
inst✝ : IsFiniteMeasure μ
C : Set (Set α)
hμν : ∀ (s : Set α), s ∈ C → ↑↑μ s = ↑↑ν s
m : MeasurableSpace α
h : m ≤ m₀
hA : m = generateFrom C
hC : IsPiSystem C
h_univ : ↑↑μ univ = ↑↑ν univ
s : Set α
hs : MeasurableSet s
this : IsFiniteMeasure ν
t : Set α
h1t : MeasurableSet t
h2t : ↑↑μ t = ↑↑ν t
⊢ ↑↑μ (tᶜ) = ↑↑ν (tᶜ)
have h1t_ : @MeasurableSet α m₀ t := h _ h1t
no goals
case refine'_1
α✝ : Type ?u.846775
β : Type ?u.846778
γ : Type ?u.846781
δ : Type ?u.846784
ι : Type ?u.846787
R : Type ?u.846790
R' : Type ?u.846793
m0 : MeasurableSpace α✝
inst✝² : MeasurableSpace β
inst✝¹ : MeasurableSpace γ
μ✝ μ₁ μ₂ μ₃ ν✝ ν' ν₁ ν₂ : Measure α✝
s✝ s' t✝ : Set α✝
α : Type u_1
m₀ : MeasurableSpace α
μ ν : Measure α
inst✝ : IsFiniteMeasure μ
C : Set (Set α)
hμν : ∀ (s : Set α), s ∈ C → ↑↑μ s = ↑↑ν s
m : MeasurableSpace α
h : m ≤ m₀
hA : m = generateFrom C
hC : IsPiSystem C
h_univ : ↑↑μ univ = ↑↑ν univ
s : Set α
hs : MeasurableSet s
this : IsFiniteMeasure ν
t : Set α
h1t : MeasurableSet t
h2t : ↑↑μ t = ↑↑ν t
h1t_ : MeasurableSet t
⊢ ↑↑μ (tᶜ) = ↑↑ν (tᶜ)
rw [@measure_compl α m₀ μ t h1t_ (@measure_ne_top α m₀ μ _ t),
  @measure_compl α m₀ ν t h1t_ (@measure_ne_top α m₀ ν _ t), h_univ, h2t]
case refine'_2
α✝ : Type ?u.846775
β : Type ?u.846778
γ : Type ?u.846781
δ : Type ?u.846784
ι : Type ?u.846787
R : Type ?u.846790
R' : Type ?u.846793
m0 : MeasurableSpace α✝
inst✝² : MeasurableSpace β
inst✝¹ : MeasurableSpace γ
μ✝ μ₁ μ₂ μ₃ ν✝ ν' ν₁ ν₂ : Measure α✝
s✝ s' t : Set α✝
α : Type u_1
m₀ : MeasurableSpace α
μ ν : Measure α
inst✝ : IsFiniteMeasure μ
C : Set (Set α)
hμν : ∀ (s : Set α), s ∈ C → ↑↑μ s = ↑↑ν s
m : MeasurableSpace α
h : m ≤ m₀
hA : m = generateFrom C
hC : IsPiSystem C
h_univ : ↑↑μ univ = ↑↑ν univ
s : Set α
hs : MeasurableSet s
this : IsFiniteMeasure ν
f : ℕ → Set α
h1f : Pairwise (Disjoint on f)
h2f : ∀ (i : ℕ), MeasurableSet (f i)
h3f : ∀ (i : ℕ), ↑↑μ (f i) = ↑↑ν (f i)
⊢ ↑↑μ (⋃ (i : ℕ), f i) = ↑↑ν (⋃ (i : ℕ), f i)
case refine'_2
α✝ : Type ?u.846775
β : Type ?u.846778
γ : Type ?u.846781
δ : Type ?u.846784
ι : Type ?u.846787
R : Type ?u.846790
R' : Type ?u.846793
m0 : MeasurableSpace α✝
inst✝² : MeasurableSpace β
inst✝¹ : MeasurableSpace γ
μ✝ μ₁ μ₂ μ₃ ν✝ ν' ν₁ ν₂ : Measure α✝
s✝ s' t : Set α✝
α : Type u_1
m₀ : MeasurableSpace α
μ ν : Measure α
inst✝ : IsFiniteMeasure μ
C : Set (Set α)
hμν : ∀ (s : Set α), s ∈ C → ↑↑μ s = ↑↑ν s
m : MeasurableSpace α
h : m ≤ m₀
hA : m = generateFrom C
hC : IsPiSystem C
h_univ : ↑↑μ univ = ↑↑ν univ
s : Set α
hs : MeasurableSet s
this : IsFiniteMeasure ν
⊢ ∀ (f : ℕ → Set α),
    Pairwise (Disjoint on f) →
      (∀ (i : ℕ), MeasurableSet (f i)) →
        (∀ (i : ℕ), ↑↑μ (f i) = ↑↑ν (f i)) → ↑↑μ (⋃ (i : ℕ), f i) = ↑↑ν (⋃ (i : ℕ), f i)
intro f h1f h2f h3f
case refine'_2
α✝ : Type ?u.846775
β : Type ?u.846778
γ : Type ?u.846781
δ : Type ?u.846784
ι : Type ?u.846787
R : Type ?u.846790
R' : Type ?u.846793
m0 : MeasurableSpace α✝
inst✝² : MeasurableSpace β
inst✝¹ : MeasurableSpace γ
μ✝ μ₁ μ₂ μ₃ ν✝ ν' ν₁ ν₂ : Measure α✝
s✝ s' t : Set α✝
α : Type u_1
m₀ : MeasurableSpace α
μ ν : Measure α
inst✝ : IsFiniteMeasure μ
C : Set (Set α)
hμν : ∀ (s : Set α), s ∈ C → ↑↑μ s = ↑↑ν s
m : MeasurableSpace α
h : m ≤ m₀
hA : m = generateFrom C
hC : IsPiSystem C
h_univ : ↑↑μ univ = ↑↑ν univ
s : Set α
hs : MeasurableSet s
this : IsFiniteMeasure ν
f : ℕ → Set α
h1f : Pairwise (Disjoint on f)
h2f : ∀ (i : ℕ), MeasurableSet (f i)
h3f : ∀ (i : ℕ), ↑↑μ (f i) = ↑↑ν (f i)
h2f_ : ∀ (i : ℕ), MeasurableSet (f i)
⊢ ↑↑μ (⋃ (i : ℕ), f i) = ↑↑ν (⋃ (i : ℕ), f i)
case refine'_2
α✝ : Type ?u.846775
β : Type ?u.846778
γ : Type ?u.846781
δ : Type ?u.846784
ι : Type ?u.846787
R : Type ?u.846790
R' : Type ?u.846793
m0 : MeasurableSpace α✝
inst✝² : MeasurableSpace β
inst✝¹ : MeasurableSpace γ
μ✝ μ₁ μ₂ μ₃ ν✝ ν' ν₁ ν₂ : Measure α✝
s✝ s' t : Set α✝
α : Type u_1
m₀ : MeasurableSpace α
μ ν : Measure α
inst✝ : IsFiniteMeasure μ
C : Set (Set α)
hμν : ∀ (s : Set α), s ∈ C → ↑↑μ s = ↑↑ν s
m : MeasurableSpace α
h : m ≤ m₀
hA : m = generateFrom C
hC : IsPiSystem C
h_univ : ↑↑μ univ = ↑↑ν univ
s : Set α
hs : MeasurableSet s
this : IsFiniteMeasure ν
f : ℕ → Set α
h1f : Pairwise (Disjoint on f)
h2f : ∀ (i : ℕ), MeasurableSet (f i)
h3f : ∀ (i : ℕ), ↑↑μ (f i) = ↑↑ν (f i)
⊢ ↑↑μ (⋃ (i : ℕ), f i) = ↑↑ν (⋃ (i : ℕ), f i)
have h2f_ : ∀ i : ℕ, @MeasurableSet α m₀ (f i) := fun i => h _ (h2f i)
no goals
case refine'_2
α✝ : Type ?u.846775
β : Type ?u.846778
γ : Type ?u.846781
δ : Type ?u.846784
ι : Type ?u.846787
R : Type ?u.846790
R' : Type ?u.846793
m0 : MeasurableSpace α✝
inst✝² : MeasurableSpace β
inst✝¹ : MeasurableSpace γ
μ✝ μ₁ μ₂ μ₃ ν✝ ν' ν₁ ν₂ : Measure α✝
s✝ s' t : Set α✝
α : Type u_1
m₀ : MeasurableSpace α
μ ν : Measure α
inst✝ : IsFiniteMeasure μ
C : Set (Set α)
hμν : ∀ (s : Set α), s ∈ C → ↑↑μ s = ↑↑ν s
m : MeasurableSpace α
h : m ≤ m₀
hA : m = generateFrom C
hC : IsPiSystem C
h_univ : ↑↑μ univ = ↑↑ν univ
s : Set α
hs : MeasurableSet s
this : IsFiniteMeasure ν
f : ℕ → Set α
h1f : Pairwise (Disjoint on f)
h2f : ∀ (i : ℕ), MeasurableSet (f i)
h3f : ∀ (i : ℕ), ↑↑μ (f i) = ↑↑ν (f i)
h2f_ : ∀ (i : ℕ), MeasurableSet (f i)
⊢ ↑↑μ (⋃ (i : ℕ), f i) = ↑↑ν (⋃ (i : ℕ), f i)
simp [measure_iUnion, h1f, h3f, h2f_]