awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Integral.IntegralEqImproper
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))
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))
⊢ 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

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

Tactic:
simp [integral, hG]

Premises used: MeasureTheory.integral
-- Module: Mathlib.MeasureTheory.Integral.IntegralEqImproper
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
⊢ 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
-- Module: Mathlib.MeasureTheory.Integral.IntegralEqImproper
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)
⊢ 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
-- Module: Mathlib.MeasureTheory.Integral.IntegralEqImproper
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)
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)
⊢ 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:
simp [integral_bilinear_hasDerivAt_right_eq_sub hu hv huv' hu'v I J]

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

Tactic:
integral_of_hasDerivAt_of_tendsto (fun x ↦ ?_) huv h_bot h_top

Premises used: MeasureTheory.integral_of_hasDerivAt_of_tendsto
-- Module: Mathlib.MeasureTheory.Integral.IntegralEqImproper
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')
refine : ∀ (x : ℝ), HasDerivAt (u * v) (u' x * v x + u x * v' x) x
⊢ (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : ℝ) ↦ u' x * v x + u x * v' x) = b' - a'

Tactic:
refine integral_of_hasDerivAt_of_tendsto (fun x ↦ ?_) huv h_bot h_top

Premises used: MeasureTheory.integral_of_hasDerivAt_of_tendsto
-- Module: Mathlib.MeasureTheory.Integral.IntegralEqImproper
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')
x : ℝ
⊢ HasDerivAt (u * v) (u' x * v x + u x * v' x) x

Tactic:
simpa [add_comm] using (ContinuousLinearMap.mul ℝ A).hasDerivAt_of_bilinear (hu x) (hv x)

Premises used: add_comm, ContinuousLinearMap.hasDerivAt_of_bilinear
-- Module: Mathlib.MeasureTheory.Integral.IntegralEqImproper
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') volume
hu'v : @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace (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) =
    b' - a' - @integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : ℝ) ↦ u' x * v x

Tactic:
integral_bilinear_hasDerivAt_right_eq_sub (L := ContinuousLinearMap.mul ℝ A)
    hu hv huv' hu'v h_bot h_top

Premises used: MeasureTheory.integral_bilinear_hasDerivAt_right_eq_sub
-- Module: Mathlib.MeasureTheory.Integral.IntegralEqImproper
Goal:
A : Type u_1
inst : NormedRing A
inst_1 : NormedAlgebra ℝ A
u v u' v' : ℝ → 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') volume
hu'v : @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace (u' * v) volume
huv : @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace (u * v) volume
⊢ Eq.{u_1 + 1} (α := A) (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : ℝ) ↦ u x * v' x)
    (-@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : ℝ) ↦ u' x * v x)

Tactic:
integral_bilinear_hasDerivAt_right_eq_neg_left_of_integrable (L := ContinuousLinearMap.mul ℝ A)
    hu hv huv' hu'v huv

Premises used: MeasureTheory.integral_bilinear_hasDerivAt_right_eq_neg_left_of_integrable
-- Module: Mathlib.MeasureTheory.Integral.IntegralEqImproper
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')
⊢ Tendsto (u * v) (𝓝[Ici a \ {a}] a) (𝓝 a')

Tactic:
rw [← Ici_diff_left] at h_zero

Premises used: Set.Ici_diff_left
-- Module: Mathlib.MeasureTheory.Integral.IntegralEqImproper
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')
h_zero₁ : Tendsto (u * v) (𝓝[Ici a \ {a}] a) (𝓝 a')
⊢ Tendsto (u * v) atTop (𝓝 b')

Tactic:
rw [← Ici_diff_left] at h_zero

Premises used: Set.Ici_diff_left
-- Module: Mathlib.MeasureTheory.Integral.IntegralEqImproper
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 : ℝ
a₁ : ∀ (hx : a < x), HasDerivAt f (u' x * v x + u x * v' x) x
⊢ x ∈ Ioi a → HasDerivAt f (u' x * v x + u x * v' x) x

Tactic:
(hx : a < x)
-- Module: Mathlib.MeasureTheory.Integral.IntegralEqImproper
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
apply : f =ᶠ[𝓝 x] u * v
⊢ HasDerivAt f (u' x * v x + u x * v' x) x

Tactic:
apply ((hu x hx).mul (hv x hx)).congr_of_eventuallyEq

Premises used: HasDerivAt.congr_of_eventuallyEq, HasDerivAt.mul
-- Module: Mathlib.MeasureTheory.Integral.IntegralEqImproper
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
h : ∀ (y : ℝ) (hy : y ≠ a), f y = (u * v) y
⊢ f =ᶠ[𝓝 x] u * v

Tactic:
filter_upwards [eventually_ne_nhds hx.ne.symm] with y hy

Premises used: eventually_ne_nhds, Ne.symm, LT.lt.ne
-- Module: Mathlib.MeasureTheory.Integral.IntegralEqImproper
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
y : ℝ
hy : y ≠ a
⊢ f y = (u * v) y

Tactic:
Function.update_of_ne hy a' (u * v)

Premises used: HMul.hMul, Function.update_of_ne
-- Module: Mathlib.MeasureTheory.Integral.IntegralEqImproper
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
y : ℝ
hy : y ≠ a
⊢ f y = (u * v) y

Tactic:
exact Function.update_of_ne hy a' (u * v)

Premises used: HMul.hMul, Function.update_of_ne
-- Module: Mathlib.MeasureTheory.Integral.IntegralEqImproper
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 ∈ 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)
-- Module: Mathlib.MeasureTheory.Integral.IntegralEqImproper
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
apply : u * v =ᶠ[atTop] f
⊢ Tendsto f atTop (𝓝 b')

Tactic:
apply h_infty.congr'

Premises used: Filter.Tendsto.congr'
-- Module: Mathlib.MeasureTheory.Integral.IntegralEqImproper
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
h : ∀ (x : ℝ) (hx : x ≠ a), (u * v) x = f x
⊢ u * v =ᶠ[atTop] f

Tactic:
filter_upwards [eventually_ne_atTop a] with x hx

Premises used: Filter.eventually_ne_atTop
-- Module: Mathlib.MeasureTheory.Integral.IntegralEqImproper
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
x : ℝ
hx : x ≠ a
⊢ (u * v) x = f x

Tactic:
(Function.update_of_ne hx a' (u * v)).symm

Premises used: HMul.hMul, Eq.symm, Function.update_of_ne
-- Module: Mathlib.MeasureTheory.Integral.IntegralEqImproper
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
x : ℝ
hx : x ≠ a
⊢ (u * v) x = f x

Tactic:
exact (Function.update_of_ne hx a' (u * v)).symm

Premises used: HMul.hMul, Eq.symm, Function.update_of_ne
-- Module: Mathlib.MeasureTheory.Integral.IntegralEqImproper
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')

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
-- Module: Mathlib.MeasureTheory.Integral.IntegralEqImproper
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
htendsto : Tendsto f atTop (𝓝 b')
⊢ (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi a)) fun (x : ℝ) ↦
      u' x * v x + u x * v' x) =
    b' - a'

Tactic:
simpa using integral_Ioi_of_hasDerivAt_of_tendsto
    (continuousWithinAt_update_same.mpr h_zero) hderiv huv htendsto

Premises used: Iff.mpr, MeasureTheory.integral_Ioi_of_hasDerivAt_of_tendsto, continuousWithinAt_update_same
-- Module: Mathlib.MeasureTheory.Integral.IntegralEqImproper
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')
⊢ 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

Premises used: Pi.mul_def
-- Module: Mathlib.MeasureTheory.Integral.IntegralEqImproper
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
⊢ 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

Premises used: Pi.mul_def
-- Module: Mathlib.MeasureTheory.Integral.IntegralEqImproper
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
hu'v₁ : IntegrableOn.{0, u_1} (ε := A) (mα := MeasureSpace.toMeasurableSpace) (fun (i : ℝ) ↦ u' i * v i) (Ioi a) volume
⊢ Tendsto (u * v) (𝓝[>] a) (𝓝 a')

Tactic:
rw [Pi.mul_def] at huv' hu'v

Premises used: Pi.mul_def