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
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 : ℝ)) < ε
have dist : ‖f x - f (↑N : ℝ)‖ =
  Norm.norm.{u_1} (E := E)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioc (↑N : ℝ) x)) fun (t : ℝ) ↦ f' t)
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
-- 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 : ℝ)
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.dist (f x) (f (↑N : ℝ)) < ε
have 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‖)
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
-- 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
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
⊢ Tendsto f atTop (𝓝 0)
have 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
Tactic: have Fderiv : ∀ x ∈ Ioi a, HasDerivAt (F ∘ f) (F (f' x)) x :=
    fun x hx ↦ F.hasFDerivAt.comp_hasDerivAt _ (hderiv x hx)
-- 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
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
⊢ Tendsto f atTop (𝓝 0)
have Fint : 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
-- 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
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
⊢ Tendsto f atTop (𝓝 0)
have F'int : 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
-- 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
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 f atTop (𝓝 0)
have A : 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
-- 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
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)))
⊢ Eq (α := Completion E) (limUnder atTop ((⇑F : (a : E) → Completion E) ∘ f)) ((F : (a : E) → Completion E) 0)
have this : 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⟩
-- 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
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
⊢ Eq (α := Completion E) (limUnder atTop ((⇑F : (a : E) → Completion E) ∘ f)) ((F : (a : E) → Completion E) 0)
have apply : ∀ (s : Set ℝ),
  Membership.mem (γ := Filter ℝ) atTop s → Eq (α := ℝ≥0∞) ((volume : (a : Set ℝ) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
Tactic: apply IntegrableAtFilter.eq_zero_of_tendsto this ?_ A
-- 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
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
⊢ Eq (α := ℝ≥0∞) ((volume : (a : Set ℝ) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
have rcases : ∀ (b : ℝ) (hb : ∀ b_1 ≥ b, b_1 ∈ s), Eq (α := ℝ≥0∞) ((volume : (a : Set ℝ) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
Tactic: rcases mem_atTop_sets.1 hs with ⟨b, hb⟩
-- 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
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
⊢ Eq (α := ℝ≥0∞) ((volume : (a : Set ℝ) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
have rw : LE.le (α := ℝ≥0∞) ((volume : (a : Set ℝ) → ℝ≥0∞) (Ici b) : ℝ≥0∞) ((volume : (a : Set ℝ) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: rw [← top_le_iff, ← volume_Ici (a := b)]
-- 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
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)))
⊢ Tendsto f atTop (𝓝 0)
have B : Eq (α := Completion E) (limUnder atTop ((⇑F : (a : E) → Completion E) ∘ f)) ((F : (a : E) → Completion E) 0)
Tactic: have B : limUnder atTop (F ∘ f) = F 0 := by
    have : IntegrableAtFilter (F ∘ f) atTop := by exact ⟨Ioi a, Ioi_mem_atTop _, Fint⟩
    apply IntegrableAtFilter.eq_zero_of_tendsto this ?_ A
    intro s hs
    rcases mem_atTop_sets.1 hs with ⟨b, hb⟩
    rw [← top_le_iff, ← volume_Ici (a := b)]
    exact measure_mono hb
-- 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
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)))
B : Eq (α := Completion E) (limUnder atTop ((⇑F : (a : E) → Completion E) ∘ f)) ((F : (a : E) → Completion E) 0)
⊢ Tendsto f atTop (𝓝 0)
have rwa : ∀ (A : Tendsto (β := Completion E) ((⇑F : (a : E) → Completion E) ∘ f) atTop (𝓝 ((F : (a : E) → Completion E) 0)))
  (B : Eq (α := Completion E) (limUnder atTop ((⇑F : (a : E) → Completion E) ∘ f)) ((F : (a : E) → Completion E) 0)),
  IsEmbedding (X := E) (Y := Completion E) (⇑F : (a : E) → Completion E)
Tactic: rwa [B, ← IsEmbedding.tendsto_nhds_iff] at A
Cleared hypotheses: A, B
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntegralEqImproper (goal)
Goal:
E : Type u_1
f f' : ℝ → E
a : ℝ
m : E
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
hcont : ContinuousWithinAt f (Ici a) a
hderiv : ∀ x ∈ Ioi a, HasDerivAt f (f' x) x
f'int : IntegrableOn (mα := MeasureSpace.toMeasurableSpace) f' (Ioi a) volume
hf : Tendsto f atTop (𝓝 m)
x : ℝ
hx : x ∈ Ici a
⊢ ContinuousWithinAt f (Ici a) x
have inl : ∀ (hx : a ∈ Ici a), ContinuousWithinAt f (Ici a) a
Tactic: rcases hx.out.eq_or_lt with rfl | hx
Cleared hypotheses: x, hx
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntegralEqImproper (goal)
Goal:
E : Type u_1
f f' : ℝ → E
a : ℝ
m : E
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
hcont : ContinuousWithinAt f (Ici a) a
hderiv : ∀ x ∈ Ioi a, HasDerivAt f (f' x) x
f'int : IntegrableOn (mα := MeasureSpace.toMeasurableSpace) f' (Ioi a) volume
hf : Tendsto f atTop (𝓝 m)
x : ℝ
hx : x ∈ Ici a
inl : ∀ (hx : a ∈ Ici a), ContinuousWithinAt f (Ici a) a
⊢ ContinuousWithinAt f (Ici a) x
have inr : ∀ (hx : a < x), ContinuousWithinAt f (Ici a) x
Tactic: rcases hx.out.eq_or_lt with rfl | hx
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntegralEqImproper (hypothesis)
Goal:
E : Type u_1
f f' : ℝ → E
a : ℝ
m : E
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
hcont : ContinuousWithinAt f (Ici a) a
hderiv : ∀ x ∈ Ioi a, HasDerivAt f (f' x) x
f'int : IntegrableOn (mα := MeasureSpace.toMeasurableSpace) f' (Ioi a) volume
hf : Tendsto f atTop (𝓝 m)
⊢ (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi a)) fun (x : ℝ) ↦ f' x) = m - f a
have hcont₁ : ContinuousOn f (Ici a)
Tactic: have hcont : ContinuousOn f (Ici a) := by
    intro x hx
    rcases hx.out.eq_or_lt with rfl | hx
    · exact hcont
    · exact (hderiv x hx).continuousAt.continuousWithinAt
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntegralEqImproper (goal)
Goal:
E : Type u_1
f f' : ℝ → E
a : ℝ
m : E
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
hcont_1 : ContinuousWithinAt f (Ici a) a
hderiv : ∀ x ∈ Ioi a, HasDerivAt f (f' x) x
f'int : IntegrableOn (mα := MeasureSpace.toMeasurableSpace) f' (Ioi a) volume
hf : Tendsto f atTop (𝓝 m)
hcont : ContinuousOn f (Ici a)
⊢ (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi a)) fun (x : ℝ) ↦ f' x) = m - f a
have refine : Tendsto (fun (i : ℝ) ↦ ∫ (x : ℝ) in a..id i, f' x) atTop (𝓝 (m - f a))
Tactic: refine tendsto_nhds_unique (intervalIntegral_tendsto_integral_Ioi a f'int tendsto_id) ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntegralEqImproper (goal)
Goal:
E : Type u_1
f f' : ℝ → E
a : ℝ
m : E
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
hcont_1 : ContinuousWithinAt f (Ici a) a
hderiv : ∀ x ∈ Ioi a, HasDerivAt f (f' x) x
f'int : IntegrableOn (mα := MeasureSpace.toMeasurableSpace) f' (Ioi a) volume
hf : Tendsto f atTop (𝓝 m)
hcont : ContinuousOn f (Ici a)
⊢ Tendsto (fun (i : ℝ) ↦ ∫ (x : ℝ) in a..id i, f' x) atTop (𝓝 (m - f a))
have apply : EventuallyEq.{0, u_1} (β := E) atTop (fun (x : ℝ) ↦ f x - f a) fun (i : ℝ) ↦ ∫ (x : ℝ) in a..id i, f' x
Tactic: apply Tendsto.congr' _ (hf.sub_const _)
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntegralEqImproper (goal)
Goal:
E : Type u_1
f f' : ℝ → E
a : ℝ
m : E
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
hcont_1 : ContinuousWithinAt f (Ici a) a
hderiv : ∀ x ∈ Ioi a, HasDerivAt f (f' x) x
f'int : IntegrableOn (mα := MeasureSpace.toMeasurableSpace) f' (Ioi a) volume
hf : Tendsto f atTop (𝓝 m)
hcont : ContinuousOn f (Ici a)
⊢ EventuallyEq.{0, u_1} (β := E) atTop (fun (x : ℝ) ↦ f x - f a) fun (i : ℝ) ↦ ∫ (x : ℝ) in a..id i, f' x
have h : ∀ (x : ℝ) (hx : x ∈ Ioi a), f x - f a = ∫ (x : ℝ) in a..id x, f' x
Tactic: filter_upwards [Ioi_mem_atTop a] with x hx
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntegralEqImproper (hypothesis)
Goal:
E : Type u_1
f f' : ℝ → E
a : ℝ
m : E
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
hcont_1 : ContinuousWithinAt f (Ici a) a
hderiv : ∀ x ∈ Ioi a, HasDerivAt f (f' x) x
f'int : IntegrableOn (mα := MeasureSpace.toMeasurableSpace) f' (Ioi a) volume
hf : Tendsto f atTop (𝓝 m)
hcont : ContinuousOn f (Ici a)
x : ℝ
hx : x ∈ Ioi a
⊢ f x - f a = ∫ (x : ℝ) in a..id x, f' x
have h'x : a ≤ id x
Tactic: have h'x : a ≤ id x := le_of_lt hx
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntegralEqImproper (goal)
Goal:
E : Type u_1
f f' : ℝ → E
a : ℝ
m : E
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
hcont_1 : ContinuousWithinAt f (Ici a) a
hderiv : ∀ x ∈ Ioi a, HasDerivAt f (f' x) x
f'int : IntegrableOn (mα := MeasureSpace.toMeasurableSpace) f' (Ioi a) volume
hf : Tendsto f atTop (𝓝 m)
hcont : ContinuousOn f (Ici a)
x : ℝ
hx : x ∈ Ioi a
h'x : a ≤ id x
⊢ f x - f a = ∫ (x : ℝ) in a..id x, f' x
have h : ∫ (x : ℝ) in a..id x, f' x = f x - f a
Tactic: symm
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntegralEqImproper (goal)
Goal:
E : Type u_1
f f' : ℝ → E
a : ℝ
m : E
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
hcont_1 : ContinuousWithinAt f (Ici a) a
hderiv : ∀ x ∈ Ioi a, HasDerivAt f (f' x) x
f'int : IntegrableOn (mα := MeasureSpace.toMeasurableSpace) f' (Ioi a) volume
hf : Tendsto f atTop (𝓝 m)
hcont : ContinuousOn f (Ici a)
x : ℝ
hx : x ∈ Ioi a
h'x : a ≤ id x
⊢ ∫ (x : ℝ) in a..id x, f' x = f x - f a
have h : IntervalIntegrable f' volume a (id x)
Tactic: apply
    intervalIntegral.integral_eq_sub_of_hasDerivAt_of_le h'x (hcont.mono Icc_subset_Ici_self)
      fun y hy => hderiv y hy.1
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntegralEqImproper (goal)
Goal:
E : Type u_1
f f' : ℝ → E
a : ℝ
m : E
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
hcont_1 : ContinuousWithinAt f (Ici a) a
hderiv : ∀ x ∈ Ioi a, HasDerivAt f (f' x) x
f'int : IntegrableOn (mα := MeasureSpace.toMeasurableSpace) f' (Ioi a) volume
hf : Tendsto f atTop (𝓝 m)
hcont : ContinuousOn f (Ici a)
x : ℝ
hx : x ∈ Ioi a
h'x : a ≤ id x
⊢ IntervalIntegrable f' volume a (id x)
have h : IntegrableOn (mα := measurableSpace) f' (Ioc a (id x)) volume
Tactic: rw [intervalIntegrable_iff_integrableOn_Ioc_of_le h'x]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntegralEqImproper (goal)
Goal:
E : Type u_1
f f' : ℝ → E
a : ℝ
m : E
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
hderiv : ∀ x ∈ Ici a, HasDerivAt f (f' x) x
f'int : IntegrableOn (mα := MeasureSpace.toMeasurableSpace) f' (Ioi a) volume
hf : Tendsto f atTop (𝓝 m)
⊢ (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi a)) fun (x : ℝ) ↦ f' x) = m - f a
have refine : ContinuousWithinAt f (Ici a) a
Tactic: refine integral_Ioi_of_hasDerivAt_of_tendsto ?_ (fun x hx => hderiv x hx.out.le)
    f'int hf
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntegralEqImproper (hypothesis)
Goal:
E : Type u_1
f : ℝ → E
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
hf : ContDiff ℝ 1 f
h2f : HasCompactSupport f
b : ℝ
⊢ (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi b)) fun (x : ℝ) ↦ deriv f x) = -f b
have this : ∀ x ∈ Ioi b, HasDerivAt f (deriv f x) x
Tactic: have := fun x (_ : x ∈ Ioi b) ↦ hf.differentiable one_ne_zero x |>.hasDerivAt
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntegralEqImproper (goal)
Goal:
E : Type u_1
f : ℝ → E
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
hf : ContDiff ℝ 1 f
h2f : HasCompactSupport f
b : ℝ
this : ∀ x ∈ Ioi b, HasDerivAt f (deriv f x) x
⊢ (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi b)) fun (x : ℝ) ↦ deriv f x) = -f b
have f'int : IntegrableOn (mα := MeasureSpace.toMeasurableSpace) (deriv f) (Ioi b) volume
Tactic: rw [integral_Ioi_of_hasDerivAt_of_tendsto hf.continuous.continuousWithinAt this, zero_sub]