awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Integral.IntegralEqImproper
Goal:
E : Type u_1
f f' : ℝ → E
a : ℝ
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
hderiv : ∀ x ∈ Ioi a, HasDerivAt f (f' x) x
f'int : IntegrableOn (mα := MeasureSpace.toMeasurableSpace) f' (Ioi a) volume
ε : ℝ
εpos : ε > 0
A :
  ∀ᶠ (n : ℕ) in atTop,
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ici (↑n : ℝ))) fun (x : ℝ) ↦ ‖f' x‖) < ε
B : ∀ᶠ (n : ℕ) in atTop, a < (↑n : ℝ)
N : ℕ
hN :
  (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ici (↑N : ℝ))) fun (x : ℝ) ↦ ‖f' x‖) < ε
h'N : a < (↑N : ℝ)
x : ℝ
hx : x ≥ (↑N : ℝ)
⊢ IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ ‖f' x‖) (Ici (↑N : ℝ)) volume

Tactic:
apply IntegrableOn.mono_set f'int.norm (Ici_subset_Ioi.2 h'N)

Premises used: Iff.mpr, MeasureTheory.IntegrableOn.mono_set, MeasureTheory.Integrable.norm, Set.Ici_subset_Ioi
-- Module: Mathlib.MeasureTheory.Integral.IntegralEqImproper
Goal:
E : Type u_1
f f' : ℝ → E
a : ℝ
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
hderiv : ∀ x ∈ Ioi a, HasDerivAt f (f' x) x
f'int : IntegrableOn (mα := MeasureSpace.toMeasurableSpace) f' (Ioi a) volume
ε : ℝ
εpos : ε > 0
A :
  ∀ᶠ (n : ℕ) in atTop,
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ici (↑n : ℝ))) fun (x : ℝ) ↦ ‖f' x‖) < ε
B : ∀ᶠ (n : ℕ) in atTop, a < (↑n : ℝ)
N : ℕ
hN :
  (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ici (↑N : ℝ))) fun (x : ℝ) ↦ ‖f' x‖) < ε
h'N : a < (↑N : ℝ)
x_1 : ℝ
hx : x_1 ≥ (↑N : ℝ)
x : ℝ
⊢ 0 x ≤ ‖f' x‖

Tactic:
norm_nonneg _

Premises used: norm_nonneg
-- Module: Mathlib.MeasureTheory.Integral.IntegralEqImproper
Goal:
E : Type u_1
f f' : ℝ → E
a : ℝ
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
hderiv : ∀ x ∈ Ioi a, HasDerivAt f (f' x) x
f'int : IntegrableOn (mα := MeasureSpace.toMeasurableSpace) f' (Ioi a) volume
ε : ℝ
εpos : ε > 0
A :
  ∀ᶠ (n : ℕ) in atTop,
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ici (↑n : ℝ))) fun (x : ℝ) ↦ ‖f' x‖) < ε
B : ∀ᶠ (n : ℕ) in atTop, a < (↑n : ℝ)
N : ℕ
hN :
  (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ici (↑N : ℝ))) fun (x : ℝ) ↦ ‖f' x‖) < ε
h'N : a < (↑N : ℝ)
x : ℝ
hx : x ≥ (↑N : ℝ)
hf :
  ∀ (a : ℝ), Membership.mem (γ := Set ℝ) {x : ℝ | (fun (x : ℝ) ↦ LE.le (α := ℝ) (0 x) ((fun (x : ℝ) ↦ ‖f' x‖) x)) x} a
hf₁ hf₂ : ∀ (x : ℝ), 0 x ≤ ‖f' x‖
⊢ (ae (F := Measure ℝ) (Measure.restrict volume (Ici (↑N : ℝ)))).EventuallyLE (β := ℝ) 0 fun (x : ℝ) ↦ ‖f' x‖

Tactic:
filter_upwards with x using norm_nonneg _

Premises used: norm_nonneg
-- Module: Mathlib.MeasureTheory.Integral.IntegralEqImproper
Goal:
E : Type u_1
f f' : ℝ → E
a : ℝ
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
hderiv : ∀ x ∈ Ioi a, HasDerivAt f (f' x) x
f'int : IntegrableOn (mα := MeasureSpace.toMeasurableSpace) f' (Ioi a) volume
ε : ℝ
εpos : ε > 0
A :
  ∀ᶠ (n : ℕ) in atTop,
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ici (↑n : ℝ))) fun (x : ℝ) ↦ ‖f' x‖) < ε
B : ∀ᶠ (n : ℕ) in atTop, a < (↑n : ℝ)
N : ℕ
hN :
  (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ici (↑N : ℝ))) fun (x : ℝ) ↦ ‖f' x‖) < ε
h'N : a < (↑N : ℝ)
x : ℝ
hx : x ≥ (↑N : ℝ)
⊢ Ioc (↑N : ℝ) x ⊆ Ici (↑N : ℝ)

Tactic:
have : Ioc (↑N) x ⊆ Ici ↑N := Ioc_subset_Ioi_self.trans Ioi_subset_Ici_self
-- Module: Mathlib.MeasureTheory.Integral.IntegralEqImproper
Goal:
E : Type u_1
f f' : ℝ → E
a : ℝ
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
hderiv : ∀ x ∈ Ioi a, HasDerivAt f (f' x) x
f'int : IntegrableOn (mα := MeasureSpace.toMeasurableSpace) f' (Ioi a) volume
ε : ℝ
εpos : ε > 0
A :
  ∀ᶠ (n : ℕ) in atTop,
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ici (↑n : ℝ))) fun (x : ℝ) ↦ ‖f' x‖) < ε
B : ∀ᶠ (n : ℕ) in atTop, a < (↑n : ℝ)
N : ℕ
hN :
  (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ici (↑N : ℝ))) fun (x : ℝ) ↦ ‖f' x‖) < ε
h'N : a < (↑N : ℝ)
x : ℝ
hx : x ≥ (↑N : ℝ)
this : Ioc (↑N : ℝ) x ⊆ Ici (↑N : ℝ)
⊢ Ioc (↑N : ℝ) x ≤ᶠ[ae (F := Measure ℝ) volume] Ici (↑N : ℝ)

Tactic:
this.eventuallyLE

Premises used: HasSubset.Subset.eventuallyLE
-- Module: Mathlib.MeasureTheory.Integral.IntegralEqImproper
Goal:
E : Type u_1
f f' : ℝ → E
a : ℝ
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
hderiv : ∀ x ∈ Ioi a, HasDerivAt f (f' x) x
f'int : IntegrableOn (mα := MeasureSpace.toMeasurableSpace) f' (Ioi a) volume
ε : ℝ
εpos : ε > 0
A :
  ∀ᶠ (n : ℕ) in atTop,
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ici (↑n : ℝ))) fun (x : ℝ) ↦ ‖f' x‖) < ε
B : ∀ᶠ (n : ℕ) in atTop, a < (↑n : ℝ)
N : ℕ
hN :
  (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ici (↑N : ℝ))) fun (x : ℝ) ↦ ‖f' x‖) < ε
h'N : a < (↑N : ℝ)
x : ℝ
hx : x ≥ (↑N : ℝ)
this : Ioc (↑N : ℝ) x ⊆ Ici (↑N : ℝ)
⊢ Ioc (↑N : ℝ) x ≤ᶠ[ae (F := Measure ℝ) volume] Ici (↑N : ℝ)

Tactic:
exact this.eventuallyLE

Premises used: HasSubset.Subset.eventuallyLE
-- Module: Mathlib.MeasureTheory.Integral.IntegralEqImproper
Goal:
E : Type u_1
f f' : ℝ → E
a : ℝ
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
hderiv : ∀ x ∈ Ioi a, HasDerivAt f (f' x) x
f'int : IntegrableOn (mα := MeasureSpace.toMeasurableSpace) f' (Ioi a) volume
ε : ℝ
εpos : ε > 0
A :
  ∀ᶠ (n : ℕ) in atTop,
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ici (↑n : ℝ))) fun (x : ℝ) ↦ ‖f' x‖) < ε
B : ∀ᶠ (n : ℕ) in atTop, a < (↑n : ℝ)
N : ℕ
hN :
  (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ici (↑N : ℝ))) fun (x : ℝ) ↦ ‖f' x‖) < ε
h'N : a < (↑N : ℝ)
x : ℝ
hx : x ≥ (↑N : ℝ)
⊢ (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ici (↑N : ℝ))) fun (t : ℝ) ↦ ‖f' t‖) < ε

Tactic:
hN
-- Module: Mathlib.MeasureTheory.Integral.IntegralEqImproper
Goal:
E : Type u_1
f f' : ℝ → E
a : ℝ
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
hderiv : ∀ x ∈ Ioi a, HasDerivAt f (f' x) x
f'int : IntegrableOn (mα := MeasureSpace.toMeasurableSpace) f' (Ioi a) volume
ε : ℝ
εpos : ε > 0
A :
  ∀ᶠ (n : ℕ) in atTop,
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ici (↑n : ℝ))) fun (x : ℝ) ↦ ‖f' x‖) < ε
B : ∀ᶠ (n : ℕ) in atTop, a < (↑n : ℝ)
N : ℕ
hN :
  (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ici (↑N : ℝ))) fun (x : ℝ) ↦ ‖f' x‖) < ε
h'N : a < (↑N : ℝ)
x : ℝ
hx : x ≥ (↑N : ℝ)
dist :
  ‖f x - f (↑N : ℝ)‖ =
    Norm.norm.{u_1} (E := E)
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioc (↑N : ℝ) x)) fun (t : ℝ) ↦ f' t)
dist₁ :
  LE.le (α := ℝ)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioc (↑N : ℝ) x)) fun (t : ℝ) ↦ ‖f' t‖)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ici (↑N : ℝ))) fun (t : ℝ) ↦ ‖f' t‖)
⊢ Dist.dist (f x) (f (↑N : ℝ)) < ε

Tactic:
calc
  dist (f x) (f ↑N)
    = ‖f x - f N‖ := dist_eq_norm _ _
  _ = ‖∫ t in Ioc ↑N x, f' t‖ := by
      rw [← intervalIntegral.integral_of_le hx, intervalIntegral.integral_eq_sub_of_hasDerivAt]
      · intro y hy
        simp only [hx, uIcc_of_le, mem_Icc] at hy
        exact hderiv _ (h'N.trans_le hy.1)
      · rw [intervalIntegrable_iff_integrableOn_Ioc_of_le hx]
        exact f'int.mono_set (Ioc_subset_Ioi_self.trans (Ioi_subset_Ioi h'N.le))
  _ ≤ ∫ t in Ioc ↑N x, ‖f' t‖ := norm_integral_le_integral_norm fun a ↦ f' a
  _ ≤ ∫ t in Ici ↑N, ‖f' t‖ := by
      apply setIntegral_mono_set
      · apply IntegrableOn.mono_set f'int.norm (Ici_subset_Ioi.2 h'N)
      · filter_upwards with x using norm_nonneg _
      · have : Ioc (↑N) x ⊆ Ici ↑N := Ioc_subset_Ioi_self.trans Ioi_subset_Ici_self
        exact this.eventuallyLE
  _ < ε := hN

Premises used: Set.Ioc, dist_eq_norm, Set.Ici, MeasureTheory.norm_integral_le_integral_norm, Nat.cast, Dist.dist
-- Module: Mathlib.MeasureTheory.Integral.IntegralEqImproper
Goal:
E : Type u_1
f f' : ℝ → E
a : ℝ
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
hderiv : ∀ x ∈ Ioi a, HasDerivAt f (f' x) x
f'int : IntegrableOn (mα := MeasureSpace.toMeasurableSpace) f' (Ioi a) volume
fint : IntegrableOn (mα := MeasureSpace.toMeasurableSpace) f (Ioi a) volume
F : E →L[ℝ] Completion E := Completion.toComplL
⊢ ∀ x ∈ Ioi a,
    HasDerivAt (F := Completion E) ((⇑F : (a : E) → Completion E) ∘ f : ℝ → Completion E)
      ((F : (a : E) → Completion E) (f' x) : Completion E) x

Tactic:
have Fderiv : ∀ x ∈ Ioi a, HasDerivAt (F ∘ f) (F (f' x)) x :=
    fun x hx ↦ F.hasFDerivAt.comp_hasDerivAt _ (hderiv x hx)
-- Module: Mathlib.MeasureTheory.Integral.IntegralEqImproper
Goal:
E : Type u_1
f f' : ℝ → E
a : ℝ
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
hderiv : ∀ x ∈ Ioi a, HasDerivAt f (f' x) x
f'int : IntegrableOn (mα := MeasureSpace.toMeasurableSpace) f' (Ioi a) volume
fint : IntegrableOn (mα := MeasureSpace.toMeasurableSpace) f (Ioi a) volume
F : E →L[ℝ] Completion E := Completion.toComplL
Fderiv :
  ∀ x ∈ Ioi a,
    HasDerivAt (F := Completion E) ((⇑F : (a : E) → Completion E) ∘ f : ℝ → Completion E)
      ((F : (a : E) → Completion E) (f' x) : Completion E) x
⊢ IntegrableOn (ε := Completion E) (mα := MeasureSpace.toMeasurableSpace) ((⇑F : (a : E) → Completion E) ∘ f) (Ioi a)
    volume

Tactic:
apply F.integrable_comp fint

Premises used: ContinuousLinearMap.integrable_comp
-- Module: Mathlib.MeasureTheory.Integral.IntegralEqImproper
Goal:
E : Type u_1
f f' : ℝ → E
a : ℝ
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
hderiv : ∀ x ∈ Ioi a, HasDerivAt f (f' x) x
f'int : IntegrableOn (mα := MeasureSpace.toMeasurableSpace) f' (Ioi a) volume
fint : IntegrableOn (mα := MeasureSpace.toMeasurableSpace) f (Ioi a) volume
F : E →L[ℝ] Completion E := Completion.toComplL
Fderiv :
  ∀ x ∈ Ioi a,
    HasDerivAt (F := Completion E) ((⇑F : (a : E) → Completion E) ∘ f : ℝ → Completion E)
      ((F : (a : E) → Completion E) (f' x) : Completion E) x
⊢ IntegrableOn (ε := Completion E) (mα := MeasureSpace.toMeasurableSpace) ((⇑F : (a : E) → Completion E) ∘ f) (Ioi a)
    volume

Tactic:
have Fint : IntegrableOn (F ∘ f) (Ioi a) := by apply F.integrable_comp fint
-- Module: Mathlib.MeasureTheory.Integral.IntegralEqImproper
Goal:
E : Type u_1
f f' : ℝ → E
a : ℝ
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
hderiv : ∀ x ∈ Ioi a, HasDerivAt f (f' x) x
f'int : IntegrableOn (mα := MeasureSpace.toMeasurableSpace) f' (Ioi a) volume
fint : IntegrableOn (mα := MeasureSpace.toMeasurableSpace) f (Ioi a) volume
F : E →L[ℝ] Completion E := Completion.toComplL
Fderiv :
  ∀ x ∈ Ioi a,
    HasDerivAt (F := Completion E) ((⇑F : (a : E) → Completion E) ∘ f : ℝ → Completion E)
      ((F : (a : E) → Completion E) (f' x) : Completion E) x
Fint :
  IntegrableOn (ε := Completion E) (mα := MeasureSpace.toMeasurableSpace) ((⇑F : (a : E) → Completion E) ∘ f) (Ioi a)
    volume
⊢ IntegrableOn (ε := Completion E) (mα := MeasureSpace.toMeasurableSpace) ((⇑F : (a : E) → Completion E) ∘ f') (Ioi a)
    volume

Tactic:
apply F.integrable_comp f'int

Premises used: ContinuousLinearMap.integrable_comp
-- Module: Mathlib.MeasureTheory.Integral.IntegralEqImproper
Goal:
E : Type u_1
f f' : ℝ → E
a : ℝ
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
hderiv : ∀ x ∈ Ioi a, HasDerivAt f (f' x) x
f'int : IntegrableOn (mα := MeasureSpace.toMeasurableSpace) f' (Ioi a) volume
fint : IntegrableOn (mα := MeasureSpace.toMeasurableSpace) f (Ioi a) volume
F : E →L[ℝ] Completion E := Completion.toComplL
Fderiv :
  ∀ x ∈ Ioi a,
    HasDerivAt (F := Completion E) ((⇑F : (a : E) → Completion E) ∘ f : ℝ → Completion E)
      ((F : (a : E) → Completion E) (f' x) : Completion E) x
Fint :
  IntegrableOn (ε := Completion E) (mα := MeasureSpace.toMeasurableSpace) ((⇑F : (a : E) → Completion E) ∘ f) (Ioi a)
    volume
⊢ IntegrableOn (ε := Completion E) (mα := MeasureSpace.toMeasurableSpace) ((⇑F : (a : E) → Completion E) ∘ f') (Ioi a)
    volume

Tactic:
have F'int : IntegrableOn (F ∘ f') (Ioi a) := by apply F.integrable_comp f'int
-- Module: Mathlib.MeasureTheory.Integral.IntegralEqImproper
Goal:
E : Type u_1
f f' : ℝ → E
a : ℝ
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
hderiv : ∀ x ∈ Ioi a, HasDerivAt f (f' x) x
f'int : IntegrableOn (mα := MeasureSpace.toMeasurableSpace) f' (Ioi a) volume
fint : IntegrableOn (mα := MeasureSpace.toMeasurableSpace) f (Ioi a) volume
F : E →L[ℝ] Completion E := Completion.toComplL
Fderiv :
  ∀ x ∈ Ioi a,
    HasDerivAt (F := Completion E) ((⇑F : (a : E) → Completion E) ∘ f : ℝ → Completion E)
      ((F : (a : E) → Completion E) (f' x) : Completion E) x
Fint :
  IntegrableOn (ε := Completion E) (mα := MeasureSpace.toMeasurableSpace) ((⇑F : (a : E) → Completion E) ∘ f) (Ioi a)
    volume
F'int :
  IntegrableOn (ε := Completion E) (mα := MeasureSpace.toMeasurableSpace) ((⇑F : (a : E) → Completion E) ∘ f') (Ioi a)
    volume
⊢ Tendsto (β := Completion E) ((⇑F : (a : E) → Completion E) ∘ f) atTop
    (𝓝 (limUnder atTop ((⇑F : (a : E) → Completion E) ∘ f)))

Tactic:
apply tendsto_limUnder_of_hasDerivAt_of_integrableOn_Ioi Fderiv F'int

Premises used: MeasureTheory.tendsto_limUnder_of_hasDerivAt_of_integrableOn_Ioi
-- Module: Mathlib.MeasureTheory.Integral.IntegralEqImproper
Goal:
E : Type u_1
f f' : ℝ → E
a : ℝ
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
hderiv : ∀ x ∈ Ioi a, HasDerivAt f (f' x) x
f'int : IntegrableOn (mα := MeasureSpace.toMeasurableSpace) f' (Ioi a) volume
fint : IntegrableOn (mα := MeasureSpace.toMeasurableSpace) f (Ioi a) volume
F : E →L[ℝ] Completion E := Completion.toComplL
Fderiv :
  ∀ x ∈ Ioi a,
    HasDerivAt (F := Completion E) ((⇑F : (a : E) → Completion E) ∘ f : ℝ → Completion E)
      ((F : (a : E) → Completion E) (f' x) : Completion E) x
Fint :
  IntegrableOn (ε := Completion E) (mα := MeasureSpace.toMeasurableSpace) ((⇑F : (a : E) → Completion E) ∘ f) (Ioi a)
    volume
F'int :
  IntegrableOn (ε := Completion E) (mα := MeasureSpace.toMeasurableSpace) ((⇑F : (a : E) → Completion E) ∘ f') (Ioi a)
    volume
⊢ Tendsto (β := Completion E) ((⇑F : (a : E) → Completion E) ∘ f) atTop
    (𝓝 (limUnder atTop ((⇑F : (a : E) → Completion E) ∘ f)))

Tactic:
have A : Tendsto (F ∘ f) atTop (𝓝 (limUnder atTop (F ∘ f))) := by
    apply tendsto_limUnder_of_hasDerivAt_of_integrableOn_Ioi Fderiv F'int
-- Module: Mathlib.MeasureTheory.Integral.IntegralEqImproper
Goal:
E : Type u_1
f f' : ℝ → E
a : ℝ
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
hderiv : ∀ x ∈ Ioi a, HasDerivAt f (f' x) x
f'int : IntegrableOn (mα := MeasureSpace.toMeasurableSpace) f' (Ioi a) volume
fint : IntegrableOn (mα := MeasureSpace.toMeasurableSpace) f (Ioi a) volume
F : E →L[ℝ] Completion E := Completion.toComplL
Fderiv :
  ∀ x ∈ Ioi a,
    HasDerivAt (F := Completion E) ((⇑F : (a : E) → Completion E) ∘ f : ℝ → Completion E)
      ((F : (a : E) → Completion E) (f' x) : Completion E) x
Fint :
  IntegrableOn (ε := Completion E) (mα := MeasureSpace.toMeasurableSpace) ((⇑F : (a : E) → Completion E) ∘ f) (Ioi a)
    volume
F'int :
  IntegrableOn (ε := Completion E) (mα := MeasureSpace.toMeasurableSpace) ((⇑F : (a : E) → Completion E) ∘ f') (Ioi a)
    volume
A :
  Tendsto (β := Completion E) ((⇑F : (a : E) → Completion E) ∘ f) atTop
    (𝓝 (limUnder atTop ((⇑F : (a : E) → Completion E) ∘ f)))
⊢ IntegrableAtFilter (ε := Completion E) (mα := MeasureSpace.toMeasurableSpace) ((⇑F : (a : E) → Completion E) ∘ f)
    atTop volume

Tactic:
⟨Ioi a, Ioi_mem_atTop _, Fint⟩

Premises used: Set.Ioi, Filter.Ioi_mem_atTop, MeasureTheory.IntegrableAtFilter, And.intro, Exists.intro
-- Module: Mathlib.MeasureTheory.Integral.IntegralEqImproper
Goal:
E : Type u_1
f f' : ℝ → E
a : ℝ
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
hderiv : ∀ x ∈ Ioi a, HasDerivAt f (f' x) x
f'int : IntegrableOn (mα := MeasureSpace.toMeasurableSpace) f' (Ioi a) volume
fint : IntegrableOn (mα := MeasureSpace.toMeasurableSpace) f (Ioi a) volume
F : E →L[ℝ] Completion E := Completion.toComplL
Fderiv :
  ∀ x ∈ Ioi a,
    HasDerivAt (F := Completion E) ((⇑F : (a : E) → Completion E) ∘ f : ℝ → Completion E)
      ((F : (a : E) → Completion E) (f' x) : Completion E) x
Fint :
  IntegrableOn (ε := Completion E) (mα := MeasureSpace.toMeasurableSpace) ((⇑F : (a : E) → Completion E) ∘ f) (Ioi a)
    volume
F'int :
  IntegrableOn (ε := Completion E) (mα := MeasureSpace.toMeasurableSpace) ((⇑F : (a : E) → Completion E) ∘ f') (Ioi a)
    volume
A :
  Tendsto (β := Completion E) ((⇑F : (a : E) → Completion E) ∘ f) atTop
    (𝓝 (limUnder atTop ((⇑F : (a : E) → Completion E) ∘ f)))
⊢ IntegrableAtFilter (ε := Completion E) (mα := MeasureSpace.toMeasurableSpace) ((⇑F : (a : E) → Completion E) ∘ f)
    atTop volume

Tactic:
exact ⟨Ioi a, Ioi_mem_atTop _, Fint⟩
-- Module: Mathlib.MeasureTheory.Integral.IntegralEqImproper
Goal:
E : Type u_1
f f' : ℝ → E
a : ℝ
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
hderiv : ∀ x ∈ Ioi a, HasDerivAt f (f' x) x
f'int : IntegrableOn (mα := MeasureSpace.toMeasurableSpace) f' (Ioi a) volume
fint : IntegrableOn (mα := MeasureSpace.toMeasurableSpace) f (Ioi a) volume
F : E →L[ℝ] Completion E := Completion.toComplL
Fderiv :
  ∀ x ∈ Ioi a,
    HasDerivAt (F := Completion E) ((⇑F : (a : E) → Completion E) ∘ f : ℝ → Completion E)
      ((F : (a : E) → Completion E) (f' x) : Completion E) x
Fint :
  IntegrableOn (ε := Completion E) (mα := MeasureSpace.toMeasurableSpace) ((⇑F : (a : E) → Completion E) ∘ f) (Ioi a)
    volume
F'int :
  IntegrableOn (ε := Completion E) (mα := MeasureSpace.toMeasurableSpace) ((⇑F : (a : E) → Completion E) ∘ f') (Ioi a)
    volume
A :
  Tendsto (β := Completion E) ((⇑F : (a : E) → Completion E) ∘ f) atTop
    (𝓝 (limUnder atTop ((⇑F : (a : E) → Completion E) ∘ f)))
⊢ IntegrableAtFilter (ε := Completion E) (mα := MeasureSpace.toMeasurableSpace) ((⇑F : (a : E) → Completion E) ∘ f)
    atTop volume

Tactic:
have : IntegrableAtFilter (F ∘ f) atTop := by exact ⟨Ioi a, Ioi_mem_atTop _, Fint⟩
-- Module: Mathlib.MeasureTheory.Integral.IntegralEqImproper
Goal:
E : Type u_1
f f' : ℝ → E
a : ℝ
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
hderiv : ∀ x ∈ Ioi a, HasDerivAt f (f' x) x
f'int : IntegrableOn (mα := MeasureSpace.toMeasurableSpace) f' (Ioi a) volume
fint : IntegrableOn (mα := MeasureSpace.toMeasurableSpace) f (Ioi a) volume
F : E →L[ℝ] Completion E := Completion.toComplL
Fderiv :
  ∀ x ∈ Ioi a,
    HasDerivAt (F := Completion E) ((⇑F : (a : E) → Completion E) ∘ f : ℝ → Completion E)
      ((F : (a : E) → Completion E) (f' x) : Completion E) x
Fint :
  IntegrableOn (ε := Completion E) (mα := MeasureSpace.toMeasurableSpace) ((⇑F : (a : E) → Completion E) ∘ f) (Ioi a)
    volume
F'int :
  IntegrableOn (ε := Completion E) (mα := MeasureSpace.toMeasurableSpace) ((⇑F : (a : E) → Completion E) ∘ f') (Ioi a)
    volume
A :
  Tendsto (β := Completion E) ((⇑F : (a : E) → Completion E) ∘ f) atTop
    (𝓝 (limUnder atTop ((⇑F : (a : E) → Completion E) ∘ f)))
this :
  IntegrableAtFilter (ε := Completion E) (mα := MeasureSpace.toMeasurableSpace) ((⇑F : (a : E) → Completion E) ∘ f)
    atTop volume
apply :
  ∀ (s : Set ℝ),
    Membership.mem (γ := Filter ℝ) atTop s → Eq (α := ℝ≥0∞) ((volume : (a : Set ℝ) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ Eq (α := Completion E) (limUnder atTop ((⇑F : (a : E) → Completion E) ∘ f)) ((F : (a : E) → Completion E) 0)

Tactic:
apply IntegrableAtFilter.eq_zero_of_tendsto this ?_ A

Premises used: MeasureTheory.IntegrableAtFilter.eq_zero_of_tendsto
-- Module: Mathlib.MeasureTheory.Integral.IntegralEqImproper
Goal:
E : Type u_1
f f' : ℝ → E
a : ℝ
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
hderiv : ∀ x ∈ Ioi a, HasDerivAt f (f' x) x
f'int : IntegrableOn (mα := MeasureSpace.toMeasurableSpace) f' (Ioi a) volume
fint : IntegrableOn (mα := MeasureSpace.toMeasurableSpace) f (Ioi a) volume
F : E →L[ℝ] Completion E := Completion.toComplL
Fderiv :
  ∀ x ∈ Ioi a,
    HasDerivAt (F := Completion E) ((⇑F : (a : E) → Completion E) ∘ f : ℝ → Completion E)
      ((F : (a : E) → Completion E) (f' x) : Completion E) x
Fint :
  IntegrableOn (ε := Completion E) (mα := MeasureSpace.toMeasurableSpace) ((⇑F : (a : E) → Completion E) ∘ f) (Ioi a)
    volume
F'int :
  IntegrableOn (ε := Completion E) (mα := MeasureSpace.toMeasurableSpace) ((⇑F : (a : E) → Completion E) ∘ f') (Ioi a)
    volume
A :
  Tendsto (β := Completion E) ((⇑F : (a : E) → Completion E) ∘ f) atTop
    (𝓝 (limUnder atTop ((⇑F : (a : E) → Completion E) ∘ f)))
this :
  IntegrableAtFilter (ε := Completion E) (mα := MeasureSpace.toMeasurableSpace) ((⇑F : (a : E) → Completion E) ∘ f)
    atTop volume
s : Set ℝ
hs : Membership.mem (γ := Filter ℝ) atTop s
rcases : ∀ (b : ℝ) (hb : ∀ b_1 ≥ b, b_1 ∈ s), Eq (α := ℝ≥0∞) ((volume : (a : Set ℝ) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((volume : (a : Set ℝ) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
rcases mem_atTop_sets.1 hs with ⟨b, hb⟩

Premises used: Filter.mem_atTop_sets, Iff.mp
-- Module: Mathlib.MeasureTheory.Integral.IntegralEqImproper
Goal:
E : Type u_1
f f' : ℝ → E
a : ℝ
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
hderiv : ∀ x ∈ Ioi a, HasDerivAt f (f' x) x
f'int : IntegrableOn (mα := MeasureSpace.toMeasurableSpace) f' (Ioi a) volume
fint : IntegrableOn (mα := MeasureSpace.toMeasurableSpace) f (Ioi a) volume
F : E →L[ℝ] Completion E := Completion.toComplL
Fderiv :
  ∀ x ∈ Ioi a,
    HasDerivAt (F := Completion E) ((⇑F : (a : E) → Completion E) ∘ f : ℝ → Completion E)
      ((F : (a : E) → Completion E) (f' x) : Completion E) x
Fint :
  IntegrableOn (ε := Completion E) (mα := MeasureSpace.toMeasurableSpace) ((⇑F : (a : E) → Completion E) ∘ f) (Ioi a)
    volume
F'int :
  IntegrableOn (ε := Completion E) (mα := MeasureSpace.toMeasurableSpace) ((⇑F : (a : E) → Completion E) ∘ f') (Ioi a)
    volume
A :
  Tendsto (β := Completion E) ((⇑F : (a : E) → Completion E) ∘ f) atTop
    (𝓝 (limUnder atTop ((⇑F : (a : E) → Completion E) ∘ f)))
this :
  IntegrableAtFilter (ε := Completion E) (mα := MeasureSpace.toMeasurableSpace) ((⇑F : (a : E) → Completion E) ∘ f)
    atTop volume
s : Set ℝ
hs : Membership.mem (γ := Filter ℝ) atTop s
b : ℝ
hb : ∀ b_1 ≥ b, b_1 ∈ s
rw : LE.le (α := ℝ≥0∞) ((volume : (a : Set ℝ) → ℝ≥0∞) (Ici b) : ℝ≥0∞) ((volume : (a : Set ℝ) → ℝ≥0∞) s : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((volume : (a : Set ℝ) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
rw [← top_le_iff, ← volume_Ici (a := b)]

Premises used: Real.volume_Ici, top_le_iff
-- Module: Mathlib.MeasureTheory.Integral.IntegralEqImproper
Goal:
E : Type u_1
f f' : ℝ → E
a : ℝ
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
hderiv : ∀ x ∈ Ioi a, HasDerivAt f (f' x) x
f'int : IntegrableOn (mα := MeasureSpace.toMeasurableSpace) f' (Ioi a) volume
fint : IntegrableOn (mα := MeasureSpace.toMeasurableSpace) f (Ioi a) volume
F : E →L[ℝ] Completion E := Completion.toComplL
Fderiv :
  ∀ x ∈ Ioi a,
    HasDerivAt (F := Completion E) ((⇑F : (a : E) → Completion E) ∘ f : ℝ → Completion E)
      ((F : (a : E) → Completion E) (f' x) : Completion E) x
Fint :
  IntegrableOn (ε := Completion E) (mα := MeasureSpace.toMeasurableSpace) ((⇑F : (a : E) → Completion E) ∘ f) (Ioi a)
    volume
F'int :
  IntegrableOn (ε := Completion E) (mα := MeasureSpace.toMeasurableSpace) ((⇑F : (a : E) → Completion E) ∘ f') (Ioi a)
    volume
A :
  Tendsto (β := Completion E) ((⇑F : (a : E) → Completion E) ∘ f) atTop
    (𝓝 (limUnder atTop ((⇑F : (a : E) → Completion E) ∘ f)))
this :
  IntegrableAtFilter (ε := Completion E) (mα := MeasureSpace.toMeasurableSpace) ((⇑F : (a : E) → Completion E) ∘ f)
    atTop volume
s : Set ℝ
hs : Membership.mem (γ := Filter ℝ) atTop s
b : ℝ
hb : ∀ b_1 ≥ b, b_1 ∈ s
⊢ LE.le (α := ℝ≥0∞) ((volume : (a : Set ℝ) → ℝ≥0∞) (Ici b) : ℝ≥0∞) ((volume : (a : Set ℝ) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
measure_mono hb

Premises used: MeasureTheory.measure_mono