-- Mathlib/MeasureTheory/Measure/MeasureSpace.lean
theorem _root_.Monotone.measure_iUnion [Preorder ι] [IsDirected ι (· ≤ ·)]
    [(atTop : Filter ι).IsCountablyGenerated] {s : ι → Set α} (hs : Monotone s) :
    μ (⋃ i, s i) = ⨆ i, μ (s i)

Proof state:
case inr.intro.intro
α : Type u_1
ι : Type u_5
m : MeasurableSpace α
μ : Measure α
inst✝² : Preorder ι
inst✝¹ : IsDirected ι fun x1 x2 => x1 ≤ x2
inst✝ : atTop.IsCountablyGenerated
s : ι → Set α
hs : Monotone s
h✝ : Nonempty ι
x : ℕ → ι
hxm : Monotone x
hx : Tendsto x atTop atTop
⊢ μ (⋃ i, s i) = ⨆ i, μ (s i)

Tactic:
rw [← hs.iUnion_comp_tendsto_atTop hx, ← Monotone.iSup_comp_tendsto_atTop _ hx]

Result:
case inr.intro.intro
α : Type u_1
ι : Type u_5
m : MeasurableSpace α
μ : Measure α
inst✝² : Preorder ι
inst✝¹ : IsDirected ι fun x1 x2 => x1 ≤ x2
inst✝ : atTop.IsCountablyGenerated
s : ι → Set α
hs : Monotone s
h✝ : Nonempty ι
x : ℕ → ι
hxm : Monotone x
hx : Tendsto x atTop atTop
⊢ μ (⋃ a, s (x a)) = ⨆ a, μ (s (x a))

α : Type u_1
ι : Type u_5
m : MeasurableSpace α
μ : Measure α
inst✝² : Preorder ι
inst✝¹ : IsDirected ι fun x1 x2 => x1 ≤ x2
inst✝ : atTop.IsCountablyGenerated
s : ι → Set α
hs : Monotone s
h✝ : Nonempty ι
x : ℕ → ι
hxm : Monotone x
hx : Tendsto x atTop atTop
⊢ Monotone fun i => μ (s i)

Proof state:
case inl
α : Type u_1
ι : Type u_5
m : MeasurableSpace α
μ : Measure α
inst✝² : Preorder ι
inst✝¹ : IsDirected ι fun x1 x2 => x1 ≤ x2
inst✝ : atTop.IsCountablyGenerated
s : ι → Set α
hs : Monotone s
h✝ : IsEmpty ι
⊢ μ (⋃ i, s i) = ⨆ i, μ (s i)

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
ι : Type u_5
m : MeasurableSpace α
μ : Measure α
inst✝² : Preorder ι
inst✝¹ : IsDirected ι fun x1 x2 => x1 ≤ x2
inst✝ : atTop.IsCountablyGenerated
s : ι → Set α
hs : Monotone s
⊢ μ (⋃ i, s i) = ⨆ i, μ (s i)

Tactic:
cases isEmpty_or_nonempty ι with
| inl _ => simp
| inr _ =>
  rcases exists_seq_monotone_tendsto_atTop_atTop ι with ⟨x, hxm, hx⟩
  rw [← hs.iUnion_comp_tendsto_atTop hx, ← Monotone.iSup_comp_tendsto_atTop _ hx]
  exacts [(hs.comp hxm).directed_le.measure_iUnion, fun _ _ h ↦ measure_mono (hs h)]

Result:
no goals

Proof state:
case inr.intro.intro
α : Type u_1
ι : Type u_5
m : MeasurableSpace α
μ : Measure α
inst✝² : Preorder ι
inst✝¹ : IsDirected ι fun x1 x2 => x1 ≤ x2
inst✝ : atTop.IsCountablyGenerated
s : ι → Set α
hs : Monotone s
h✝ : Nonempty ι
x : ℕ → ι
hxm : Monotone x
hx : Tendsto x atTop atTop
⊢ μ (⋃ a, s (x a)) = ⨆ a, μ (s (x a))

α : Type u_1
ι : Type u_5
m : MeasurableSpace α
μ : Measure α
inst✝² : Preorder ι
inst✝¹ : IsDirected ι fun x1 x2 => x1 ≤ x2
inst✝ : atTop.IsCountablyGenerated
s : ι → Set α
hs : Monotone s
h✝ : Nonempty ι
x : ℕ → ι
hxm : Monotone x
hx : Tendsto x atTop atTop
⊢ Monotone fun i => μ (s i)

Tactic:
exacts [(hs.comp hxm).directed_le.measure_iUnion, fun _ _ h ↦ measure_mono (hs h)]

Result:
no goals

Proof state:
case inr
α : Type u_1
ι : Type u_5
m : MeasurableSpace α
μ : Measure α
inst✝² : Preorder ι
inst✝¹ : IsDirected ι fun x1 x2 => x1 ≤ x2
inst✝ : atTop.IsCountablyGenerated
s : ι → Set α
hs : Monotone s
h✝ : Nonempty ι
⊢ μ (⋃ i, s i) = ⨆ i, μ (s i)

Tactic:
rcases exists_seq_monotone_tendsto_atTop_atTop ι with ⟨x, hxm, hx⟩

Result:
case inr.intro.intro
α : Type u_1
ι : Type u_5
m : MeasurableSpace α
μ : Measure α
inst✝² : Preorder ι
inst✝¹ : IsDirected ι fun x1 x2 => x1 ≤ x2
inst✝ : atTop.IsCountablyGenerated
s : ι → Set α
hs : Monotone s
h✝ : Nonempty ι
x : ℕ → ι
hxm : Monotone x
hx : Tendsto x atTop atTop
⊢ μ (⋃ i, s i) = ⨆ i, μ (s i)