-- Mathlib/MeasureTheory/Measure/MeasureSpace.lean
theorem _root_.Monotone.measure_iInter [Preorder ι] [IsDirected ι (· ≥ ·)]
    [(atBot : Filter ι).IsCountablyGenerated] {s : ι → Set α} (hs : Monotone s)
    (hsm : ∀ i, NullMeasurableSet (s i) μ) (hfin : ∃ i, μ (s i) ≠ ∞) :
    μ (⋂ i, s i) = ⨅ i, μ (s i)

Proof state:
α : Type u_1
ι : Type u_5
m : MeasurableSpace α
μ : Measure α
inst✝² : Preorder ι
inst✝¹ : IsDirected ι fun x1 x2 => x1 ≥ x2
inst✝ : atBot.IsCountablyGenerated
s : ι → Set α
hs : Monotone s
hsm : ∀ (i : ι), NullMeasurableSet (s i) μ
hfin : ∃ i, μ (s i) ≠ ⊤
⊢ μ (⋂ i, s i) = ⨅ i, μ (s i)

Tactic:
refine le_antisymm (le_iInf fun i ↦ measure_mono <| iInter_subset _ _) ?_

Result:
α : Type u_1
ι : Type u_5
m : MeasurableSpace α
μ : Measure α
inst✝² : Preorder ι
inst✝¹ : IsDirected ι fun x1 x2 => x1 ≥ x2
inst✝ : atBot.IsCountablyGenerated
s : ι → Set α
hs : Monotone s
hsm : ∀ (i : ι), NullMeasurableSet (s i) μ
hfin : ∃ i, μ (s i) ≠ ⊤
⊢ ⨅ i, μ (s i) ≤ μ (⋂ i, s i)

Proof state:
α : Type u_1
ι : Type u_5
m : MeasurableSpace α
μ : Measure α
inst✝² : Preorder ι
inst✝¹ : IsDirected ι fun x1 x2 => x1 ≥ x2
inst✝ : atBot.IsCountablyGenerated
s : ι → Set α
hs : Monotone s
hsm : ∀ (i : ι), NullMeasurableSet (s i) μ
hfin : ∃ i, μ (s i) ≠ ⊤
⊢ ⨅ i, μ (s i) ≤ μ (⋂ i, s i)

Tactic:
have := hfin.nonempty

Result:
α : Type u_1
ι : Type u_5
m : MeasurableSpace α
μ : Measure α
inst✝² : Preorder ι
inst✝¹ : IsDirected ι fun x1 x2 => x1 ≥ x2
inst✝ : atBot.IsCountablyGenerated
s : ι → Set α
hs : Monotone s
hsm : ∀ (i : ι), NullMeasurableSet (s i) μ
hfin : ∃ i, μ (s i) ≠ ⊤
this : Nonempty ι
⊢ ⨅ i, μ (s i) ≤ μ (⋂ i, s i)

Proof state:
α : Type u_1
ι : Type u_5
m : MeasurableSpace α
μ : Measure α
inst✝² : Preorder ι
inst✝¹ : IsDirected ι fun x1 x2 => x1 ≥ x2
inst✝ : atBot.IsCountablyGenerated
s : ι → Set α
hs : Monotone s
hsm : ∀ (i : ι), NullMeasurableSet (s i) μ
hfin : ∃ i, μ (s i) ≠ ⊤
this : Nonempty ι
x : ℕ → ι
hxm : Antitone x
hx : Tendsto x atTop atBot
⊢ ⨅ n, μ (s (x n)) = μ (⋂ n, s (x n))

Tactic:
refine .symm <| (hs.comp_antitone hxm).directed_ge.measure_iInter (fun n ↦ hsm _) ?_

Result:
α : Type u_1
ι : Type u_5
m : MeasurableSpace α
μ : Measure α
inst✝² : Preorder ι
inst✝¹ : IsDirected ι fun x1 x2 => x1 ≥ x2
inst✝ : atBot.IsCountablyGenerated
s : ι → Set α
hs : Monotone s
hsm : ∀ (i : ι), NullMeasurableSet (s i) μ
hfin : ∃ i, μ (s i) ≠ ⊤
this : Nonempty ι
x : ℕ → ι
hxm : Antitone x
hx : Tendsto x atTop atBot
⊢ ∃ i, μ (s (x i)) ≠ ⊤

Proof state:
α : Type u_1
ι : Type u_5
m : MeasurableSpace α
μ : Measure α
inst✝² : Preorder ι
inst✝¹ : IsDirected ι fun x1 x2 => x1 ≥ x2
inst✝ : atBot.IsCountablyGenerated
s : ι → Set α
hs : Monotone s
hsm : ∀ (i : ι), NullMeasurableSet (s i) μ
hfin : ∃ i, μ (s i) ≠ ⊤
this : Nonempty ι
x : ℕ → ι
hxm : Antitone x
hx : Tendsto x atTop atBot
⊢ μ (⋂ n, s (x n)) ≤ μ (⋂ i, s i)

Tactic:
refine measure_mono <| iInter_mono' fun i ↦ ?_

Result:
α : Type u_1
ι : Type u_5
m : MeasurableSpace α
μ : Measure α
inst✝² : Preorder ι
inst✝¹ : IsDirected ι fun x1 x2 => x1 ≥ x2
inst✝ : atBot.IsCountablyGenerated
s : ι → Set α
hs : Monotone s
hsm : ∀ (i : ι), NullMeasurableSet (s i) μ
hfin : ∃ i, μ (s i) ≠ ⊤
this : Nonempty ι
x : ℕ → ι
hxm : Antitone x
hx : Tendsto x atTop atBot
i : ι
⊢ ∃ i_1, s (x i_1) ⊆ s i

Proof state:
case intro.intro
α : Type u_1
ι : Type u_5
m : MeasurableSpace α
μ : Measure α
inst✝² : Preorder ι
inst✝¹ : IsDirected ι fun x1 x2 => x1 ≥ x2
inst✝ : atBot.IsCountablyGenerated
s : ι → Set α
hs : Monotone s
hsm : ∀ (i : ι), NullMeasurableSet (s i) μ
hfin : ∃ i, μ (s i) ≠ ⊤
this : Nonempty ι
x : ℕ → ι
hxm : Antitone x
hx : Tendsto x atTop atBot
⊢ ⨅ i, μ (s i) ≤ μ (⋂ i, s i)

Tactic:
calc
  ⨅ i, μ (s i) ≤ ⨅ n, μ (s (x n)) := le_iInf_comp (μ ∘ s) x
  _ = μ (⋂ n, s (x n)) := by
    refine .symm <| (hs.comp_antitone hxm).directed_ge.measure_iInter (fun n ↦ hsm _) ?_
    rcases hfin with ⟨k, hk⟩
    rcases (hx.eventually_le_atBot k).exists with ⟨n, hn⟩
    exact ⟨n, ne_top_of_le_ne_top hk <| measure_mono <| hs hn⟩
  _ ≤ μ (⋂ i, s i) := by
    refine measure_mono <| iInter_mono' fun i ↦ ?_
    rcases (hx.eventually_le_atBot i).exists with ⟨n, hn⟩
    exact ⟨n, hs hn⟩

Result:
no goals

Proof state:
α : Type u_1
ι : Type u_5
m : MeasurableSpace α
μ : Measure α
inst✝² : Preorder ι
inst✝¹ : IsDirected ι fun x1 x2 => x1 ≥ x2
inst✝ : atBot.IsCountablyGenerated
s : ι → Set α
hs : Monotone s
hsm : ∀ (i : ι), NullMeasurableSet (s i) μ
hfin : ∃ i, μ (s i) ≠ ⊤
this : Nonempty ι
x : ℕ → ι
hxm : Antitone x
hx : Tendsto x atTop atBot
⊢ ∃ i, μ (s (x i)) ≠ ⊤

Tactic:
rcases hfin with ⟨k, hk⟩

Result:
case intro
α : Type u_1
ι : Type u_5
m : MeasurableSpace α
μ : Measure α
inst✝² : Preorder ι
inst✝¹ : IsDirected ι fun x1 x2 => x1 ≥ x2
inst✝ : atBot.IsCountablyGenerated
s : ι → Set α
hs : Monotone s
hsm : ∀ (i : ι), NullMeasurableSet (s i) μ
this : Nonempty ι
x : ℕ → ι
hxm : Antitone x
hx : Tendsto x atTop atBot
k : ι
hk : μ (s k) ≠ ⊤
⊢ ∃ i, μ (s (x i)) ≠ ⊤

Proof state:
case intro.intro
α : Type u_1
ι : Type u_5
m : MeasurableSpace α
μ : Measure α
inst✝² : Preorder ι
inst✝¹ : IsDirected ι fun x1 x2 => x1 ≥ x2
inst✝ : atBot.IsCountablyGenerated
s : ι → Set α
hs : Monotone s
hsm : ∀ (i : ι), NullMeasurableSet (s i) μ
this : Nonempty ι
x : ℕ → ι
hxm : Antitone x
hx : Tendsto x atTop atBot
k : ι
hk : μ (s k) ≠ ⊤
n : ℕ
hn : x n ≤ k
⊢ ∃ i, μ (s (x i)) ≠ ⊤

Tactic:
exact ⟨n, ne_top_of_le_ne_top hk <| measure_mono <| hs hn⟩

Result:
no goals

Proof state:
case intro
α : Type u_1
ι : Type u_5
m : MeasurableSpace α
μ : Measure α
inst✝² : Preorder ι
inst✝¹ : IsDirected ι fun x1 x2 => x1 ≥ x2
inst✝ : atBot.IsCountablyGenerated
s : ι → Set α
hs : Monotone s
hsm : ∀ (i : ι), NullMeasurableSet (s i) μ
this : Nonempty ι
x : ℕ → ι
hxm : Antitone x
hx : Tendsto x atTop atBot
k : ι
hk : μ (s k) ≠ ⊤
⊢ ∃ i, μ (s (x i)) ≠ ⊤

Tactic:
rcases (hx.eventually_le_atBot k).exists with ⟨n, hn⟩

Result:
case intro.intro
α : Type u_1
ι : Type u_5
m : MeasurableSpace α
μ : Measure α
inst✝² : Preorder ι
inst✝¹ : IsDirected ι fun x1 x2 => x1 ≥ x2
inst✝ : atBot.IsCountablyGenerated
s : ι → Set α
hs : Monotone s
hsm : ∀ (i : ι), NullMeasurableSet (s i) μ
this : Nonempty ι
x : ℕ → ι
hxm : Antitone x
hx : Tendsto x atTop atBot
k : ι
hk : μ (s k) ≠ ⊤
n : ℕ
hn : x n ≤ k
⊢ ∃ i, μ (s (x i)) ≠ ⊤

Proof state:
case intro
α : Type u_1
ι : Type u_5
m : MeasurableSpace α
μ : Measure α
inst✝² : Preorder ι
inst✝¹ : IsDirected ι fun x1 x2 => x1 ≥ x2
inst✝ : atBot.IsCountablyGenerated
s : ι → Set α
hs : Monotone s
hsm : ∀ (i : ι), NullMeasurableSet (s i) μ
hfin : ∃ i, μ (s i) ≠ ⊤
this : Nonempty ι
x : ℕ → ι
hxm : Antitone x
hx : Tendsto x atTop atBot
i : ι
n : ℕ
hn : x n ≤ i
⊢ ∃ i_1, s (x i_1) ⊆ s i

Tactic:
exact ⟨n, hs hn⟩

Result:
no goals

Proof state:
α : Type u_1
ι : Type u_5
m : MeasurableSpace α
μ : Measure α
inst✝² : Preorder ι
inst✝¹ : IsDirected ι fun x1 x2 => x1 ≥ x2
inst✝ : atBot.IsCountablyGenerated
s : ι → Set α
hs : Monotone s
hsm : ∀ (i : ι), NullMeasurableSet (s i) μ
hfin : ∃ i, μ (s i) ≠ ⊤
this : Nonempty ι
x : ℕ → ι
hxm : Antitone x
hx : Tendsto x atTop atBot
i : ι
⊢ ∃ i_1, s (x i_1) ⊆ s i

Tactic:
rcases (hx.eventually_le_atBot i).exists with ⟨n, hn⟩

Result:
case intro
α : Type u_1
ι : Type u_5
m : MeasurableSpace α
μ : Measure α
inst✝² : Preorder ι
inst✝¹ : IsDirected ι fun x1 x2 => x1 ≥ x2
inst✝ : atBot.IsCountablyGenerated
s : ι → Set α
hs : Monotone s
hsm : ∀ (i : ι), NullMeasurableSet (s i) μ
hfin : ∃ i, μ (s i) ≠ ⊤
this : Nonempty ι
x : ℕ → ι
hxm : Antitone x
hx : Tendsto x atTop atBot
i : ι
n : ℕ
hn : x n ≤ i
⊢ ∃ i_1, s (x i_1) ⊆ s i