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
hderiv : ∀ x ∈ Iic a, HasDerivAt f (f' x) x
f'int : IntegrableOn (mα := MeasureSpace.toMeasurableSpace) f' (Iic a) volume
fint : IntegrableOn (mα := MeasureSpace.toMeasurableSpace) f (Iic a) volume
F : E →L[ℝ] Completion E := Completion.toComplL
Fderiv :
  ∀ x ∈ Iic 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) (Iic a)
    volume
F'int :
  IntegrableOn (ε := Completion E) (mα := MeasureSpace.toMeasurableSpace) ((⇑F : (a : E) → Completion E) ∘ f') (Iic a)
    volume
A :
  Tendsto (β := Completion E) ((⇑F : (a : E) → Completion E) ∘ f) atBot
    (𝓝 (limUnder atBot ((⇑F : (a : E) → Completion E) ∘ f)))
this :
  IntegrableAtFilter (ε := Completion E) (mα := MeasureSpace.toMeasurableSpace) ((⇑F : (a : E) → Completion E) ∘ f)
    atBot volume
s : Set ℝ
hs : Membership.mem (γ := Filter ℝ) atBot s
b : ℝ
hb : ∀ b_1 ≤ b, b_1 ∈ s
⊢ Eq (α := ℝ≥0∞) ((volume : (a : Set ℝ) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
have apply : LE.le (α := ℝ≥0∞) (∞ : ℝ≥0∞) ((volume : (a : Set ℝ) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: apply le_antisymm (le_top)
-- 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 ∈ Iic a, HasDerivAt f (f' x) x
f'int : IntegrableOn (mα := MeasureSpace.toMeasurableSpace) f' (Iic a) volume
fint : IntegrableOn (mα := MeasureSpace.toMeasurableSpace) f (Iic a) volume
F : E →L[ℝ] Completion E := Completion.toComplL
Fderiv :
  ∀ x ∈ Iic 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) (Iic a)
    volume
F'int :
  IntegrableOn (ε := Completion E) (mα := MeasureSpace.toMeasurableSpace) ((⇑F : (a : E) → Completion E) ∘ f') (Iic a)
    volume
A :
  Tendsto (β := Completion E) ((⇑F : (a : E) → Completion E) ∘ f) atBot
    (𝓝 (limUnder atBot ((⇑F : (a : E) → Completion E) ∘ f)))
this :
  IntegrableAtFilter (ε := Completion E) (mα := MeasureSpace.toMeasurableSpace) ((⇑F : (a : E) → Completion E) ∘ f)
    atBot volume
s : Set ℝ
hs : Membership.mem (γ := Filter ℝ) atBot s
b : ℝ
hb : ∀ b_1 ≤ b, b_1 ∈ s
⊢ LE.le (α := ℝ≥0∞) (∞ : ℝ≥0∞) ((volume : (a : Set ℝ) → ℝ≥0∞) s : ℝ≥0∞)
have rw : LE.le (α := ℝ≥0∞) ((volume : (a : Set ℝ) → ℝ≥0∞) (Iic b) : ℝ≥0∞) ((volume : (a : Set ℝ) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: rw [← volume_Iic (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 ∈ Iic a, HasDerivAt f (f' x) x
f'int : IntegrableOn (mα := MeasureSpace.toMeasurableSpace) f' (Iic a) volume
fint : IntegrableOn (mα := MeasureSpace.toMeasurableSpace) f (Iic a) volume
F : E →L[ℝ] Completion E := Completion.toComplL
Fderiv :
  ∀ x ∈ Iic 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) (Iic a)
    volume
F'int :
  IntegrableOn (ε := Completion E) (mα := MeasureSpace.toMeasurableSpace) ((⇑F : (a : E) → Completion E) ∘ f') (Iic a)
    volume
A :
  Tendsto (β := Completion E) ((⇑F : (a : E) → Completion E) ∘ f) atBot
    (𝓝 (limUnder atBot ((⇑F : (a : E) → Completion E) ∘ f)))
⊢ Tendsto f atBot (𝓝 0)
have B : Eq (α := Completion E) (limUnder atBot ((⇑F : (a : E) → Completion E) ∘ f)) ((F : (a : E) → Completion E) 0)
Tactic: have B : limUnder atBot (F ∘ f) = F 0 := by
    have : IntegrableAtFilter (F ∘ f) atBot := by exact ⟨Iic a, Iic_mem_atBot _, Fint⟩
    apply IntegrableAtFilter.eq_zero_of_tendsto this ?_ A
    intro s hs
    rcases mem_atBot_sets.1 hs with ⟨b, hb⟩
    apply le_antisymm (le_top)
    rw [← volume_Iic (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 ∈ Iic a, HasDerivAt f (f' x) x
f'int : IntegrableOn (mα := MeasureSpace.toMeasurableSpace) f' (Iic a) volume
fint : IntegrableOn (mα := MeasureSpace.toMeasurableSpace) f (Iic a) volume
F : E →L[ℝ] Completion E := Completion.toComplL
Fderiv :
  ∀ x ∈ Iic 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) (Iic a)
    volume
F'int :
  IntegrableOn (ε := Completion E) (mα := MeasureSpace.toMeasurableSpace) ((⇑F : (a : E) → Completion E) ∘ f') (Iic a)
    volume
A :
  Tendsto (β := Completion E) ((⇑F : (a : E) → Completion E) ∘ f) atBot
    (𝓝 (limUnder atBot ((⇑F : (a : E) → Completion E) ∘ f)))
B : Eq (α := Completion E) (limUnder atBot ((⇑F : (a : E) → Completion E) ∘ f)) ((F : (a : E) → Completion E) 0)
⊢ Tendsto f atBot (𝓝 0)
have rwa : ∀ (A : Tendsto (β := Completion E) ((⇑F : (a : E) → Completion E) ∘ f) atBot (𝓝 ((F : (a : E) → Completion E) 0)))
  (B : Eq (α := Completion E) (limUnder atBot ((⇑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 (Iic a) a
hderiv : ∀ x ∈ Iio a, HasDerivAt f (f' x) x
f'int : IntegrableOn (mα := MeasureSpace.toMeasurableSpace) f' (Iic a) volume
hf : Tendsto f atBot (𝓝 m)
x : ℝ
hx : x ∈ Iic a
⊢ ContinuousWithinAt f (Iic a) x
have inl : ∀ (hcont : ContinuousWithinAt f (Iic x) x) (hderiv : ∀ x_1 ∈ Iio x, HasDerivAt f (f' x_1) x_1)
  (f'int : IntegrableOn (mα := MeasureSpace.toMeasurableSpace) f' (Iic x) volume) (hx : x ∈ Iic x),
  ContinuousWithinAt f (Iic x) x
Tactic: rcases hx.out.eq_or_lt with rfl | hx
Cleared hypotheses: a, hcont, hderiv, f'int, 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 (Iic a) a
hderiv : ∀ x ∈ Iio a, HasDerivAt f (f' x) x
f'int : IntegrableOn (mα := MeasureSpace.toMeasurableSpace) f' (Iic a) volume
hf : Tendsto f atBot (𝓝 m)
x : ℝ
hx : x ∈ Iic a
inl :
  ∀ (hcont : ContinuousWithinAt f (Iic x) x) (hderiv : ∀ x_1 ∈ Iio x, HasDerivAt f (f' x_1) x_1)
    (f'int : IntegrableOn (mα := MeasureSpace.toMeasurableSpace) f' (Iic x) volume) (hx : x ∈ Iic x),
    ContinuousWithinAt f (Iic x) x
⊢ ContinuousWithinAt f (Iic a) x
have inr : ∀ (hx : x < a), ContinuousWithinAt f (Iic 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 (Iic a) a
hderiv : ∀ x ∈ Iio a, HasDerivAt f (f' x) x
f'int : IntegrableOn (mα := MeasureSpace.toMeasurableSpace) f' (Iic a) volume
hf : Tendsto f atBot (𝓝 m)
⊢ (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Iic a)) fun (x : ℝ) ↦ f' x) = f a - m
have hcont₁ : ContinuousOn f (Iic a)
Tactic: have hcont : ContinuousOn f (Iic 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 (Iic a) a
hderiv : ∀ x ∈ Iio a, HasDerivAt f (f' x) x
f'int : IntegrableOn (mα := MeasureSpace.toMeasurableSpace) f' (Iic a) volume
hf : Tendsto f atBot (𝓝 m)
hcont : ContinuousOn f (Iic a)
⊢ (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Iic a)) fun (x : ℝ) ↦ f' x) = f a - m
have refine : Tendsto (fun (i : ℝ) ↦ ∫ (x : ℝ) in id i..a, f' x) atBot (𝓝 (f a - m))
Tactic: refine tendsto_nhds_unique (intervalIntegral_tendsto_integral_Iic 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 (Iic a) a
hderiv : ∀ x ∈ Iio a, HasDerivAt f (f' x) x
f'int : IntegrableOn (mα := MeasureSpace.toMeasurableSpace) f' (Iic a) volume
hf : Tendsto f atBot (𝓝 m)
hcont : ContinuousOn f (Iic a)
⊢ Tendsto (fun (i : ℝ) ↦ ∫ (x : ℝ) in id i..a, f' x) atBot (𝓝 (f a - m))
have apply : EventuallyEq.{0, u_1} (β := E) atBot (fun (x : ℝ) ↦ f a - f x) fun (i : ℝ) ↦ ∫ (x : ℝ) in id i..a, f' x
Tactic: apply Tendsto.congr' _ (hf.const_sub _)
-- 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 (Iic a) a
hderiv : ∀ x ∈ Iio a, HasDerivAt f (f' x) x
f'int : IntegrableOn (mα := MeasureSpace.toMeasurableSpace) f' (Iic a) volume
hf : Tendsto f atBot (𝓝 m)
hcont : ContinuousOn f (Iic a)
⊢ EventuallyEq.{0, u_1} (β := E) atBot (fun (x : ℝ) ↦ f a - f x) fun (i : ℝ) ↦ ∫ (x : ℝ) in id i..a, f' x
have h : ∀ (x : ℝ) (hx : x ∈ Iic a), f a - f x = ∫ (x : ℝ) in id x..a, f' x
Tactic: filter_upwards [Iic_mem_atBot a] with 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_1 : ContinuousWithinAt f (Iic a) a
hderiv : ∀ x ∈ Iio a, HasDerivAt f (f' x) x
f'int : IntegrableOn (mα := MeasureSpace.toMeasurableSpace) f' (Iic a) volume
hf : Tendsto f atBot (𝓝 m)
hcont : ContinuousOn f (Iic a)
x : ℝ
hx : x ∈ Iic a
⊢ f a - f x = ∫ (x : ℝ) in id x..a, f' x
have h : ∫ (x : ℝ) in id x..a, f' x = f a - f x
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 (Iic a) a
hderiv : ∀ x ∈ Iio a, HasDerivAt f (f' x) x
f'int : IntegrableOn (mα := MeasureSpace.toMeasurableSpace) f' (Iic a) volume
hf : Tendsto f atBot (𝓝 m)
hcont : ContinuousOn f (Iic a)
x : ℝ
hx : x ∈ Iic a
⊢ ∫ (x : ℝ) in id x..a, f' x = f a - f x
have h : IntervalIntegrable f' volume x a
Tactic: apply intervalIntegral.integral_eq_sub_of_hasDerivAt_of_le hx
    (hcont.mono Icc_subset_Iic_self) fun y hy => hderiv y hy.2
-- 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 (Iic a) a
hderiv : ∀ x ∈ Iio a, HasDerivAt f (f' x) x
f'int : IntegrableOn (mα := MeasureSpace.toMeasurableSpace) f' (Iic a) volume
hf : Tendsto f atBot (𝓝 m)
hcont : ContinuousOn f (Iic a)
x : ℝ
hx : x ∈ Iic a
⊢ IntervalIntegrable f' volume x a
have h : IntegrableOn (mα := measurableSpace) f' (Ioc x a) 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 : ℝ
m : E
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
hderiv : ∀ x ∈ Iic a, HasDerivAt f (f' x) x
f'int : IntegrableOn (mα := MeasureSpace.toMeasurableSpace) f' (Iic a) volume
hf : Tendsto f atBot (𝓝 m)
⊢ (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Iic a)) fun (x : ℝ) ↦ f' x) = f a - m
have refine : ContinuousWithinAt f (Iic a) a
Tactic: refine integral_Iic_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 (Iic b)) fun (x : ℝ) ↦ deriv f x) = f b
have this : ∀ x ∈ Iio b, HasDerivAt f (deriv f x) x
Tactic: have := fun x (_ : x ∈ Iio 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 ∈ Iio b, HasDerivAt f (deriv f x) x
⊢ (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Iic b)) fun (x : ℝ) ↦ deriv f x) = f b
have f'int : IntegrableOn (mα := MeasureSpace.toMeasurableSpace) (deriv f) (Iic b) volume
Tactic: rw [integral_Iic_of_hasDerivAt_of_tendsto hf.continuous.continuousWithinAt this, sub_zero]
-- 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 ∈ Iio b, HasDerivAt f (deriv f x) x
f'int : IntegrableOn (mα := MeasureSpace.toMeasurableSpace) (deriv f) (Iic b) volume
⊢ (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Iic b)) fun (x : ℝ) ↦ deriv f x) = f b
have hf₁ : Tendsto f atBot (𝓝 0)
Tactic: rw [integral_Iic_of_hasDerivAt_of_tendsto hf.continuous.continuousWithinAt this, sub_zero]
-- 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 ∈ Iio b, HasDerivAt f (deriv f x) x
⊢ Tendsto f atBot (𝓝 0)
have hf₁ : ∀ (h2f : f =ᶠ[cocompact ℝ] 0) (b : ℝ) (this : ∀ x ∈ Iio b, HasDerivAt f (deriv f x) x), Tendsto f atBot (𝓝 0)
Tactic: rw [hasCompactSupport_iff_eventuallyEq, Filter.coclosedCompact_eq_cocompact] at h2f
Cleared hypotheses: h2f, b, this
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntegralEqImproper (hypothesis)
Goal:
F : Type u_2
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
f : ℝ → F
hf : ContDiff ℝ 1 f
h'f : HasCompactSupport f
x : ℝ
I : F →L[ℝ] Completion F := Completion.toComplL
f' : ℝ → Completion F := (⇑I : (a : F) → Completion F) ∘ f
⊢ ‖f x‖ₑ ≤ ∫⁻ (y : ℝ) in Iic x, ‖deriv f y‖ₑ
have hf' : ContDiff ℝ 1 f'
Tactic: have hf' : ContDiff ℝ 1 f' := hf.continuousLinearMap_comp I
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntegralEqImproper (hypothesis)
Goal:
F : Type u_2
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
f : ℝ → F
hf : ContDiff ℝ 1 f
h'f : HasCompactSupport f
x : ℝ
I : F →L[ℝ] Completion F := Completion.toComplL
f' : ℝ → Completion F := (⇑I : (a : F) → Completion F) ∘ f
hf' : ContDiff ℝ 1 f'
⊢ ‖f x‖ₑ ≤ ∫⁻ (y : ℝ) in Iic x, ‖deriv f y‖ₑ
have h'f' : HasCompactSupport f'
Tactic: have h'f' : HasCompactSupport f' := h'f.comp_left rfl
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntegralEqImproper (goal)
Goal:
F : Type u_2
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
f : ℝ → F
hf : ContDiff ℝ 1 f
h'f : HasCompactSupport f
x : ℝ
I : F →L[ℝ] Completion F := Completion.toComplL
f' : ℝ → Completion F := (⇑I : (a : F) → Completion F) ∘ f
hf' : ContDiff ℝ 1 f'
h'f' : HasCompactSupport f'
⊢ ‖f' x‖ₑ ≤ ∫⁻ (y : ℝ) in Iic x, ‖deriv f' y‖ₑ
have rw : enorm.{u_2} (E := Completion F)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Iic x)) fun (x : ℝ) ↦ deriv f' x) ≤
  ∫⁻ (y : ℝ) in Iic x, ‖deriv f' y‖ₑ
Tactic: rw [← HasCompactSupport.integral_Iic_deriv_eq hf' h'f' x]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntegralEqImproper (hypothesis)
Goal:
F : Type u_2
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
f : ℝ → F
hf : ContDiff ℝ 1 f
h'f : HasCompactSupport f
x : ℝ
I : F →L[ℝ] Completion F := Completion.toComplL
f' : ℝ → Completion F := (⇑I : (a : F) → Completion F) ∘ f
hf' : ContDiff ℝ 1 f'
h'f' : HasCompactSupport f'
⊢ ‖f x‖ₑ ≤ ∫⁻ (y : ℝ) in Iic x, ‖deriv f y‖ₑ
have this : ‖f' x‖ₑ ≤ ∫⁻ (y : ℝ) in Iic x, ‖deriv f' y‖ₑ
Tactic: have : ‖f' x‖ₑ ≤ ∫⁻ y in Iic x, ‖deriv f' y‖ₑ := by
    rw [← HasCompactSupport.integral_Iic_deriv_eq hf' h'f' x]
    exact enorm_integral_le_lintegral_enorm _
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntegralEqImproper (goal)
Goal:
F : Type u_2
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
f : ℝ → F
hf : ContDiff ℝ 1 f
h'f : HasCompactSupport f
x : ℝ
I : F →L[ℝ] Completion F := Completion.toComplL
f' : ℝ → Completion F := (⇑I : (a : F) → Completion F) ∘ f
hf' : ContDiff ℝ 1 f'
h'f' : HasCompactSupport f'
this : ‖f' x‖ₑ ≤ ∫⁻ (y : ℝ) in Iic x, ‖deriv f' y‖ₑ
⊢ ‖f x‖ₑ ≤ ∫⁻ (y : ℝ) in Iic x, ‖deriv f y‖ₑ
have h : ‖f x‖ₑ = ‖f' x‖ₑ
Tactic: convert! this with y
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntegralEqImproper (goal)
Goal:
F : Type u_2
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
f : ℝ → F
hf : ContDiff ℝ 1 f
h'f : HasCompactSupport f
x : ℝ
I : F →L[ℝ] Completion F := Completion.toComplL
f' : ℝ → Completion F := (⇑I : (a : F) → Completion F) ∘ f
hf' : ContDiff ℝ 1 f'
h'f' : HasCompactSupport f'
this : ‖f' x‖ₑ ≤ ∫⁻ (y : ℝ) in Iic x, ‖deriv f' y‖ₑ
h : ‖f x‖ₑ = ‖f' x‖ₑ
⊢ ‖f x‖ₑ ≤ ∫⁻ (y : ℝ) in Iic x, ‖deriv f y‖ₑ
have h₁ : ∀ (y : ℝ), ‖deriv f y‖ₑ = ‖deriv f' y‖ₑ
Tactic: convert! this with y
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntegralEqImproper (goal)
Goal:
F : Type u_2
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
f : ℝ → F
hf : ContDiff ℝ 1 f
h'f : HasCompactSupport f
x : ℝ
I : F →L[ℝ] Completion F := Completion.toComplL
f' : ℝ → Completion F := (⇑I : (a : F) → Completion F) ∘ f
hf' : ContDiff ℝ 1 f'
h'f' : HasCompactSupport f'
this : ‖f' x‖ₑ ≤ ∫⁻ (y : ℝ) in Iic x, ‖deriv f' y‖ₑ
y : ℝ
⊢ ‖deriv f y‖ₑ = ‖deriv f' y‖ₑ
have h : ‖deriv f y‖ₑ =
  enorm (E := Completion F)
    ((fderiv ℝ (⇑I : (a : F) → Completion F) (f y) : (a : F) → Completion F) (deriv f y) : Completion F)
Tactic: rw [fderiv_comp_deriv _ I.differentiableAt (hf.differentiable one_ne_zero _)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntegralEqImproper (goal)
Goal:
F : Type u_2
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
f : ℝ → F
hf : ContDiff ℝ 1 f
h'f : HasCompactSupport f
x : ℝ
I : F →L[ℝ] Completion F := Completion.toComplL
f' : ℝ → Completion F := (⇑I : (a : F) → Completion F) ∘ f
hf' : ContDiff ℝ 1 f'
h'f' : HasCompactSupport f'
this : ‖f' x‖ₑ ≤ ∫⁻ (y : ℝ) in Iic x, ‖deriv f' y‖ₑ
y : ℝ
⊢ ‖deriv f y‖ₑ =
    enorm (E := Completion F)
      ((fderiv ℝ (⇑I : (a : F) → Completion F) (f y) : (a : F) → Completion F) (deriv f y) : Completion F)
have h : ‖deriv f y‖ₑ = enorm (E := Completion F) ((I : (a : F) → Completion F) (deriv f y) : Completion F)
Tactic: simp only [ContinuousLinearMap.fderiv]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntegralEqImproper (goal)
Goal:
E : Type u_1
f f' : ℝ → E
m n : E
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
hderiv : ∀ (x : ℝ), HasDerivAt f (f' x) x
hf' : @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace f' volume
hbot : Tendsto f atBot (𝓝 m)
htop : Tendsto f atTop (𝓝 n)
⊢ (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : ℝ) ↦ f' x) = n - m
have rw : f 0 - m + (n - f 0) = n - m
Tactic: rw [← setIntegral_univ, ← Set.Iic_union_Ioi (a := 0),
    setIntegral_union (Iic_disjoint_Ioi le_rfl) measurableSet_Ioi hf'.integrableOn hf'.integrableOn,
    integral_Iic_of_hasDerivAt_of_tendsto' (fun x _ ↦ hderiv x) hf'.integrableOn hbot,
    integral_Ioi_of_hasDerivAt_of_tendsto' (fun x _ ↦ hderiv x) hf'.integrableOn htop]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntegralEqImproper (goal)
Goal:
E : Type u_1
f f' : ℝ → E
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
hderiv : ∀ (x : ℝ), HasDerivAt f (f' x) x
hf' : @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace f' volume
hf : @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace f volume
⊢ Eq.{u_1 + 1} (α := E) (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : ℝ) ↦ f' x) 0
have pos : ∀ (hE : CompleteSpace E),
  Eq.{u_1 + 1} (α := E) (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : ℝ) ↦ f' x) 0
Tactic: by_cases hE : CompleteSpace E
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntegralEqImproper (goal)
Goal:
E : Type u_1
f f' : ℝ → E
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
hderiv : ∀ (x : ℝ), HasDerivAt f (f' x) x
hf' : @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace f' volume
hf : @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace f volume
pos :
  ∀ (hE : CompleteSpace E),
    Eq.{u_1 + 1} (α := E) (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : ℝ) ↦ f' x) 0
⊢ Eq.{u_1 + 1} (α := E) (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : ℝ) ↦ f' x) 0
have neg : ∀ (hE : ¬CompleteSpace E),
  Eq.{u_1 + 1} (α := E) (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : ℝ) ↦ f' x) 0
Tactic: by_cases hE : CompleteSpace E
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntegralEqImproper (hypothesis)
Goal:
E : Type u_1
f f' : ℝ → E
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
hderiv : ∀ (x : ℝ), HasDerivAt f (f' x) x
hf' : @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace f' volume
hf : @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace f volume
hE : CompleteSpace E
⊢ Eq.{u_1 + 1} (α := E) (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : ℝ) ↦ f' x) 0
have A : Tendsto f atBot (𝓝 0)
Tactic: have A : Tendsto f atBot (𝓝 0) :=
    tendsto_zero_of_hasDerivAt_of_integrableOn_Iic (a := 0) (fun x _hx ↦ hderiv x)
      hf'.integrableOn hf.integrableOn
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntegralEqImproper (hypothesis)
Goal:
E : Type u_1
f f' : ℝ → E
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
hderiv : ∀ (x : ℝ), HasDerivAt f (f' x) x
hf' : @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace f' volume
hf : @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace f volume
hE : CompleteSpace E
A : Tendsto f atBot (𝓝 0)
⊢ Eq.{u_1 + 1} (α := E) (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : ℝ) ↦ f' x) 0
have B : Tendsto f atTop (𝓝 0)
Tactic: have B : Tendsto f atTop (𝓝 0) :=
    tendsto_zero_of_hasDerivAt_of_integrableOn_Ioi (a := 0) (fun x _hx ↦ hderiv x)
      hf'.integrableOn hf.integrableOn
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntegralEqImproper (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f f' : ℝ → ℝ
g : ℝ → E
a : ℝ
hf : ContinuousOn f (Ici a)
hft : Tendsto f atTop atTop
hff' : ∀ x ∈ Ioi a, HasDerivWithinAt f (f' x) (Ioi x) x
hg_cont : ContinuousOn g (f '' Ioi a)
hg1 : IntegrableOn (mα := MeasureSpace.toMeasurableSpace) g (f '' Ici a) volume
hg2 :
  IntegrableOn.{0, u_1} (ε := E) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ f' x • (g ∘ f) x) (Ici a) volume
b : ℝ
hb : a < b
⊢ Ioo (min a b) (max a b) ⊆ Ioi a
have rw : Ioo a (max a b) ⊆ Ioi a
Tactic: rw [min_eq_left hb.le]