awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus
Goal:
g' g : ℝ → ℝ
a b : ℝ
hcont : ContinuousOn g (Icc a b)
hderiv : ∀ x ∈ Ioo a b, HasDerivWithinAt g (g' x) (Ioi x) x
g'pos : ∀ x ∈ Ioo a b, 0 ≤ g' x
hab : a < b
meas_g' : AEMeasurable (_m := MeasureSpace.toMeasurableSpace) g' (Measure.restrict volume (Ioo a b))
H : ENNReal.ofReal (g b - g a) < ∫⁻ (x : ℝ) in Ioo a b, (↑‖g' x‖₊ : ℝ≥0∞)
f : SimpleFunc ℝ ℝ≥0
fle : ∀ (x : ℝ), (f : (a : ℝ) → ℝ≥0) x ≤ ‖g' x‖₊
fint : ∫⁻ (x : ℝ) in Ioo a b, (↑((f : (a : ℝ) → ℝ≥0) x) : ℝ≥0∞) < ∞
F : ℝ → ℝ := NNReal.toReal ∘ (⇑f : (a : ℝ) → ℝ≥0)
hf :
  ENNReal.ofReal (g b - g a) <
    ENNReal.ofReal
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioo a b)) fun (x : ℝ) ↦ F x)
intF : IntegrableOn (mα := MeasureSpace.toMeasurableSpace) F (Ioo a b) volume
A :
  ∫⁻ (x : ℝ) in Ioo a b, (↑((f : (a : ℝ) → ℝ≥0) x) : ℝ≥0∞) =
    ENNReal.ofReal
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioo a b)) fun (x : ℝ) ↦ F x)
x : ℝ
hx : x ∈ Ioo a b
⊢ (↑((f : (a : ℝ) → ℝ≥0) x) : ℝ) ≤ (↑‖g' x‖₊ : ℝ)

Tactic:
NNReal.coe_le_coe.2 (fle x)

Premises used: Iff.mpr, NNReal.coe_le_coe
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus
Goal:
g' g : ℝ → ℝ
a b : ℝ
hcont : ContinuousOn g (Icc a b)
hderiv : ∀ x ∈ Ioo a b, HasDerivWithinAt g (g' x) (Ioi x) x
g'pos : ∀ x ∈ Ioo a b, 0 ≤ g' x
hab : a < b
meas_g' : AEMeasurable (_m := MeasureSpace.toMeasurableSpace) g' (Measure.restrict volume (Ioo a b))
H : ENNReal.ofReal (g b - g a) < ∫⁻ (x : ℝ) in Ioo a b, (↑‖g' x‖₊ : ℝ≥0∞)
f : SimpleFunc ℝ ℝ≥0
fle : ∀ (x : ℝ), (f : (a : ℝ) → ℝ≥0) x ≤ ‖g' x‖₊
fint : ∫⁻ (x : ℝ) in Ioo a b, (↑((f : (a : ℝ) → ℝ≥0) x) : ℝ≥0∞) < ∞
F : ℝ → ℝ := NNReal.toReal ∘ (⇑f : (a : ℝ) → ℝ≥0)
hf :
  ENNReal.ofReal (g b - g a) <
    ENNReal.ofReal
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioo a b)) fun (x : ℝ) ↦ F x)
intF : IntegrableOn (mα := MeasureSpace.toMeasurableSpace) F (Ioo a b) volume
A :
  ∫⁻ (x : ℝ) in Ioo a b, (↑((f : (a : ℝ) → ℝ≥0) x) : ℝ≥0∞) =
    ENNReal.ofReal
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioo a b)) fun (x : ℝ) ↦ F x)
x : ℝ
hx : x ∈ Ioo a b
h : g' x = (↑‖g' x‖₊ : ℝ)
⊢ F x ≤ g' x

Tactic:
convert! NNReal.coe_le_coe.2 (fle x)

Premises used: Iff.mpr, NNReal.coe_le_coe
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus
Goal:
g' g : ℝ → ℝ
a b : ℝ
hcont : ContinuousOn g (Icc a b)
hderiv : ∀ x ∈ Ioo a b, HasDerivWithinAt g (g' x) (Ioi x) x
g'pos : ∀ x ∈ Ioo a b, 0 ≤ g' x
hab : a < b
meas_g' : AEMeasurable (_m := MeasureSpace.toMeasurableSpace) g' (Measure.restrict volume (Ioo a b))
H : ENNReal.ofReal (g b - g a) < ∫⁻ (x : ℝ) in Ioo a b, (↑‖g' x‖₊ : ℝ≥0∞)
f : SimpleFunc ℝ ℝ≥0
fle : ∀ (x : ℝ), (f : (a : ℝ) → ℝ≥0) x ≤ ‖g' x‖₊
fint : ∫⁻ (x : ℝ) in Ioo a b, (↑((f : (a : ℝ) → ℝ≥0) x) : ℝ≥0∞) < ∞
F : ℝ → ℝ := NNReal.toReal ∘ (⇑f : (a : ℝ) → ℝ≥0)
hf :
  ENNReal.ofReal (g b - g a) <
    ENNReal.ofReal
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioo a b)) fun (x : ℝ) ↦ F x)
intF : IntegrableOn (mα := MeasureSpace.toMeasurableSpace) F (Ioo a b) volume
A :
  ∫⁻ (x : ℝ) in Ioo a b, (↑((f : (a : ℝ) → ℝ≥0) x) : ℝ≥0∞) =
    ENNReal.ofReal
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioo a b)) fun (x : ℝ) ↦ F x)
x : ℝ
hx : x ∈ Ioo a b
⊢ g' x = (↑‖g' x‖₊ : ℝ)

Tactic:
simp only [Real.norm_of_nonneg (g'pos x hx), coe_nnnorm]

Premises used: coe_nnnorm, Real.norm_of_nonneg
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus
Goal:
g' g : ℝ → ℝ
a b : ℝ
hcont : ContinuousOn g (Icc a b)
hderiv : ∀ x ∈ Ioo a b, HasDerivWithinAt g (g' x) (Ioi x) x
g'pos : ∀ x ∈ Ioo a b, 0 ≤ g' x
hab : a < b
meas_g' : AEMeasurable (_m := MeasureSpace.toMeasurableSpace) g' (Measure.restrict volume (Ioo a b))
H : ENNReal.ofReal (g b - g a) < ∫⁻ (x : ℝ) in Ioo a b, (↑‖g' x‖₊ : ℝ≥0∞)
f : SimpleFunc ℝ ℝ≥0
fle : ∀ (x : ℝ), (f : (a : ℝ) → ℝ≥0) x ≤ ‖g' x‖₊
fint : ∫⁻ (x : ℝ) in Ioo a b, (↑((f : (a : ℝ) → ℝ≥0) x) : ℝ≥0∞) < ∞
F : ℝ → ℝ := NNReal.toReal ∘ (⇑f : (a : ℝ) → ℝ≥0)
hf :
  ENNReal.ofReal (g b - g a) <
    ENNReal.ofReal
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioo a b)) fun (x : ℝ) ↦ F x)
intF : IntegrableOn (mα := MeasureSpace.toMeasurableSpace) F (Ioo a b) volume
A :
  ∫⁻ (x : ℝ) in Ioo a b, (↑((f : (a : ℝ) → ℝ≥0) x) : ℝ≥0∞) =
    ENNReal.ofReal
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioo a b)) fun (x : ℝ) ↦ F x)
⊢ (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioo a b)) fun (x : ℝ) ↦ F x) ≤ g b - g a

Tactic:
have B : (∫ x : ℝ in Ioo a b, F x) ≤ g b - g a := by
    rw [← integral_Ioc_eq_integral_Ioo, ← intervalIntegral.integral_of_le hab.le]
    refine integral_le_sub_of_hasDeriv_right_of_le hab.le hcont hderiv ?_ fun x hx => ?_
    · rwa [integrableOn_Icc_iff_integrableOn_Ioo]
    · convert! NNReal.coe_le_coe.2 (fle x)
      simp only [Real.norm_of_nonneg (g'pos x hx), coe_nnnorm]
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus
Goal:
g' g : ℝ → ℝ
a b : ℝ
hcont : ContinuousOn g (Icc a b)
hderiv : ∀ x ∈ Ioo a b, HasDerivWithinAt g (g' x) (Ioi x) x
g'pos : ∀ x ∈ Ioo a b, 0 ≤ g' x
hab : a < b
meas_g' : AEMeasurable (_m := MeasureSpace.toMeasurableSpace) g' (Measure.restrict volume (Ioo a b))
H : ENNReal.ofReal (g b - g a) < ∫⁻ (x : ℝ) in Ioo a b, (↑‖g' x‖₊ : ℝ≥0∞)
f : SimpleFunc ℝ ℝ≥0
fle : ∀ (x : ℝ), (f : (a : ℝ) → ℝ≥0) x ≤ ‖g' x‖₊
fint : ∫⁻ (x : ℝ) in Ioo a b, (↑((f : (a : ℝ) → ℝ≥0) x) : ℝ≥0∞) < ∞
F : ℝ → ℝ := NNReal.toReal ∘ (⇑f : (a : ℝ) → ℝ≥0)
hf :
  ENNReal.ofReal (g b - g a) <
    ENNReal.ofReal
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioo a b)) fun (x : ℝ) ↦ F x)
intF : IntegrableOn (mα := MeasureSpace.toMeasurableSpace) F (Ioo a b) volume
A :
  ∫⁻ (x : ℝ) in Ioo a b, (↑((f : (a : ℝ) → ℝ≥0) x) : ℝ≥0∞) =
    ENNReal.ofReal
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioo a b)) fun (x : ℝ) ↦ F x)
B : (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioo a b)) fun (x : ℝ) ↦ F x) ≤ g b - g a
⊢ False

Tactic:
lt_irrefl _ (hf.trans_le (ENNReal.ofReal_le_ofReal B))

Premises used: lt_irrefl, ENNReal.ofReal_le_ofReal, LT.lt.trans_le
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus
Goal:
g' g : ℝ → ℝ
a b : ℝ
hcont : ContinuousOn g (Icc a b)
hderiv : ∀ x ∈ Ioo a b, HasDerivWithinAt g (g' x) (Ioi x) x
g'pos : ∀ x ∈ Ioo a b, 0 ≤ g' x
hab : a < b
meas_g' : AEMeasurable (_m := MeasureSpace.toMeasurableSpace) g' (Measure.restrict volume (Ioo a b))
H : ENNReal.ofReal (g b - g a) < ∫⁻ (x : ℝ) in Ioo a b, (↑‖g' x‖₊ : ℝ≥0∞)
f : SimpleFunc ℝ ℝ≥0
fle : ∀ (x : ℝ), (f : (a : ℝ) → ℝ≥0) x ≤ ‖g' x‖₊
fint : ∫⁻ (x : ℝ) in Ioo a b, (↑((f : (a : ℝ) → ℝ≥0) x) : ℝ≥0∞) < ∞
F : ℝ → ℝ := NNReal.toReal ∘ (⇑f : (a : ℝ) → ℝ≥0)
hf :
  ENNReal.ofReal (g b - g a) <
    ENNReal.ofReal
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioo a b)) fun (x : ℝ) ↦ F x)
intF : IntegrableOn (mα := MeasureSpace.toMeasurableSpace) F (Ioo a b) volume
A :
  ∫⁻ (x : ℝ) in Ioo a b, (↑((f : (a : ℝ) → ℝ≥0) x) : ℝ≥0∞) =
    ENNReal.ofReal
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioo a b)) fun (x : ℝ) ↦ F x)
B : (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioo a b)) fun (x : ℝ) ↦ F x) ≤ g b - g a
⊢ False

Tactic:
exact lt_irrefl _ (hf.trans_le (ENNReal.ofReal_le_ofReal B))

Premises used: lt_irrefl, ENNReal.ofReal_le_ofReal, LT.lt.trans_le
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus
Goal:
g' g : ℝ → ℝ
a b : ℝ
hcont : ContinuousOn g (Icc a b)
hderiv : ∀ x ∈ Ioo a b, HasDerivAt g (g' x) x
g'pos : ∀ x ∈ Ioo a b, 0 ≤ g' x
⊢ IntegrableOn (mα := MeasureSpace.toMeasurableSpace) g' (Ioc a b) volume

Tactic:
integrableOn_deriv_right_of_nonneg hcont (fun x hx => (hderiv x hx).hasDerivWithinAt) g'pos

Premises used: HasDerivAt.hasDerivWithinAt, intervalIntegral.integrableOn_deriv_right_of_nonneg
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus
Goal:
g' g : ℝ → ℝ
a b : ℝ
hcont : ContinuousOn g [[a, b]]
hderiv : ∀ x ∈ Ioo (min a b) (max a b), HasDerivAt g (g' x) x
hpos : ∀ x ∈ Ioo (min a b) (max a b), 0 ≤ g' x
inl : ∀ (hab : a ≤ b), IntervalIntegrable g' volume a b
inr : ∀ (hab : b ≤ a), IntervalIntegrable g' volume a b
⊢ IntervalIntegrable g' volume a b

Tactic:
rcases le_total a b with hab | hab

Premises used: le_total
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus
Goal:
g' g : ℝ → ℝ
a b : ℝ
hcont : ContinuousOn g [[a, b]]
hderiv : ∀ x ∈ Ioo (min a b) (max a b), HasDerivAt g (g' x) x
hpos : ∀ x ∈ Ioo (min a b) (max a b), 0 ≤ g' x
hab : a ≤ b
inl :
  ∀ (hcont : ContinuousOn g (Icc a b)) (hderiv : ∀ x ∈ Ioo a b, HasDerivAt g (g' x) x) (hpos : ∀ x ∈ Ioo a b, 0 ≤ g' x),
    IntegrableOn (mα := Real.measurableSpace) g' (Ioc a b) volume
⊢ IntervalIntegrable g' volume a b

Tactic:
simp only [uIcc_of_le, min_eq_left, max_eq_right, IntervalIntegrable, hab,
      Ioc_eq_empty_of_le, integrableOn_empty, and_true] at hcont hderiv hpos ⊢

Premises used: and_true, IntervalIntegrable, Set.uIcc_of_le, max_eq_right, MeasureTheory.integrableOn_empty, min_eq_left, Set.Ioc_eq_empty_of_le
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus
Goal:
g' g : ℝ → ℝ
a b : ℝ
hab : a ≤ b
hcont : ContinuousOn g (Icc a b)
hderiv : ∀ x ∈ Ioo a b, HasDerivAt g (g' x) x
hpos : ∀ x ∈ Ioo a b, 0 ≤ g' x
⊢ IntegrableOn (mα := Real.measurableSpace) g' (Ioc a b) volume

Tactic:
integrableOn_deriv_of_nonneg hcont hderiv hpos

Premises used: intervalIntegral.integrableOn_deriv_of_nonneg
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus
Goal:
g' g : ℝ → ℝ
a b : ℝ
hab : a ≤ b
hcont : ContinuousOn g (Icc a b)
hderiv : ∀ x ∈ Ioo a b, HasDerivAt g (g' x) x
hpos : ∀ x ∈ Ioo a b, 0 ≤ g' x
⊢ IntegrableOn (mα := Real.measurableSpace) g' (Ioc a b) volume

Tactic:
exact integrableOn_deriv_of_nonneg hcont hderiv hpos

Premises used: intervalIntegral.integrableOn_deriv_of_nonneg
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus
Goal:
g' g : ℝ → ℝ
a b : ℝ
hcont : ContinuousOn g [[a, b]]
hderiv : ∀ x ∈ Ioo (min a b) (max a b), HasDerivAt g (g' x) x
hpos : ∀ x ∈ Ioo (min a b) (max a b), 0 ≤ g' x
hab : b ≤ a
inr :
  ∀ (hcont : ContinuousOn g (Icc b a)) (hderiv : ∀ x ∈ Ioo b a, HasDerivAt g (g' x) x) (hpos : ∀ x ∈ Ioo b a, 0 ≤ g' x),
    IntegrableOn (mα := Real.measurableSpace) g' (Ioc b a) volume
⊢ IntervalIntegrable g' volume a b

Tactic:
simp only [uIcc_of_ge, min_eq_right, max_eq_left, hab, IntervalIntegrable, Ioc_eq_empty_of_le,
      integrableOn_empty, true_and] at hcont hderiv hpos ⊢

Premises used: IntervalIntegrable, Set.uIcc_of_ge, max_eq_left, min_eq_right, MeasureTheory.integrableOn_empty, Set.Ioc_eq_empty_of_le, true_and
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus
Goal:
g' g : ℝ → ℝ
a b : ℝ
hab : b ≤ a
hcont : ContinuousOn g (Icc b a)
hderiv : ∀ x ∈ Ioo b a, HasDerivAt g (g' x) x
hpos : ∀ x ∈ Ioo b a, 0 ≤ g' x
⊢ IntegrableOn (mα := Real.measurableSpace) g' (Ioc b a) volume

Tactic:
integrableOn_deriv_of_nonneg hcont hderiv hpos

Premises used: intervalIntegral.integrableOn_deriv_of_nonneg
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus
Goal:
g' g : ℝ → ℝ
a b : ℝ
hab : b ≤ a
hcont : ContinuousOn g (Icc b a)
hderiv : ∀ x ∈ Ioo b a, HasDerivAt g (g' x) x
hpos : ∀ x ∈ Ioo b a, 0 ≤ g' x
⊢ IntegrableOn (mα := Real.measurableSpace) g' (Ioc b a) volume

Tactic:
exact integrableOn_deriv_of_nonneg hcont hderiv hpos

Premises used: intervalIntegral.integrableOn_deriv_of_nonneg
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.IntegrationByParts
Goal:
a b : ℝ
A : Type u_1
inst : NormedRing A
inst_1 : NormedAlgebra ℝ A
inst_2 : CompleteSpace A
u v u' v' : ℝ → A
hu : ContinuousOn u [[a, b]]
hv : ContinuousOn v [[a, b]]
huu' : ∀ x ∈ Ioo (min a b) (max a b), HasDerivWithinAt u (u' x) (Ioi x) x
hvv' : ∀ x ∈ Ioo (min a b) (max a b), HasDerivWithinAt v (v' x) (Ioi x) x
hu' : IntervalIntegrable u' volume a b
hv' : IntervalIntegrable v' volume a b
apply : IntervalIntegrable.{u_1} (ε := A) (fun (x : ℝ) ↦ u' x * v x + u x * v' x) volume a b
⊢ ∫ (x : ℝ) in a..b, u' x * v x + u x * v' x = u b * v b - u a * v a

Tactic:
apply integral_eq_sub_of_hasDeriv_right (hu.mul hv) fun x hx ↦ (huu' x hx).mul (hvv' x hx)

Premises used: HasDerivWithinAt.mul, intervalIntegral.integral_eq_sub_of_hasDeriv_right, ContinuousOn.mul
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.IntegrationByParts
Goal:
a b : ℝ
A : Type u_1
inst : NormedRing A
inst_1 : NormedAlgebra ℝ A
inst_2 : CompleteSpace A
u v u' v' : ℝ → A
hu : ContinuousOn u [[a, b]]
hv : ContinuousOn v [[a, b]]
huu' : ∀ x ∈ Ioo (min a b) (max a b), HasDerivWithinAt u (u' x) (Ioi x) x
hvv' : ∀ x ∈ Ioo (min a b) (max a b), HasDerivWithinAt v (v' x) (Ioi x) x
hu' : IntervalIntegrable u' volume a b
hv' : IntervalIntegrable v' volume a b
⊢ IntervalIntegrable.{u_1} (ε := A) (fun (x : ℝ) ↦ u' x * v x + u x * v' x) volume a b

Tactic:
(hu'.mul_continuousOn hv).add (hv'.continuousOn_mul hu)

Premises used: IntervalIntegrable.mul_continuousOn, IntervalIntegrable.continuousOn_mul, IntervalIntegrable.add
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.IntegrationByParts
Goal:
a b : ℝ
A : Type u_1
inst : NormedRing A
inst_1 : NormedAlgebra ℝ A
inst_2 : CompleteSpace A
u v u' v' : ℝ → A
hu : ContinuousOn u [[a, b]]
hv : ContinuousOn v [[a, b]]
huu' : ∀ x ∈ Ioo (min a b) (max a b), HasDerivWithinAt u (u' x) (Ioi x) x
hvv' : ∀ x ∈ Ioo (min a b) (max a b), HasDerivWithinAt v (v' x) (Ioi x) x
hu' : IntervalIntegrable u' volume a b
hv' : IntervalIntegrable v' volume a b
⊢ IntervalIntegrable.{u_1} (ε := A) (fun (x : ℝ) ↦ u' x * v x + u x * v' x) volume a b

Tactic:
exact (hu'.mul_continuousOn hv).add (hv'.continuousOn_mul hu)

Premises used: IntervalIntegrable.mul_continuousOn, IntervalIntegrable.continuousOn_mul, IntervalIntegrable.add
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.IntegrationByParts
Goal:
a b : ℝ
A : Type u_1
inst : NormedRing A
inst_1 : NormedAlgebra ℝ A
inst_2 : CompleteSpace A
u v u' v' : ℝ → A
hu : ContinuousOn u [[a, b]]
hv : ContinuousOn v [[a, b]]
huu' : ∀ x ∈ Ioo (min a b) (max a b), HasDerivAt u (u' x) x
hvv' : ∀ x ∈ Ioo (min a b) (max a b), HasDerivAt v (v' x) x
hu' : IntervalIntegrable u' volume a b
hv' : IntervalIntegrable v' volume a b
⊢ ∫ (x : ℝ) in a..b, u' x * v x + u x * v' x = u b * v b - u a * v a

Tactic:
integral_deriv_mul_eq_sub_of_hasDeriv_right hu hv
    (fun x hx ↦ huu' x hx |>.hasDerivWithinAt) (fun x hx ↦ hvv' x hx |>.hasDerivWithinAt) hu' hv'

Premises used: HasDerivAt.hasDerivWithinAt, intervalIntegral.integral_deriv_mul_eq_sub_of_hasDeriv_right
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.IntegrationByParts
Goal:
a b : ℝ
A : Type u_1
inst : NormedRing A
inst_1 : NormedAlgebra ℝ A
inst_2 : CompleteSpace A
u v u' v' : ℝ → A
hu : ∀ x ∈ [[a, b]], HasDerivWithinAt u (u' x) [[a, b]] x
hv : ∀ x ∈ [[a, b]], HasDerivWithinAt v (v' x) [[a, b]] x
hu' : IntervalIntegrable u' volume a b
hv' : IntervalIntegrable v' volume a b
⊢ ∫ (x : ℝ) in a..b, u' x * v x + u x * v' x = u b * v b - u a * v a

Tactic:
integral_deriv_mul_eq_sub_of_hasDerivAt
    (fun x hx ↦ (hu x hx).continuousWithinAt)
    (fun x hx ↦ (hv x hx).continuousWithinAt)
    (fun x hx ↦ hu x (mem_Icc_of_Ioo hx) |>.hasDerivAt (Icc_mem_nhds hx.1 hx.2))
    (fun x hx ↦ hv x (mem_Icc_of_Ioo hx) |>.hasDerivAt (Icc_mem_nhds hx.1 hx.2))
    hu' hv'

Premises used: intervalIntegral.integral_deriv_mul_eq_sub_of_hasDerivAt, Set.mem_Icc_of_Ioo, And.right, And.left, HasDerivWithinAt.hasDerivAt, HasDerivWithinAt.continuousWithinAt, Icc_mem_nhds
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.IntegrationByParts
Goal:
a b : ℝ
A : Type u_1
inst : NormedRing A
inst_1 : NormedAlgebra ℝ A
inst_2 : CompleteSpace A
u v u' v' : ℝ → A
hu : ∀ x ∈ [[a, b]], HasDerivAt u (u' x) x
hv : ∀ x ∈ [[a, b]], HasDerivAt v (v' x) x
hu' : IntervalIntegrable u' volume a b
hv' : IntervalIntegrable v' volume a b
⊢ ∫ (x : ℝ) in a..b, u' x * v x + u x * v' x = u b * v b - u a * v a

Tactic:
integral_deriv_mul_eq_sub_of_hasDerivWithinAt
    (fun x hx ↦ hu x hx |>.hasDerivWithinAt) (fun x hx ↦ hv x hx |>.hasDerivWithinAt) hu' hv'

Premises used: HasDerivAt.hasDerivWithinAt, intervalIntegral.integral_deriv_mul_eq_sub_of_hasDerivWithinAt
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.IntegrationByParts
Goal:
a b : ℝ
A : Type u_1
inst : NormedRing A
inst_1 : NormedAlgebra ℝ A
inst_2 : CompleteSpace A
u v u' v' : ℝ → A
hu : ContinuousOn u [[a, b]]
hv : ContinuousOn v [[a, b]]
huu' : ∀ x ∈ Ioo (min a b) (max a b), HasDerivWithinAt u (u' x) (Ioi x) x
hvv' : ∀ x ∈ Ioo (min a b) (max a b), HasDerivWithinAt v (v' x) (Ioi x) x
hu' : IntervalIntegrable u' volume a b
hv' : IntervalIntegrable v' volume a b
rw : Eq.{u_1 + 1} (α := A) (∫ (x : ℝ) in a..b, u x * v' x) (∫ (x : ℝ) in a..b, u' x * v x + u x * v' x - u' x * v x)
hf : IntervalIntegrable.{u_1} (ε := A) (fun (x : ℝ) ↦ u' x * v x + u x * v' x) volume a b
hg : IntervalIntegrable.{u_1} (ε := A) (fun (x : ℝ) ↦ u' x * v x) volume a b
⊢ ∫ (x : ℝ) in a..b, u x * v' x = u b * v b - u a * v a - ∫ (x : ℝ) in a..b, u' x * v x

Tactic:
rw [← integral_deriv_mul_eq_sub_of_hasDeriv_right hu hv huu' hvv' hu' hv', ← integral_sub]

Premises used: intervalIntegral.integral_sub, intervalIntegral.integral_deriv_mul_eq_sub_of_hasDeriv_right
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.IntegrationByParts
Goal:
a b : ℝ
A : Type u_1
inst : NormedRing A
inst_1 : NormedAlgebra ℝ A
inst_2 : CompleteSpace A
u v u' v' : ℝ → A
hu : ContinuousOn u [[a, b]]
hv : ContinuousOn v [[a, b]]
huu' : ∀ x ∈ Ioo (min a b) (max a b), HasDerivWithinAt u (u' x) (Ioi x) x
hvv' : ∀ x ∈ Ioo (min a b) (max a b), HasDerivWithinAt v (v' x) (Ioi x) x
hu' : IntervalIntegrable u' volume a b
hv' : IntervalIntegrable v' volume a b
⊢ Eq.{u_1 + 1} (α := A) (∫ (x : ℝ) in a..b, u x * v' x) (∫ (x : ℝ) in a..b, u' x * v x + u x * v' x - u' x * v x)

Tactic:
simp_rw [add_sub_cancel_left]

Premises used: add_sub_cancel_left
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.IntegrationByParts
Goal:
a b : ℝ
A : Type u_1
inst : NormedRing A
inst_1 : NormedAlgebra ℝ A
inst_2 : CompleteSpace A
u v u' v' : ℝ → A
hu : ContinuousOn u [[a, b]]
hv : ContinuousOn v [[a, b]]
huu' : ∀ x ∈ Ioo (min a b) (max a b), HasDerivWithinAt u (u' x) (Ioi x) x
hvv' : ∀ x ∈ Ioo (min a b) (max a b), HasDerivWithinAt v (v' x) (Ioi x) x
hu' : IntervalIntegrable u' volume a b
hv' : IntervalIntegrable v' volume a b
⊢ IntervalIntegrable.{u_1} (ε := A) (fun (x : ℝ) ↦ u' x * v x) volume a b

Tactic:
hu'.mul_continuousOn hv

Premises used: IntervalIntegrable.mul_continuousOn
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.IntegrationByParts
Goal:
a b : ℝ
A : Type u_1
inst : NormedRing A
inst_1 : NormedAlgebra ℝ A
inst_2 : CompleteSpace A
u v u' v' : ℝ → A
hu : ContinuousOn u [[a, b]]
hv : ContinuousOn v [[a, b]]
huu' : ∀ x ∈ Ioo (min a b) (max a b), HasDerivWithinAt u (u' x) (Ioi x) x
hvv' : ∀ x ∈ Ioo (min a b) (max a b), HasDerivWithinAt v (v' x) (Ioi x) x
hu' : IntervalIntegrable u' volume a b
hv' : IntervalIntegrable v' volume a b
⊢ IntervalIntegrable.{u_1} (ε := A) (fun (x : ℝ) ↦ u' x * v x) volume a b

Tactic:
exact hu'.mul_continuousOn hv

Premises used: IntervalIntegrable.mul_continuousOn
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.IntegrationByParts
Goal:
a b : ℝ
A : Type u_1
inst : NormedRing A
inst_1 : NormedAlgebra ℝ A
inst_2 : CompleteSpace A
u v u' v' : ℝ → A
hu : ContinuousOn u [[a, b]]
hv : ContinuousOn v [[a, b]]
huu' : ∀ x ∈ Ioo (min a b) (max a b), HasDerivAt u (u' x) x
hvv' : ∀ x ∈ Ioo (min a b) (max a b), HasDerivAt v (v' x) x
hu' : IntervalIntegrable u' volume a b
hv' : IntervalIntegrable v' volume a b
⊢ ∫ (x : ℝ) in a..b, u x * v' x = u b * v b - u a * v a - ∫ (x : ℝ) in a..b, u' x * v x

Tactic:
integral_mul_deriv_eq_deriv_mul_of_hasDeriv_right hu hv
        (fun x hx ↦ (huu' x hx).hasDerivWithinAt) (fun x hx ↦ (hvv' x hx).hasDerivWithinAt) hu' hv'

Premises used: HasDerivAt.hasDerivWithinAt, intervalIntegral.integral_mul_deriv_eq_deriv_mul_of_hasDeriv_right
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.IntegrationByParts
Goal:
a b : ℝ
A : Type u_1
inst : NormedRing A
inst_1 : NormedAlgebra ℝ A
inst_2 : CompleteSpace A
u v u' v' : ℝ → A
hu : ∀ x ∈ [[a, b]], HasDerivWithinAt u (u' x) [[a, b]] x
hv : ∀ x ∈ [[a, b]], HasDerivWithinAt v (v' x) [[a, b]] x
hu' : IntervalIntegrable u' volume a b
hv' : IntervalIntegrable v' volume a b
⊢ ∫ (x : ℝ) in a..b, u x * v' x = u b * v b - u a * v a - ∫ (x : ℝ) in a..b, u' x * v x

Tactic:
integral_mul_deriv_eq_deriv_mul_of_hasDerivAt
    (fun x hx ↦ (hu x hx).continuousWithinAt)
    (fun x hx ↦ (hv x hx).continuousWithinAt)
    (fun x hx ↦ hu x (mem_Icc_of_Ioo hx) |>.hasDerivAt (Icc_mem_nhds hx.1 hx.2))
    (fun x hx ↦ hv x (mem_Icc_of_Ioo hx) |>.hasDerivAt (Icc_mem_nhds hx.1 hx.2))
    hu' hv'

Premises used: Set.mem_Icc_of_Ioo, And.right, And.left, intervalIntegral.integral_mul_deriv_eq_deriv_mul_of_hasDerivAt, HasDerivWithinAt.hasDerivAt, HasDerivWithinAt.continuousWithinAt, Icc_mem_nhds
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.IntegrationByParts
Goal:
a b : ℝ
A : Type u_1
inst : NormedRing A
inst_1 : NormedAlgebra ℝ A
inst_2 : CompleteSpace A
u v u' v' : ℝ → A
hu : ∀ x ∈ [[a, b]], HasDerivAt u (u' x) x
hv : ∀ x ∈ [[a, b]], HasDerivAt v (v' x) x
hu' : IntervalIntegrable u' volume a b
hv' : IntervalIntegrable v' volume a b
⊢ ∫ (x : ℝ) in a..b, u x * v' x = u b * v b - u a * v a - ∫ (x : ℝ) in a..b, u' x * v x

Tactic:
integral_mul_deriv_eq_deriv_mul_of_hasDerivWithinAt
    (fun x hx ↦ (hu x hx).hasDerivWithinAt) (fun x hx ↦ (hv x hx).hasDerivWithinAt) hu' hv'

Premises used: HasDerivAt.hasDerivWithinAt, intervalIntegral.integral_mul_deriv_eq_deriv_mul_of_hasDerivWithinAt
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.IntegrationByParts
Goal:
a b : ℝ
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAlgebra ℝ 𝕜
E : Type u_2
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
inst_4 : NormedSpace ℝ E
inst_5 : CompleteSpace E
inst_6 : IsScalarTower ℝ 𝕜 E
u u' : ℝ → 𝕜
v v' : ℝ → E
hu : ContinuousOn u [[a, b]]
hv : ContinuousOn v [[a, b]]
huu' : ∀ x ∈ Ioo (min a b) (max a b), HasDerivWithinAt u (u' x) (Ioi x) x
hvv' : ∀ x ∈ Ioo (min a b) (max a b), HasDerivWithinAt v (v' x) (Ioi x) x
hu' : IntervalIntegrable u' volume a b
hv' : IntervalIntegrable v' volume a b
simp_rw : ∫ (x : ℝ) in a..b, u x • v' x + u' x • v x = u b • v b - u a • v a
⊢ ∫ (x : ℝ) in a..b, u' x • v x + u x • v' x = u b • v b - u a • v a

Tactic:
simp_rw [add_comm]

Premises used: add_comm
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.IntegrationByParts
Goal:
a b : ℝ
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAlgebra ℝ 𝕜
E : Type u_2
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
inst_4 : NormedSpace ℝ E
inst_5 : CompleteSpace E
inst_6 : IsScalarTower ℝ 𝕜 E
u u' : ℝ → 𝕜
v v' : ℝ → E
hu : ContinuousOn u [[a, b]]
hv : ContinuousOn v [[a, b]]
huu' : ∀ x ∈ Ioo (min a b) (max a b), HasDerivWithinAt u (u' x) (Ioi x) x
hvv' : ∀ x ∈ Ioo (min a b) (max a b), HasDerivWithinAt v (v' x) (Ioi x) x
hu' : IntervalIntegrable u' volume a b
hv' : IntervalIntegrable v' volume a b
apply : IntervalIntegrable.{u_2} (ε := E) (fun (x : ℝ) ↦ u x • v' x + u' x • v x) volume a b
⊢ ∫ (x : ℝ) in a..b, u x • v' x + u' x • v x = u b • v b - u a • v a

Tactic:
apply integral_eq_sub_of_hasDeriv_right (hu.smul hv) fun x hx ↦ (huu' x hx).smul (hvv' x hx)

Premises used: intervalIntegral.integral_eq_sub_of_hasDeriv_right, HasDerivWithinAt.smul, ContinuousOn.smul