awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
f'int : IntegrableOn (mα := MeasureSpace.toMeasurableSpace) (deriv f) (Ioi b) volume
⊢ (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi b)) fun (x : ℝ) ↦ deriv f x) = -f b
have hf₁ : Tendsto f atTop (𝓝 0)
Tactic: rw [integral_Ioi_of_hasDerivAt_of_tendsto hf.continuous.continuousWithinAt this, zero_sub]
-- 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
⊢ Tendsto f atTop (𝓝 0)
have hf₁ : ∀ (h2f : f =ᶠ[cocompact ℝ] 0) (b : ℝ) (this : ∀ x ∈ Ioi b, HasDerivAt f (deriv f x) x), Tendsto f atTop (𝓝 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 (goal)
Goal:
g g' : ℝ → ℝ
a l : ℝ
hcont : ContinuousWithinAt g (Ici a) a
hderiv : ∀ x ∈ Ioi a, HasDerivAt g (g' x) x
g'pos : ∀ x ∈ Ioi a, 0 ≤ g' x
hg : Tendsto g atTop (𝓝 l)
x : ℝ
hx : x ∈ Ici a
⊢ ContinuousWithinAt g (Ici a) x
have inl : ∀ (hx : a ∈ Ici a), ContinuousWithinAt g (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:
g g' : ℝ → ℝ
a l : ℝ
hcont : ContinuousWithinAt g (Ici a) a
hderiv : ∀ x ∈ Ioi a, HasDerivAt g (g' x) x
g'pos : ∀ x ∈ Ioi a, 0 ≤ g' x
hg : Tendsto g atTop (𝓝 l)
x : ℝ
hx : x ∈ Ici a
inl : ∀ (hx : a ∈ Ici a), ContinuousWithinAt g (Ici a) a
⊢ ContinuousWithinAt g (Ici a) x
have inr : ∀ (hx : a < x), ContinuousWithinAt g (Ici a) x
Tactic: rcases hx.out.eq_or_lt with rfl | hx
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntegralEqImproper (hypothesis)
Goal:
g g' : ℝ → ℝ
a l : ℝ
hcont : ContinuousWithinAt g (Ici a) a
hderiv : ∀ x ∈ Ioi a, HasDerivAt g (g' x) x
g'pos : ∀ x ∈ Ioi a, 0 ≤ g' x
hg : Tendsto g atTop (𝓝 l)
⊢ IntegrableOn (mα := MeasureSpace.toMeasurableSpace) g' (Ioi a) volume
have hcont₁ : ContinuousOn g (Ici a)
Tactic: have hcont : ContinuousOn g (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:
g g' : ℝ → ℝ
a l : ℝ
hcont_1 : ContinuousWithinAt g (Ici a) a
hderiv : ∀ x ∈ Ioi a, HasDerivAt g (g' x) x
g'pos : ∀ x ∈ Ioi a, 0 ≤ g' x
hg : Tendsto g atTop (𝓝 l)
hcont : ContinuousOn g (Ici a)
⊢ IntegrableOn (mα := MeasureSpace.toMeasurableSpace) g' (Ioi a) volume
have refine_1 : ∀ (x : ℝ), IntegrableOn (mα := measurableSpace) g' (Ioc a (id x)) volume
Tactic: refine integrableOn_Ioi_of_intervalIntegral_norm_tendsto (l - g a) a (fun x => ?_) tendsto_id ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntegralEqImproper (goal)
Goal:
g g' : ℝ → ℝ
a l : ℝ
hcont_1 : ContinuousWithinAt g (Ici a) a
hderiv : ∀ x ∈ Ioi a, HasDerivAt g (g' x) x
g'pos : ∀ x ∈ Ioi a, 0 ≤ g' x
hg : Tendsto g atTop (𝓝 l)
hcont : ContinuousOn g (Ici a)
refine_1 : ∀ (x : ℝ), IntegrableOn (mα := measurableSpace) g' (Ioc a (id x)) volume
⊢ IntegrableOn (mα := MeasureSpace.toMeasurableSpace) g' (Ioi a) volume
have refine_2 : Tendsto (fun (i : ℝ) ↦ ∫ (x : ℝ) in a..id i, ‖g' x‖) atTop (𝓝 (l - g a))
Tactic: refine integrableOn_Ioi_of_intervalIntegral_norm_tendsto (l - g a) a (fun x => ?_) tendsto_id ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntegralEqImproper (goal)
Goal:
g g' : ℝ → ℝ
a l : ℝ
hcont_1 : ContinuousWithinAt g (Ici a) a
hderiv : ∀ x ∈ Ioi a, HasDerivAt g (g' x) x
g'pos : ∀ x ∈ Ioi a, 0 ≤ g' x
hg : Tendsto g atTop (𝓝 l)
hcont : ContinuousOn g (Ici a)
⊢ Tendsto (fun (i : ℝ) ↦ ∫ (x : ℝ) in a..id i, ‖g' x‖) atTop (𝓝 (l - g a))
have apply : EventuallyEq (β := ℝ) atTop (fun (x : ℝ) ↦ g x - g a) fun (i : ℝ) ↦ ∫ (x : ℝ) in a..id i, ‖g' x‖
Tactic: apply Tendsto.congr' _ (hg.sub_const _)
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntegralEqImproper (goal)
Goal:
g g' : ℝ → ℝ
a l : ℝ
hcont_1 : ContinuousWithinAt g (Ici a) a
hderiv : ∀ x ∈ Ioi a, HasDerivAt g (g' x) x
g'pos : ∀ x ∈ Ioi a, 0 ≤ g' x
hg : Tendsto g atTop (𝓝 l)
hcont : ContinuousOn g (Ici a)
⊢ EventuallyEq (β := ℝ) atTop (fun (x : ℝ) ↦ g x - g a) fun (i : ℝ) ↦ ∫ (x : ℝ) in a..id i, ‖g' x‖
have h : ∀ (x : ℝ) (hx : x ∈ Ioi a), g x - g a = ∫ (x : ℝ) in a..id x, ‖g' x‖
Tactic: filter_upwards [Ioi_mem_atTop a] with x hx
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntegralEqImproper (hypothesis)
Goal:
g g' : ℝ → ℝ
a l : ℝ
hcont_1 : ContinuousWithinAt g (Ici a) a
hderiv : ∀ x ∈ Ioi a, HasDerivAt g (g' x) x
g'pos : ∀ x ∈ Ioi a, 0 ≤ g' x
hg : Tendsto g atTop (𝓝 l)
hcont : ContinuousOn g (Ici a)
x : ℝ
hx : x ∈ Ioi a
⊢ g x - g a = ∫ (x : ℝ) in a..id x, ‖g' 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:
g g' : ℝ → ℝ
a l : ℝ
hcont_1 : ContinuousWithinAt g (Ici a) a
hderiv : ∀ x ∈ Ioi a, HasDerivAt g (g' x) x
g'pos : ∀ x ∈ Ioi a, 0 ≤ g' x
hg : Tendsto g atTop (𝓝 l)
hcont : ContinuousOn g (Ici a)
x : ℝ
hx : x ∈ Ioi a
h'x : a ≤ id x
⊢ g x - g a = ∫ (y : ℝ) in a..id x, g' y
have symm : ∫ (y : ℝ) in a..id x, g' y = g x - g a
Tactic: symm
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntegralEqImproper (goal)
Goal:
g g' : ℝ → ℝ
a l : ℝ
hcont_1 : ContinuousWithinAt g (Ici a) a
hderiv : ∀ x ∈ Ioi a, HasDerivAt g (g' x) x
g'pos : ∀ x ∈ Ioi a, 0 ≤ g' x
hg : Tendsto g atTop (𝓝 l)
hcont : ContinuousOn g (Ici a)
x : ℝ
hx : x ∈ Ioi a
h'x : a ≤ id x
⊢ ∫ (y : ℝ) in a..id x, g' y = g x - g a
have apply : IntervalIntegrable g' 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:
g g' : ℝ → ℝ
a l : ℝ
hcont_1 : ContinuousWithinAt g (Ici a) a
hderiv : ∀ x ∈ Ioi a, HasDerivAt g (g' x) x
g'pos : ∀ x ∈ Ioi a, 0 ≤ g' x
hg : Tendsto g atTop (𝓝 l)
hcont : ContinuousOn g (Ici a)
x : ℝ
hx : x ∈ Ioi a
h'x : a ≤ id x
⊢ IntervalIntegrable g' volume a (id x)
have rw : IntegrableOn (mα := measurableSpace) g' (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:
g g' : ℝ → ℝ
a l : ℝ
hcont_1 : ContinuousWithinAt g (Ici a) a
hderiv : ∀ x ∈ Ioi a, HasDerivAt g (g' x) x
g'pos : ∀ x ∈ Ioi a, 0 ≤ g' x
hg : Tendsto g atTop (𝓝 l)
hcont : ContinuousOn g (Ici a)
x : ℝ
hx : x ∈ Ioi a
h'x : a ≤ id x
⊢ Eq (α := ℝ) (∫ (y : ℝ) in a..id x, g' y) (∫ (y : ℝ) in a..id x, ‖g' y‖)
have simp_rw : Eq (α := ℝ) (@integral _ _ _ _ measurableSpace (Measure.restrict volume (Ioc a (id x))) fun (y : ℝ) ↦ g' y)
  (@integral _ _ _ _ measurableSpace (Measure.restrict volume (Ioc a (id x))) fun (y : ℝ) ↦ ‖g' y‖)
Tactic: simp_rw [intervalIntegral.integral_of_le h'x]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntegralEqImproper (goal)
Goal:
g g' : ℝ → ℝ
a l : ℝ
hcont_1 : ContinuousWithinAt g (Ici a) a
hderiv : ∀ x ∈ Ioi a, HasDerivAt g (g' x) x
g'pos : ∀ x ∈ Ioi a, 0 ≤ g' x
hg : Tendsto g atTop (𝓝 l)
hcont : ContinuousOn g (Ici a)
x : ℝ
hx : x ∈ Ioi a
h'x : a ≤ id x
⊢ Eq (α := ℝ) (@integral _ _ _ _ measurableSpace (Measure.restrict volume (Ioc a (id x))) fun (y : ℝ) ↦ g' y)
    (@integral _ _ _ _ measurableSpace (Measure.restrict volume (Ioc a (id x))) fun (y : ℝ) ↦ ‖g' y‖)
have refine : ∀ (y : ℝ) (hy : y ∈ Ioc a (id x)), g' y = ‖g' y‖
Tactic: refine setIntegral_congr_fun measurableSet_Ioc fun y hy => ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntegralEqImproper (goal)
Goal:
g g' : ℝ → ℝ
a l : ℝ
hcont_1 : ContinuousWithinAt g (Ici a) a
hderiv : ∀ x ∈ Ioi a, HasDerivAt g (g' x) x
g'pos : ∀ x ∈ Ioi a, 0 ≤ g' x
hg : Tendsto g atTop (𝓝 l)
hcont : ContinuousOn g (Ici a)
x : ℝ
hx : x ∈ Ioi a
h'x : a ≤ id x
y : ℝ
hy : y ∈ Ioc a (id x)
⊢ g' y = |g' y|
have rw : 0 ≤ g' y
Tactic: rw [abs_of_nonneg]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntegralEqImproper (goal)
Goal:
g g' : ℝ → ℝ
a l : ℝ
hcont_1 : ContinuousWithinAt g (Ici a) a
hderiv : ∀ x ∈ Ioi a, HasDerivAt g (g' x) x
g'pos : ∀ x ∈ Ioi a, 0 ≤ g' x
hg : Tendsto g atTop (𝓝 l)
hcont : ContinuousOn g (Ici a)
x : ℝ
hx : x ∈ Ioi a
h'x : a ≤ id x
⊢ g x - g a = ∫ (x : ℝ) in a..id x, ‖g' x‖
have g₁ : g x - g a = ∫ (y : ℝ) in a..id x, g' y
Tactic: calc
    g x - g a = ∫ y in a..id x, g' y := by
      symm
      apply intervalIntegral.integral_eq_sub_of_hasDerivAt_of_le h'x
        (hcont.mono Icc_subset_Ici_self) fun y hy => hderiv y hy.1
      rw [intervalIntegrable_iff_integrableOn_Ioc_of_le h'x]
      exact intervalIntegral.integrableOn_deriv_of_nonneg (hcont.mono Icc_subset_Ici_self)
        (fun y hy => hderiv y hy.1) fun y hy => g'pos y hy.1
    _ = ∫ y in a..id x, ‖g' y‖ := by
      simp_rw [intervalIntegral.integral_of_le h'x]
      refine setIntegral_congr_fun measurableSet_Ioc fun y hy => ?_
      dsimp
      rw [abs_of_nonneg]
      exact g'pos _ hy.1
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntegralEqImproper (goal)
Goal:
g g' : ℝ → ℝ
a l : ℝ
hcont_1 : ContinuousWithinAt g (Ici a) a
hderiv : ∀ x ∈ Ioi a, HasDerivAt g (g' x) x
g'pos : ∀ x ∈ Ioi a, 0 ≤ g' x
hg : Tendsto g atTop (𝓝 l)
hcont : ContinuousOn g (Ici a)
x : ℝ
hx : x ∈ Ioi a
h'x : a ≤ id x
g₁ : g x - g a = ∫ (y : ℝ) in a..id x, g' y
⊢ g x - g a = ∫ (x : ℝ) in a..id x, ‖g' x‖
have g₂ : Eq (α := ℝ) (∫ (y : ℝ) in a..id x, g' y) (∫ (y : ℝ) in a..id x, ‖g' y‖)
Tactic: calc
    g x - g a = ∫ y in a..id x, g' y := by
      symm
      apply intervalIntegral.integral_eq_sub_of_hasDerivAt_of_le h'x
        (hcont.mono Icc_subset_Ici_self) fun y hy => hderiv y hy.1
      rw [intervalIntegrable_iff_integrableOn_Ioc_of_le h'x]
      exact intervalIntegral.integrableOn_deriv_of_nonneg (hcont.mono Icc_subset_Ici_self)
        (fun y hy => hderiv y hy.1) fun y hy => g'pos y hy.1
    _ = ∫ y in a..id x, ‖g' y‖ := by
      simp_rw [intervalIntegral.integral_of_le h'x]
      refine setIntegral_congr_fun measurableSet_Ioc fun y hy => ?_
      dsimp
      rw [abs_of_nonneg]
      exact g'pos _ hy.1
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntegralEqImproper (goal)
Goal:
g g' : ℝ → ℝ
a l : ℝ
hderiv : ∀ x ∈ Ici a, HasDerivAt g (g' x) x
g'pos : ∀ x ∈ Ioi a, 0 ≤ g' x
hg : Tendsto g atTop (𝓝 l)
⊢ IntegrableOn (mα := MeasureSpace.toMeasurableSpace) g' (Ioi a) volume
have refine : ContinuousWithinAt g (Ici a) a
Tactic: refine integrableOn_Ioi_deriv_of_nonneg ?_ (fun x hx => hderiv x hx.out.le) g'pos hg
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntegralEqImproper (goal)
Goal:
g g' : ℝ → ℝ
a l : ℝ
hcont : ContinuousWithinAt g (Ici a) a
hderiv : ∀ x ∈ Ioi a, HasDerivAt g (g' x) x
g'neg : ∀ x ∈ Ioi a, g' x ≤ 0
hg : Tendsto g atTop (𝓝 l)
⊢ IntegrableOn (mα := MeasureSpace.toMeasurableSpace) g' (Ioi a) volume
have apply : @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace (-g') (Measure.restrict volume (Ioi a))
Tactic: apply integrable_neg_iff.1
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntegralEqImproper (goal)
Goal:
g g' : ℝ → ℝ
a l : ℝ
hderiv : ∀ x ∈ Ici a, HasDerivAt g (g' x) x
g'neg : ∀ x ∈ Ioi a, g' x ≤ 0
hg : Tendsto g atTop (𝓝 l)
⊢ IntegrableOn (mα := MeasureSpace.toMeasurableSpace) g' (Ioi a) volume
have refine : ContinuousWithinAt g (Ici a) a
Tactic: refine integrableOn_Ioi_deriv_of_nonpos ?_ (fun x hx ↦ hderiv x hx.out.le) g'neg hg
-- 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 ∈ Iic a, HasDerivAt f (f' x) x
f'int : IntegrableOn (mα := MeasureSpace.toMeasurableSpace) f' (Iic a) volume
⊢ Tendsto f atBot (𝓝 (limUnder atBot f))
have suffices : ∃ (a : E), Tendsto f atBot (𝓝 a)
Tactic: suffices ∃ a, Tendsto f atBot (𝓝 a) from tendsto_nhds_limUnder this
-- 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 ∈ Iic a, HasDerivAt f (f' x) x
f'int : IntegrableOn (mα := MeasureSpace.toMeasurableSpace) f' (Iic a) volume
g : ℝ → E := f ∘ fun (x : ℝ) ↦ -x
x : ℝ
hx : x ∈ Ioi (-a)
⊢ HasDerivAt g (-f' (-x)) x
have this : -x ∈ Iic a
Tactic: have : -x ∈ Iic a := by grind
-- 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 ∈ Iic a, HasDerivAt f (f' x) x
f'int : IntegrableOn (mα := MeasureSpace.toMeasurableSpace) f' (Iic a) volume
g : ℝ → E := f ∘ fun (x : ℝ) ↦ -x
⊢ ∃ (a : E), Tendsto f atBot (𝓝 a)
have hdg : ∀ x ∈ Ioi (-a), HasDerivAt g (-f' (-x)) x
Tactic: have hdg : ∀ x ∈ Ioi (-a), HasDerivAt g (-f' (-x)) x := by
    intro x hx
    have : -x ∈ Iic a := by grind
    simpa using HasDerivAt.scomp x (hderiv (-x) this) (hasDerivAt_neg' x)
-- 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 ∈ Iic a, HasDerivAt f (f' x) x
f'int : IntegrableOn (mα := MeasureSpace.toMeasurableSpace) f' (Iic a) volume
g : ℝ → E := f ∘ fun (x : ℝ) ↦ -x
hdg : ∀ x ∈ Ioi (-a), HasDerivAt g (-f' (-x)) x
⊢ Tendsto g atTop (𝓝 (limUnder atTop g))
have apply : IntegrableOn.{0, u_1} (ε := E) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ -f' (-x)) (Ioi (-a)) volume
Tactic: apply tendsto_limUnder_of_hasDerivAt_of_integrableOn_Ioi hdg
-- 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 ∈ Iic a, HasDerivAt f (f' x) x
f'int : IntegrableOn (mα := MeasureSpace.toMeasurableSpace) f' (Iic a) volume
g : ℝ → E := f ∘ fun (x : ℝ) ↦ -x
hdg : ∀ x ∈ Ioi (-a), HasDerivAt g (-f' (-x)) x
⊢ ∃ (a : E), Tendsto f atBot (𝓝 a)
have L : Tendsto g atTop (𝓝 (limUnder atTop g))
Tactic: have L : Tendsto g atTop (𝓝 (limUnder atTop g)) := by
    apply tendsto_limUnder_of_hasDerivAt_of_integrableOn_Ioi hdg
    exact ((MeasurePreserving.integrableOn_comp_preimage (Measure.measurePreserving_neg _)
      (Homeomorph.neg ℝ).measurableEmbedding).2 f'int.neg).mono_set (by simp)
-- 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 ∈ Iic a, HasDerivAt f (f' x) x
f'int : IntegrableOn (mα := MeasureSpace.toMeasurableSpace) f' (Iic a) volume
g : ℝ → E := f ∘ fun (x : ℝ) ↦ -x
hdg : ∀ x ∈ Ioi (-a), HasDerivAt g (-f' (-x)) x
L : Tendsto g atTop (𝓝 (limUnder atTop g))
⊢ ∃ (a : E), Tendsto f atBot (𝓝 a)
have refine : Tendsto f atBot (𝓝 (limUnder atTop g))
Tactic: refine ⟨limUnder atTop g, ?_⟩
-- 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 ∈ Iic a, HasDerivAt f (f' x) x
f'int : IntegrableOn (mα := MeasureSpace.toMeasurableSpace) f' (Iic a) volume
g : ℝ → E := f ∘ fun (x : ℝ) ↦ -x
hdg : ∀ x ∈ Ioi (-a), HasDerivAt g (-f' (-x)) x
L : Tendsto g atTop (𝓝 (limUnder atTop g))
⊢ Tendsto f atBot (𝓝 (limUnder atTop g))
have this : Tendsto (fun (x : ℝ) ↦ g (-x)) atBot (𝓝 (limUnder atTop g))
Tactic: have : Tendsto (fun x ↦ g (-x)) atBot (𝓝 (limUnder atTop g)) := L.comp tendsto_neg_atBot_atTop
-- 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
⊢ Tendsto f atBot (𝓝 0)
have 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
Tactic: have Fderiv : ∀ x ∈ Iic 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 ∈ 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
⊢ Tendsto f atBot (𝓝 0)
have Fint : IntegrableOn (ε := Completion E) (mα := MeasureSpace.toMeasurableSpace) ((⇑F : (a : E) → Completion E) ∘ f) (Iic a)
  volume
Tactic: have Fint : IntegrableOn (F ∘ f) (Iic 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 ∈ 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
⊢ Tendsto f atBot (𝓝 0)
have F'int : IntegrableOn (ε := Completion E) (mα := MeasureSpace.toMeasurableSpace) ((⇑F : (a : E) → Completion E) ∘ f') (Iic a)
  volume
Tactic: have F'int : IntegrableOn (F ∘ f') (Iic 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 ∈ 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
⊢ Tendsto f atBot (𝓝 0)
have A : Tendsto (β := Completion E) ((⇑F : (a : E) → Completion E) ∘ f) atBot
  (𝓝 (limUnder atBot ((⇑F : (a : E) → Completion E) ∘ f)))
Tactic: have A : Tendsto (F ∘ f) atBot (𝓝 (limUnder atBot (F ∘ f))) := by
    apply tendsto_limUnder_of_hasDerivAt_of_integrableOn_Iic 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 ∈ 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)))
⊢ Eq (α := Completion E) (limUnder atBot ((⇑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) atBot
  volume
Tactic: have : IntegrableAtFilter (F ∘ f) atBot := by exact ⟨Iic a, Iic_mem_atBot _, 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 ∈ 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
⊢ Eq (α := Completion E) (limUnder atBot ((⇑F : (a : E) → Completion E) ∘ f)) ((F : (a : E) → Completion E) 0)
have apply : ∀ (s : Set ℝ),
  Membership.mem (γ := Filter ℝ) atBot 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 ∈ 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
⊢ 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_atBot_sets.1 hs with ⟨b, hb⟩