awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.DominatedConvergence
Goal:
α : Type u_2
mα : MeasurableSpace α
f : ℕ → α → ℝ≥0∞
F : α → ℝ≥0∞
μ : Measure α
hf_meas : ∀ (n : ℕ), AEMeasurable (f n) μ
hf_tendsto : Tendsto (fun (i : ℕ) ↦ ∫⁻ (a : α), f i a ∂μ) atTop (𝓝 (∫⁻ (a : α), F a ∂μ))
hf_mono : ∀ᵐ (a : α) ∂μ, Antitone (β := ℝ≥0∞) fun (i : ℕ) ↦ f i a
h_bound : ∀ᵐ (a : α) ∂μ, ∀ (i : ℕ), F a ≤ f i a
h0 : ∫⁻ (a : α), f 0 a ∂μ ≠ ∞
h_int_finite : ∫⁻ (a : α), F a ∂μ ≠ ∞
h_exists : ∀ᵐ (a : α) ∂μ, ∃ (l : ℝ≥0∞), Tendsto (fun (i : ℕ) ↦ f i a) atTop (𝓝 l)
F' : α → ℝ≥0∞ :=
  fun (a : α) ↦
    if h : ∃ (l : ℝ≥0∞), Tendsto (fun (i : ℕ) ↦ f i a) atTop (𝓝 l) then
      h.choose (p := fun (l : ℝ≥0∞) ↦ Tendsto (fun (i : ℕ) ↦ f i a) atTop (𝓝 l))
    else ∞
h :
  ∀ (a : α) (ha : ∃ (l : ℝ≥0∞), Tendsto (fun (i : ℕ) ↦ f i a) atTop (𝓝 l)),
    Tendsto (fun (i : ℕ) ↦ f i a) atTop (𝓝 (F' a))
⊢ ∀ᵐ (a : α) ∂μ, Tendsto (fun (i : ℕ) ↦ f i a) atTop (𝓝 (F' a))

Tactic:
filter_upwards [h_exists] with a ha
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.DominatedConvergence
Goal:
α : Type u_2
mα : MeasurableSpace α
f : ℕ → α → ℝ≥0∞
F : α → ℝ≥0∞
μ : Measure α
hf_meas : ∀ (n : ℕ), AEMeasurable (f n) μ
hf_tendsto : Tendsto (fun (i : ℕ) ↦ ∫⁻ (a : α), f i a ∂μ) atTop (𝓝 (∫⁻ (a : α), F a ∂μ))
hf_mono : ∀ᵐ (a : α) ∂μ, Antitone (β := ℝ≥0∞) fun (i : ℕ) ↦ f i a
h_bound : ∀ᵐ (a : α) ∂μ, ∀ (i : ℕ), F a ≤ f i a
h0 : ∫⁻ (a : α), f 0 a ∂μ ≠ ∞
h_int_finite : ∫⁻ (a : α), F a ∂μ ≠ ∞
h_exists : ∀ᵐ (a : α) ∂μ, ∃ (l : ℝ≥0∞), Tendsto (fun (i : ℕ) ↦ f i a) atTop (𝓝 l)
F' : α → ℝ≥0∞ :=
  fun (a : α) ↦
    if h : ∃ (l : ℝ≥0∞), Tendsto (fun (i : ℕ) ↦ f i a) atTop (𝓝 l) then
      h.choose (p := fun (l : ℝ≥0∞) ↦ Tendsto (fun (i : ℕ) ↦ f i a) atTop (𝓝 l))
    else ∞
a : α
ha : ∃ (l : ℝ≥0∞), Tendsto (fun (i : ℕ) ↦ f i a) atTop (𝓝 l)
h :
  Tendsto (fun (i : ℕ) ↦ f i a) atTop (𝓝 (ha.choose (p := fun (l : ℝ≥0∞) ↦ Tendsto (fun (i : ℕ) ↦ f i a) atTop (𝓝 l))))
⊢ Tendsto (fun (i : ℕ) ↦ f i a) atTop (𝓝 (F' a))

Tactic:
simp_rw [F', dif_pos ha]

Premises used: dif_pos
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.DominatedConvergence
Goal:
α : Type u_2
mα : MeasurableSpace α
f : ℕ → α → ℝ≥0∞
F : α → ℝ≥0∞
μ : Measure α
hf_meas : ∀ (n : ℕ), AEMeasurable (f n) μ
hf_tendsto : Tendsto (fun (i : ℕ) ↦ ∫⁻ (a : α), f i a ∂μ) atTop (𝓝 (∫⁻ (a : α), F a ∂μ))
hf_mono : ∀ᵐ (a : α) ∂μ, Antitone (β := ℝ≥0∞) fun (i : ℕ) ↦ f i a
h_bound : ∀ᵐ (a : α) ∂μ, ∀ (i : ℕ), F a ≤ f i a
h0 : ∫⁻ (a : α), f 0 a ∂μ ≠ ∞
h_int_finite : ∫⁻ (a : α), F a ∂μ ≠ ∞
h_exists : ∀ᵐ (a : α) ∂μ, ∃ (l : ℝ≥0∞), Tendsto (fun (i : ℕ) ↦ f i a) atTop (𝓝 l)
F' : α → ℝ≥0∞ :=
  fun (a : α) ↦
    if h : ∃ (l : ℝ≥0∞), Tendsto (fun (i : ℕ) ↦ f i a) atTop (𝓝 l) then
      h.choose (p := fun (l : ℝ≥0∞) ↦ Tendsto (fun (i : ℕ) ↦ f i a) atTop (𝓝 l))
    else ∞
a : α
ha : ∃ (l : ℝ≥0∞), Tendsto (fun (i : ℕ) ↦ f i a) atTop (𝓝 l)
⊢ Tendsto (fun (i : ℕ) ↦ f i a) atTop (𝓝 (ha.choose (p := fun (l : ℝ≥0∞) ↦ Tendsto (fun (i : ℕ) ↦ f i a) atTop (𝓝 l))))

Tactic:
ha.choose_spec

Premises used: Exists.choose_spec
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.DominatedConvergence
Goal:
α : Type u_2
mα : MeasurableSpace α
f : ℕ → α → ℝ≥0∞
F : α → ℝ≥0∞
μ : Measure α
hf_meas : ∀ (n : ℕ), AEMeasurable (f n) μ
hf_tendsto : Tendsto (fun (i : ℕ) ↦ ∫⁻ (a : α), f i a ∂μ) atTop (𝓝 (∫⁻ (a : α), F a ∂μ))
hf_mono : ∀ᵐ (a : α) ∂μ, Antitone (β := ℝ≥0∞) fun (i : ℕ) ↦ f i a
h_bound : ∀ᵐ (a : α) ∂μ, ∀ (i : ℕ), F a ≤ f i a
h0 : ∫⁻ (a : α), f 0 a ∂μ ≠ ∞
h_int_finite : ∫⁻ (a : α), F a ∂μ ≠ ∞
h_exists : ∀ᵐ (a : α) ∂μ, ∃ (l : ℝ≥0∞), Tendsto (fun (i : ℕ) ↦ f i a) atTop (𝓝 l)
F' : α → ℝ≥0∞ :=
  fun (a : α) ↦
    if h : ∃ (l : ℝ≥0∞), Tendsto (fun (i : ℕ) ↦ f i a) atTop (𝓝 l) then
      h.choose (p := fun (l : ℝ≥0∞) ↦ Tendsto (fun (i : ℕ) ↦ f i a) atTop (𝓝 l))
    else ∞
a : α
ha : ∃ (l : ℝ≥0∞), Tendsto (fun (i : ℕ) ↦ f i a) atTop (𝓝 l)
⊢ Tendsto (fun (i : ℕ) ↦ f i a) atTop (𝓝 (ha.choose (p := fun (l : ℝ≥0∞) ↦ Tendsto (fun (i : ℕ) ↦ f i a) atTop (𝓝 l))))

Tactic:
exact ha.choose_spec

Premises used: Exists.choose_spec
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.DominatedConvergence
Goal:
α : Type u_2
mα : MeasurableSpace α
f : ℕ → α → ℝ≥0∞
F : α → ℝ≥0∞
μ : Measure α
hf_meas : ∀ (n : ℕ), AEMeasurable (f n) μ
hf_tendsto : Tendsto (fun (i : ℕ) ↦ ∫⁻ (a : α), f i a ∂μ) atTop (𝓝 (∫⁻ (a : α), F a ∂μ))
hf_mono : ∀ᵐ (a : α) ∂μ, Antitone (β := ℝ≥0∞) fun (i : ℕ) ↦ f i a
h_bound : ∀ᵐ (a : α) ∂μ, ∀ (i : ℕ), F a ≤ f i a
h0 : ∫⁻ (a : α), f 0 a ∂μ ≠ ∞
h_int_finite : ∫⁻ (a : α), F a ∂μ ≠ ∞
h_exists : ∀ᵐ (a : α) ∂μ, ∃ (l : ℝ≥0∞), Tendsto (fun (i : ℕ) ↦ f i a) atTop (𝓝 l)
F' : α → ℝ≥0∞ :=
  fun (a : α) ↦
    if h : ∃ (l : ℝ≥0∞), Tendsto (fun (i : ℕ) ↦ f i a) atTop (𝓝 l) then
      h.choose (p := fun (l : ℝ≥0∞) ↦ Tendsto (fun (i : ℕ) ↦ f i a) atTop (𝓝 l))
    else ∞
⊢ ∀ᵐ (a : α) ∂μ, Tendsto (fun (i : ℕ) ↦ f i a) atTop (𝓝 (F' a))

Tactic:
have hF'_tendsto : ∀ᵐ a ∂μ, Tendsto (fun i ↦ f i a) atTop (𝓝 (F' a)) := by
    filter_upwards [h_exists] with a ha
    simp_rw [F', dif_pos ha]
    exact ha.choose_spec
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.DominatedConvergence
Goal:
α : Type u_2
mα : MeasurableSpace α
f : ℕ → α → ℝ≥0∞
F : α → ℝ≥0∞
μ : Measure α
hf_meas : ∀ (n : ℕ), AEMeasurable (f n) μ
hf_tendsto : Tendsto (fun (i : ℕ) ↦ ∫⁻ (a : α), f i a ∂μ) atTop (𝓝 (∫⁻ (a : α), F a ∂μ))
hf_mono : ∀ᵐ (a : α) ∂μ, Antitone (β := ℝ≥0∞) fun (i : ℕ) ↦ f i a
h_bound : ∀ᵐ (a : α) ∂μ, ∀ (i : ℕ), F a ≤ f i a
h0 : ∫⁻ (a : α), f 0 a ∂μ ≠ ∞
h_int_finite : ∫⁻ (a : α), F a ∂μ ≠ ∞
h_exists : ∀ᵐ (a : α) ∂μ, ∃ (l : ℝ≥0∞), Tendsto (fun (i : ℕ) ↦ f i a) atTop (𝓝 l)
F' : α → ℝ≥0∞ :=
  fun (a : α) ↦
    if h : ∃ (l : ℝ≥0∞), Tendsto (fun (i : ℕ) ↦ f i a) atTop (𝓝 l) then
      h.choose (p := fun (l : ℝ≥0∞) ↦ Tendsto (fun (i : ℕ) ↦ f i a) atTop (𝓝 l))
    else ∞
hF'_tendsto : ∀ᵐ (a : α) ∂μ, Tendsto (fun (i : ℕ) ↦ f i a) atTop (𝓝 (F' a))
this : F' =ᶠ[ae μ] F
a : α
h_eq : F' a = F a
h_tendsto : Tendsto (fun (i : ℕ) ↦ f i a) atTop (𝓝 (F' a))
⊢ Tendsto (fun (i : ℕ) ↦ f i a) atTop (𝓝 (F a))

Tactic:
h_eq ▸ h_tendsto

Premises used: Eq.rec
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.DominatedConvergence
Goal:
α : Type u_2
mα : MeasurableSpace α
f : ℕ → α → ℝ≥0∞
F : α → ℝ≥0∞
μ : Measure α
hf_meas : ∀ (n : ℕ), AEMeasurable (f n) μ
hf_tendsto : Tendsto (fun (i : ℕ) ↦ ∫⁻ (a : α), f i a ∂μ) atTop (𝓝 (∫⁻ (a : α), F a ∂μ))
hf_mono : ∀ᵐ (a : α) ∂μ, Antitone (β := ℝ≥0∞) fun (i : ℕ) ↦ f i a
h_bound : ∀ᵐ (a : α) ∂μ, ∀ (i : ℕ), F a ≤ f i a
h0 : ∫⁻ (a : α), f 0 a ∂μ ≠ ∞
h_int_finite : ∫⁻ (a : α), F a ∂μ ≠ ∞
h_exists : ∀ᵐ (a : α) ∂μ, ∃ (l : ℝ≥0∞), Tendsto (fun (i : ℕ) ↦ f i a) atTop (𝓝 l)
F' : α → ℝ≥0∞ :=
  fun (a : α) ↦
    if h : ∃ (l : ℝ≥0∞), Tendsto (fun (i : ℕ) ↦ f i a) atTop (𝓝 l) then
      h.choose (p := fun (l : ℝ≥0∞) ↦ Tendsto (fun (i : ℕ) ↦ f i a) atTop (𝓝 l))
    else ∞
hF'_tendsto : ∀ᵐ (a : α) ∂μ, Tendsto (fun (i : ℕ) ↦ f i a) atTop (𝓝 (F' a))
this : F' =ᶠ[ae μ] F
h :
  ∀ (a : α),
    Membership.mem (γ := Set α)
      {x : α |
        Membership.mem (γ := Set α) {x : α | (fun (x : α) ↦ F' x = F x) x} x →
          Membership.mem (γ := Set α)
            {x : α |
              Membership.mem (γ := Set α) {x : α | (fun (a : α) ↦ Tendsto (fun (i : ℕ) ↦ f i a) atTop (𝓝 (F' a))) x} x →
                Membership.mem (γ := Set α) {x : α | (fun (a : α) ↦ Tendsto (fun (i : ℕ) ↦ f i a) atTop (𝓝 (F a))) x} x}
            x}
      a
h₁ h₂ :
  ∀ (a : α) (h_eq : F' a = F a) (h_tendsto : Tendsto (fun (i : ℕ) ↦ f i a) atTop (𝓝 (F' a))),
    Tendsto (fun (i : ℕ) ↦ f i a) atTop (𝓝 (F a))
⊢ ∀ᵐ (a : α) ∂μ, Tendsto (fun (i : ℕ) ↦ f i a) atTop (𝓝 (F a))

Tactic:
filter_upwards [this, hF'_tendsto] with a h_eq h_tendsto using h_eq ▸ h_tendsto
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.DominatedConvergence
Goal:
α : Type u_2
mα : MeasurableSpace α
f : ℕ → α → ℝ≥0∞
F : α → ℝ≥0∞
μ : Measure α
hf_meas : ∀ (n : ℕ), AEMeasurable (f n) μ
hf_tendsto : Tendsto (fun (i : ℕ) ↦ ∫⁻ (a : α), f i a ∂μ) atTop (𝓝 (∫⁻ (a : α), F a ∂μ))
hf_mono : ∀ᵐ (a : α) ∂μ, Antitone (β := ℝ≥0∞) fun (i : ℕ) ↦ f i a
h_bound : ∀ᵐ (a : α) ∂μ, ∀ (i : ℕ), F a ≤ f i a
h0 : ∫⁻ (a : α), f 0 a ∂μ ≠ ∞
h_int_finite : ∫⁻ (a : α), F a ∂μ ≠ ∞
h_exists : ∀ᵐ (a : α) ∂μ, ∃ (l : ℝ≥0∞), Tendsto (fun (i : ℕ) ↦ f i a) atTop (𝓝 l)
F' : α → ℝ≥0∞ :=
  fun (a : α) ↦
    if h : ∃ (l : ℝ≥0∞), Tendsto (fun (i : ℕ) ↦ f i a) atTop (𝓝 l) then
      h.choose (p := fun (l : ℝ≥0∞) ↦ Tendsto (fun (i : ℕ) ↦ f i a) atTop (𝓝 l))
    else ∞
hF'_tendsto : ∀ᵐ (a : α) ∂μ, Tendsto (fun (i : ℕ) ↦ f i a) atTop (𝓝 (F' a))
suffices : F' =ᶠ[ae μ] F
⊢ ∀ᵐ (a : α) ∂μ, Tendsto (fun (i : ℕ) ↦ f i a) atTop (𝓝 (F a))

Tactic:
suffices F' =ᵐ[μ] F by
    filter_upwards [this, hF'_tendsto] with a h_eq h_tendsto using h_eq ▸ h_tendsto
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.DominatedConvergence
Goal:
α : Type u_2
mα : MeasurableSpace α
f : ℕ → α → ℝ≥0∞
F : α → ℝ≥0∞
μ : Measure α
hf_meas : ∀ (n : ℕ), AEMeasurable (f n) μ
hf_tendsto : Tendsto (fun (i : ℕ) ↦ ∫⁻ (a : α), f i a ∂μ) atTop (𝓝 (∫⁻ (a : α), F a ∂μ))
hf_mono : ∀ᵐ (a : α) ∂μ, Antitone (β := ℝ≥0∞) fun (i : ℕ) ↦ f i a
h_bound : ∀ᵐ (a : α) ∂μ, ∀ (i : ℕ), F a ≤ f i a
h0 : ∫⁻ (a : α), f 0 a ∂μ ≠ ∞
h_int_finite : ∫⁻ (a : α), F a ∂μ ≠ ∞
h_exists : ∀ᵐ (a : α) ∂μ, ∃ (l : ℝ≥0∞), Tendsto (fun (i : ℕ) ↦ f i a) atTop (𝓝 l)
F' : α → ℝ≥0∞ :=
  fun (a : α) ↦
    if h : ∃ (l : ℝ≥0∞), Tendsto (fun (i : ℕ) ↦ f i a) atTop (𝓝 l) then
      h.choose (p := fun (l : ℝ≥0∞) ↦ Tendsto (fun (i : ℕ) ↦ f i a) atTop (𝓝 l))
    else ∞
hF'_tendsto : ∀ᵐ (a : α) ∂μ, Tendsto (fun (i : ℕ) ↦ f i a) atTop (𝓝 (F' a))
h : ∀ (a : α) (h_le : ∀ (i : ℕ), F a ≤ f i a) (h_tendsto : Tendsto (fun (i : ℕ) ↦ f i a) atTop (𝓝 (F' a))), F a ≤ F' a
⊢ F ≤ᶠ[ae μ] F'

Tactic:
filter_upwards [h_bound, hF'_tendsto] with a h_le h_tendsto
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.DominatedConvergence
Goal:
α : Type u_2
mα : MeasurableSpace α
f : ℕ → α → ℝ≥0∞
F : α → ℝ≥0∞
μ : Measure α
hf_meas : ∀ (n : ℕ), AEMeasurable (f n) μ
hf_tendsto : Tendsto (fun (i : ℕ) ↦ ∫⁻ (a : α), f i a ∂μ) atTop (𝓝 (∫⁻ (a : α), F a ∂μ))
hf_mono : ∀ᵐ (a : α) ∂μ, Antitone (β := ℝ≥0∞) fun (i : ℕ) ↦ f i a
h_bound : ∀ᵐ (a : α) ∂μ, ∀ (i : ℕ), F a ≤ f i a
h0 : ∫⁻ (a : α), f 0 a ∂μ ≠ ∞
h_int_finite : ∫⁻ (a : α), F a ∂μ ≠ ∞
h_exists : ∀ᵐ (a : α) ∂μ, ∃ (l : ℝ≥0∞), Tendsto (fun (i : ℕ) ↦ f i a) atTop (𝓝 l)
F' : α → ℝ≥0∞ :=
  fun (a : α) ↦
    if h : ∃ (l : ℝ≥0∞), Tendsto (fun (i : ℕ) ↦ f i a) atTop (𝓝 l) then
      h.choose (p := fun (l : ℝ≥0∞) ↦ Tendsto (fun (i : ℕ) ↦ f i a) atTop (𝓝 l))
    else ∞
hF'_tendsto : ∀ᵐ (a : α) ∂μ, Tendsto (fun (i : ℕ) ↦ f i a) atTop (𝓝 (F' a))
a : α
h_le : ∀ (i : ℕ), F a ≤ f i a
h_tendsto : Tendsto (fun (i : ℕ) ↦ f i a) atTop (𝓝 (F' a))
⊢ F a ≤ F' a

Tactic:
ge_of_tendsto' h_tendsto (fun m ↦ h_le _)

Premises used: ge_of_tendsto'
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.DominatedConvergence
Goal:
α : Type u_2
mα : MeasurableSpace α
f : ℕ → α → ℝ≥0∞
F : α → ℝ≥0∞
μ : Measure α
hf_meas : ∀ (n : ℕ), AEMeasurable (f n) μ
hf_tendsto : Tendsto (fun (i : ℕ) ↦ ∫⁻ (a : α), f i a ∂μ) atTop (𝓝 (∫⁻ (a : α), F a ∂μ))
hf_mono : ∀ᵐ (a : α) ∂μ, Antitone (β := ℝ≥0∞) fun (i : ℕ) ↦ f i a
h_bound : ∀ᵐ (a : α) ∂μ, ∀ (i : ℕ), F a ≤ f i a
h0 : ∫⁻ (a : α), f 0 a ∂μ ≠ ∞
h_int_finite : ∫⁻ (a : α), F a ∂μ ≠ ∞
h_exists : ∀ᵐ (a : α) ∂μ, ∃ (l : ℝ≥0∞), Tendsto (fun (i : ℕ) ↦ f i a) atTop (𝓝 l)
F' : α → ℝ≥0∞ :=
  fun (a : α) ↦
    if h : ∃ (l : ℝ≥0∞), Tendsto (fun (i : ℕ) ↦ f i a) atTop (𝓝 l) then
      h.choose (p := fun (l : ℝ≥0∞) ↦ Tendsto (fun (i : ℕ) ↦ f i a) atTop (𝓝 l))
    else ∞
hF'_tendsto : ∀ᵐ (a : α) ∂μ, Tendsto (fun (i : ℕ) ↦ f i a) atTop (𝓝 (F' a))
a : α
h_le : ∀ (i : ℕ), F a ≤ f i a
h_tendsto : Tendsto (fun (i : ℕ) ↦ f i a) atTop (𝓝 (F' a))
⊢ F a ≤ F' a

Tactic:
exact ge_of_tendsto' h_tendsto (fun m ↦ h_le _)

Premises used: ge_of_tendsto'
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.DominatedConvergence
Goal:
α : Type u_2
mα : MeasurableSpace α
f : ℕ → α → ℝ≥0∞
F : α → ℝ≥0∞
μ : Measure α
hf_meas : ∀ (n : ℕ), AEMeasurable (f n) μ
hf_tendsto : Tendsto (fun (i : ℕ) ↦ ∫⁻ (a : α), f i a ∂μ) atTop (𝓝 (∫⁻ (a : α), F a ∂μ))
hf_mono : ∀ᵐ (a : α) ∂μ, Antitone (β := ℝ≥0∞) fun (i : ℕ) ↦ f i a
h_bound : ∀ᵐ (a : α) ∂μ, ∀ (i : ℕ), F a ≤ f i a
h0 : ∫⁻ (a : α), f 0 a ∂μ ≠ ∞
h_int_finite : ∫⁻ (a : α), F a ∂μ ≠ ∞
h_exists : ∀ᵐ (a : α) ∂μ, ∃ (l : ℝ≥0∞), Tendsto (fun (i : ℕ) ↦ f i a) atTop (𝓝 l)
F' : α → ℝ≥0∞ :=
  fun (a : α) ↦
    if h : ∃ (l : ℝ≥0∞), Tendsto (fun (i : ℕ) ↦ f i a) atTop (𝓝 l) then
      h.choose (p := fun (l : ℝ≥0∞) ↦ Tendsto (fun (i : ℕ) ↦ f i a) atTop (𝓝 l))
    else ∞
hF'_tendsto : ∀ᵐ (a : α) ∂μ, Tendsto (fun (i : ℕ) ↦ f i a) atTop (𝓝 (F' a))
⊢ F ≤ᶠ[ae μ] F'

Tactic:
have hF'_le : F ≤ᵐ[μ] F' := by
    filter_upwards [h_bound, hF'_tendsto] with a h_le h_tendsto
    exact ge_of_tendsto' h_tendsto (fun m ↦ h_le _)
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.DominatedConvergence
Goal:
α : Type u_2
mα : MeasurableSpace α
f : ℕ → α → ℝ≥0∞
F : α → ℝ≥0∞
μ : Measure α
hf_meas : ∀ (n : ℕ), AEMeasurable (f n) μ
hf_tendsto : Tendsto (fun (i : ℕ) ↦ ∫⁻ (a : α), f i a ∂μ) atTop (𝓝 (∫⁻ (a : α), F a ∂μ))
hf_mono : ∀ᵐ (a : α) ∂μ, Antitone (β := ℝ≥0∞) fun (i : ℕ) ↦ f i a
h_bound : ∀ᵐ (a : α) ∂μ, ∀ (i : ℕ), F a ≤ f i a
h0 : ∫⁻ (a : α), f 0 a ∂μ ≠ ∞
h_int_finite : ∫⁻ (a : α), F a ∂μ ≠ ∞
h_exists : ∀ᵐ (a : α) ∂μ, ∃ (l : ℝ≥0∞), Tendsto (fun (i : ℕ) ↦ f i a) atTop (𝓝 l)
F' : α → ℝ≥0∞ :=
  fun (a : α) ↦
    if h : ∃ (l : ℝ≥0∞), Tendsto (fun (i : ℕ) ↦ f i a) atTop (𝓝 l) then
      h.choose (p := fun (l : ℝ≥0∞) ↦ Tendsto (fun (i : ℕ) ↦ f i a) atTop (𝓝 l))
    else ∞
hF'_tendsto : ∀ᵐ (a : α) ∂μ, Tendsto (fun (i : ℕ) ↦ f i a) atTop (𝓝 (F' a))
hF'_le : F ≤ᶠ[ae μ] F'
this : ∫⁻ (a : α), F' a ∂μ = ∫⁻ (a : α), F a ∂μ
⊢ F' =ᶠ[ae μ] F

Tactic:
(ae_eq_of_ae_le_of_lintegral_le hF'_le h_int_finite ?_ this.le).symm

Premises used: Eq.le, MeasureTheory.ae_eq_of_ae_le_of_lintegral_le, Filter.EventuallyEq.symm
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.DominatedConvergence
Goal:
α : Type u_2
mα : MeasurableSpace α
f : ℕ → α → ℝ≥0∞
F : α → ℝ≥0∞
μ : Measure α
hf_meas : ∀ (n : ℕ), AEMeasurable (f n) μ
hf_tendsto : Tendsto (fun (i : ℕ) ↦ ∫⁻ (a : α), f i a ∂μ) atTop (𝓝 (∫⁻ (a : α), F a ∂μ))
hf_mono : ∀ᵐ (a : α) ∂μ, Antitone (β := ℝ≥0∞) fun (i : ℕ) ↦ f i a
h_bound : ∀ᵐ (a : α) ∂μ, ∀ (i : ℕ), F a ≤ f i a
h0 : ∫⁻ (a : α), f 0 a ∂μ ≠ ∞
h_int_finite : ∫⁻ (a : α), F a ∂μ ≠ ∞
h_exists : ∀ᵐ (a : α) ∂μ, ∃ (l : ℝ≥0∞), Tendsto (fun (i : ℕ) ↦ f i a) atTop (𝓝 l)
F' : α → ℝ≥0∞ :=
  fun (a : α) ↦
    if h : ∃ (l : ℝ≥0∞), Tendsto (fun (i : ℕ) ↦ f i a) atTop (𝓝 l) then
      h.choose (p := fun (l : ℝ≥0∞) ↦ Tendsto (fun (i : ℕ) ↦ f i a) atTop (𝓝 l))
    else ∞
hF'_tendsto : ∀ᵐ (a : α) ∂μ, Tendsto (fun (i : ℕ) ↦ f i a) atTop (𝓝 (F' a))
hF'_le : F ≤ᶠ[ae μ] F'
this : ∫⁻ (a : α), F' a ∂μ = ∫⁻ (a : α), F a ∂μ
refine : AEMeasurable F' μ
⊢ F' =ᶠ[ae μ] F

Tactic:
refine (ae_eq_of_ae_le_of_lintegral_le hF'_le h_int_finite ?_ this.le).symm

Premises used: Eq.le, MeasureTheory.ae_eq_of_ae_le_of_lintegral_le, Filter.EventuallyEq.symm
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.DominatedConvergence
Goal:
α : Type u_2
mα : MeasurableSpace α
f : ℕ → α → ℝ≥0∞
F : α → ℝ≥0∞
μ : Measure α
hf_meas : ∀ (n : ℕ), AEMeasurable (f n) μ
hf_tendsto : Tendsto (fun (i : ℕ) ↦ ∫⁻ (a : α), f i a ∂μ) atTop (𝓝 (∫⁻ (a : α), F a ∂μ))
hf_mono : ∀ᵐ (a : α) ∂μ, Antitone (β := ℝ≥0∞) fun (i : ℕ) ↦ f i a
h_bound : ∀ᵐ (a : α) ∂μ, ∀ (i : ℕ), F a ≤ f i a
h0 : ∫⁻ (a : α), f 0 a ∂μ ≠ ∞
h_int_finite : ∫⁻ (a : α), F a ∂μ ≠ ∞
h_exists : ∀ᵐ (a : α) ∂μ, ∃ (l : ℝ≥0∞), Tendsto (fun (i : ℕ) ↦ f i a) atTop (𝓝 l)
F' : α → ℝ≥0∞ :=
  fun (a : α) ↦
    if h : ∃ (l : ℝ≥0∞), Tendsto (fun (i : ℕ) ↦ f i a) atTop (𝓝 l) then
      h.choose (p := fun (l : ℝ≥0∞) ↦ Tendsto (fun (i : ℕ) ↦ f i a) atTop (𝓝 l))
    else ∞
hF'_tendsto : ∀ᵐ (a : α) ∂μ, Tendsto (fun (i : ℕ) ↦ f i a) atTop (𝓝 (F' a))
hF'_le : F ≤ᶠ[ae μ] F'
this : ∫⁻ (a : α), F' a ∂μ = ∫⁻ (a : α), F a ∂μ
⊢ AEMeasurable F' μ

Tactic:
ENNReal.aemeasurable_of_tendsto hf_meas hF'_tendsto

Premises used: ENNReal.aemeasurable_of_tendsto
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.DominatedConvergence
Goal:
α : Type u_2
mα : MeasurableSpace α
f : ℕ → α → ℝ≥0∞
F : α → ℝ≥0∞
μ : Measure α
hf_meas : ∀ (n : ℕ), AEMeasurable (f n) μ
hf_tendsto : Tendsto (fun (i : ℕ) ↦ ∫⁻ (a : α), f i a ∂μ) atTop (𝓝 (∫⁻ (a : α), F a ∂μ))
hf_mono : ∀ᵐ (a : α) ∂μ, Antitone (β := ℝ≥0∞) fun (i : ℕ) ↦ f i a
h_bound : ∀ᵐ (a : α) ∂μ, ∀ (i : ℕ), F a ≤ f i a
h0 : ∫⁻ (a : α), f 0 a ∂μ ≠ ∞
h_int_finite : ∫⁻ (a : α), F a ∂μ ≠ ∞
h_exists : ∀ᵐ (a : α) ∂μ, ∃ (l : ℝ≥0∞), Tendsto (fun (i : ℕ) ↦ f i a) atTop (𝓝 l)
F' : α → ℝ≥0∞ :=
  fun (a : α) ↦
    if h : ∃ (l : ℝ≥0∞), Tendsto (fun (i : ℕ) ↦ f i a) atTop (𝓝 l) then
      h.choose (p := fun (l : ℝ≥0∞) ↦ Tendsto (fun (i : ℕ) ↦ f i a) atTop (𝓝 l))
    else ∞
hF'_tendsto : ∀ᵐ (a : α) ∂μ, Tendsto (fun (i : ℕ) ↦ f i a) atTop (𝓝 (F' a))
hF'_le : F ≤ᶠ[ae μ] F'
this : ∫⁻ (a : α), F' a ∂μ = ∫⁻ (a : α), F a ∂μ
⊢ AEMeasurable F' μ

Tactic:
exact ENNReal.aemeasurable_of_tendsto hf_meas hF'_tendsto

Premises used: ENNReal.aemeasurable_of_tendsto
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.DominatedConvergence
Goal:
α : Type u_2
mα : MeasurableSpace α
f : ℕ → α → ℝ≥0∞
F : α → ℝ≥0∞
μ : Measure α
hf_meas : ∀ (n : ℕ), AEMeasurable (f n) μ
hf_tendsto : Tendsto (fun (i : ℕ) ↦ ∫⁻ (a : α), f i a ∂μ) atTop (𝓝 (∫⁻ (a : α), F a ∂μ))
hf_mono : ∀ᵐ (a : α) ∂μ, Antitone (β := ℝ≥0∞) fun (i : ℕ) ↦ f i a
h_bound : ∀ᵐ (a : α) ∂μ, ∀ (i : ℕ), F a ≤ f i a
h0 : ∫⁻ (a : α), f 0 a ∂μ ≠ ∞
h_int_finite : ∫⁻ (a : α), F a ∂μ ≠ ∞
h_exists : ∀ᵐ (a : α) ∂μ, ∃ (l : ℝ≥0∞), Tendsto (fun (i : ℕ) ↦ f i a) atTop (𝓝 l)
F' : α → ℝ≥0∞ :=
  fun (a : α) ↦
    if h : ∃ (l : ℝ≥0∞), Tendsto (fun (i : ℕ) ↦ f i a) atTop (𝓝 l) then
      h.choose (p := fun (l : ℝ≥0∞) ↦ Tendsto (fun (i : ℕ) ↦ f i a) atTop (𝓝 l))
    else ∞
hF'_tendsto : ∀ᵐ (a : α) ∂μ, Tendsto (fun (i : ℕ) ↦ f i a) atTop (𝓝 (F' a))
hF'_le : F ≤ᶠ[ae μ] F'
suffices : ∫⁻ (a : α), F' a ∂μ = ∫⁻ (a : α), F a ∂μ
⊢ F' =ᶠ[ae μ] F

Tactic:
suffices ∫⁻ a, F' a ∂μ = ∫⁻ a, F a ∂μ by
    refine (ae_eq_of_ae_le_of_lintegral_le hF'_le h_int_finite ?_ this.le).symm
    exact ENNReal.aemeasurable_of_tendsto hf_meas hF'_tendsto
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.DominatedConvergence
Goal:
α : Type u_2
mα : MeasurableSpace α
f : ℕ → α → ℝ≥0∞
F : α → ℝ≥0∞
μ : Measure α
hf_meas : ∀ (n : ℕ), AEMeasurable (f n) μ
hf_tendsto : Tendsto (fun (i : ℕ) ↦ ∫⁻ (a : α), f i a ∂μ) atTop (𝓝 (∫⁻ (a : α), F a ∂μ))
hf_mono : ∀ᵐ (a : α) ∂μ, Antitone (β := ℝ≥0∞) fun (i : ℕ) ↦ f i a
h_bound : ∀ᵐ (a : α) ∂μ, ∀ (i : ℕ), F a ≤ f i a
h0 : ∫⁻ (a : α), f 0 a ∂μ ≠ ∞
h_int_finite : ∫⁻ (a : α), F a ∂μ ≠ ∞
h_exists : ∀ᵐ (a : α) ∂μ, ∃ (l : ℝ≥0∞), Tendsto (fun (i : ℕ) ↦ f i a) atTop (𝓝 l)
F' : α → ℝ≥0∞ :=
  fun (a : α) ↦
    if h : ∃ (l : ℝ≥0∞), Tendsto (fun (i : ℕ) ↦ f i a) atTop (𝓝 l) then
      h.choose (p := fun (l : ℝ≥0∞) ↦ Tendsto (fun (i : ℕ) ↦ f i a) atTop (𝓝 l))
    else ∞
hF'_tendsto : ∀ᵐ (a : α) ∂μ, Tendsto (fun (i : ℕ) ↦ f i a) atTop (𝓝 (F' a))
hF'_le : F ≤ᶠ[ae μ] F'
⊢ ∫⁻ (a : α), F' a ∂μ = ∫⁻ (a : α), F a ∂μ

Tactic:
tendsto_nhds_unique ?_ hf_tendsto

Premises used: tendsto_nhds_unique
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.DominatedConvergence
Goal:
α : Type u_2
mα : MeasurableSpace α
f : ℕ → α → ℝ≥0∞
F : α → ℝ≥0∞
μ : Measure α
hf_meas : ∀ (n : ℕ), AEMeasurable (f n) μ
hf_tendsto : Tendsto (fun (i : ℕ) ↦ ∫⁻ (a : α), f i a ∂μ) atTop (𝓝 (∫⁻ (a : α), F a ∂μ))
hf_mono : ∀ᵐ (a : α) ∂μ, Antitone (β := ℝ≥0∞) fun (i : ℕ) ↦ f i a
h_bound : ∀ᵐ (a : α) ∂μ, ∀ (i : ℕ), F a ≤ f i a
h0 : ∫⁻ (a : α), f 0 a ∂μ ≠ ∞
h_int_finite : ∫⁻ (a : α), F a ∂μ ≠ ∞
h_exists : ∀ᵐ (a : α) ∂μ, ∃ (l : ℝ≥0∞), Tendsto (fun (i : ℕ) ↦ f i a) atTop (𝓝 l)
F' : α → ℝ≥0∞ :=
  fun (a : α) ↦
    if h : ∃ (l : ℝ≥0∞), Tendsto (fun (i : ℕ) ↦ f i a) atTop (𝓝 l) then
      h.choose (p := fun (l : ℝ≥0∞) ↦ Tendsto (fun (i : ℕ) ↦ f i a) atTop (𝓝 l))
    else ∞
hF'_tendsto : ∀ᵐ (a : α) ∂μ, Tendsto (fun (i : ℕ) ↦ f i a) atTop (𝓝 (F' a))
hF'_le : F ≤ᶠ[ae μ] F'
refine : Tendsto (fun (i : ℕ) ↦ ∫⁻ (a : α), f i a ∂μ) atTop (𝓝 (∫⁻ (a : α), F' a ∂μ))
⊢ ∫⁻ (a : α), F' a ∂μ = ∫⁻ (a : α), F a ∂μ

Tactic:
refine tendsto_nhds_unique ?_ hf_tendsto

Premises used: tendsto_nhds_unique
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.DominatedConvergence
Goal:
α : Type u_2
mα : MeasurableSpace α
f : ℕ → α → ℝ≥0∞
F : α → ℝ≥0∞
μ : Measure α
hf_meas : ∀ (n : ℕ), AEMeasurable (f n) μ
hf_tendsto : Tendsto (fun (i : ℕ) ↦ ∫⁻ (a : α), f i a ∂μ) atTop (𝓝 (∫⁻ (a : α), F a ∂μ))
hf_mono : ∀ᵐ (a : α) ∂μ, Antitone (β := ℝ≥0∞) fun (i : ℕ) ↦ f i a
h_bound : ∀ᵐ (a : α) ∂μ, ∀ (i : ℕ), F a ≤ f i a
h0 : ∫⁻ (a : α), f 0 a ∂μ ≠ ∞
h_int_finite : ∫⁻ (a : α), F a ∂μ ≠ ∞
h_exists : ∀ᵐ (a : α) ∂μ, ∃ (l : ℝ≥0∞), Tendsto (fun (i : ℕ) ↦ f i a) atTop (𝓝 l)
F' : α → ℝ≥0∞ :=
  fun (a : α) ↦
    if h : ∃ (l : ℝ≥0∞), Tendsto (fun (i : ℕ) ↦ f i a) atTop (𝓝 l) then
      h.choose (p := fun (l : ℝ≥0∞) ↦ Tendsto (fun (i : ℕ) ↦ f i a) atTop (𝓝 l))
    else ∞
hF'_tendsto : ∀ᵐ (a : α) ∂μ, Tendsto (fun (i : ℕ) ↦ f i a) atTop (𝓝 (F' a))
hF'_le : F ≤ᶠ[ae μ] F'
⊢ Tendsto (fun (i : ℕ) ↦ ∫⁻ (a : α), f i a ∂μ) atTop (𝓝 (∫⁻ (a : α), F' a ∂μ))

Tactic:
lintegral_tendsto_of_tendsto_of_antitone hf_meas hf_mono h0 hF'_tendsto

Premises used: MeasureTheory.lintegral_tendsto_of_tendsto_of_antitone
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.DominatedConvergence
Goal:
α : Type u_2
mα : MeasurableSpace α
f : ℕ → α → ℝ≥0∞
F : α → ℝ≥0∞
μ : Measure α
hf_meas : ∀ (n : ℕ), AEMeasurable (f n) μ
hf_tendsto : Tendsto (fun (i : ℕ) ↦ ∫⁻ (a : α), f i a ∂μ) atTop (𝓝 (∫⁻ (a : α), F a ∂μ))
hf_mono : ∀ᵐ (a : α) ∂μ, Antitone (β := ℝ≥0∞) fun (i : ℕ) ↦ f i a
h_bound : ∀ᵐ (a : α) ∂μ, ∀ (i : ℕ), F a ≤ f i a
h0 : ∫⁻ (a : α), f 0 a ∂μ ≠ ∞
h_int_finite : ∫⁻ (a : α), F a ∂μ ≠ ∞
h_exists : ∀ᵐ (a : α) ∂μ, ∃ (l : ℝ≥0∞), Tendsto (fun (i : ℕ) ↦ f i a) atTop (𝓝 l)
F' : α → ℝ≥0∞ :=
  fun (a : α) ↦
    if h : ∃ (l : ℝ≥0∞), Tendsto (fun (i : ℕ) ↦ f i a) atTop (𝓝 l) then
      h.choose (p := fun (l : ℝ≥0∞) ↦ Tendsto (fun (i : ℕ) ↦ f i a) atTop (𝓝 l))
    else ∞
hF'_tendsto : ∀ᵐ (a : α) ∂μ, Tendsto (fun (i : ℕ) ↦ f i a) atTop (𝓝 (F' a))
hF'_le : F ≤ᶠ[ae μ] F'
⊢ Tendsto (fun (i : ℕ) ↦ ∫⁻ (a : α), f i a ∂μ) atTop (𝓝 (∫⁻ (a : α), F' a ∂μ))

Tactic:
exact lintegral_tendsto_of_tendsto_of_antitone hf_meas hf_mono h0 hF'_tendsto

Premises used: MeasureTheory.lintegral_tendsto_of_tendsto_of_antitone
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Map
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
μ : Measure α
f : β → ℝ≥0∞
g : α → β
hf : Measurable f
hg : Measurable g
rw : ⨆ (n : ℕ), SimpleFunc.lintegral (_m := inst_1) (eapprox f n) (Measure.map g μ) = ∫⁻ (a : α), f (g a) ∂μ
⊢ ∫⁻ (a : β), f a ∂Measure.map g μ = ∫⁻ (a : α), f (g a) ∂μ

Tactic:
rw [lintegral_eq_iSup_eapprox_lintegral hf]

Premises used: MeasureTheory.lintegral_eq_iSup_eapprox_lintegral
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Map
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
μ : Measure α
f : β → ℝ≥0∞
g : α → β
hf : Measurable f
hg : Measurable g
simp : ⨆ (n : ℕ), SimpleFunc.lintegral (_m := inst_1) (eapprox f n) (Measure.map g μ) = ∫⁻ (a : α), (f ∘ g) a ∂μ
⊢ ⨆ (n : ℕ), SimpleFunc.lintegral (_m := inst_1) (eapprox f n) (Measure.map g μ) = ∫⁻ (a : α), f (g a) ∂μ

Tactic:
simp only [← Function.comp_apply (f := f) (g := g)]

Premises used: Function.comp_apply
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Map
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
μ : Measure α
f : β → ℝ≥0∞
g : α → β
hf : Measurable f
hg : Measurable g
rw :
  Eq (α := ℝ≥0∞) (⨆ (n : ℕ), SimpleFunc.lintegral (_m := inst_1) (eapprox f n) (Measure.map g μ))
    (⨆ (n : ℕ), SimpleFunc.lintegral (eapprox (f ∘ g) n) μ)
⊢ ⨆ (n : ℕ), SimpleFunc.lintegral (_m := inst_1) (eapprox f n) (Measure.map g μ) = ∫⁻ (a : α), (f ∘ g) a ∂μ

Tactic:
rw [lintegral_eq_iSup_eapprox_lintegral (hf.comp hg)]

Premises used: Measurable.comp, MeasureTheory.lintegral_eq_iSup_eapprox_lintegral