awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntegralEqImproper (goal)
Goal:
E : Type u_1
F : Type u_2
G : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
inst_4 : NormedAddCommGroup G
inst_5 : NormedSpace ℝ G
L : E →L[ℝ] F →L[ℝ] G
u : ℝ → E
v : ℝ → F
u' : ℝ → E
v' : ℝ → F
m n : G
inst_6 : CompleteSpace G
hu : ∀ x ∈ tsupport v, HasDerivAt u (u' x) x
hv : ∀ x ∈ tsupport u, HasDerivAt v (v' x) x
huv' :
  @Integrable.{u_3, 0} G _ _ _ MeasureSpace.toMeasurableSpace
    (fun (x : ℝ) ↦ (((L : (a : E) → F →L[ℝ] G) (u x) : F →L[ℝ] G) : (a : F) → G) (v' x)) volume
hu'v :
  @Integrable.{u_3, 0} G _ _ _ MeasureSpace.toMeasurableSpace
    (fun (x : ℝ) ↦ (((L : (a : E) → F →L[ℝ] G) (u' x) : F →L[ℝ] G) : (a : F) → G) (v x)) volume
h_bot : Tendsto (fun (x : ℝ) ↦ (((L : (a : E) → F →L[ℝ] G) (u x) : F →L[ℝ] G) : (a : F) → G) (v x)) atBot (𝓝 m)
h_top : Tendsto (fun (x : ℝ) ↦ (((L : (a : E) → F →L[ℝ] G) (u x) : F →L[ℝ] G) : (a : F) → G) (v x)) atTop (𝓝 n)
⊢ (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : ℝ) ↦
      (((L : (a : E) → F →L[ℝ] G) (u x) : F →L[ℝ] G) : (a : F) → G) (v' x)) =
    n - m -
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : ℝ) ↦
        (((L : (a : E) → F →L[ℝ] G) (u' x) : F →L[ℝ] G) : (a : F) → G) (v x)
have rw : (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (a : ℝ) ↦
    HAdd.hAdd (α := G) (β := G) ((((L : (a : E) → F →L[ℝ] G) (u a) : F →L[ℝ] G) : (a : F) → G) (v' a) : G)
      ((((L : (a : E) → F →L[ℝ] G) (u' a) : F →L[ℝ] G) : (a : F) → G) (v a) : G)) =
  n - m
Tactic: rw [eq_sub_iff_add_eq, ← integral_add huv' hu'v]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntegralEqImproper (goal)
Goal:
E : Type u_1
F : Type u_2
G : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
inst_4 : NormedAddCommGroup G
inst_5 : NormedSpace ℝ G
L : E →L[ℝ] F →L[ℝ] G
u : ℝ → E
v : ℝ → F
u' : ℝ → E
v' : ℝ → F
hu : ∀ x ∈ tsupport v, HasDerivAt u (u' x) x
hv : ∀ x ∈ tsupport u, HasDerivAt v (v' x) x
huv' :
  @Integrable.{u_3, 0} G _ _ _ MeasureSpace.toMeasurableSpace
    (fun (x : ℝ) ↦ (((L : (a : E) → F →L[ℝ] G) (u x) : F →L[ℝ] G) : (a : F) → G) (v' x)) volume
hu'v :
  @Integrable.{u_3, 0} G _ _ _ MeasureSpace.toMeasurableSpace
    (fun (x : ℝ) ↦ (((L : (a : E) → F →L[ℝ] G) (u' x) : F →L[ℝ] G) : (a : F) → G) (v x)) volume
huv :
  @Integrable.{u_3, 0} G _ _ _ MeasureSpace.toMeasurableSpace
    (fun (x : ℝ) ↦ (((L : (a : E) → F →L[ℝ] G) (u x) : F →L[ℝ] G) : (a : F) → G) (v x)) volume
⊢ Eq.{u_3 + 1} (α := G)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : ℝ) ↦
      (((L : (a : E) → F →L[ℝ] G) (u x) : F →L[ℝ] G) : (a : F) → G) (v' x))
    (-@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : ℝ) ↦
        (((L : (a : E) → F →L[ℝ] G) (u' x) : F →L[ℝ] G) : (a : F) → G) (v x))
have pos : ∀ (hG : CompleteSpace G),
  Eq.{u_3 + 1} (α := G)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : ℝ) ↦
      (((L : (a : E) → F →L[ℝ] G) (u x) : F →L[ℝ] G) : (a : F) → G) (v' x))
    (-@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : ℝ) ↦
        (((L : (a : E) → F →L[ℝ] G) (u' x) : F →L[ℝ] G) : (a : F) → G) (v x))
Tactic: by_cases hG : CompleteSpace G
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntegralEqImproper (goal)
Goal:
E : Type u_1
F : Type u_2
G : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
inst_4 : NormedAddCommGroup G
inst_5 : NormedSpace ℝ G
L : E →L[ℝ] F →L[ℝ] G
u : ℝ → E
v : ℝ → F
u' : ℝ → E
v' : ℝ → F
hu : ∀ x ∈ tsupport v, HasDerivAt u (u' x) x
hv : ∀ x ∈ tsupport u, HasDerivAt v (v' x) x
huv' :
  @Integrable.{u_3, 0} G _ _ _ MeasureSpace.toMeasurableSpace
    (fun (x : ℝ) ↦ (((L : (a : E) → F →L[ℝ] G) (u x) : F →L[ℝ] G) : (a : F) → G) (v' x)) volume
hu'v :
  @Integrable.{u_3, 0} G _ _ _ MeasureSpace.toMeasurableSpace
    (fun (x : ℝ) ↦ (((L : (a : E) → F →L[ℝ] G) (u' x) : F →L[ℝ] G) : (a : F) → G) (v x)) volume
huv :
  @Integrable.{u_3, 0} G _ _ _ MeasureSpace.toMeasurableSpace
    (fun (x : ℝ) ↦ (((L : (a : E) → F →L[ℝ] G) (u x) : F →L[ℝ] G) : (a : F) → G) (v x)) volume
pos :
  ∀ (hG : CompleteSpace G),
    Eq.{u_3 + 1} (α := G)
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : ℝ) ↦
        (((L : (a : E) → F →L[ℝ] G) (u x) : F →L[ℝ] G) : (a : F) → G) (v' x))
      (-@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : ℝ) ↦
          (((L : (a : E) → F →L[ℝ] G) (u' x) : F →L[ℝ] G) : (a : F) → G) (v x))
⊢ Eq.{u_3 + 1} (α := G)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : ℝ) ↦
      (((L : (a : E) → F →L[ℝ] G) (u x) : F →L[ℝ] G) : (a : F) → G) (v' x))
    (-@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : ℝ) ↦
        (((L : (a : E) → F →L[ℝ] G) (u' x) : F →L[ℝ] G) : (a : F) → G) (v x))
have neg : ∀ (hG : ¬CompleteSpace G),
  Eq.{u_3 + 1} (α := G)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : ℝ) ↦
      (((L : (a : E) → F →L[ℝ] G) (u x) : F →L[ℝ] G) : (a : F) → G) (v' x))
    (-@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : ℝ) ↦
        (((L : (a : E) → F →L[ℝ] G) (u' x) : F →L[ℝ] G) : (a : F) → G) (v x))
Tactic: by_cases hG : CompleteSpace G
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntegralEqImproper (hypothesis)
Goal:
E : Type u_1
F : Type u_2
G : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
inst_4 : NormedAddCommGroup G
inst_5 : NormedSpace ℝ G
L : E →L[ℝ] F →L[ℝ] G
u : ℝ → E
v : ℝ → F
u' : ℝ → E
v' : ℝ → F
hu : ∀ x ∈ tsupport v, HasDerivAt u (u' x) x
hv : ∀ x ∈ tsupport u, HasDerivAt v (v' x) x
huv' :
  @Integrable.{u_3, 0} G _ _ _ MeasureSpace.toMeasurableSpace
    (fun (x : ℝ) ↦ (((L : (a : E) → F →L[ℝ] G) (u x) : F →L[ℝ] G) : (a : F) → G) (v' x)) volume
hu'v :
  @Integrable.{u_3, 0} G _ _ _ MeasureSpace.toMeasurableSpace
    (fun (x : ℝ) ↦ (((L : (a : E) → F →L[ℝ] G) (u' x) : F →L[ℝ] G) : (a : F) → G) (v x)) volume
huv :
  @Integrable.{u_3, 0} G _ _ _ MeasureSpace.toMeasurableSpace
    (fun (x : ℝ) ↦ (((L : (a : E) → F →L[ℝ] G) (u x) : F →L[ℝ] G) : (a : F) → G) (v x)) volume
hG : CompleteSpace G
⊢ Eq.{u_3 + 1} (α := G)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : ℝ) ↦
      (((L : (a : E) → F →L[ℝ] G) (u x) : F →L[ℝ] G) : (a : F) → G) (v' x))
    (-@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : ℝ) ↦
        (((L : (a : E) → F →L[ℝ] G) (u' x) : F →L[ℝ] G) : (a : F) → G) (v x))
have I : Tendsto.{0, u_3} (β := G) (fun (x : ℝ) ↦ (((L : (a : E) → F →L[ℝ] G) (u x) : F →L[ℝ] G) : (a : F) → G) (v x)) atBot
  (𝓝 0)
Tactic: have I : Tendsto (fun x ↦ L (u x) (v x)) atBot (𝓝 0) :=
    tendsto_zero_of_hasDerivAt_of_integrableOn_Iic (a := 0)
      (fun x _hx ↦ L.hasDerivAt_of_bilinear (hu x) (hv x))
      (huv'.add hu'v).integrableOn huv.integrableOn
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntegralEqImproper (hypothesis)
Goal:
E : Type u_1
F : Type u_2
G : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
inst_4 : NormedAddCommGroup G
inst_5 : NormedSpace ℝ G
L : E →L[ℝ] F →L[ℝ] G
u : ℝ → E
v : ℝ → F
u' : ℝ → E
v' : ℝ → F
hu : ∀ x ∈ tsupport v, HasDerivAt u (u' x) x
hv : ∀ x ∈ tsupport u, HasDerivAt v (v' x) x
huv' :
  @Integrable.{u_3, 0} G _ _ _ MeasureSpace.toMeasurableSpace
    (fun (x : ℝ) ↦ (((L : (a : E) → F →L[ℝ] G) (u x) : F →L[ℝ] G) : (a : F) → G) (v' x)) volume
hu'v :
  @Integrable.{u_3, 0} G _ _ _ MeasureSpace.toMeasurableSpace
    (fun (x : ℝ) ↦ (((L : (a : E) → F →L[ℝ] G) (u' x) : F →L[ℝ] G) : (a : F) → G) (v x)) volume
huv :
  @Integrable.{u_3, 0} G _ _ _ MeasureSpace.toMeasurableSpace
    (fun (x : ℝ) ↦ (((L : (a : E) → F →L[ℝ] G) (u x) : F →L[ℝ] G) : (a : F) → G) (v x)) volume
hG : CompleteSpace G
I :
  Tendsto.{0, u_3} (β := G) (fun (x : ℝ) ↦ (((L : (a : E) → F →L[ℝ] G) (u x) : F →L[ℝ] G) : (a : F) → G) (v x)) atBot
    (𝓝 0)
⊢ Eq.{u_3 + 1} (α := G)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : ℝ) ↦
      (((L : (a : E) → F →L[ℝ] G) (u x) : F →L[ℝ] G) : (a : F) → G) (v' x))
    (-@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : ℝ) ↦
        (((L : (a : E) → F →L[ℝ] G) (u' x) : F →L[ℝ] G) : (a : F) → G) (v x))
have J : Tendsto.{0, u_3} (β := G) (fun (x : ℝ) ↦ (((L : (a : E) → F →L[ℝ] G) (u x) : F →L[ℝ] G) : (a : F) → G) (v x)) atTop
  (𝓝 0)
Tactic: have J : Tendsto (fun x ↦ L (u x) (v x)) atTop (𝓝 0) :=
    tendsto_zero_of_hasDerivAt_of_integrableOn_Ioi (a := 0)
      (fun x _hx ↦ L.hasDerivAt_of_bilinear (hu x) (hv x))
      (huv'.add hu'v).integrableOn huv.integrableOn
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntegralEqImproper (goal)
Goal:
A : Type u_1
inst : NormedRing A
inst_1 : NormedAlgebra ℝ A
a' b' : A
u v u' v' : ℝ → A
inst_2 : CompleteSpace A
hu : ∀ x ∈ tsupport v, HasDerivAt u (u' x) x
hv : ∀ x ∈ tsupport u, HasDerivAt v (v' x) x
huv : @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace (u' * v + u * v') volume
h_bot : Tendsto (u * v) atBot (𝓝 a')
h_top : Tendsto (u * v) atTop (𝓝 b')
⊢ (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : ℝ) ↦ u' x * v x + u x * v' x) = b' - a'
have refine : ∀ (x : ℝ), HasDerivAt (u * v) (u' x * v x + u x * v' x) x
Tactic: refine integral_of_hasDerivAt_of_tendsto (fun x ↦ ?_) huv h_bot h_top
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntegralEqImproper (hypothesis)
Goal:
A : Type u_1
inst : NormedRing A
inst_1 : NormedAlgebra ℝ A
a : ℝ
a' b' : A
u v u' v' : ℝ → A
inst_2 : CompleteSpace A
hu : ∀ x ∈ Ioi a, HasDerivAt u (u' x) x
hv : ∀ x ∈ Ioi a, HasDerivAt v (v' x) x
huv : IntegrableOn (mα := MeasureSpace.toMeasurableSpace) (u' * v + u * v') (Ioi a) volume
h_zero : Tendsto (u * v) (𝓝[>] a) (𝓝 a')
h_infty : Tendsto (u * v) atTop (𝓝 b')
⊢ (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi a)) fun (x : ℝ) ↦
      u' x * v x + u x * v' x) =
    b' - a'
have h_zero₁ : Tendsto (u * v) (𝓝[Ici a \ {a}] a) (𝓝 a')
Tactic: rw [← Ici_diff_left] at h_zero
Cleared hypotheses: h_zero, h_infty
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntegralEqImproper (goal)
Goal:
A : Type u_1
inst : NormedRing A
inst_1 : NormedAlgebra ℝ A
a : ℝ
a' b' : A
u v u' v' : ℝ → A
inst_2 : CompleteSpace A
hu : ∀ x ∈ Ioi a, HasDerivAt u (u' x) x
hv : ∀ x ∈ Ioi a, HasDerivAt v (v' x) x
huv : IntegrableOn (mα := MeasureSpace.toMeasurableSpace) (u' * v + u * v') (Ioi a) volume
h_zero : Tendsto (u * v) (𝓝[Ici a \ {a}] a) (𝓝 a')
h_infty : Tendsto (u * v) atTop (𝓝 b')
f : (a : ℝ) → A := Function.update (β := fun (a : ℝ) ↦ A) (u * v) a a'
x : ℝ
⊢ x ∈ Ioi a → HasDerivAt f (u' x * v x + u x * v' x) x
have a₁ : ∀ (hx : a < x), HasDerivAt f (u' x * v x + u x * v' x) x
Tactic: (hx : a < x)
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntegralEqImproper (goal)
Goal:
A : Type u_1
inst : NormedRing A
inst_1 : NormedAlgebra ℝ A
a : ℝ
a' b' : A
u v u' v' : ℝ → A
inst_2 : CompleteSpace A
hu : ∀ x ∈ Ioi a, HasDerivAt u (u' x) x
hv : ∀ x ∈ Ioi a, HasDerivAt v (v' x) x
huv : IntegrableOn (mα := MeasureSpace.toMeasurableSpace) (u' * v + u * v') (Ioi a) volume
h_zero : Tendsto (u * v) (𝓝[Ici a \ {a}] a) (𝓝 a')
h_infty : Tendsto (u * v) atTop (𝓝 b')
f : (a : ℝ) → A := Function.update (β := fun (a : ℝ) ↦ A) (u * v) a a'
x : ℝ
hx : a < x
⊢ HasDerivAt f (u' x * v x + u x * v' x) x
have apply : f =ᶠ[𝓝 x] u * v
Tactic: apply ((hu x hx).mul (hv x hx)).congr_of_eventuallyEq
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntegralEqImproper (goal)
Goal:
A : Type u_1
inst : NormedRing A
inst_1 : NormedAlgebra ℝ A
a : ℝ
a' b' : A
u v u' v' : ℝ → A
inst_2 : CompleteSpace A
hu : ∀ x ∈ Ioi a, HasDerivAt u (u' x) x
hv : ∀ x ∈ Ioi a, HasDerivAt v (v' x) x
huv : IntegrableOn (mα := MeasureSpace.toMeasurableSpace) (u' * v + u * v') (Ioi a) volume
h_zero : Tendsto (u * v) (𝓝[Ici a \ {a}] a) (𝓝 a')
h_infty : Tendsto (u * v) atTop (𝓝 b')
f : (a : ℝ) → A := Function.update (β := fun (a : ℝ) ↦ A) (u * v) a a'
x : ℝ
hx : a < x
⊢ f =ᶠ[𝓝 x] u * v
have h : ∀ (y : ℝ) (hy : y ≠ a), f y = (u * v) y
Tactic: filter_upwards [eventually_ne_nhds hx.ne.symm] with y hy
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntegralEqImproper (hypothesis)
Goal:
A : Type u_1
inst : NormedRing A
inst_1 : NormedAlgebra ℝ A
a : ℝ
a' b' : A
u v u' v' : ℝ → A
inst_2 : CompleteSpace A
hu : ∀ x ∈ Ioi a, HasDerivAt u (u' x) x
hv : ∀ x ∈ Ioi a, HasDerivAt v (v' x) x
huv : IntegrableOn (mα := MeasureSpace.toMeasurableSpace) (u' * v + u * v') (Ioi a) volume
h_zero : Tendsto (u * v) (𝓝[Ici a \ {a}] a) (𝓝 a')
h_infty : Tendsto (u * v) atTop (𝓝 b')
f : (a : ℝ) → A := Function.update (β := fun (a : ℝ) ↦ A) (u * v) a a'
⊢ (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi a)) fun (x : ℝ) ↦
      u' x * v x + u x * v' x) =
    b' - a'
have hderiv : ∀ x ∈ Ioi a, HasDerivAt f (u' x * v x + u x * v' x) x
Tactic: have hderiv : ∀ x ∈ Ioi a, HasDerivAt f (u' x * v x + u x * v' x) x := by
    intro x (hx : a < x)
    apply ((hu x hx).mul (hv x hx)).congr_of_eventuallyEq
    filter_upwards [eventually_ne_nhds hx.ne.symm] with y hy
    exact Function.update_of_ne hy a' (u * v)
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntegralEqImproper (goal)
Goal:
A : Type u_1
inst : NormedRing A
inst_1 : NormedAlgebra ℝ A
a : ℝ
a' b' : A
u v u' v' : ℝ → A
inst_2 : CompleteSpace A
hu : ∀ x ∈ Ioi a, HasDerivAt u (u' x) x
hv : ∀ x ∈ Ioi a, HasDerivAt v (v' x) x
huv : IntegrableOn (mα := MeasureSpace.toMeasurableSpace) (u' * v + u * v') (Ioi a) volume
h_zero : Tendsto (u * v) (𝓝[Ici a \ {a}] a) (𝓝 a')
h_infty : Tendsto (u * v) atTop (𝓝 b')
f : (a : ℝ) → A := Function.update (β := fun (a : ℝ) ↦ A) (u * v) a a'
hderiv : ∀ x ∈ Ioi a, HasDerivAt f (u' x * v x + u x * v' x) x
⊢ Tendsto f atTop (𝓝 b')
have apply : u * v =ᶠ[atTop] f
Tactic: apply h_infty.congr'
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntegralEqImproper (goal)
Goal:
A : Type u_1
inst : NormedRing A
inst_1 : NormedAlgebra ℝ A
a : ℝ
a' b' : A
u v u' v' : ℝ → A
inst_2 : CompleteSpace A
hu : ∀ x ∈ Ioi a, HasDerivAt u (u' x) x
hv : ∀ x ∈ Ioi a, HasDerivAt v (v' x) x
huv : IntegrableOn (mα := MeasureSpace.toMeasurableSpace) (u' * v + u * v') (Ioi a) volume
h_zero : Tendsto (u * v) (𝓝[Ici a \ {a}] a) (𝓝 a')
h_infty : Tendsto (u * v) atTop (𝓝 b')
f : (a : ℝ) → A := Function.update (β := fun (a : ℝ) ↦ A) (u * v) a a'
hderiv : ∀ x ∈ Ioi a, HasDerivAt f (u' x * v x + u x * v' x) x
⊢ u * v =ᶠ[atTop] f
have h : ∀ (x : ℝ) (hx : x ≠ a), (u * v) x = f x
Tactic: filter_upwards [eventually_ne_atTop a] with x hx
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntegralEqImproper (hypothesis)
Goal:
A : Type u_1
inst : NormedRing A
inst_1 : NormedAlgebra ℝ A
a : ℝ
a' b' : A
u v u' v' : ℝ → A
inst_2 : CompleteSpace A
hu : ∀ x ∈ Ioi a, HasDerivAt u (u' x) x
hv : ∀ x ∈ Ioi a, HasDerivAt v (v' x) x
huv : IntegrableOn (mα := MeasureSpace.toMeasurableSpace) (u' * v + u * v') (Ioi a) volume
h_zero : Tendsto (u * v) (𝓝[Ici a \ {a}] a) (𝓝 a')
h_infty : Tendsto (u * v) atTop (𝓝 b')
f : (a : ℝ) → A := Function.update (β := fun (a : ℝ) ↦ A) (u * v) a a'
hderiv : ∀ x ∈ Ioi a, HasDerivAt f (u' x * v x + u x * v' x) x
⊢ (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi a)) fun (x : ℝ) ↦
      u' x * v x + u x * v' x) =
    b' - a'
have htendsto : Tendsto f atTop (𝓝 b')
Tactic: have htendsto : Tendsto f atTop (𝓝 b') := by
    apply h_infty.congr'
    filter_upwards [eventually_ne_atTop a] with x hx
    exact (Function.update_of_ne hx a' (u * v)).symm
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntegralEqImproper (hypothesis)
Goal:
A : Type u_1
inst : NormedRing A
inst_1 : NormedAlgebra ℝ A
a : ℝ
a' b' : A
u v u' v' : ℝ → A
inst_2 : CompleteSpace A
hu : ∀ x ∈ Ioi a, HasDerivAt u (u' x) x
hv : ∀ x ∈ Ioi a, HasDerivAt v (v' x) x
huv' : IntegrableOn (mα := MeasureSpace.toMeasurableSpace) (u * v') (Ioi a) volume
hu'v : IntegrableOn (mα := MeasureSpace.toMeasurableSpace) (u' * v) (Ioi a) volume
h_zero : Tendsto (u * v) (𝓝[>] a) (𝓝 a')
h_infty : Tendsto (u * v) atTop (𝓝 b')
⊢ (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi a)) fun (x : ℝ) ↦ u x * v' x) =
    b' - a' -
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi a)) fun (x : ℝ) ↦ u' x * v x
have huv'₁ : IntegrableOn.{0, u_1} (ε := A) (mα := MeasureSpace.toMeasurableSpace) (fun (i : ℝ) ↦ u i * v' i) (Ioi a) volume
Tactic: rw [Pi.mul_def] at huv' hu'v
Cleared hypotheses: huv', hu'v, h_zero, h_infty
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntegralEqImproper (hypothesis)
Goal:
A : Type u_1
inst : NormedRing A
inst_1 : NormedAlgebra ℝ A
a : ℝ
a' b' : A
u v u' v' : ℝ → A
inst_2 : CompleteSpace A
hu : ∀ x ∈ Ioi a, HasDerivAt u (u' x) x
hv : ∀ x ∈ Ioi a, HasDerivAt v (v' x) x
huv' : IntegrableOn (mα := MeasureSpace.toMeasurableSpace) (u * v') (Ioi a) volume
hu'v : IntegrableOn (mα := MeasureSpace.toMeasurableSpace) (u' * v) (Ioi a) volume
h_zero : Tendsto (u * v) (𝓝[>] a) (𝓝 a')
h_infty : Tendsto (u * v) atTop (𝓝 b')
huv'₁ : IntegrableOn.{0, u_1} (ε := A) (mα := MeasureSpace.toMeasurableSpace) (fun (i : ℝ) ↦ u i * v' i) (Ioi a) volume
⊢ (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi a)) fun (x : ℝ) ↦ u x * v' x) =
    b' - a' -
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi a)) fun (x : ℝ) ↦ u' x * v x
have hu'v₁ : IntegrableOn.{0, u_1} (ε := A) (mα := MeasureSpace.toMeasurableSpace) (fun (i : ℝ) ↦ u' i * v i) (Ioi a) volume
Tactic: rw [Pi.mul_def] at huv' hu'v
Cleared hypotheses: huv', hu'v, h_zero, h_infty
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntegralEqImproper (goal)
Goal:
A : Type u_1
inst : NormedRing A
inst_1 : NormedAlgebra ℝ A
a : ℝ
a' b' : A
u v u' v' : ℝ → A
inst_2 : CompleteSpace A
hu : ∀ x ∈ Ioi a, HasDerivAt u (u' x) x
hv : ∀ x ∈ Ioi a, HasDerivAt v (v' x) x
huv' : IntegrableOn.{0, u_1} (ε := A) (mα := MeasureSpace.toMeasurableSpace) (fun (i : ℝ) ↦ u i * v' i) (Ioi a) volume
hu'v : IntegrableOn.{0, u_1} (ε := A) (mα := MeasureSpace.toMeasurableSpace) (fun (i : ℝ) ↦ u' i * v i) (Ioi a) volume
h_zero : Tendsto (u * v) (𝓝[>] a) (𝓝 a')
h_infty : Tendsto (u * v) atTop (𝓝 b')
⊢ (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi a)) fun (x : ℝ) ↦ u x * v' x) =
    b' - a' -
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi a)) fun (x : ℝ) ↦ u' x * v x
have rw : (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi a)) fun (a : ℝ) ↦
    u a * v' a + u' a * v a) =
  b' - a'
Tactic: rw [eq_sub_iff_add_eq, ← integral_add huv' hu'v]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntegralEqImproper (hypothesis)
Goal:
A : Type u_1
inst : NormedRing A
inst_1 : NormedAlgebra ℝ A
a : ℝ
a' b' : A
u v u' v' : ℝ → A
inst_2 : CompleteSpace A
hu : ∀ x ∈ Iio a, HasDerivAt u (u' x) x
hv : ∀ x ∈ Iio a, HasDerivAt v (v' x) x
huv : IntegrableOn (mα := MeasureSpace.toMeasurableSpace) (u' * v + u * v') (Iic a) volume
h_zero : Tendsto (u * v) (𝓝[<] a) (𝓝 a')
h_infty : Tendsto (u * v) atBot (𝓝 b')
⊢ (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Iic a)) fun (x : ℝ) ↦
      u' x * v x + u x * v' x) =
    a' - b'
have h_zero₁ : Tendsto (u * v) (𝓝[Iic a \ {a}] a) (𝓝 a')
Tactic: rw [← Iic_diff_right] at h_zero
Cleared hypotheses: h_zero, h_infty
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntegralEqImproper (goal)
Goal:
A : Type u_1
inst : NormedRing A
inst_1 : NormedAlgebra ℝ A
a : ℝ
a' b' : A
u v u' v' : ℝ → A
inst_2 : CompleteSpace A
hu : ∀ x ∈ Iio a, HasDerivAt u (u' x) x
hv : ∀ x ∈ Iio a, HasDerivAt v (v' x) x
huv : IntegrableOn (mα := MeasureSpace.toMeasurableSpace) (u' * v + u * v') (Iic a) volume
h_zero : Tendsto (u * v) (𝓝[Iic a \ {a}] a) (𝓝 a')
h_infty : Tendsto (u * v) atBot (𝓝 b')
f : (a : ℝ) → A := Function.update (β := fun (a : ℝ) ↦ A) (u * v) a a'
x : ℝ
hx : x ∈ Iio a
⊢ HasDerivAt f (u' x * v x + u x * v' x) x
have apply : f =ᶠ[𝓝 x] u * v
Tactic: apply ((hu x hx).mul (hv x hx)).congr_of_eventuallyEq
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntegralEqImproper (goal)
Goal:
A : Type u_1
inst : NormedRing A
inst_1 : NormedAlgebra ℝ A
a : ℝ
a' b' : A
u v u' v' : ℝ → A
inst_2 : CompleteSpace A
hu : ∀ x ∈ Iio a, HasDerivAt u (u' x) x
hv : ∀ x ∈ Iio a, HasDerivAt v (v' x) x
huv : IntegrableOn (mα := MeasureSpace.toMeasurableSpace) (u' * v + u * v') (Iic a) volume
h_zero : Tendsto (u * v) (𝓝[Iic a \ {a}] a) (𝓝 a')
h_infty : Tendsto (u * v) atBot (𝓝 b')
f : (a : ℝ) → A := Function.update (β := fun (a : ℝ) ↦ A) (u * v) a a'
x_1 : ℝ
hx : x_1 ∈ Iio a
x : ℝ
⊢ x ∈ Iio a → f x = (u * v) x
have h : ∀ (hx : x < a), f x = (u * v) x
Tactic: (hx : x < a)
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntegralEqImproper (goal)
Goal:
A : Type u_1
inst : NormedRing A
inst_1 : NormedAlgebra ℝ A
a : ℝ
a' b' : A
u v u' v' : ℝ → A
inst_2 : CompleteSpace A
hu : ∀ x ∈ Iio a, HasDerivAt u (u' x) x
hv : ∀ x ∈ Iio a, HasDerivAt v (v' x) x
huv : IntegrableOn (mα := MeasureSpace.toMeasurableSpace) (u' * v + u * v') (Iic a) volume
h_zero : Tendsto (u * v) (𝓝[Iic a \ {a}] a) (𝓝 a')
h_infty : Tendsto (u * v) atBot (𝓝 b')
f : (a : ℝ) → A := Function.update (β := fun (a : ℝ) ↦ A) (u * v) a a'
x : ℝ
hx : x ∈ Iio a
⊢ f =ᶠ[𝓝 x] u * v
have h : ∀ (x : ℝ) (hx : x < a), f x = (u * v) x
Tactic: filter_upwards [Iio_mem_nhds hx] with x (hx : x < a)
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntegralEqImproper (hypothesis)
Goal:
A : Type u_1
inst : NormedRing A
inst_1 : NormedAlgebra ℝ A
a : ℝ
a' b' : A
u v u' v' : ℝ → A
inst_2 : CompleteSpace A
hu : ∀ x ∈ Iio a, HasDerivAt u (u' x) x
hv : ∀ x ∈ Iio a, HasDerivAt v (v' x) x
huv : IntegrableOn (mα := MeasureSpace.toMeasurableSpace) (u' * v + u * v') (Iic a) volume
h_zero : Tendsto (u * v) (𝓝[Iic a \ {a}] a) (𝓝 a')
h_infty : Tendsto (u * v) atBot (𝓝 b')
f : (a : ℝ) → A := Function.update (β := fun (a : ℝ) ↦ A) (u * v) a a'
⊢ (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Iic a)) fun (x : ℝ) ↦
      u' x * v x + u x * v' x) =
    a' - b'
have hderiv : ∀ x ∈ Iio a, HasDerivAt f (u' x * v x + u x * v' x) x
Tactic: have hderiv : ∀ x ∈ Iio a, HasDerivAt f (u' x * v x + u x * v' x) x := by
    intro x hx
    apply ((hu x hx).mul (hv x hx)).congr_of_eventuallyEq
    filter_upwards [Iio_mem_nhds hx] with x (hx : x < a)
    exact Function.update_of_ne (ne_of_lt hx) a' (u * v)
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntegralEqImproper (goal)
Goal:
A : Type u_1
inst : NormedRing A
inst_1 : NormedAlgebra ℝ A
a : ℝ
a' b' : A
u v u' v' : ℝ → A
inst_2 : CompleteSpace A
hu : ∀ x ∈ Iio a, HasDerivAt u (u' x) x
hv : ∀ x ∈ Iio a, HasDerivAt v (v' x) x
huv : IntegrableOn (mα := MeasureSpace.toMeasurableSpace) (u' * v + u * v') (Iic a) volume
h_zero : Tendsto (u * v) (𝓝[Iic a \ {a}] a) (𝓝 a')
h_infty : Tendsto (u * v) atBot (𝓝 b')
f : (a : ℝ) → A := Function.update (β := fun (a : ℝ) ↦ A) (u * v) a a'
hderiv : ∀ x ∈ Iio a, HasDerivAt f (u' x * v x + u x * v' x) x
⊢ Tendsto f atBot (𝓝 b')
have apply : u * v =ᶠ[atBot] f
Tactic: apply h_infty.congr'
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntegralEqImproper (goal)
Goal:
A : Type u_1
inst : NormedRing A
inst_1 : NormedAlgebra ℝ A
a : ℝ
a' b' : A
u v u' v' : ℝ → A
inst_2 : CompleteSpace A
hu : ∀ x ∈ Iio a, HasDerivAt u (u' x) x
hv : ∀ x ∈ Iio a, HasDerivAt v (v' x) x
huv : IntegrableOn (mα := MeasureSpace.toMeasurableSpace) (u' * v + u * v') (Iic a) volume
h_zero : Tendsto (u * v) (𝓝[Iic a \ {a}] a) (𝓝 a')
h_infty : Tendsto (u * v) atBot (𝓝 b')
f : (a : ℝ) → A := Function.update (β := fun (a : ℝ) ↦ A) (u * v) a a'
hderiv : ∀ x ∈ Iio a, HasDerivAt f (u' x * v x + u x * v' x) x
x : ℝ
⊢ x ∈ Iio a → (u * v) x = f x
have h : ∀ (hx : x < a), (u * v) x = f x
Tactic: (hx : x < a)