-- Mathlib/MeasureTheory/Measure/MeasureSpace.lean
theorem _root_.Directed.measure_iInter [Countable ι] {s : ι → Set α}
    (h : ∀ i, NullMeasurableSet (s i) μ) (hd : Directed (· ⊇ ·) s) (hfin : ∃ i, μ (s i) ≠ ∞) :
    μ (⋂ i, s i) = ⨅ i, μ (s i)

Proof state:
case intro.e_a
α : Type u_1
ι : Type u_5
m : MeasurableSpace α
μ : Measure α
inst✝ : Countable ι
s : ι → Set α
h : ∀ (i : ι), NullMeasurableSet (s i) μ
hd : Directed (fun x1 x2 => x1 ⊇ x2) s
k : ι
hk : μ (s k) ≠ ⊤
this : ∀ t ⊆ s k, μ t ≠ ⊤
⊢ ⨆ i, μ (s k \ s i) = ⨆ i, μ (s k) - μ (s i)

Tactic:
refine le_antisymm (iSup_mono' fun i => ?_) (iSup_mono fun i => le_measure_diff)

Result:
case intro.e_a
α : Type u_1
ι : Type u_5
m : MeasurableSpace α
μ : Measure α
inst✝ : Countable ι
s : ι → Set α
h : ∀ (i : ι), NullMeasurableSet (s i) μ
hd : Directed (fun x1 x2 => x1 ⊇ x2) s
k : ι
hk : μ (s k) ≠ ⊤
this : ∀ t ⊆ s k, μ t ≠ ⊤
i : ι
⊢ ∃ i', μ (s k \ s i) ≤ μ (s k) - μ (s i')

Proof state:
case intro
α : Type u_1
ι : Type u_5
m : MeasurableSpace α
μ : Measure α
inst✝ : Countable ι
s : ι → Set α
h : ∀ (i : ι), NullMeasurableSet (s i) μ
hd : Directed (fun x1 x2 => x1 ⊇ x2) s
k : ι
hk : μ (s k) ≠ ⊤
this : ∀ t ⊆ s k, μ t ≠ ⊤
⊢ μ (s k) - ⨆ i, μ (s k \ s i) = μ (s k) - ⨆ i, μ (s k) - μ (s i)

Tactic:
congr 1

Result:
case intro.e_a
α : Type u_1
ι : Type u_5
m : MeasurableSpace α
μ : Measure α
inst✝ : Countable ι
s : ι → Set α
h : ∀ (i : ι), NullMeasurableSet (s i) μ
hd : Directed (fun x1 x2 => x1 ⊇ x2) s
k : ι
hk : μ (s k) ≠ ⊤
this : ∀ t ⊆ s k, μ t ≠ ⊤
⊢ ⨆ i, μ (s k \ s i) = ⨆ i, μ (s k) - μ (s i)

Proof state:
case h
α : Type u_1
ι : Type u_5
m : MeasurableSpace α
μ : Measure α
inst✝ : Countable ι
s : ι → Set α
h : ∀ (i : ι), NullMeasurableSet (s i) μ
hd : Directed (fun x1 x2 => x1 ⊇ x2) s
k : ι
hk : μ (s k) ≠ ⊤
this : ∀ t ⊆ s k, μ t ≠ ⊤
i j : ι
hji : s i ⊇ s j
hjk : s k ⊇ s j
⊢ μ (s k \ s i) ≤ μ (s k) - μ (s j)

Tactic:
rw [← measure_diff hjk (h _) (this _ hjk)]

Result:
case h
α : Type u_1
ι : Type u_5
m : MeasurableSpace α
μ : Measure α
inst✝ : Countable ι
s : ι → Set α
h : ∀ (i : ι), NullMeasurableSet (s i) μ
hd : Directed (fun x1 x2 => x1 ⊇ x2) s
k : ι
hk : μ (s k) ≠ ⊤
this : ∀ t ⊆ s k, μ t ≠ ⊤
i j : ι
hji : s i ⊇ s j
hjk : s k ⊇ s j
⊢ μ (s k \ s i) ≤ μ (s k \ s j)

Proof state:
case intro
α : Type u_1
ι : Type u_5
m : MeasurableSpace α
μ : Measure α
inst✝ : Countable ι
s : ι → Set α
h : ∀ (i : ι), NullMeasurableSet (s i) μ
hd : Directed (fun x1 x2 => x1 ⊇ x2) s
k : ι
hk : μ (s k) ≠ ⊤
⊢ μ (⋂ i, s i) = ⨅ i, μ (s i)

Tactic:
have : ∀ t ⊆ s k, μ t ≠ ∞ := fun t ht => ne_top_of_le_ne_top hk (measure_mono ht)

Result:
case intro
α : Type u_1
ι : Type u_5
m : MeasurableSpace α
μ : Measure α
inst✝ : Countable ι
s : ι → Set α
h : ∀ (i : ι), NullMeasurableSet (s i) μ
hd : Directed (fun x1 x2 => x1 ⊇ x2) s
k : ι
hk : μ (s k) ≠ ⊤
this : ∀ t ⊆ s k, μ t ≠ ⊤
⊢ μ (⋂ i, s i) = ⨅ i, μ (s i)

Proof state:
case intro
α : Type u_1
ι : Type u_5
m : MeasurableSpace α
μ : Measure α
inst✝ : Countable ι
s : ι → Set α
h : ∀ (i : ι), NullMeasurableSet (s i) μ
hd : Directed (fun x1 x2 => x1 ⊇ x2) s
k : ι
hk : μ (s k) ≠ ⊤
this : ∀ t ⊆ s k, μ t ≠ ⊤
⊢ Directed (fun x1 x2 => x1 ⊆ x2) fun i => s k \ s i

Tactic:
exact hd.mono_comp _ fun _ _ => diff_subset_diff_right

Result:
no goals

Proof state:
case intro
α : Type u_1
ι : Type u_5
m : MeasurableSpace α
μ : Measure α
inst✝ : Countable ι
s : ι → Set α
h : ∀ (i : ι), NullMeasurableSet (s i) μ
hd : Directed (fun x1 x2 => x1 ⊇ x2) s
k : ι
hk : μ (s k) ≠ ⊤
this : ∀ t ⊆ s k, μ t ≠ ⊤
⊢ μ (⋂ i, s i) = ⨅ i, μ (s i)

Tactic:
rw [← ENNReal.sub_sub_cancel hk (iInf_le (fun i => μ (s i)) k), ENNReal.sub_iInf, ←
  ENNReal.sub_sub_cancel hk (measure_mono (iInter_subset _ k)), ←
  measure_diff (iInter_subset _ k) (.iInter h) (this _ (iInter_subset _ k)),
  diff_iInter, Directed.measure_iUnion]

Result:
case intro
α : Type u_1
ι : Type u_5
m : MeasurableSpace α
μ : Measure α
inst✝ : Countable ι
s : ι → Set α
h : ∀ (i : ι), NullMeasurableSet (s i) μ
hd : Directed (fun x1 x2 => x1 ⊇ x2) s
k : ι
hk : μ (s k) ≠ ⊤
this : ∀ t ⊆ s k, μ t ≠ ⊤
⊢ μ (s k) - ⨆ i, μ (s k \ s i) = μ (s k) - ⨆ i, μ (s k) - μ (s i)

case intro
α : Type u_1
ι : Type u_5
m : MeasurableSpace α
μ : Measure α
inst✝ : Countable ι
s : ι → Set α
h : ∀ (i : ι), NullMeasurableSet (s i) μ
hd : Directed (fun x1 x2 => x1 ⊇ x2) s
k : ι
hk : μ (s k) ≠ ⊤
this : ∀ t ⊆ s k, μ t ≠ ⊤
⊢ Directed (fun x1 x2 => x1 ⊆ x2) fun i => s k \ s i

Proof state:
case h
α : Type u_1
ι : Type u_5
m : MeasurableSpace α
μ : Measure α
inst✝ : Countable ι
s : ι → Set α
h : ∀ (i : ι), NullMeasurableSet (s i) μ
hd : Directed (fun x1 x2 => x1 ⊇ x2) s
k : ι
hk : μ (s k) ≠ ⊤
this : ∀ t ⊆ s k, μ t ≠ ⊤
i j : ι
hji : s i ⊇ s j
hjk : s k ⊇ s j
⊢ μ (s k \ s i) ≤ μ (s k \ s j)

Tactic:
gcongr

Result:
no goals

Proof state:
case intro.e_a.intro.intro
α : Type u_1
ι : Type u_5
m : MeasurableSpace α
μ : Measure α
inst✝ : Countable ι
s : ι → Set α
h : ∀ (i : ι), NullMeasurableSet (s i) μ
hd : Directed (fun x1 x2 => x1 ⊇ x2) s
k : ι
hk : μ (s k) ≠ ⊤
this : ∀ t ⊆ s k, μ t ≠ ⊤
i j : ι
hji : s i ⊇ s j
hjk : s k ⊇ s j
⊢ ∃ i', μ (s k \ s i) ≤ μ (s k) - μ (s i')

Tactic:
use j

Result:
case h
α : Type u_1
ι : Type u_5
m : MeasurableSpace α
μ : Measure α
inst✝ : Countable ι
s : ι → Set α
h : ∀ (i : ι), NullMeasurableSet (s i) μ
hd : Directed (fun x1 x2 => x1 ⊇ x2) s
k : ι
hk : μ (s k) ≠ ⊤
this : ∀ t ⊆ s k, μ t ≠ ⊤
i j : ι
hji : s i ⊇ s j
hjk : s k ⊇ s j
⊢ μ (s k \ s i) ≤ μ (s k) - μ (s j)

Proof state:
case intro.e_a
α : Type u_1
ι : Type u_5
m : MeasurableSpace α
μ : Measure α
inst✝ : Countable ι
s : ι → Set α
h : ∀ (i : ι), NullMeasurableSet (s i) μ
hd : Directed (fun x1 x2 => x1 ⊇ x2) s
k : ι
hk : μ (s k) ≠ ⊤
this : ∀ t ⊆ s k, μ t ≠ ⊤
i : ι
⊢ ∃ i', μ (s k \ s i) ≤ μ (s k) - μ (s i')

Tactic:
rcases hd i k with ⟨j, hji, hjk⟩

Result:
case intro.e_a.intro.intro
α : Type u_1
ι : Type u_5
m : MeasurableSpace α
μ : Measure α
inst✝ : Countable ι
s : ι → Set α
h : ∀ (i : ι), NullMeasurableSet (s i) μ
hd : Directed (fun x1 x2 => x1 ⊇ x2) s
k : ι
hk : μ (s k) ≠ ⊤
this : ∀ t ⊆ s k, μ t ≠ ⊤
i j : ι
hji : s i ⊇ s j
hjk : s k ⊇ s j
⊢ ∃ i', μ (s k \ s i) ≤ μ (s k) - μ (s i')

Proof state:
α : Type u_1
ι : Type u_5
m : MeasurableSpace α
μ : Measure α
inst✝ : Countable ι
s : ι → Set α
h : ∀ (i : ι), NullMeasurableSet (s i) μ
hd : Directed (fun x1 x2 => x1 ⊇ x2) s
hfin : ∃ i, μ (s i) ≠ ⊤
⊢ μ (⋂ i, s i) = ⨅ i, μ (s i)

Tactic:
rcases hfin with ⟨k, hk⟩

Result:
case intro
α : Type u_1
ι : Type u_5
m : MeasurableSpace α
μ : Measure α
inst✝ : Countable ι
s : ι → Set α
h : ∀ (i : ι), NullMeasurableSet (s i) μ
hd : Directed (fun x1 x2 => x1 ⊇ x2) s
k : ι
hk : μ (s k) ≠ ⊤
⊢ μ (⋂ i, s i) = ⨅ i, μ (s i)