awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
h_zero₁ : Tendsto (u * v) (𝓝[>] a) (𝓝 a')
⊢ Tendsto (u * v) atTop (𝓝 b')

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.{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')
rw :
  (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi a)) fun (a : ℝ) ↦
      u a * v' a + u' a * v a) =
    b' - a'
⊢ (@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

Tactic:
rw [eq_sub_iff_add_eq, ← integral_add huv' hu'v]

Premises used: eq_sub_iff_add_eq, MeasureTheory.integral_add
-- 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.{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 (a : ℝ) ↦
      u a * v' a + u' a * v a) =
    b' - a'

Tactic:
simpa only [add_comm] using integral_Ioi_deriv_mul_eq_sub hu hv (hu'v.add huv') h_zero h_infty

Premises used: MeasureTheory.integral_Ioi_deriv_mul_eq_sub, add_comm, MeasureTheory.IntegrableOn.add
-- 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 ∈ 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')
⊢ Tendsto (u * v) (𝓝[Iic a \ {a}] a) (𝓝 a')

Tactic:
rw [← Iic_diff_right] at h_zero

Premises used: Set.Iic_diff_right
-- 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 ∈ 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')
h_zero₁ : Tendsto (u * v) (𝓝[Iic a \ {a}] a) (𝓝 a')
⊢ Tendsto (u * v) atBot (𝓝 b')

Tactic:
rw [← Iic_diff_right] at h_zero

Premises used: Set.Iic_diff_right
-- 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 ∈ 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
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 ∈ 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 : ℝ
h : ∀ (hx : x < a), f x = (u * v) x
⊢ x ∈ Iio a → f x = (u * v) x

Tactic:
(hx : x < a)
-- 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 ∈ 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
h : ∀ (x : ℝ) (hx : x < a), f x = (u * v) x
⊢ f =ᶠ[𝓝 x] u * v

Tactic:
filter_upwards [Iio_mem_nhds hx] with x (hx : x < a)

Premises used: Iio_mem_nhds
-- 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 ∈ 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_1 : x_1 ∈ Iio a
x : ℝ
hx : x < a
⊢ f x = (u * v) x

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

Premises used: HMul.hMul, ne_of_lt, 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 ∈ 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_1 : x_1 ∈ Iio a
x : ℝ
hx : x < a
⊢ f x = (u * v) x

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

Premises used: HMul.hMul, ne_of_lt, 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 ∈ 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 ∈ 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)
-- 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 ∈ 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
apply : u * v =ᶠ[atBot] f
⊢ Tendsto f atBot (𝓝 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 ∈ 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 : ℝ
h : ∀ (hx : x < a), (u * v) x = f x
⊢ x ∈ Iio a → (u * v) x = f x

Tactic:
(hx : x < a)
-- 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 ∈ 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
h : ∀ (x : ℝ) (hx : x < a), (u * v) x = f x
⊢ u * v =ᶠ[atBot] f

Tactic:
filter_upwards [Iio_mem_atBot a] with x (hx : x < a)

Premises used: Filter.Iio_mem_atBot
-- 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 ∈ 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 : ℝ
hx : x < a
⊢ (u * v) x = f x

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

Premises used: HMul.hMul, Eq.symm, ne_of_lt, 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 ∈ 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 : ℝ
hx : x < a
⊢ (u * v) x = f x

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

Premises used: HMul.hMul, Eq.symm, ne_of_lt, 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 ∈ 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')

Tactic:
have htendsto : Tendsto f atBot (𝓝 b') := by
    apply h_infty.congr'
    filter_upwards [Iio_mem_atBot a] with x (hx : x < a)
    exact (Function.update_of_ne (ne_of_lt 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 ∈ 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
htendsto : Tendsto f atBot (𝓝 b')
⊢ (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Iic a)) fun (x : ℝ) ↦
      u' x * v x + u x * v' x) =
    a' - b'

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

Premises used: Iff.mpr, MeasureTheory.integral_Iic_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 ∈ Iio a, HasDerivAt u (u' x) x
hv : ∀ x ∈ Iio a, HasDerivAt v (v' x) x
huv' : IntegrableOn (mα := MeasureSpace.toMeasurableSpace) (u * v') (Iic a) volume
hu'v : IntegrableOn (mα := MeasureSpace.toMeasurableSpace) (u' * v) (Iic a) volume
h_zero : Tendsto (u * v) (𝓝[<] a) (𝓝 a')
h_infty : Tendsto (u * v) atBot (𝓝 b')
⊢ IntegrableOn.{0, u_1} (ε := A) (mα := MeasureSpace.toMeasurableSpace) (fun (i : ℝ) ↦ u i * v' i) (Iic 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 ∈ Iio a, HasDerivAt u (u' x) x
hv : ∀ x ∈ Iio a, HasDerivAt v (v' x) x
huv' : IntegrableOn (mα := MeasureSpace.toMeasurableSpace) (u * v') (Iic a) volume
hu'v : IntegrableOn (mα := MeasureSpace.toMeasurableSpace) (u' * v) (Iic a) volume
h_zero : Tendsto (u * v) (𝓝[<] a) (𝓝 a')
h_infty : Tendsto (u * v) atBot (𝓝 b')
huv'₁ : IntegrableOn.{0, u_1} (ε := A) (mα := MeasureSpace.toMeasurableSpace) (fun (i : ℝ) ↦ u i * v' i) (Iic a) volume
⊢ IntegrableOn.{0, u_1} (ε := A) (mα := MeasureSpace.toMeasurableSpace) (fun (i : ℝ) ↦ u' i * v i) (Iic 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 ∈ Iio a, HasDerivAt u (u' x) x
hv : ∀ x ∈ Iio a, HasDerivAt v (v' x) x
huv' : IntegrableOn (mα := MeasureSpace.toMeasurableSpace) (u * v') (Iic a) volume
hu'v : IntegrableOn (mα := MeasureSpace.toMeasurableSpace) (u' * v) (Iic a) volume
h_zero : Tendsto (u * v) (𝓝[<] a) (𝓝 a')
h_infty : Tendsto (u * v) atBot (𝓝 b')
huv'₁ : IntegrableOn.{0, u_1} (ε := A) (mα := MeasureSpace.toMeasurableSpace) (fun (i : ℝ) ↦ u i * v' i) (Iic a) volume
hu'v₁ : IntegrableOn.{0, u_1} (ε := A) (mα := MeasureSpace.toMeasurableSpace) (fun (i : ℝ) ↦ u' i * v i) (Iic a) volume
⊢ Tendsto (u * v) (𝓝[<] a) (𝓝 a')

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 ∈ Iio a, HasDerivAt u (u' x) x
hv : ∀ x ∈ Iio a, HasDerivAt v (v' x) x
huv' : IntegrableOn (mα := MeasureSpace.toMeasurableSpace) (u * v') (Iic a) volume
hu'v : IntegrableOn (mα := MeasureSpace.toMeasurableSpace) (u' * v) (Iic a) volume
h_zero : Tendsto (u * v) (𝓝[<] a) (𝓝 a')
h_infty : Tendsto (u * v) atBot (𝓝 b')
huv'₁ : IntegrableOn.{0, u_1} (ε := A) (mα := MeasureSpace.toMeasurableSpace) (fun (i : ℝ) ↦ u i * v' i) (Iic a) volume
hu'v₁ : IntegrableOn.{0, u_1} (ε := A) (mα := MeasureSpace.toMeasurableSpace) (fun (i : ℝ) ↦ u' i * v i) (Iic a) volume
h_zero₁ : Tendsto (u * v) (𝓝[<] a) (𝓝 a')
⊢ Tendsto (u * v) atBot (𝓝 b')

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 ∈ Iio a, HasDerivAt u (u' x) x
hv : ∀ x ∈ Iio a, HasDerivAt v (v' x) x
huv' : IntegrableOn.{0, u_1} (ε := A) (mα := MeasureSpace.toMeasurableSpace) (fun (i : ℝ) ↦ u i * v' i) (Iic a) volume
hu'v : IntegrableOn.{0, u_1} (ε := A) (mα := MeasureSpace.toMeasurableSpace) (fun (i : ℝ) ↦ u' i * v i) (Iic a) volume
h_zero : Tendsto (u * v) (𝓝[<] a) (𝓝 a')
h_infty : Tendsto (u * v) atBot (𝓝 b')
rw :
  (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Iic a)) fun (a : ℝ) ↦
      u a * v' a + u' a * v a) =
    a' - b'
⊢ (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Iic a)) fun (x : ℝ) ↦ u x * v' x) =
    a' - b' -
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Iic a)) fun (x : ℝ) ↦ u' x * v x

Tactic:
rw [eq_sub_iff_add_eq, ← integral_add huv' hu'v]

Premises used: eq_sub_iff_add_eq, MeasureTheory.integral_add
-- 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 ∈ Iio a, HasDerivAt u (u' x) x
hv : ∀ x ∈ Iio a, HasDerivAt v (v' x) x
huv' : IntegrableOn.{0, u_1} (ε := A) (mα := MeasureSpace.toMeasurableSpace) (fun (i : ℝ) ↦ u i * v' i) (Iic a) volume
hu'v : IntegrableOn.{0, u_1} (ε := A) (mα := MeasureSpace.toMeasurableSpace) (fun (i : ℝ) ↦ u' i * v i) (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 (a : ℝ) ↦
      u a * v' a + u' a * v a) =
    a' - b'

Tactic:
simpa only [add_comm] using integral_Iic_deriv_mul_eq_sub hu hv (hu'v.add huv') h_zero h_infty

Premises used: add_comm, MeasureTheory.IntegrableOn.add, MeasureTheory.integral_Iic_deriv_mul_eq_sub
-- Module: Mathlib.MeasureTheory.Integral.IntervalAverage
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
rw :
  HSMul.hSMul (β := E) (Measure.real (m := MeasureSpace.toMeasurableSpace) volume (Ι a b))⁻¹
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ι a b)) fun (x : ℝ) ↦ f x) =
    ⨍ (x : ℝ) in b..a, f x
rw₁ :
  HSMul.hSMul (β := E) (Measure.real (m := MeasureSpace.toMeasurableSpace) volume (Ι a b))⁻¹
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ι a b)) fun (x : ℝ) ↦ f x) =
    HSMul.hSMul (β := E) (Measure.real (m := MeasureSpace.toMeasurableSpace) volume (Ι b a))⁻¹
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ι b a)) fun (x : ℝ) ↦ f x)
rw₂ rw₃ :
  HSMul.hSMul (β := E) (Measure.real (m := MeasureSpace.toMeasurableSpace) volume (Ι b a))⁻¹
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ι b a)) fun (x : ℝ) ↦ f x) =
    HSMul.hSMul (β := E) (Measure.real (m := MeasureSpace.toMeasurableSpace) volume (Ι b a))⁻¹
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ι b a)) fun (x : ℝ) ↦ f x)
⊢ Eq.{u_1 + 1} (α := E) (⨍ (x : ℝ) in a..b, f x) (⨍ (x : ℝ) in b..a, f x)

Tactic:
rw [setAverage_eq, setAverage_eq, uIoc_comm]

Premises used: Set.uIoc_comm, MeasureTheory.setAverage_eq
-- Module: Mathlib.MeasureTheory.Integral.IntervalAverage
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
inl : ∀ (h : a ≤ b), ⨍ (x : ℝ) in a..b, f x = HSMul.hSMul (β := E) (b - a)⁻¹ (∫ (x : ℝ) in a..b, f x)
inr : ∀ (h : b < a), ⨍ (x : ℝ) in a..b, f x = HSMul.hSMul (β := E) (b - a)⁻¹ (∫ (x : ℝ) in a..b, f x)
⊢ ⨍ (x : ℝ) in a..b, f x = HSMul.hSMul (β := E) (b - a)⁻¹ (∫ (x : ℝ) in a..b, f x)

Tactic:
rcases le_or_gt a b with h | h

Premises used: le_or_gt
-- Module: Mathlib.MeasureTheory.Integral.IntervalAverage
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
h : a ≤ b
inl :
  HSMul.hSMul (β := E) (Measure.real (m := MeasureSpace.toMeasurableSpace) volume (Ι a b))⁻¹
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ι a b)) fun (x : ℝ) ↦ f x) =
    HSMul.hSMul (β := E) (b - a)⁻¹ (∫ (x : ℝ) in a..b, f x)
inl₁ :
  HSMul.hSMul (β := E) (Measure.real (m := MeasureSpace.toMeasurableSpace) volume (Ioc a b))⁻¹
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioc a b)) fun (x : ℝ) ↦ f x) =
    HSMul.hSMul (β := E) (b - a)⁻¹ (∫ (x : ℝ) in a..b, f x)
inl₂ :
  HSMul.hSMul (β := E) (b - a)⁻¹
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioc a b)) fun (x : ℝ) ↦ f x) =
    HSMul.hSMul (β := E) (b - a)⁻¹ (∫ (x : ℝ) in a..b, f x)
inl₃ inl₄ :
  HSMul.hSMul (β := E) (b - a)⁻¹
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioc a b)) fun (x : ℝ) ↦ f x) =
    HSMul.hSMul (β := E) (b - a)⁻¹
      (@integral _ _ _ _ Real.measurableSpace (Measure.restrict volume (Ioc a b)) fun (x : ℝ) ↦ f x)
⊢ ⨍ (x : ℝ) in a..b, f x = HSMul.hSMul (β := E) (b - a)⁻¹ (∫ (x : ℝ) in a..b, f x)

Tactic:
rw [setAverage_eq, uIoc_of_le h, Real.volume_real_Ioc_of_le h, integral_of_le h]

Premises used: Real.volume_real_Ioc_of_le, MeasureTheory.setAverage_eq, intervalIntegral.integral_of_le, Set.uIoc_of_le