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
n : ℕ
hn : a < (↑n : ℝ)
⊢ ∃ (i : ℕ), IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ ‖f' x‖) (Ici (↑i : ℝ)) volume

Tactic:
⟨n, IntegrableOn.mono_set f'int.norm (Ici_subset_Ioi.2 hn)⟩

Premises used: Iff.mpr, MeasureTheory.IntegrableOn.mono_set, Exists.intro, 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
n : ℕ
hn : a < (↑n : ℝ)
⊢ ∃ (i : ℕ), IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ ‖f' x‖) (Ici (↑i : ℝ)) volume

Tactic:
exact ⟨n, IntegrableOn.mono_set f'int.norm (Ici_subset_Ioi.2 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
⊢ Tendsto (β := ℝ)
    (fun (n : ℕ) ↦
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ici (↑n : ℝ))) fun (x : ℝ) ↦ ‖f' x‖)
    atTop
    (𝓝
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (⋂ (n : ℕ), Ici (↑n : ℝ)))
        fun (x : ℝ) ↦ ‖f' x‖))

Tactic:
have L : Tendsto (fun (n : ℕ) ↦ ∫ x in Ici (n : ℝ), ‖f' x‖) atTop
        (𝓝 (∫ x in ⋂ (n : ℕ), Ici (n : ℝ), ‖f' x‖)) := by
      apply tendsto_setIntegral_of_antitone (fun n ↦ measurableSet_Ici)
      · intro m n hmn
        exact Ici_subset_Ici.2 (Nat.cast_le.mpr hmn)
      · rcases exists_nat_gt a with ⟨n, hn⟩
        exact ⟨n, IntegrableOn.mono_set f'int.norm (Ici_subset_Ioi.2 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
L :
  Tendsto (β := ℝ)
    (fun (n : ℕ) ↦
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ici (↑n : ℝ))) fun (x : ℝ) ↦ ‖f' x‖)
    atTop
    (𝓝
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (⋂ (n : ℕ), Ici (↑n : ℝ)))
        fun (x : ℝ) ↦ ‖f' x‖))
apply : ∀ (x : ℝ), x ∉ ⋂ (n : ℕ), Ici (↑n : ℝ)
⊢ Eq (α := Set ℝ) (⋂ (n : ℕ), Ici (↑n : ℝ)) ∅

Tactic:
apply eq_empty_of_forall_notMem (fun x ↦ ?_)

Premises used: Set.eq_empty_of_forall_notMem
-- 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
L :
  Tendsto (β := ℝ)
    (fun (n : ℕ) ↦
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ici (↑n : ℝ))) fun (x : ℝ) ↦ ‖f' x‖)
    atTop
    (𝓝
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (⋂ (n : ℕ), Ici (↑n : ℝ)))
        fun (x : ℝ) ↦ ‖f' x‖))
x : ℝ
⊢ x ∉ ⋂ (n : ℕ), Ici (↑n : ℝ)

Tactic:
simpa only [mem_iInter, mem_Ici, not_forall, not_le] using exists_nat_gt x

Premises used: not_le, Set.mem_iInter, Set.mem_Ici, exists_nat_gt, Classical.not_forall
-- 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
L :
  Tendsto (β := ℝ)
    (fun (n : ℕ) ↦
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ici (↑n : ℝ))) fun (x : ℝ) ↦ ‖f' x‖)
    atTop
    (𝓝
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (⋂ (n : ℕ), Ici (↑n : ℝ)))
        fun (x : ℝ) ↦ ‖f' x‖))
⊢ Eq (α := Set ℝ) (⋂ (n : ℕ), Ici (↑n : ℝ)) ∅

Tactic:
have B : ⋂ (n : ℕ), Ici (n : ℝ) = ∅ := by
      apply eq_empty_of_forall_notMem (fun x ↦ ?_)
      simpa only [mem_iInter, mem_Ici, not_forall, not_le] using exists_nat_gt x
-- 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
L :
  Tendsto (β := ℝ)
    (fun (n : ℕ) ↦
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ici (↑n : ℝ))) fun (x : ℝ) ↦ ‖f' x‖)
    atTop
    (𝓝
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (⋂ (n : ℕ), Ici (↑n : ℝ)))
        fun (x : ℝ) ↦ ‖f' x‖))
B : Eq (α := Set ℝ) (⋂ (n : ℕ), Ici (↑n : ℝ)) ∅
⊢ Tendsto (β := ℝ)
    (fun (n : ℕ) ↦
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ici (↑n : ℝ))) fun (x : ℝ) ↦ ‖f' x‖)
    atTop (𝓝 0)

Tactic:
simp only [B, Measure.restrict_empty, integral_zero_measure] at L

Premises used: MeasureTheory.Measure.restrict_empty, MeasureTheory.integral_zero_measure
-- 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
B : Eq (α := Set ℝ) (⋂ (n : ℕ), Ici (↑n : ℝ)) ∅
L :
  Tendsto (β := ℝ)
    (fun (n : ℕ) ↦
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ici (↑n : ℝ))) fun (x : ℝ) ↦ ‖f' x‖)
    atTop (𝓝 0)
⊢ ∀ᶠ (n : ℕ) in atTop,
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ici (↑n : ℝ))) fun (x : ℝ) ↦ ‖f' x‖) < ε

Tactic:
(tendsto_order.1 L).2 _ εpos

Premises used: tendsto_order, And.right, Iff.mp
-- 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
B : Eq (α := Set ℝ) (⋂ (n : ℕ), Ici (↑n : ℝ)) ∅
L :
  Tendsto (β := ℝ)
    (fun (n : ℕ) ↦
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ici (↑n : ℝ))) fun (x : ℝ) ↦ ‖f' x‖)
    atTop (𝓝 0)
⊢ ∀ᶠ (n : ℕ) in atTop,
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ici (↑n : ℝ))) fun (x : ℝ) ↦ ‖f' x‖) < ε

Tactic:
exact (tendsto_order.1 L).2 _ εpos

Premises used: tendsto_order, And.right, Iff.mp
-- 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
⊢ ∀ᶠ (n : ℕ) in atTop,
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ici (↑n : ℝ))) fun (x : ℝ) ↦ ‖f' x‖) < ε

Tactic:
have A : ∀ᶠ (n : ℕ) in atTop, ∫ (x : ℝ) in Ici ↑n, ‖f' x‖ < ε := by
    have L : Tendsto (fun (n : ℕ) ↦ ∫ x in Ici (n : ℝ), ‖f' x‖) atTop
        (𝓝 (∫ x in ⋂ (n : ℕ), Ici (n : ℝ), ‖f' x‖)) := by
      apply tendsto_setIntegral_of_antitone (fun n ↦ measurableSet_Ici)
      · intro m n hmn
        exact Ici_subset_Ici.2 (Nat.cast_le.mpr hmn)
      · rcases exists_nat_gt a with ⟨n, hn⟩
        exact ⟨n, IntegrableOn.mono_set f'int.norm (Ici_subset_Ioi.2 hn)⟩
    have B : ⋂ (n : ℕ), Ici (n : ℝ) = ∅ := by
      apply eq_empty_of_forall_notMem (fun x ↦ ?_)
      simpa only [mem_iInter, mem_Ici, not_forall, not_le] using exists_nat_gt x
    simp only [B, Measure.restrict_empty, integral_zero_measure] at L
    exact (tendsto_order.1 L).2 _ εpos
-- 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‖) < ε
rcases : ∀ (n : ℕ) (hn : a < (↑n : ℝ)), ∀ᶠ (n : ℕ) in atTop, a < (↑n : ℝ)
⊢ ∀ᶠ (n : ℕ) in atTop, a < (↑n : ℝ)

Tactic:
rcases exists_nat_gt a with ⟨n, hn⟩

Premises used: exists_nat_gt
-- 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‖) < ε
n : ℕ
hn : a < (↑n : ℝ)
m : ℕ
h : ∀ (hm : n < m), a < (↑m : ℝ)
⊢ m ∈ Ioi n → a < (↑m : ℝ)

Tactic:
(hm : n < m)
-- 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‖) < ε
n : ℕ
hn : a < (↑n : ℝ)
m : ℕ
hm : n < m
⊢ a < (↑m : ℝ)

Tactic:
hn.trans (Nat.cast_lt.mpr hm)

Premises used: Iff.mpr, LT.lt.trans, Nat.cast_lt
-- 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‖) < ε
n : ℕ
hn : a < (↑n : ℝ)
h :
  ∀ (a_1 : ℕ),
    Membership.mem (γ := Set ℕ)
      {x : ℕ | x ∈ Ioi n → Membership.mem (γ := Set ℕ) {x : ℕ | (fun (n : ℕ) ↦ a < (↑n : ℝ)) x} x} a_1
h₁ : ∀ a_1 ∈ Ioi n, a < (↑a_1 : ℝ)
h₂ : ∀ (m : ℕ) (hm : n < m), a < (↑m : ℝ)
⊢ ∀ᶠ (n : ℕ) in atTop, a < (↑n : ℝ)

Tactic:
filter_upwards [Ioi_mem_atTop n] with m (hm : n < m) using hn.trans (Nat.cast_lt.mpr hm)

Premises used: Filter.Ioi_mem_atTop
-- 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‖) < ε
⊢ ∀ᶠ (n : ℕ) in atTop, a < (↑n : ℝ)

Tactic:
have B : ∀ᶠ (n : ℕ) in atTop, a < n := by
    rcases exists_nat_gt a with ⟨n, hn⟩
    filter_upwards [Ioi_mem_atTop n] with m (hm : n < m) using hn.trans (Nat.cast_lt.mpr hm)
-- 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 : ℝ)
rcases :
  ∀ (N : ℕ)
    (hN :
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ici (↑N : ℝ))) fun (x : ℝ) ↦ ‖f' x‖) <
        ε)
    (h'N : a < (↑N : ℝ)), ∃ (N : ℝ), ∀ n ≥ N, dist (f n) (f N) < ε
⊢ ∃ (N : ℝ), ∀ n ≥ N, dist (f n) (f N) < ε

Tactic:
rcases (A.and B).exists with ⟨N, hN, h'N⟩

Premises used: Filter.Eventually.and, Filter.Eventually.exists
-- 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 : ℝ)
⊢ ∃ (N : ℝ), ∀ n ≥ N, dist (f n) (f N) < ε

Tactic:
⟨N, fun x hx ↦ ?_⟩

Premises used: Nat.cast, Exists.intro
-- 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 : ℝ)
refine : ∀ (x : ℝ) (hx : x ≥ (↑N : ℝ)), dist (f x) (f (↑N : ℝ)) < ε
⊢ ∃ (N : ℝ), ∀ n ≥ N, dist (f n) (f N) < ε

Tactic:
refine ⟨N, fun x hx ↦ ?_⟩
-- 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 : ℝ)) = ‖f x - f (↑N : ℝ)‖

Tactic:
dist_eq_norm _ _

Premises used: dist_eq_norm
-- 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 : ℝ)
hderiv₁ : ∀ x_1 ∈ [[(↑N : ℝ), x]], HasDerivAt f (f' x_1) x_1
hint : IntervalIntegrable f' volume (↑N : ℝ) x
⊢ ‖f x - f (↑N : ℝ)‖ =
    Norm.norm.{u_1} (E := E)
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioc (↑N : ℝ) x)) fun (t : ℝ) ↦ f' t)

Tactic:
rw [← intervalIntegral.integral_of_le hx, intervalIntegral.integral_eq_sub_of_hasDerivAt]

Premises used: intervalIntegral.integral_eq_sub_of_hasDerivAt, intervalIntegral.integral_of_le
-- 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 : ℝ)
y : ℝ
hy : y ∈ [[(↑N : ℝ), x]]
⊢ (↑N : ℝ) ≤ y ∧ y ≤ x

Tactic:
simp only [hx, uIcc_of_le, mem_Icc] at hy

Premises used: Set.uIcc_of_le, Set.mem_Icc
-- 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 : ℝ)
y : ℝ
hy : (↑N : ℝ) ≤ y ∧ y ≤ x
⊢ HasDerivAt f (f' y) y

Tactic:
hderiv _ (h'N.trans_le hy.1)

Premises used: And.left, LT.lt.trans_le
-- 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 : ℝ)
y : ℝ
hy : (↑N : ℝ) ≤ y ∧ y ≤ x
⊢ HasDerivAt f (f' y) y

Tactic:
exact hderiv _ (h'N.trans_le hy.1)

Premises used: And.left, LT.lt.trans_le
-- 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 : ℝ)
hint : IntegrableOn (mα := measurableSpace) f' (Ioc (↑N : ℝ) x) volume
⊢ IntervalIntegrable f' volume (↑N : ℝ) x

Tactic:
rw [intervalIntegrable_iff_integrableOn_Ioc_of_le hx]

Premises used: intervalIntegrable_iff_integrableOn_Ioc_of_le
-- 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α := measurableSpace) f' (Ioc (↑N : ℝ) x) volume

Tactic:
f'int.mono_set (Ioc_subset_Ioi_self.trans (Ioi_subset_Ioi h'N.le))

Premises used: HasSubset.Subset.trans, LT.lt.le, Set.Ioc_subset_Ioi_self, MeasureTheory.IntegrableOn.mono_set, Set.Ioi_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 : ℝ
hx : x ≥ (↑N : ℝ)
⊢ IntegrableOn (mα := measurableSpace) f' (Ioc (↑N : ℝ) x) volume

Tactic:
exact f'int.mono_set (Ioc_subset_Ioi_self.trans (Ioi_subset_Ioi h'N.le))

Premises used: HasSubset.Subset.trans, LT.lt.le, Set.Ioc_subset_Ioi_self, MeasureTheory.IntegrableOn.mono_set, Set.Ioi_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 : ℝ
hx : x ≥ (↑N : ℝ)
⊢ Norm.norm.{u_1} (E := E)
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioc (↑N : ℝ) x)) fun (t : ℝ) ↦ f' t) ≤
    @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioc (↑N : ℝ) x)) fun (t : ℝ) ↦ ‖f' t‖

Tactic:
norm_integral_le_integral_norm fun a ↦ f' a

Premises used: MeasureTheory.norm_integral_le_integral_norm
-- 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 : ℝ)
hfi : IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ ‖f' x‖) (Ici (↑N : ℝ)) volume
hf : (ae (F := Measure ℝ) (Measure.restrict volume (Ici (↑N : ℝ)))).EventuallyLE (β := ℝ) 0 fun (x : ℝ) ↦ ‖f' x‖
hst : Ioc (↑N : ℝ) x ≤ᶠ[ae (F := Measure ℝ) volume] Ici (↑N : ℝ)
⊢ 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‖)

Tactic:
apply setIntegral_mono_set

Premises used: MeasureTheory.setIntegral_mono_set