-- Mathlib/MeasureTheory/OuterMeasure/Basic.lean
theorem measure_iUnion_of_tendsto_zero {ι} (μ : F) {s : ι → Set α} (l : Filter ι) [NeBot l]
    (h0 : Tendsto (fun k => μ ((⋃ n, s n) \ s k)) l (𝓝 0)) : μ (⋃ n, s n) = ⨆ n, μ (s n)

Proof state:
α : Type u_1
F : Type u_3
inst✝² : FunLike F (Set α) ℝ≥0∞
inst✝¹ : OuterMeasureClass F α
ι : Type u_4
μ : F
s : ι → Set α
l : Filter ι
inst✝ : l.NeBot
S : Set α := ⋃ n, s n
h0 : Tendsto (fun k => μ (S \ s k)) l (𝓝 0)
M : ℝ≥0∞ := ⨆ n, μ (s n)
k : ι
⊢ μ (S ∩ s k) + μ (S \ s k) ≤ μ (s k) + μ (S \ s k)

Tactic:
gcongr

Result:
case bc.h
α : Type u_1
F : Type u_3
inst✝² : FunLike F (Set α) ℝ≥0∞
inst✝¹ : OuterMeasureClass F α
ι : Type u_4
μ : F
s : ι → Set α
l : Filter ι
inst✝ : l.NeBot
S : Set α := ⋃ n, s n
h0 : Tendsto (fun k => μ (S \ s k)) l (𝓝 0)
M : ℝ≥0∞ := ⨆ n, μ (s n)
k : ι
⊢ S ∩ s k ⊆ s k

Proof state:
α : Type u_1
F : Type u_3
inst✝² : FunLike F (Set α) ℝ≥0∞
inst✝¹ : OuterMeasureClass F α
ι : Type u_4
μ : F
s : ι → Set α
l : Filter ι
inst✝ : l.NeBot
h0 : Tendsto (fun k => μ ((⋃ n, s n) \ s k)) l (𝓝 0)
⊢ μ (⋃ n, s n) = ⨆ n, μ (s n)

Tactic:
refine le_antisymm ?_ <| iSup_le fun n ↦ measure_mono <| subset_iUnion _ _

Result:
α : Type u_1
F : Type u_3
inst✝² : FunLike F (Set α) ℝ≥0∞
inst✝¹ : OuterMeasureClass F α
ι : Type u_4
μ : F
s : ι → Set α
l : Filter ι
inst✝ : l.NeBot
h0 : Tendsto (fun k => μ ((⋃ n, s n) \ s k)) l (𝓝 0)
⊢ μ (⋃ n, s n) ≤ ⨆ n, μ (s n)

Proof state:
case bc.h
α : Type u_1
F : Type u_3
inst✝² : FunLike F (Set α) ℝ≥0∞
inst✝¹ : OuterMeasureClass F α
ι : Type u_4
μ : F
s : ι → Set α
l : Filter ι
inst✝ : l.NeBot
S : Set α := ⋃ n, s n
h0 : Tendsto (fun k => μ (S \ s k)) l (𝓝 0)
M : ℝ≥0∞ := ⨆ n, μ (s n)
k : ι
⊢ S ∩ s k ⊆ s k

Tactic:
apply inter_subset_right

Result:
no goals

Proof state:
α : Type u_1
F : Type u_3
inst✝² : FunLike F (Set α) ℝ≥0∞
inst✝¹ : OuterMeasureClass F α
ι : Type u_4
μ : F
s : ι → Set α
l : Filter ι
inst✝ : l.NeBot
S : Set α := ⋃ n, s n
h0 : Tendsto (fun k => μ (S \ s k)) l (𝓝 0)
⊢ μ S ≤ ⨆ n, μ (s n)

Tactic:
set M := ⨆ n, μ (s n)

Result:
α : Type u_1
F : Type u_3
inst✝² : FunLike F (Set α) ℝ≥0∞
inst✝¹ : OuterMeasureClass F α
ι : Type u_4
μ : F
s : ι → Set α
l : Filter ι
inst✝ : l.NeBot
S : Set α := ⋃ n, s n
h0 : Tendsto (fun k => μ (S \ s k)) l (𝓝 0)
M : ℝ≥0∞ := ⨆ n, μ (s n)
⊢ μ S ≤ M

Proof state:
α : Type u_1
F : Type u_3
inst✝² : FunLike F (Set α) ℝ≥0∞
inst✝¹ : OuterMeasureClass F α
ι : Type u_4
μ : F
s : ι → Set α
l : Filter ι
inst✝ : l.NeBot
h0 : Tendsto (fun k => μ ((⋃ n, s n) \ s k)) l (𝓝 0)
⊢ μ (⋃ n, s n) ≤ ⨆ n, μ (s n)

Tactic:
set S := ⋃ n, s n

Result:
α : Type u_1
F : Type u_3
inst✝² : FunLike F (Set α) ℝ≥0∞
inst✝¹ : OuterMeasureClass F α
ι : Type u_4
μ : F
s : ι → Set α
l : Filter ι
inst✝ : l.NeBot
S : Set α := ⋃ n, s n
h0 : Tendsto (fun k => μ (S \ s k)) l (𝓝 0)
⊢ μ S ≤ ⨆ n, μ (s n)

Proof state:
α : Type u_1
F : Type u_3
inst✝² : FunLike F (Set α) ℝ≥0∞
inst✝¹ : OuterMeasureClass F α
ι : Type u_4
μ : F
s : ι → Set α
l : Filter ι
inst✝ : l.NeBot
S : Set α := ⋃ n, s n
h0 : Tendsto (fun k => μ (S \ s k)) l (𝓝 0)
M : ℝ≥0∞ := ⨆ n, μ (s n)
⊢ μ S ≤ M

Tactic:
have A : ∀ k, μ S ≤ M + μ (S \ s k) := fun k ↦ calc
  μ S ≤ μ (S ∩ s k) + μ (S \ s k) := measure_le_inter_add_diff _ _ _
  _ ≤ μ (s k) + μ (S \ s k) := by gcongr; apply inter_subset_right
  _ ≤ M + μ (S \ s k) := by gcongr; exact le_iSup (μ ∘ s) k

Result:
α : Type u_1
F : Type u_3
inst✝² : FunLike F (Set α) ℝ≥0∞
inst✝¹ : OuterMeasureClass F α
ι : Type u_4
μ : F
s : ι → Set α
l : Filter ι
inst✝ : l.NeBot
S : Set α := ⋃ n, s n
h0 : Tendsto (fun k => μ (S \ s k)) l (𝓝 0)
M : ℝ≥0∞ := ⨆ n, μ (s n)
A : ∀ (k : ι), μ S ≤ M + μ (S \ s k)
⊢ μ S ≤ M

Proof state:
α : Type u_1
F : Type u_3
inst✝² : FunLike F (Set α) ℝ≥0∞
inst✝¹ : OuterMeasureClass F α
ι : Type u_4
μ : F
s : ι → Set α
l : Filter ι
inst✝ : l.NeBot
S : Set α := ⋃ n, s n
h0 : Tendsto (fun k => μ (S \ s k)) l (𝓝 0)
M : ℝ≥0∞ := ⨆ n, μ (s n)
k : ι
⊢ μ (s k) + μ (S \ s k) ≤ M + μ (S \ s k)

Tactic:
gcongr

Result:
case bc
α : Type u_1
F : Type u_3
inst✝² : FunLike F (Set α) ℝ≥0∞
inst✝¹ : OuterMeasureClass F α
ι : Type u_4
μ : F
s : ι → Set α
l : Filter ι
inst✝ : l.NeBot
S : Set α := ⋃ n, s n
h0 : Tendsto (fun k => μ (S \ s k)) l (𝓝 0)
M : ℝ≥0∞ := ⨆ n, μ (s n)
k : ι
⊢ μ (s k) ≤ M

Proof state:
α : Type u_1
F : Type u_3
inst✝² : FunLike F (Set α) ℝ≥0∞
inst✝¹ : OuterMeasureClass F α
ι : Type u_4
μ : F
s : ι → Set α
l : Filter ι
inst✝ : l.NeBot
S : Set α := ⋃ n, s n
h0 : Tendsto (fun k => μ (S \ s k)) l (𝓝 0)
M : ℝ≥0∞ := ⨆ n, μ (s n)
A : ∀ (k : ι), μ S ≤ M + μ (S \ s k)
⊢ μ S ≤ M

Tactic:
have B : Tendsto (fun k ↦ M + μ (S \ s k)) l (𝓝 M) := by simpa using tendsto_const_nhds.add h0

Result:
α : Type u_1
F : Type u_3
inst✝² : FunLike F (Set α) ℝ≥0∞
inst✝¹ : OuterMeasureClass F α
ι : Type u_4
μ : F
s : ι → Set α
l : Filter ι
inst✝ : l.NeBot
S : Set α := ⋃ n, s n
h0 : Tendsto (fun k => μ (S \ s k)) l (𝓝 0)
M : ℝ≥0∞ := ⨆ n, μ (s n)
A : ∀ (k : ι), μ S ≤ M + μ (S \ s k)
B : Tendsto (fun k => M + μ (S \ s k)) l (𝓝 M)
⊢ μ S ≤ M

Proof state:
α : Type u_1
F : Type u_3
inst✝² : FunLike F (Set α) ℝ≥0∞
inst✝¹ : OuterMeasureClass F α
ι : Type u_4
μ : F
s : ι → Set α
l : Filter ι
inst✝ : l.NeBot
S : Set α := ⋃ n, s n
h0 : Tendsto (fun k => μ (S \ s k)) l (𝓝 0)
M : ℝ≥0∞ := ⨆ n, μ (s n)
A : ∀ (k : ι), μ S ≤ M + μ (S \ s k)
B : Tendsto (fun k => M + μ (S \ s k)) l (𝓝 M)
⊢ μ S ≤ M

Tactic:
exact ge_of_tendsto' B A

Result:
no goals

Proof state:
α : Type u_1
F : Type u_3
inst✝² : FunLike F (Set α) ℝ≥0∞
inst✝¹ : OuterMeasureClass F α
ι : Type u_4
μ : F
s : ι → Set α
l : Filter ι
inst✝ : l.NeBot
S : Set α := ⋃ n, s n
h0 : Tendsto (fun k => μ (S \ s k)) l (𝓝 0)
M : ℝ≥0∞ := ⨆ n, μ (s n)
A : ∀ (k : ι), μ S ≤ M + μ (S \ s k)
⊢ Tendsto (fun k => M + μ (S \ s k)) l (𝓝 M)

Tactic:
simpa using tendsto_const_nhds.add h0

Result:
no goals

Proof state:
case bc
α : Type u_1
F : Type u_3
inst✝² : FunLike F (Set α) ℝ≥0∞
inst✝¹ : OuterMeasureClass F α
ι : Type u_4
μ : F
s : ι → Set α
l : Filter ι
inst✝ : l.NeBot
S : Set α := ⋃ n, s n
h0 : Tendsto (fun k => μ (S \ s k)) l (𝓝 0)
M : ℝ≥0∞ := ⨆ n, μ (s n)
k : ι
⊢ μ (s k) ≤ M

Tactic:
exact le_iSup (μ ∘ s) k

Result:
no goals