awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntegralEqImproper (goal)
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‖))
have h_anti : Antitone (β := Set ℝ) fun (n : ℕ) ↦ Ici (↑n : ℝ)
Tactic: apply tendsto_setIntegral_of_antitone (fun n ↦ measurableSet_Ici)
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntegralEqImproper (goal)
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
h_anti : Antitone (β := Set ℝ) fun (n : ℕ) ↦ Ici (↑n : ℝ)
⊢ 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‖))
have hfi : ∃ (i : ℕ), IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ ‖f' x‖) (Ici (↑i : ℝ)) volume
Tactic: apply tendsto_setIntegral_of_antitone (fun n ↦ measurableSet_Ici)
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntegralEqImproper (goal)
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
⊢ ∃ (i : ℕ), IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ ‖f' x‖) (Ici (↑i : ℝ)) volume
have hfi : ∀ (n : ℕ) (hn : a < (↑n : ℝ)),
  ∃ (i : ℕ), IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ ‖f' x‖) (Ici (↑i : ℝ)) volume
Tactic: rcases exists_nat_gt a with ⟨n, hn⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntegralEqImproper (hypothesis)
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‖) < ε
have 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‖))
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)⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntegralEqImproper (goal)
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 : ℝ)) ∅
have apply : ∀ (x : ℝ), x ∉ ⋂ (n : ℕ), Ici (↑n : ℝ)
Tactic: apply eq_empty_of_forall_notMem (fun x ↦ ?_)
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntegralEqImproper (hypothesis)
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‖))
⊢ ∀ᶠ (n : ℕ) in atTop,
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ici (↑n : ℝ))) fun (x : ℝ) ↦ ‖f' x‖) < ε
have B : 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
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntegralEqImproper (hypothesis)
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 : ℝ)) ∅
⊢ ∀ᶠ (n : ℕ) in atTop,
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ici (↑n : ℝ))) fun (x : ℝ) ↦ ‖f' x‖) < ε
have L₁ : 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
Cleared hypotheses: L
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntegralEqImproper (hypothesis)
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 : ℝ), ∀ n ≥ N, dist (f n) (f N) < ε
have A : ∀ᶠ (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
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntegralEqImproper (goal)
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 : ℝ)
have rcases : ∀ (n : ℕ) (hn : a < (↑n : ℝ)), ∀ᶠ (n : ℕ) in atTop, a < (↑n : ℝ)
Tactic: rcases exists_nat_gt a with ⟨n, hn⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntegralEqImproper (goal)
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 : ℕ
⊢ m ∈ Ioi n → a < (↑m : ℝ)
have h : ∀ (hm : n < m), a < (↑m : ℝ)
Tactic: (hm : n < m)
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntegralEqImproper (goal)
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 : ℝ)
⊢ ∀ᶠ (n : ℕ) in atTop, a < (↑n : ℝ)
have h : ∀ (a_1 : ℕ),
  Membership.mem (γ := Set ℕ)
    {x : ℕ | x ∈ Ioi n → Membership.mem (γ := Set ℕ) {x : ℕ | (fun (n : ℕ) ↦ a < (↑n : ℝ)) x} x} a_1
Tactic: filter_upwards [Ioi_mem_atTop n] with m (hm : n < m) using hn.trans (Nat.cast_lt.mpr hm)
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntegralEqImproper (goal)
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
⊢ ∀ᶠ (n : ℕ) in atTop, a < (↑n : ℝ)
have h₁ : ∀ a_1 ∈ Ioi n, a < (↑a_1 : ℝ)
Tactic: filter_upwards [Ioi_mem_atTop n] with m (hm : n < m) using hn.trans (Nat.cast_lt.mpr hm)
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntegralEqImproper (goal)
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 : ℝ)
⊢ ∀ᶠ (n : ℕ) in atTop, a < (↑n : ℝ)
have h₂ : ∀ (m : ℕ) (hm : n < m), a < (↑m : ℝ)
Tactic: filter_upwards [Ioi_mem_atTop n] with m (hm : n < m) using hn.trans (Nat.cast_lt.mpr hm)
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntegralEqImproper (hypothesis)
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 : ℝ), ∀ n ≥ N, dist (f n) (f N) < ε
have B : ∀ᶠ (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)
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntegralEqImproper (goal)
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 : ℝ), ∀ n ≥ N, dist (f n) (f N) < ε
have 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) < ε
Tactic: rcases (A.and B).exists with ⟨N, hN, h'N⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntegralEqImproper (goal)
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) < ε
have refine : ∀ (x : ℝ) (hx : x ≥ (↑N : ℝ)), dist (f x) (f (↑N : ℝ)) < ε
Tactic: refine ⟨N, fun x hx ↦ ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntegralEqImproper (goal)
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 : ℝ)
⊢ ‖f x - f (↑N : ℝ)‖ =
    Norm.norm.{u_1} (E := E)
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioc (↑N : ℝ) x)) fun (t : ℝ) ↦ f' t)
have hderiv₁ : ∀ x_1 ∈ [[(↑N : ℝ), x]], HasDerivAt f (f' x_1) x_1
Tactic: rw [← intervalIntegral.integral_of_le hx, intervalIntegral.integral_eq_sub_of_hasDerivAt]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntegralEqImproper (goal)
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
⊢ ‖f x - f (↑N : ℝ)‖ =
    Norm.norm.{u_1} (E := E)
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioc (↑N : ℝ) x)) fun (t : ℝ) ↦ f' t)
have hint : IntervalIntegrable f' volume (↑N : ℝ) x
Tactic: rw [← intervalIntegral.integral_of_le hx, intervalIntegral.integral_eq_sub_of_hasDerivAt]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntegralEqImproper (hypothesis)
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]]
⊢ HasDerivAt f (f' y) y
have hy₁ : (↑N : ℝ) ≤ y ∧ y ≤ x
Tactic: simp only [hx, uIcc_of_le, mem_Icc] at hy
Cleared hypotheses: hy
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntegralEqImproper (goal)
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 : ℝ)
⊢ IntervalIntegrable f' volume (↑N : ℝ) x
have hint : IntegrableOn (mα := measurableSpace) f' (Ioc (↑N : ℝ) x) volume
Tactic: rw [intervalIntegrable_iff_integrableOn_Ioc_of_le hx]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntegralEqImproper (goal)
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 : ℝ)
⊢ 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‖)
have hfi : IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ ‖f' x‖) (Ici (↑N : ℝ)) volume
Tactic: apply setIntegral_mono_set
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntegralEqImproper (goal)
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
⊢ 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‖)
have hf : (ae (F := Measure ℝ) (Measure.restrict volume (Ici (↑N : ℝ)))).EventuallyLE (β := ℝ) 0 fun (x : ℝ) ↦ ‖f' x‖
Tactic: apply setIntegral_mono_set
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntegralEqImproper (goal)
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‖
⊢ 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‖)
have hst : Ioc (↑N : ℝ) x ≤ᶠ[ae (F := Measure ℝ) volume] Ici (↑N : ℝ)
Tactic: apply setIntegral_mono_set
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntegralEqImproper (goal)
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 : ℝ)
⊢ (ae (F := Measure ℝ) (Measure.restrict volume (Ici (↑N : ℝ)))).EventuallyLE (β := ℝ) 0 fun (x : ℝ) ↦ ‖f' x‖
have hf : ∀ (a : ℝ), Membership.mem (γ := Set ℝ) {x : ℝ | (fun (x : ℝ) ↦ LE.le (α := ℝ) (0 x) ((fun (x : ℝ) ↦ ‖f' x‖) x)) x} a
Tactic: filter_upwards with x using norm_nonneg _
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntegralEqImproper (goal)
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
⊢ (ae (F := Measure ℝ) (Measure.restrict volume (Ici (↑N : ℝ)))).EventuallyLE (β := ℝ) 0 fun (x : ℝ) ↦ ‖f' x‖
have hf₁ : ∀ (a : ℝ), 0 a ≤ ‖f' a‖
Tactic: filter_upwards with x using norm_nonneg _
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntegralEqImproper (hypothesis)
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 ≤ᶠ[ae (F := Measure ℝ) volume] Ici (↑N : ℝ)
have this : Ioc (↑N : ℝ) x ⊆ Ici (↑N : ℝ)
Tactic: have : Ioc (↑N) x ⊆ Ici ↑N := Ioc_subset_Ioi_self.trans Ioi_subset_Ici_self