-- Mathlib/MeasureTheory/Integral/Lebesgue.lean
theorem lintegral_tendsto_of_tendsto_of_antitone {f : ℕ → α → ℝ≥0∞} {F : α → ℝ≥0∞}
    (hf : ∀ n, AEMeasurable (f n) μ) (h_anti : ∀ᵐ x ∂μ, Antitone fun n ↦ f n x)
    (h0 : ∫⁻ a, f 0 a ∂μ ≠ ∞)
    (h_tendsto : ∀ᵐ x ∂μ, Tendsto (fun n ↦ f n x) atTop (𝓝 (F x))) :
    Tendsto (fun n ↦ ∫⁻ x, f n x ∂μ) atTop (𝓝 (∫⁻ x, F x ∂μ))

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ℕ → α → ℝ≥0∞
F : α → ℝ≥0∞
hf : ∀ (n : ℕ), AEMeasurable (f n) μ
h_anti : ∀ᵐ (x : α) ∂μ, Antitone fun n => f n x
h0 : ∫⁻ (a : α), f 0 a ∂μ ≠ ⊤
h_tendsto : ∀ᵐ (x : α) ∂μ, Tendsto (fun n => f n x) atTop (𝓝 (F x))
this : Antitone fun n => ∫⁻ (x : α), f n x ∂μ
⊢ ∫⁻ (x : α), F x ∂μ = ∫⁻ (a : α), ⨅ n, f n a ∂μ

Tactic:
refine lintegral_congr_ae ?_

Result:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ℕ → α → ℝ≥0∞
F : α → ℝ≥0∞
hf : ∀ (n : ℕ), AEMeasurable (f n) μ
h_anti : ∀ᵐ (x : α) ∂μ, Antitone fun n => f n x
h0 : ∫⁻ (a : α), f 0 a ∂μ ≠ ⊤
h_tendsto : ∀ᵐ (x : α) ∂μ, Tendsto (fun n => f n x) atTop (𝓝 (F x))
this : Antitone fun n => ∫⁻ (x : α), f n x ∂μ
⊢ F =ᶠ[ae μ] fun a => ⨅ n, f n a

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ℕ → α → ℝ≥0∞
F : α → ℝ≥0∞
hf : ∀ (n : ℕ), AEMeasurable (f n) μ
h_anti : ∀ᵐ (x : α) ∂μ, Antitone fun n => f n x
h0 : ∫⁻ (a : α), f 0 a ∂μ ≠ ⊤
h_tendsto : ∀ᵐ (x : α) ∂μ, Tendsto (fun n => f n x) atTop (𝓝 (F x))
this : Antitone fun n => ∫⁻ (x : α), f n x ∂μ
⊢ ∫⁻ (x : α), F x ∂μ = ⨅ n, ∫⁻ (x : α), f n x ∂μ

Tactic:
rw [← lintegral_iInf' hf h_anti h0]

Result:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ℕ → α → ℝ≥0∞
F : α → ℝ≥0∞
hf : ∀ (n : ℕ), AEMeasurable (f n) μ
h_anti : ∀ᵐ (x : α) ∂μ, Antitone fun n => f n x
h0 : ∫⁻ (a : α), f 0 a ∂μ ≠ ⊤
h_tendsto : ∀ᵐ (x : α) ∂μ, Tendsto (fun n => f n x) atTop (𝓝 (F x))
this : Antitone fun n => ∫⁻ (x : α), f n x ∂μ
⊢ ∫⁻ (x : α), F x ∂μ = ∫⁻ (a : α), ⨅ n, f n a ∂μ

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ℕ → α → ℝ≥0∞
F : α → ℝ≥0∞
hf : ∀ (n : ℕ), AEMeasurable (f n) μ
h_anti : ∀ᵐ (x : α) ∂μ, Antitone fun n => f n x
h0 : ∫⁻ (a : α), f 0 a ∂μ ≠ ⊤
h_tendsto : ∀ᵐ (x : α) ∂μ, Tendsto (fun n => f n x) atTop (𝓝 (F x))
this : Antitone fun n => ∫⁻ (x : α), f n x ∂μ
⊢ F =ᶠ[ae μ] fun a => ⨅ n, f n a

Tactic:
filter_upwards [h_anti, h_tendsto] with _ hx_anti hx_tendsto
  using tendsto_nhds_unique hx_tendsto (tendsto_atTop_iInf hx_anti)

Result:
no goals

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ℕ → α → ℝ≥0∞
F : α → ℝ≥0∞
hf : ∀ (n : ℕ), AEMeasurable (f n) μ
h_anti : ∀ᵐ (x : α) ∂μ, Antitone fun n => f n x
h0 : ∫⁻ (a : α), f 0 a ∂μ ≠ ⊤
h_tendsto : ∀ᵐ (x : α) ∂μ, Tendsto (fun n => f n x) atTop (𝓝 (F x))
⊢ Tendsto (fun n => ∫⁻ (x : α), f n x ∂μ) atTop (𝓝 (∫⁻ (x : α), F x ∂μ))

Tactic:
have : Antitone fun n ↦ ∫⁻ x, f n x ∂μ := fun i j hij ↦
  lintegral_mono_ae (h_anti.mono fun x hx ↦ hx hij)

Result:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ℕ → α → ℝ≥0∞
F : α → ℝ≥0∞
hf : ∀ (n : ℕ), AEMeasurable (f n) μ
h_anti : ∀ᵐ (x : α) ∂μ, Antitone fun n => f n x
h0 : ∫⁻ (a : α), f 0 a ∂μ ≠ ⊤
h_tendsto : ∀ᵐ (x : α) ∂μ, Tendsto (fun n => f n x) atTop (𝓝 (F x))
this : Antitone fun n => ∫⁻ (x : α), f n x ∂μ
⊢ Tendsto (fun n => ∫⁻ (x : α), f n x ∂μ) atTop (𝓝 (∫⁻ (x : α), F x ∂μ))

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ℕ → α → ℝ≥0∞
F : α → ℝ≥0∞
hf : ∀ (n : ℕ), AEMeasurable (f n) μ
h_anti : ∀ᵐ (x : α) ∂μ, Antitone fun n => f n x
h0 : ∫⁻ (a : α), f 0 a ∂μ ≠ ⊤
h_tendsto : ∀ᵐ (x : α) ∂μ, Tendsto (fun n => f n x) atTop (𝓝 (F x))
this : Antitone fun n => ∫⁻ (x : α), f n x ∂μ
key : ∫⁻ (x : α), F x ∂μ = ⨅ n, ∫⁻ (x : α), f n x ∂μ
⊢ Tendsto (fun n => ∫⁻ (x : α), f n x ∂μ) atTop (𝓝 (∫⁻ (x : α), F x ∂μ))

Tactic:
rw [key]

Result:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ℕ → α → ℝ≥0∞
F : α → ℝ≥0∞
hf : ∀ (n : ℕ), AEMeasurable (f n) μ
h_anti : ∀ᵐ (x : α) ∂μ, Antitone fun n => f n x
h0 : ∫⁻ (a : α), f 0 a ∂μ ≠ ⊤
h_tendsto : ∀ᵐ (x : α) ∂μ, Tendsto (fun n => f n x) atTop (𝓝 (F x))
this : Antitone fun n => ∫⁻ (x : α), f n x ∂μ
key : ∫⁻ (x : α), F x ∂μ = ⨅ n, ∫⁻ (x : α), f n x ∂μ
⊢ Tendsto (fun n => ∫⁻ (x : α), f n x ∂μ) atTop (𝓝 (⨅ n, ∫⁻ (x : α), f n x ∂μ))

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ℕ → α → ℝ≥0∞
F : α → ℝ≥0∞
hf : ∀ (n : ℕ), AEMeasurable (f n) μ
h_anti : ∀ᵐ (x : α) ∂μ, Antitone fun n => f n x
h0 : ∫⁻ (a : α), f 0 a ∂μ ≠ ⊤
h_tendsto : ∀ᵐ (x : α) ∂μ, Tendsto (fun n => f n x) atTop (𝓝 (F x))
this : Antitone fun n => ∫⁻ (x : α), f n x ∂μ
key : ∫⁻ (x : α), F x ∂μ = ⨅ n, ∫⁻ (x : α), f n x ∂μ
⊢ Tendsto (fun n => ∫⁻ (x : α), f n x ∂μ) atTop (𝓝 (⨅ n, ∫⁻ (x : α), f n x ∂μ))

Tactic:
exact tendsto_atTop_iInf this

Result:
no goals

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ℕ → α → ℝ≥0∞
F : α → ℝ≥0∞
hf : ∀ (n : ℕ), AEMeasurable (f n) μ
h_anti : ∀ᵐ (x : α) ∂μ, Antitone fun n => f n x
h0 : ∫⁻ (a : α), f 0 a ∂μ ≠ ⊤
h_tendsto : ∀ᵐ (x : α) ∂μ, Tendsto (fun n => f n x) atTop (𝓝 (F x))
this : Antitone fun n => ∫⁻ (x : α), f n x ∂μ
⊢ Tendsto (fun n => ∫⁻ (x : α), f n x ∂μ) atTop (𝓝 (∫⁻ (x : α), F x ∂μ))

Tactic:
suffices key : ∫⁻ x, F x ∂μ = ⨅ n, ∫⁻ x, f n x ∂μ by
  rw [key]
  exact tendsto_atTop_iInf this

Result:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ℕ → α → ℝ≥0∞
F : α → ℝ≥0∞
hf : ∀ (n : ℕ), AEMeasurable (f n) μ
h_anti : ∀ᵐ (x : α) ∂μ, Antitone fun n => f n x
h0 : ∫⁻ (a : α), f 0 a ∂μ ≠ ⊤
h_tendsto : ∀ᵐ (x : α) ∂μ, Tendsto (fun n => f n x) atTop (𝓝 (F x))
this : Antitone fun n => ∫⁻ (x : α), f n x ∂μ
⊢ ∫⁻ (x : α), F x ∂μ = ⨅ n, ∫⁻ (x : α), f n x ∂μ