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 ∈ 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)
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)
⊢ Tendsto f atBot (𝓝 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 ∈ 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 (𝓝 ((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:
(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 ∈ 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 (𝓝 ((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:
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 (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
inr : ∀ (hx : x < a), ContinuousWithinAt f (Iic a) x
⊢ ContinuousWithinAt f (Iic 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
m : E
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
hf : Tendsto f atBot (𝓝 m)
x : ℝ
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:
hcont
-- Module: Mathlib.MeasureTheory.Integral.IntegralEqImproper
Goal:
E : Type u_1
f f' : ℝ → E
m : E
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
hf : Tendsto f atBot (𝓝 m)
x : ℝ
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:
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 (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_1 : x ∈ Iic a
hx : x < a
⊢ ContinuousWithinAt f (Iic 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 (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_1 : x ∈ Iic a
hx : x < a
⊢ ContinuousWithinAt f (Iic 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 (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)
⊢ 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
-- 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 (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

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

Premises used: MeasureTheory.intervalIntegral_tendsto_integral_Iic, Filter.tendsto_id, 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 (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)
refine : Tendsto (fun (i : ℝ) ↦ ∫ (x : ℝ) in id i..a, f' x) atBot (𝓝 (f a - m))
⊢ (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Iic a)) fun (x : ℝ) ↦ f' x) = f a - m

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

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

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

Premises used: Filter.Tendsto.const_sub, 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 (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)
h : ∀ (x : ℝ) (hx : x ∈ Iic a), f a - f x = ∫ (x : ℝ) in id x..a, f' x
⊢ EventuallyEq.{0, u_1} (β := E) atBot (fun (x : ℝ) ↦ f a - f x) fun (i : ℝ) ↦ ∫ (x : ℝ) in id i..a, f' x

Tactic:
filter_upwards [Iic_mem_atBot a] with x hx

Premises used: Filter.Iic_mem_atBot
-- 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 (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
h : ∫ (x : ℝ) in id x..a, f' x = f a - f x
⊢ f a - f x = ∫ (x : ℝ) in id x..a, 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 (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
h : IntervalIntegrable f' volume x a
⊢ ∫ (x : ℝ) in id x..a, f' x = f a - f x

Tactic:
apply intervalIntegral.integral_eq_sub_of_hasDerivAt_of_le hx
    (hcont.mono Icc_subset_Iic_self) fun y hy => hderiv y hy.2

Premises used: Set.Icc_subset_Iic_self, intervalIntegral.integral_eq_sub_of_hasDerivAt_of_le, And.right, ContinuousOn.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 (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
h : IntegrableOn (mα := measurableSpace) f' (Ioc x a) volume
⊢ IntervalIntegrable f' volume x a

Tactic:
rw [intervalIntegrable_iff_integrableOn_Ioc_of_le hx]

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 (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
⊢ IntegrableOn (mα := measurableSpace) f' (Ioc x a) volume

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

Premises used: le_rfl, And.right, 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 (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
⊢ IntegrableOn (mα := measurableSpace) f' (Ioc x a) volume

Tactic:
exact f'int.mono (fun y hy => hy.2) 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 ∈ 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

Tactic:
integral_Iic_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_Iic_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 ∈ Iic a, HasDerivAt f (f' x) x
f'int : IntegrableOn (mα := MeasureSpace.toMeasurableSpace) f' (Iic a) volume
hf : Tendsto f atBot (𝓝 m)
refine : ContinuousWithinAt f (Iic a) a
⊢ (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Iic a)) fun (x : ℝ) ↦ f' x) = f a - m

Tactic:
refine integral_Iic_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_Iic_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 ∈ Iic a, HasDerivAt f (f' x) x
f'int : IntegrableOn (mα := MeasureSpace.toMeasurableSpace) f' (Iic a) volume
hf : Tendsto f atBot (𝓝 m)
⊢ ContinuousWithinAt f (Iic a) a

Tactic:
(hderiv a self_mem_Iic).continuousAt.continuousWithinAt

Premises used: Set.self_mem_Iic, 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
hderiv : ∀ x ∈ Iic a, HasDerivAt f (f' x) x
f'int : IntegrableOn (mα := MeasureSpace.toMeasurableSpace) f' (Iic a) volume
hf : Tendsto f atBot (𝓝 m)
⊢ ContinuousWithinAt f (Iic a) a

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

Premises used: Set.self_mem_Iic, ContinuousAt.continuousWithinAt, HasDerivAt.continuousAt
-- 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 ∈ Iio b, HasDerivAt f (deriv f x) x

Tactic:
have := fun x (_ : x ∈ Iio 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 ∈ Iio b, HasDerivAt f (deriv f x) x
f'int : IntegrableOn (mα := MeasureSpace.toMeasurableSpace) (deriv f) (Iic b) volume
hf₁ : Tendsto f atBot (𝓝 0)
⊢ (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Iic b)) fun (x : ℝ) ↦ deriv f x) = f b

Tactic:
rw [integral_Iic_of_hasDerivAt_of_tendsto hf.continuous.continuousWithinAt this, sub_zero]

Premises used: sub_zero, ContDiff.continuous, MeasureTheory.integral_Iic_of_hasDerivAt_of_tendsto, Continuous.continuousWithinAt
-- 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 ∈ Iio b, HasDerivAt f (deriv f x) x
⊢ IntegrableOn (mα := MeasureSpace.toMeasurableSpace) (deriv f) (Iic 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 ∈ Iio b, HasDerivAt f (deriv f x) x
⊢ IntegrableOn (mα := MeasureSpace.toMeasurableSpace) (deriv f) (Iic 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 ∈ Iio b, HasDerivAt f (deriv f x) x
hf₁ : ∀ (h2f : f =ᶠ[cocompact ℝ] 0) (b : ℝ) (this : ∀ x ∈ Iio b, HasDerivAt f (deriv f x) x), Tendsto f atBot (𝓝 0)
⊢ Tendsto f atBot (𝓝 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 ∈ Iio b, HasDerivAt f (deriv f x) x
⊢ Tendsto f atBot (𝓝 0)

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

Premises used: Filter.EventuallyEq.filter_mono, Filter.EventuallyEq.tendsto, atBot_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 ∈ Iio b, HasDerivAt f (deriv f x) x
⊢ Tendsto f atBot (𝓝 0)

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

Premises used: Filter.EventuallyEq.filter_mono, Filter.EventuallyEq.tendsto, atBot_le_cocompact
-- Module: Mathlib.MeasureTheory.Integral.IntegralEqImproper
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
⊢ ContDiff ℝ 1 f'

Tactic:
have hf' : ContDiff ℝ 1 f' := hf.continuousLinearMap_comp I
-- Module: Mathlib.MeasureTheory.Integral.IntegralEqImproper
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'
⊢ HasCompactSupport f'

Tactic:
have h'f' : HasCompactSupport f' := h'f.comp_left rfl
-- Module: Mathlib.MeasureTheory.Integral.IntegralEqImproper
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'
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‖ₑ
⊢ ‖f' x‖ₑ ≤ ∫⁻ (y : ℝ) in Iic x, ‖deriv f' y‖ₑ

Tactic:
rw [← HasCompactSupport.integral_Iic_deriv_eq hf' h'f' x]

Premises used: HasCompactSupport.integral_Iic_deriv_eq
-- Module: Mathlib.MeasureTheory.Integral.IntegralEqImproper
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'
⊢ 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:
enorm_integral_le_lintegral_enorm _

Premises used: MeasureTheory.enorm_integral_le_lintegral_enorm
-- Module: Mathlib.MeasureTheory.Integral.IntegralEqImproper
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'
⊢ 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:
exact enorm_integral_le_lintegral_enorm _

Premises used: MeasureTheory.enorm_integral_le_lintegral_enorm
-- Module: Mathlib.MeasureTheory.Integral.IntegralEqImproper
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‖ₑ

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 _
-- Module: Mathlib.MeasureTheory.Integral.IntegralEqImproper
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‖ₑ

Tactic:
this
-- Module: Mathlib.MeasureTheory.Integral.IntegralEqImproper
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‖ₑ
h₁ : ∀ (y : ℝ), ‖deriv f y‖ₑ = ‖deriv f' y‖ₑ
⊢ ‖f x‖ₑ ≤ ∫⁻ (y : ℝ) in Iic x, ‖deriv f y‖ₑ

Tactic:
convert! this with y