-- Mathlib/MeasureTheory/Measure/MeasureSpace.lean
theorem _root_.Directed.measure_iUnion [Countable ι] {s : ι → Set α} (hd : Directed (· ⊆ ·) s) :
    μ (⋃ i, s i) = ⨆ i, μ (s i)

Proof state:
case intro
α : Type u_1
ι : Type u_5
m : MeasurableSpace α
μ : Measure α
inst✝ : Countable ι
s : ι → Set α
e : ι → ℕ
he : Injective e
t : ℕ → Set α
ht : Function.extend e s ⊥ = t
hd : Directed (fun x1 x2 => x1 ⊆ x2) t
⊢ μ (⋃ i, s i) = ⨆ i, μ (s i)

Tactic:
suffices μ (⋃ n, t n) = ⨆ n, μ (t n) by
  simp only [← ht, Function.apply_extend μ, ← iSup_eq_iUnion, iSup_extend_bot he,
    Function.comp_def, Pi.bot_apply, bot_eq_empty, measure_empty] at this
  exact this.trans (iSup_extend_bot he _)

Result:
case intro
α : Type u_1
ι : Type u_5
m : MeasurableSpace α
μ : Measure α
inst✝ : Countable ι
s : ι → Set α
e : ι → ℕ
he : Injective e
t : ℕ → Set α
ht : Function.extend e s ⊥ = t
hd : Directed (fun x1 x2 => x1 ⊆ x2) t
⊢ μ (⋃ n, t n) = ⨆ n, μ (t n)

Proof state:
case intro
α : Type u_1
m : MeasurableSpace α
μ : Measure α
t : ℕ → Set α
hd : Directed (fun x1 x2 => x1 ⊆ x2) t
T : ℕ → Set α := fun n => toMeasurable μ (t n)
Td : ℕ → Set α := disjointed T
⊢ μ (⋃ n, t n) ≤ ⨆ n, μ (t n)

Tactic:
have hm : ∀ n, MeasurableSet (Td n) := .disjointed fun n ↦ measurableSet_toMeasurable _ _

Result:
case intro
α : Type u_1
m : MeasurableSpace α
μ : Measure α
t : ℕ → Set α
hd : Directed (fun x1 x2 => x1 ⊆ x2) t
T : ℕ → Set α := fun n => toMeasurable μ (t n)
Td : ℕ → Set α := disjointed T
hm : ∀ (n : ℕ), MeasurableSet (Td n)
⊢ μ (⋃ n, t n) ≤ ⨆ n, μ (t n)

Proof state:
case intro
α : Type u_1
m : MeasurableSpace α
μ : Measure α
t : ℕ → Set α
hd : Directed (fun x1 x2 => x1 ⊆ x2) t
T : ℕ → Set α := fun n => toMeasurable μ (t n)
⊢ μ (⋃ n, t n) ≤ ⨆ n, μ (t n)

Tactic:
set Td : ℕ → Set α := disjointed T

Result:
case intro
α : Type u_1
m : MeasurableSpace α
μ : Measure α
t : ℕ → Set α
hd : Directed (fun x1 x2 => x1 ⊆ x2) t
T : ℕ → Set α := fun n => toMeasurable μ (t n)
Td : ℕ → Set α := disjointed T
⊢ μ (⋃ n, t n) ≤ ⨆ n, μ (t n)

Proof state:
α : Type u_1
ι : Type u_5
m : MeasurableSpace α
μ : Measure α
inst✝ : Countable ι
s : ι → Set α
hd : Directed (fun x1 x2 => x1 ⊆ x2) s
⊢ μ (⋃ i, s i) = ⨆ i, μ (s i)

Tactic:
rcases Countable.exists_injective_nat ι with ⟨e, he⟩

Result:
case intro
α : Type u_1
ι : Type u_5
m : MeasurableSpace α
μ : Measure α
inst✝ : Countable ι
s : ι → Set α
hd : Directed (fun x1 x2 => x1 ⊆ x2) s
e : ι → ℕ
he : Injective e
⊢ μ (⋃ i, s i) = ⨆ i, μ (s i)

Proof state:
α : Type u_1
ι : Type u_5
m : MeasurableSpace α
μ : Measure α
inst✝ : Countable ι
s : ι → Set α
e : ι → ℕ
he : Injective e
t : ℕ → Set α
ht : Function.extend e s ⊥ = t
hd : Directed (fun x1 x2 => x1 ⊆ x2) t
this : μ (⨆ i, s i) = ⨆ n, Function.extend e (fun x => μ (s x)) (fun x => 0) n
⊢ μ (⋃ i, s i) = ⨆ i, μ (s i)

Tactic:
exact this.trans (iSup_extend_bot he _)

Result:
no goals

Proof state:
case intro
α : Type u_1
m : MeasurableSpace α
μ : Measure α
t : ℕ → Set α
hd : Directed (fun x1 x2 => x1 ⊆ x2) t
⊢ μ (⋃ n, t n) ≤ ⨆ n, μ (t n)

Tactic:
set T : ℕ → Set α := fun n => toMeasurable μ (t n)

Result:
case intro
α : Type u_1
m : MeasurableSpace α
μ : Measure α
t : ℕ → Set α
hd : Directed (fun x1 x2 => x1 ⊆ x2) t
T : ℕ → Set α := fun n => toMeasurable μ (t n)
⊢ μ (⋃ n, t n) ≤ ⨆ n, μ (t n)

Proof state:
case intro
α : Type u_1
m : MeasurableSpace α
μ : Measure α
t : ℕ → Set α
hd : Directed (fun x1 x2 => x1 ⊆ x2) t
T : ℕ → Set α := fun n => toMeasurable μ (t n)
Td : ℕ → Set α := disjointed T
hm : ∀ (n : ℕ), MeasurableSet (Td n)
⊢ μ (⋃ n, t n) ≤ ⨆ n, μ (t n)

Tactic:
calc
  μ (⋃ n, t n) = μ (⋃ n, Td n) := by rw [iUnion_disjointed, measure_iUnion_toMeasurable]
  _ ≤ ∑' n, μ (Td n) := measure_iUnion_le _
  _ = ⨆ I : Finset ℕ, ∑ n ∈ I, μ (Td n) := ENNReal.tsum_eq_iSup_sum
  _ ≤ ⨆ n, μ (t n) := iSup_le fun I => by
    rcases hd.finset_le I with ⟨N, hN⟩
    calc
      (∑ n ∈ I, μ (Td n)) = μ (⋃ n ∈ I, Td n) :=
        (measure_biUnion_finset ((disjoint_disjointed T).set_pairwise I) fun n _ => hm n).symm
      _ ≤ μ (⋃ n ∈ I, T n) := measure_mono (iUnion₂_mono fun n _hn => disjointed_subset _ _)
      _ = μ (⋃ n ∈ I, t n) := measure_biUnion_toMeasurable I.countable_toSet _
      _ ≤ μ (t N) := measure_mono (iUnion₂_subset hN)
      _ ≤ ⨆ n, μ (t n) := le_iSup (μ ∘ t) N

Result:
no goals

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
t : ℕ → Set α
hd : Directed (fun x1 x2 => x1 ⊆ x2) t
T : ℕ → Set α := fun n => toMeasurable μ (t n)
Td : ℕ → Set α := disjointed T
hm : ∀ (n : ℕ), MeasurableSet (Td n)
⊢ μ (⋃ n, t n) = μ (⋃ n, Td n)

Tactic:
rw [iUnion_disjointed, measure_iUnion_toMeasurable]

Result:
no goals

Proof state:
case intro
α : Type u_1
m : MeasurableSpace α
μ : Measure α
t : ℕ → Set α
hd : Directed (fun x1 x2 => x1 ⊆ x2) t
⊢ μ (⋃ n, t n) = ⨆ n, μ (t n)

Tactic:
refine le_antisymm ?_ (iSup_le fun i ↦ measure_mono <| subset_iUnion _ _)

Result:
case intro
α : Type u_1
m : MeasurableSpace α
μ : Measure α
t : ℕ → Set α
hd : Directed (fun x1 x2 => x1 ⊆ x2) t
⊢ μ (⋃ n, t n) ≤ ⨆ n, μ (t n)

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
t : ℕ → Set α
hd : Directed (fun x1 x2 => x1 ⊆ x2) t
T : ℕ → Set α := fun n => toMeasurable μ (t n)
Td : ℕ → Set α := disjointed T
hm : ∀ (n : ℕ), MeasurableSet (Td n)
I : Finset ℕ
⊢ ∑ n ∈ I, μ (Td n) ≤ ⨆ n, μ (t n)

Tactic:
rcases hd.finset_le I with ⟨N, hN⟩

Result:
case intro
α : Type u_1
m : MeasurableSpace α
μ : Measure α
t : ℕ → Set α
hd : Directed (fun x1 x2 => x1 ⊆ x2) t
T : ℕ → Set α := fun n => toMeasurable μ (t n)
Td : ℕ → Set α := disjointed T
hm : ∀ (n : ℕ), MeasurableSet (Td n)
I : Finset ℕ
N : ℕ
hN : ∀ i ∈ I, t i ⊆ t N
⊢ ∑ n ∈ I, μ (Td n) ≤ ⨆ n, μ (t n)

Proof state:
α : Type u_1
ι : Type u_5
m : MeasurableSpace α
μ : Measure α
inst✝ : Countable ι
s : ι → Set α
e : ι → ℕ
he : Injective e
t : ℕ → Set α
ht : Function.extend e s ⊥ = t
hd : Directed (fun x1 x2 => x1 ⊆ x2) t
this : μ (⋃ n, t n) = ⨆ n, μ (t n)
⊢ μ (⋃ i, s i) = ⨆ i, μ (s i)

Tactic:
simp only [← ht, Function.apply_extend μ, ← iSup_eq_iUnion, iSup_extend_bot he,
  Function.comp_def, Pi.bot_apply, bot_eq_empty, measure_empty] at this

Result:
α : Type u_1
ι : Type u_5
m : MeasurableSpace α
μ : Measure α
inst✝ : Countable ι
s : ι → Set α
e : ι → ℕ
he : Injective e
t : ℕ → Set α
ht : Function.extend e s ⊥ = t
hd : Directed (fun x1 x2 => x1 ⊆ x2) t
this : μ (⨆ i, s i) = ⨆ n, Function.extend e (fun x => μ (s x)) (fun x => 0) n
⊢ μ (⋃ i, s i) = ⨆ i, μ (s i)

Proof state:
case intro
α : Type u_1
ι : Type u_5
m : MeasurableSpace α
μ : Measure α
inst✝ : Countable ι
s : ι → Set α
e : ι → ℕ
he : Injective e
t : ℕ → Set α
ht : Function.extend e s ⊥ = t
hd : Directed (fun x1 x2 => x1 ⊆ x2) t
⊢ μ (⋃ n, t n) = ⨆ n, μ (t n)

Tactic:
clear! ι

Result:
case intro
α : Type u_1
m : MeasurableSpace α
μ : Measure α
t : ℕ → Set α
hd : Directed (fun x1 x2 => x1 ⊆ x2) t
⊢ μ (⋃ n, t n) = ⨆ n, μ (t n)

Proof state:
case intro
α : Type u_1
ι : Type u_5
m : MeasurableSpace α
μ : Measure α
inst✝ : Countable ι
s : ι → Set α
hd : Directed (fun x1 x2 => x1 ⊆ x2) s
e : ι → ℕ
he : Injective e
⊢ μ (⋃ i, s i) = ⨆ i, μ (s i)

Tactic:
generalize ht : Function.extend e s ⊥ = t

Result:
case intro
α : Type u_1
ι : Type u_5
m : MeasurableSpace α
μ : Measure α
inst✝ : Countable ι
s : ι → Set α
hd : Directed (fun x1 x2 => x1 ⊆ x2) s
e : ι → ℕ
he : Injective e
t : ℕ → Set α
ht : Function.extend e s ⊥ = t
⊢ μ (⋃ i, s i) = ⨆ i, μ (s i)