-- Mathlib/MeasureTheory/Integral/SetIntegral.lean
theorem tendsto_setIntegral_of_antitone
    {ι : Type*} [Preorder ι] [(atTop : Filter ι).IsCountablyGenerated]
    {s : ι → Set X} (hsm : ∀ i, MeasurableSet (s i)) (h_anti : Antitone s)
    (hfi : ∃ i, IntegrableOn f (s i) μ) :
    Tendsto (fun i ↦ ∫ x in s i, f x ∂μ) atTop (𝓝 (∫ x in ⋂ n, s n, f x ∂μ))

Proof state:
case intro.refine_1
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
f : X → E
μ : Measure X
ι : Type u_5
inst✝¹ : Preorder ι
inst✝ : atTop.IsCountablyGenerated
s : ι → Set X
hsm : ∀ (i : ι), MeasurableSet (s i)
h_anti : Antitone s
hne : atTop.NeBot
this : IsDirected ι fun x1 x2 => x1 ≤ x2
i₀ : ι
hi₀ : IntegrableOn f (s i₀) μ
⊢ Monotone fun x => s i₀ \ s x

Tactic:
exact fun i j h ↦ diff_subset_diff_right (h_anti h)

Result:
no goals

Proof state:
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
f : X → E
μ : Measure X
ι : Type u_5
inst✝¹ : Preorder ι
inst✝ : atTop.IsCountablyGenerated
s : ι → Set X
hsm : ∀ (i : ι), MeasurableSet (s i)
h_anti : Antitone s
hne : atTop.NeBot
this✝ : IsDirected ι fun x1 x2 => x1 ≤ x2
i₀ : ι
hi₀ : IntegrableOn f (s i₀) μ
this :
  Tendsto (fun x => ∫ (x : X) in s i₀, f x ∂μ - ∫ (x : X) in s i₀ \ s x, f x ∂μ) atTop
    (𝓝 (∫ (x : X) in s i₀, f x ∂μ - ∫ (x : X) in ⋃ i, s i₀ \ s i, f x ∂μ))
⊢ MeasurableSet (⋂ i, s i)

Tactic:
exact .iInter_of_antitone h_anti hsm

Result:
no goals

Proof state:
case intro.refine_2
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
f : X → E
μ : Measure X
ι : Type u_5
inst✝¹ : Preorder ι
inst✝ : atTop.IsCountablyGenerated
s : ι → Set X
hsm : ∀ (i : ι), MeasurableSet (s i)
h_anti : Antitone s
hne : atTop.NeBot
this : IsDirected ι fun x1 x2 => x1 ≤ x2
i₀ : ι
hi₀ : IntegrableOn f (s i₀) μ
⊢ IntegrableOn f (s i₀ \ ⋂ i, s i) μ

Tactic:
exact hi₀.mono_set diff_subset

Result:
no goals

Proof state:
case h.e'_5.h.e'_3
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
f : X → E
μ : Measure X
ι : Type u_5
inst✝¹ : Preorder ι
inst✝ : atTop.IsCountablyGenerated
s : ι → Set X
hsm : ∀ (i : ι), MeasurableSet (s i)
h_anti : Antitone s
hne : atTop.NeBot
this✝ : IsDirected ι fun x1 x2 => x1 ≤ x2
i₀ : ι
hi₀ : IntegrableOn f (s i₀) μ
this :
  Tendsto (fun x => ∫ (x : X) in s i₀, f x ∂μ - ∫ (x : X) in s i₀ \ s x, f x ∂μ) atTop
    (𝓝 (∫ (x : X) in s i₀, f x ∂μ - ∫ (x : X) in ⋃ i, s i₀ \ s i, f x ∂μ))
⊢ ∫ (x : X) in ⋂ n, s n, f x ∂μ = ∫ (x : X) in s i₀, f x ∂μ - ∫ (x : X) in ⋃ i, s i₀ \ s i, f x ∂μ

Tactic:
rw [← diff_iInter, integral_diff _ hi₀ (iInter_subset _ _), sub_sub_cancel]

Result:
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
f : X → E
μ : Measure X
ι : Type u_5
inst✝¹ : Preorder ι
inst✝ : atTop.IsCountablyGenerated
s : ι → Set X
hsm : ∀ (i : ι), MeasurableSet (s i)
h_anti : Antitone s
hne : atTop.NeBot
this✝ : IsDirected ι fun x1 x2 => x1 ≤ x2
i₀ : ι
hi₀ : IntegrableOn f (s i₀) μ
this :
  Tendsto (fun x => ∫ (x : X) in s i₀, f x ∂μ - ∫ (x : X) in s i₀ \ s x, f x ∂μ) atTop
    (𝓝 (∫ (x : X) in s i₀, f x ∂μ - ∫ (x : X) in ⋃ i, s i₀ \ s i, f x ∂μ))
⊢ MeasurableSet (⋂ i, s i)

Proof state:
case intro
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
f : X → E
μ : Measure X
ι : Type u_5
inst✝¹ : Preorder ι
inst✝ : atTop.IsCountablyGenerated
s : ι → Set X
hsm : ∀ (i : ι), MeasurableSet (s i)
h_anti : Antitone s
hne : atTop.NeBot
this : IsDirected ι fun x1 x2 => x1 ≤ x2
i₀ : ι
hi₀ : IntegrableOn f (s i₀) μ
⊢ Tendsto (fun x => ∫ (x : X) in s i₀ \ s x, f x ∂μ) atTop (𝓝 (∫ (x : X) in ⋃ i, s i₀ \ s i, f x ∂μ))

Tactic:
refine tendsto_setIntegral_of_monotone (by measurability) ?_ ?_

Result:
case intro.refine_1
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
f : X → E
μ : Measure X
ι : Type u_5
inst✝¹ : Preorder ι
inst✝ : atTop.IsCountablyGenerated
s : ι → Set X
hsm : ∀ (i : ι), MeasurableSet (s i)
h_anti : Antitone s
hne : atTop.NeBot
this : IsDirected ι fun x1 x2 => x1 ≤ x2
i₀ : ι
hi₀ : IntegrableOn f (s i₀) μ
⊢ Monotone fun x => s i₀ \ s x

case intro.refine_2
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
f : X → E
μ : Measure X
ι : Type u_5
inst✝¹ : Preorder ι
inst✝ : atTop.IsCountablyGenerated
s : ι → Set X
hsm : ∀ (i : ι), MeasurableSet (s i)
h_anti : Antitone s
hne : atTop.NeBot
this : IsDirected ι fun x1 x2 => x1 ≤ x2
i₀ : ι
hi₀ : IntegrableOn f (s i₀) μ
⊢ IntegrableOn f (⋃ n, s i₀ \ s n) μ

Proof state:
case intro.refine_2
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
f : X → E
μ : Measure X
ι : Type u_5
inst✝¹ : Preorder ι
inst✝ : atTop.IsCountablyGenerated
s : ι → Set X
hsm : ∀ (i : ι), MeasurableSet (s i)
h_anti : Antitone s
hne : atTop.NeBot
this : IsDirected ι fun x1 x2 => x1 ≤ x2
i₀ : ι
hi₀ : IntegrableOn f (s i₀) μ
⊢ IntegrableOn f (⋃ n, s i₀ \ s n) μ

Tactic:
rw [← diff_iInter]

Result:
case intro.refine_2
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
f : X → E
μ : Measure X
ι : Type u_5
inst✝¹ : Preorder ι
inst✝ : atTop.IsCountablyGenerated
s : ι → Set X
hsm : ∀ (i : ι), MeasurableSet (s i)
h_anti : Antitone s
hne : atTop.NeBot
this : IsDirected ι fun x1 x2 => x1 ≤ x2
i₀ : ι
hi₀ : IntegrableOn f (s i₀) μ
⊢ IntegrableOn f (s i₀ \ ⋂ i, s i) μ

Proof state:
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
f : X → E
μ : Measure X
ι : Type u_5
inst✝¹ : Preorder ι
inst✝ : atTop.IsCountablyGenerated
s : ι → Set X
hsm : ∀ (i : ι), MeasurableSet (s i)
h_anti : Antitone s
hfi : ∃ i, IntegrableOn f (s i) μ
hne : atTop.NeBot
this : IsDirected ι fun x1 x2 => x1 ≤ x2
⊢ Tendsto (fun i => ∫ (x : X) in s i, f x ∂μ) atTop (𝓝 (∫ (x : X) in ⋂ n, s n, f x ∂μ))

Tactic:
rcases hfi with ⟨i₀, hi₀⟩

Result:
case intro
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
f : X → E
μ : Measure X
ι : Type u_5
inst✝¹ : Preorder ι
inst✝ : atTop.IsCountablyGenerated
s : ι → Set X
hsm : ∀ (i : ι), MeasurableSet (s i)
h_anti : Antitone s
hne : atTop.NeBot
this : IsDirected ι fun x1 x2 => x1 ≤ x2
i₀ : ι
hi₀ : IntegrableOn f (s i₀) μ
⊢ Tendsto (fun i => ∫ (x : X) in s i, f x ∂μ) atTop (𝓝 (∫ (x : X) in ⋂ n, s n, f x ∂μ))

Proof state:
case intro
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
f : X → E
μ : Measure X
ι : Type u_5
inst✝¹ : Preorder ι
inst✝ : atTop.IsCountablyGenerated
s : ι → Set X
hsm : ∀ (i : ι), MeasurableSet (s i)
h_anti : Antitone s
hne : atTop.NeBot
this : IsDirected ι fun x1 x2 => x1 ≤ x2
i₀ : ι
hi₀ : IntegrableOn f (s i₀) μ
⊢ Tendsto (fun x => ∫ (x : X) in s i₀, f x ∂μ - ∫ (x : X) in s i₀ \ s x, f x ∂μ) atTop
    (𝓝 (∫ (x : X) in s i₀, f x ∂μ - ∫ (x : X) in ⋃ i, s i₀ \ s i, f x ∂μ))

Tactic:
apply tendsto_const_nhds.sub

Result:
case intro
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
f : X → E
μ : Measure X
ι : Type u_5
inst✝¹ : Preorder ι
inst✝ : atTop.IsCountablyGenerated
s : ι → Set X
hsm : ∀ (i : ι), MeasurableSet (s i)
h_anti : Antitone s
hne : atTop.NeBot
this : IsDirected ι fun x1 x2 => x1 ≤ x2
i₀ : ι
hi₀ : IntegrableOn f (s i₀) μ
⊢ Tendsto (fun x => ∫ (x : X) in s i₀ \ s x, f x ∂μ) atTop (𝓝 (∫ (x : X) in ⋃ i, s i₀ \ s i, f x ∂μ))