awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Integral.IntegralEqImproper
Goal:
E : Type u_1
f f' : ℝ → E
a : ℝ
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
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
⊢ LE.le (α := ℝ≥0∞) ((volume : (a : Set ℝ) → ℝ≥0∞) (Ici b) : ℝ≥0∞) ((volume : (a : Set ℝ) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
exact measure_mono hb

Premises used: MeasureTheory.measure_mono
-- Module: Mathlib.MeasureTheory.Integral.IntegralEqImproper
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)

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
-- Module: Mathlib.MeasureTheory.Integral.IntegralEqImproper
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)
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)
⊢ Tendsto f atTop (𝓝 0)

Tactic:
rwa [B, ← IsEmbedding.tendsto_nhds_iff] at A

Premises used: Topology.IsEmbedding.tendsto_nhds_iff
-- Module: Mathlib.MeasureTheory.Integral.IntegralEqImproper
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 (𝓝 ((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:
(Completion.isUniformEmbedding_coe E).isEmbedding

Premises used: UniformSpace.Completion.coe', UniformSpace.Completion.isUniformEmbedding_coe, SeparationQuotient.mk, IsUniformEmbedding.isEmbedding
-- Module: Mathlib.MeasureTheory.Integral.IntegralEqImproper
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 (𝓝 ((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:
exact (Completion.isUniformEmbedding_coe E).isEmbedding

Premises used: UniformSpace.Completion.isUniformEmbedding_coe, IsUniformEmbedding.isEmbedding
-- Module: Mathlib.MeasureTheory.Integral.IntegralEqImproper
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
inr : ∀ (hx : a < x), ContinuousWithinAt f (Ici a) x
⊢ ContinuousWithinAt f (Ici a) x

Tactic:
rcases hx.out.eq_or_lt with rfl | hx

Premises used: LE.le.eq_or_lt, Membership.mem.out, rfl
-- Module: Mathlib.MeasureTheory.Integral.IntegralEqImproper
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)
hx : a ∈ Ici a
⊢ ContinuousWithinAt f (Ici a) a

Tactic:
hcont
-- Module: Mathlib.MeasureTheory.Integral.IntegralEqImproper
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)
hx : a ∈ Ici a
⊢ ContinuousWithinAt f (Ici a) a

Tactic:
exact hcont
-- Module: Mathlib.MeasureTheory.Integral.IntegralEqImproper
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_1 : x ∈ Ici a
hx : a < x
⊢ ContinuousWithinAt f (Ici a) x

Tactic:
(hderiv x hx).continuousAt.continuousWithinAt

Premises used: ContinuousAt.continuousWithinAt, HasDerivAt.continuousAt
-- Module: Mathlib.MeasureTheory.Integral.IntegralEqImproper
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_1 : x ∈ Ici a
hx : a < x
⊢ ContinuousWithinAt f (Ici a) x

Tactic:
exact (hderiv x hx).continuousAt.continuousWithinAt

Premises used: ContinuousAt.continuousWithinAt, HasDerivAt.continuousAt
-- Module: Mathlib.MeasureTheory.Integral.IntegralEqImproper
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)
⊢ 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
-- Module: Mathlib.MeasureTheory.Integral.IntegralEqImproper
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

Tactic:
tendsto_nhds_unique (intervalIntegral_tendsto_integral_Ioi a f'int tendsto_id) ?_

Premises used: Filter.tendsto_id, MeasureTheory.intervalIntegral_tendsto_integral_Ioi, tendsto_nhds_unique
-- Module: Mathlib.MeasureTheory.Integral.IntegralEqImproper
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)
refine : Tendsto (fun (i : ℝ) ↦ ∫ (x : ℝ) in a..id i, f' x) atTop (𝓝 (m - f a))
⊢ (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi a)) fun (x : ℝ) ↦ f' x) = m - f a

Tactic:
refine tendsto_nhds_unique (intervalIntegral_tendsto_integral_Ioi a f'int tendsto_id) ?_

Premises used: Filter.tendsto_id, MeasureTheory.intervalIntegral_tendsto_integral_Ioi, tendsto_nhds_unique
-- Module: Mathlib.MeasureTheory.Integral.IntegralEqImproper
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)
apply : EventuallyEq.{0, u_1} (β := E) atTop (fun (x : ℝ) ↦ f x - f a) fun (i : ℝ) ↦ ∫ (x : ℝ) in a..id i, f' x
⊢ Tendsto (fun (i : ℝ) ↦ ∫ (x : ℝ) in a..id i, f' x) atTop (𝓝 (m - f a))

Tactic:
apply Tendsto.congr' _ (hf.sub_const _)

Premises used: Filter.Tendsto.sub_const, Filter.Tendsto.congr'
-- Module: Mathlib.MeasureTheory.Integral.IntegralEqImproper
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)
h : ∀ (x : ℝ) (hx : x ∈ Ioi a), f x - f a = ∫ (x : ℝ) in a..id x, f' x
⊢ EventuallyEq.{0, u_1} (β := E) atTop (fun (x : ℝ) ↦ f x - f a) fun (i : ℝ) ↦ ∫ (x : ℝ) in a..id i, f' x

Tactic:
filter_upwards [Ioi_mem_atTop a] with x hx

Premises used: Filter.Ioi_mem_atTop
-- Module: Mathlib.MeasureTheory.Integral.IntegralEqImproper
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
⊢ a ≤ id x

Tactic:
have h'x : a ≤ id x := le_of_lt hx
-- Module: Mathlib.MeasureTheory.Integral.IntegralEqImproper
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
h : ∫ (x : ℝ) in a..id x, f' x = f x - f a
⊢ f x - f a = ∫ (x : ℝ) in a..id x, f' x

Tactic:
symm
-- Module: Mathlib.MeasureTheory.Integral.IntegralEqImproper
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
h : IntervalIntegrable f' volume a (id x)
⊢ ∫ (x : ℝ) in a..id x, f' x = f x - f a

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

Premises used: intervalIntegral.integral_eq_sub_of_hasDerivAt_of_le, And.left, ContinuousOn.mono, Set.Icc_subset_Ici_self
-- Module: Mathlib.MeasureTheory.Integral.IntegralEqImproper
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
h : IntegrableOn (mα := measurableSpace) f' (Ioc a (id x)) volume
⊢ IntervalIntegrable f' volume a (id x)

Tactic:
rw [intervalIntegrable_iff_integrableOn_Ioc_of_le h'x]

Premises used: intervalIntegrable_iff_integrableOn_Ioc_of_le
-- Module: Mathlib.MeasureTheory.Integral.IntegralEqImproper
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
⊢ IntegrableOn (mα := measurableSpace) f' (Ioc a (id x)) volume

Tactic:
f'int.mono (fun y hy => hy.1) le_rfl

Premises used: le_rfl, And.left, MeasureTheory.IntegrableOn.mono
-- Module: Mathlib.MeasureTheory.Integral.IntegralEqImproper
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
⊢ IntegrableOn (mα := measurableSpace) f' (Ioc a (id x)) volume

Tactic:
exact f'int.mono (fun y hy => hy.1) le_rfl

Premises used: le_rfl, MeasureTheory.IntegrableOn.mono
-- Module: Mathlib.MeasureTheory.Integral.IntegralEqImproper
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

Tactic:
integral_Ioi_of_hasDerivAt_of_tendsto ?_ (fun x hx => hderiv x hx.out.le)
    f'int hf

Premises used: Membership.mem.out, LT.lt.le, MeasureTheory.integral_Ioi_of_hasDerivAt_of_tendsto
-- Module: Mathlib.MeasureTheory.Integral.IntegralEqImproper
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)
refine : ContinuousWithinAt f (Ici a) a
⊢ (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi a)) fun (x : ℝ) ↦ f' x) = m - f a

Tactic:
refine integral_Ioi_of_hasDerivAt_of_tendsto ?_ (fun x hx => hderiv x hx.out.le)
    f'int hf

Premises used: Membership.mem.out, LT.lt.le, MeasureTheory.integral_Ioi_of_hasDerivAt_of_tendsto
-- Module: Mathlib.MeasureTheory.Integral.IntegralEqImproper
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)
⊢ ContinuousWithinAt f (Ici a) a

Tactic:
(hderiv a self_mem_Ici).continuousAt.continuousWithinAt

Premises used: ContinuousAt.continuousWithinAt, HasDerivAt.continuousAt, Set.self_mem_Ici
-- Module: Mathlib.MeasureTheory.Integral.IntegralEqImproper
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)
⊢ ContinuousWithinAt f (Ici a) a

Tactic:
exact (hderiv a self_mem_Ici).continuousAt.continuousWithinAt

Premises used: ContinuousAt.continuousWithinAt, HasDerivAt.continuousAt, Set.self_mem_Ici
-- Module: Mathlib.MeasureTheory.Integral.IntegralEqImproper
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 : ℝ
⊢ ∀ x ∈ Ioi b, HasDerivAt f (deriv f x) x

Tactic:
have := fun x (_ : x ∈ Ioi b) ↦ hf.differentiable one_ne_zero x |>.hasDerivAt
-- Module: Mathlib.MeasureTheory.Integral.IntegralEqImproper
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
hf₁ : Tendsto f atTop (𝓝 0)
⊢ (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi b)) fun (x : ℝ) ↦ deriv f x) = -f b

Tactic:
rw [integral_Ioi_of_hasDerivAt_of_tendsto hf.continuous.continuousWithinAt this, zero_sub]

Premises used: ContDiff.continuous, MeasureTheory.integral_Ioi_of_hasDerivAt_of_tendsto, Continuous.continuousWithinAt, zero_sub
-- Module: Mathlib.MeasureTheory.Integral.IntegralEqImproper
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
⊢ IntegrableOn (mα := MeasureSpace.toMeasurableSpace) (deriv f) (Ioi b) volume

Tactic:
hf.continuous_deriv le_rfl |>.integrable_of_hasCompactSupport h2f.deriv |>.integrableOn

Premises used: le_rfl, ContDiff.continuous_deriv, Continuous.integrable_of_hasCompactSupport, MeasureTheory.Integrable.integrableOn, HasCompactSupport.deriv
-- Module: Mathlib.MeasureTheory.Integral.IntegralEqImproper
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
⊢ IntegrableOn (mα := MeasureSpace.toMeasurableSpace) (deriv f) (Ioi b) volume

Tactic:
refine hf.continuous_deriv le_rfl |>.integrable_of_hasCompactSupport h2f.deriv |>.integrableOn

Premises used: le_rfl, ContDiff.continuous_deriv, Continuous.integrable_of_hasCompactSupport, MeasureTheory.Integrable.integrableOn, HasCompactSupport.deriv
-- Module: Mathlib.MeasureTheory.Integral.IntegralEqImproper
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
hf₁ : ∀ (h2f : f =ᶠ[cocompact ℝ] 0) (b : ℝ) (this : ∀ x ∈ Ioi b, HasDerivAt f (deriv f x) x), Tendsto f atTop (𝓝 0)
⊢ Tendsto f atTop (𝓝 0)

Tactic:
rw [hasCompactSupport_iff_eventuallyEq, Filter.coclosedCompact_eq_cocompact] at h2f

Premises used: hasCompactSupport_iff_eventuallyEq, Filter.coclosedCompact_eq_cocompact
-- Module: Mathlib.MeasureTheory.Integral.IntegralEqImproper
Goal:
E : Type u_1
f : ℝ → E
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
hf : ContDiff ℝ 1 f
h2f : f =ᶠ[cocompact ℝ] 0
b : ℝ
this : ∀ x ∈ Ioi b, HasDerivAt f (deriv f x) x
⊢ Tendsto f atTop (𝓝 0)

Tactic:
h2f.filter_mono _root_.atTop_le_cocompact |>.tendsto

Premises used: Filter.EventuallyEq.filter_mono, Filter.EventuallyEq.tendsto, atTop_le_cocompact
-- Module: Mathlib.MeasureTheory.Integral.IntegralEqImproper
Goal:
E : Type u_1
f : ℝ → E
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
hf : ContDiff ℝ 1 f
h2f : f =ᶠ[cocompact ℝ] 0
b : ℝ
this : ∀ x ∈ Ioi b, HasDerivAt f (deriv f x) x
⊢ Tendsto f atTop (𝓝 0)

Tactic:
exact h2f.filter_mono _root_.atTop_le_cocompact |>.tendsto

Premises used: Filter.EventuallyEq.filter_mono, Filter.EventuallyEq.tendsto, atTop_le_cocompact
-- Module: Mathlib.MeasureTheory.Integral.IntegralEqImproper
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
inr : ∀ (hx : a < x), ContinuousWithinAt g (Ici a) x
⊢ ContinuousWithinAt g (Ici a) x

Tactic:
rcases hx.out.eq_or_lt with rfl | hx

Premises used: LE.le.eq_or_lt, Membership.mem.out, rfl
-- Module: Mathlib.MeasureTheory.Integral.IntegralEqImproper
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)
hx : a ∈ Ici a
⊢ ContinuousWithinAt g (Ici a) a

Tactic:
hcont
-- Module: Mathlib.MeasureTheory.Integral.IntegralEqImproper
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)
hx : a ∈ Ici a
⊢ ContinuousWithinAt g (Ici a) a

Tactic:
exact hcont