awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
Goal:
E : Type u_5
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
μ : Measure ℝ
h : ¬a ≤ b
⊢ ∫ (x : ℝ) in a..b, f x ∂μ = HSMul.hSMul (α := ℝ) (β := E) (-1) (∫ (x : ℝ) in Ι a b, f x ∂μ)

Tactic:
simp only [integral_of_ge (not_le.1 h).le, uIoc_of_ge (not_le.1 h).le, neg_one_smul]

Premises used: not_le, neg_one_smul, LT.lt.le, intervalIntegral.integral_of_ge, Iff.mp, Set.uIoc_of_ge
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
Goal:
E : Type u_5
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
μ : Measure ℝ
simp_rw :
  norm (E := ℝ) (if a ≤ b then 1 else -1) * norm.{u_5} (E := E) (∫ (x : ℝ) in Ι a b, f x ∂μ) =
    norm.{u_5} (E := E) (∫ (x : ℝ) in Ι a b, f x ∂μ)
⊢ norm.{u_5} (E := E) (∫ (x : ℝ) in a..b, f x ∂μ) = norm.{u_5} (E := E) (∫ (x : ℝ) in Ι a b, f x ∂μ)

Tactic:
simp_rw [intervalIntegral_eq_integral_uIoc, norm_smul]

Premises used: intervalIntegral.intervalIntegral_eq_integral_uIoc, norm_smul
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
Goal:
E : Type u_5
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
μ : Measure ℝ
pos :
  a ≤ b →
    norm (E := ℝ) 1 * norm.{u_5} (E := E) (∫ (x : ℝ) in Ι a b, f x ∂μ) =
      norm.{u_5} (E := E) (∫ (x : ℝ) in Ι a b, f x ∂μ)
neg :
  ¬a ≤ b →
    norm (E := ℝ) (-1) * norm.{u_5} (E := E) (∫ (x : ℝ) in Ι a b, f x ∂μ) =
      norm.{u_5} (E := E) (∫ (x : ℝ) in Ι a b, f x ∂μ)
⊢ norm (E := ℝ) (if a ≤ b then 1 else -1) * norm.{u_5} (E := E) (∫ (x : ℝ) in Ι a b, f x ∂μ) =
    norm.{u_5} (E := E) (∫ (x : ℝ) in Ι a b, f x ∂μ)

Tactic:
split_ifs
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
Goal:
E : Type u_5
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
μ : Measure ℝ
h : a ≤ b
⊢ norm (E := ℝ) 1 * norm.{u_5} (E := E) (∫ (x : ℝ) in Ι a b, f x ∂μ) = norm.{u_5} (E := E) (∫ (x : ℝ) in Ι a b, f x ∂μ)

Tactic:
simp only [norm_neg, norm_one, one_mul]

Premises used: NormOneClass.norm_one, norm_neg, one_mul
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
Goal:
E : Type u_5
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
μ : Measure ℝ
h : ¬a ≤ b
⊢ norm (E := ℝ) (-1) * norm.{u_5} (E := E) (∫ (x : ℝ) in Ι a b, f x ∂μ) =
    norm.{u_5} (E := E) (∫ (x : ℝ) in Ι a b, f x ∂μ)

Tactic:
simp only [norm_neg, norm_one, one_mul]

Premises used: NormOneClass.norm_one, norm_neg, one_mul
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
Goal:
f : ℝ → ℝ
a b : ℝ
μ : Measure ℝ
⊢ Eq (α := ℝ) |∫ (x : ℝ) in a..b, f x ∂μ| |∫ (x : ℝ) in Ι a b, f x ∂μ|

Tactic:
norm_intervalIntegral_eq f a b μ

Premises used: intervalIntegral.norm_intervalIntegral_eq
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
Goal:
E : Type u_5
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
μ : Measure ℝ
f : ℝ → E
a b : ℝ
rw :
  Membership.mem (γ := Set E) {∫ (x : ℝ) in Ι a b, f x ∂μ, -∫ (x : ℝ) in Ι a b, f x ∂μ}
    (HSMul.hSMul (α := ℝ) (β := E) (if a ≤ b then 1 else -1) (∫ (x : ℝ) in Ι a b, f x ∂μ))
⊢ Membership.mem (γ := Set E) {∫ (x : ℝ) in Ι a b, f x ∂μ, -∫ (x : ℝ) in Ι a b, f x ∂μ} (∫ (x : ℝ) in a..b, f x ∂μ)

Tactic:
rw [intervalIntegral_eq_integral_uIoc]

Premises used: intervalIntegral.intervalIntegral_eq_integral_uIoc
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
Goal:
E : Type u_5
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
μ : Measure ℝ
f : ℝ → E
a b : ℝ
pos :
  a ≤ b →
    Membership.mem (γ := Set E) {∫ (x : ℝ) in Ι a b, f x ∂μ, -∫ (x : ℝ) in Ι a b, f x ∂μ}
      (HSMul.hSMul (α := ℝ) (β := E) 1 (∫ (x : ℝ) in Ι a b, f x ∂μ))
neg :
  ¬a ≤ b →
    Membership.mem (γ := Set E) {∫ (x : ℝ) in Ι a b, f x ∂μ, -∫ (x : ℝ) in Ι a b, f x ∂μ}
      (HSMul.hSMul (α := ℝ) (β := E) (-1) (∫ (x : ℝ) in Ι a b, f x ∂μ))
⊢ Membership.mem (γ := Set E) {∫ (x : ℝ) in Ι a b, f x ∂μ, -∫ (x : ℝ) in Ι a b, f x ∂μ}
    (HSMul.hSMul (α := ℝ) (β := E) (if a ≤ b then 1 else -1) (∫ (x : ℝ) in Ι a b, f x ∂μ))

Tactic:
split_ifs
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
Goal:
E : Type u_5
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
μ : Measure ℝ
f : ℝ → E
a b : ℝ
h : a ≤ b
⊢ Membership.mem (γ := Set E) {∫ (x : ℝ) in Ι a b, f x ∂μ, -∫ (x : ℝ) in Ι a b, f x ∂μ}
    (HSMul.hSMul (α := ℝ) (β := E) 1 (∫ (x : ℝ) in Ι a b, f x ∂μ))

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
Goal:
E : Type u_5
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
μ : Measure ℝ
f : ℝ → E
a b : ℝ
h : ¬a ≤ b
⊢ Membership.mem (γ := Set E) {∫ (x : ℝ) in Ι a b, f x ∂μ, -∫ (x : ℝ) in Ι a b, f x ∂μ}
    (HSMul.hSMul (α := ℝ) (β := E) (-1) (∫ (x : ℝ) in Ι a b, f x ∂μ))

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
Goal:
E : Type u_5
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
a b : ℝ
f : ℝ → E
μ : Measure ℝ
h : ¬IntervalIntegrable f μ a b
⊢ ¬IntegrableOn f (Ι a b) μ

Tactic:
rw [intervalIntegrable_iff] at h

Premises used: intervalIntegrable_iff
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
Goal:
E : Type u_5
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
a b : ℝ
f : ℝ → E
μ : Measure ℝ
h : ¬IntegrableOn f (Ι a b) μ
rw : HSMul.hSMul (α := ℝ) (β := E) (if a ≤ b then 1 else -1) (∫ (x : ℝ) in Ι a b, f x ∂μ) = 0
rw₁ : HSMul.hSMul (α := ℝ) (β := E) (if a ≤ b then 1 else -1) 0 = 0
rw₂ rw₃ : Eq.{u_5 + 1} (α := E) 0 0
⊢ Eq.{u_5 + 1} (α := E) (∫ (x : ℝ) in a..b, f x ∂μ) 0

Tactic:
rw [intervalIntegral_eq_integral_uIoc, integral_undef h, smul_zero]

Premises used: intervalIntegral.intervalIntegral_eq_integral_uIoc, smul_zero
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
Goal:
E : Type u_5
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
a b : ℝ
f : ℝ → E
μ : Measure ℝ
h : Ne.{u_5 + 1} (α := E) (∫ (x : ℝ) in a..b, f x ∂μ) 0
⊢ IntervalIntegrable f μ a b

Tactic:
not_imp_comm.1 integral_undef h

Premises used: not_imp_comm, Iff.mp, intervalIntegral.integral_undef
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
Goal:
E : Type u_5
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
a b : ℝ
f : ℝ → E
μ : Measure ℝ
hf : ¬AEStronglyMeasurable f (μ.restrict (Ι a b))
rw : HSMul.hSMul (α := ℝ) (β := E) (if a ≤ b then 1 else -1) (∫ (x : ℝ) in Ι a b, f x ∂μ) = 0
rw₁ : HSMul.hSMul (α := ℝ) (β := E) (if a ≤ b then 1 else -1) 0 = 0
rw₂ rw₃ : Eq.{u_5 + 1} (α := E) 0 0
⊢ Eq.{u_5 + 1} (α := E) (∫ (x : ℝ) in a..b, f x ∂μ) 0

Tactic:
rw [intervalIntegral_eq_integral_uIoc, integral_non_aestronglyMeasurable hf, smul_zero]

Premises used: intervalIntegral.intervalIntegral_eq_integral_uIoc, smul_zero, intervalIntegral.integral_non_aestronglyMeasurable
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
Goal:
E : Type u_5
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
a b : ℝ
f : ℝ → E
μ : Measure ℝ
h : a ≤ b
hf : ¬AEStronglyMeasurable f (μ.restrict (Ioc a b))
rwa rwa₁ rwa₂ rwa₃ : ¬AEStronglyMeasurable f (μ.restrict (Ioc a b))
⊢ ¬AEStronglyMeasurable f (μ.restrict (Ι a b))

Tactic:
rwa [uIoc_of_le h]

Premises used: Set.uIoc_of_le
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
Goal:
E : Type u_5
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
a b : ℝ
μ : Measure ℝ
f : ℝ → E
inl :
  a ≤ b → norm.{u_5} (E := E) (∫ (x : ℝ) in min a b..max a b, f x ∂μ) = norm.{u_5} (E := E) (∫ (x : ℝ) in a..b, f x ∂μ)
inr :
  b ≤ a → norm.{u_5} (E := E) (∫ (x : ℝ) in min a b..max a b, f x ∂μ) = norm.{u_5} (E := E) (∫ (x : ℝ) in a..b, f x ∂μ)
⊢ norm.{u_5} (E := E) (∫ (x : ℝ) in min a b..max a b, f x ∂μ) = norm.{u_5} (E := E) (∫ (x : ℝ) in a..b, f x ∂μ)

Tactic:
cases le_total a b

Premises used: le_total
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
Goal:
E : Type u_5
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
a b : ℝ
μ : Measure ℝ
f : ℝ → E
h : a ≤ b
⊢ norm.{u_5} (E := E) (∫ (x : ℝ) in min a b..max a b, f x ∂μ) = norm.{u_5} (E := E) (∫ (x : ℝ) in a..b, f x ∂μ)

Tactic:
simp [*, integral_symm a b]

Premises used: intervalIntegral.integral_symm
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
Goal:
E : Type u_5
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
a b : ℝ
μ : Measure ℝ
f : ℝ → E
h : b ≤ a
⊢ norm.{u_5} (E := E) (∫ (x : ℝ) in min a b..max a b, f x ∂μ) = norm.{u_5} (E := E) (∫ (x : ℝ) in a..b, f x ∂μ)

Tactic:
simp [*, integral_symm a b]

Premises used: intervalIntegral.integral_symm
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
Goal:
E : Type u_5
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
a b : ℝ
μ : Measure ℝ
f : ℝ → E
rw : norm.{u_5} (E := E) (∫ (x : ℝ) in min a b..max a b, f x ∂μ) = norm.{u_5} (E := E) (∫ (x : ℝ) in Ι a b, f x ∂μ)
rw₁ :
  norm.{u_5} (E := E) (∫ (x : ℝ) in Ioc (min a b) (max a b), f x ∂μ) = norm.{u_5} (E := E) (∫ (x : ℝ) in Ι a b, f x ∂μ)
rw₂ rw₃ :
  norm.{u_5} (E := E) (∫ (x : ℝ) in Ioc (min a b) (max a b), f x ∂μ) =
    norm.{u_5} (E := E) (∫ (x : ℝ) in Ioc (min a b) (max a b), f x ∂μ)
⊢ norm.{u_5} (E := E) (∫ (x : ℝ) in a..b, f x ∂μ) = norm.{u_5} (E := E) (∫ (x : ℝ) in Ι a b, f x ∂μ)

Tactic:
rw [← norm_integral_min_max, integral_of_le min_le_max, uIoc]

Premises used: min_le_max, Set.uIoc, intervalIntegral.integral_of_le, intervalIntegral.norm_integral_min_max
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
Goal:
a b : ℝ
μ : Measure ℝ
f : ℝ → ℝ
⊢ Eq (α := ℝ) |∫ (x : ℝ) in a..b, f x ∂μ| |∫ (x : ℝ) in Ι a b, f x ∂μ|

Tactic:
norm_integral_eq_norm_integral_uIoc f

Premises used: intervalIntegral.norm_integral_eq_norm_integral_uIoc
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
Goal:
E : Type u_5
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
a b : ℝ
f : ℝ → E
μ : Measure ℝ
⊢ norm.{u_5} (E := E) (∫ (x : ℝ) in a..b, f x ∂μ) ≤ ∫ (x : ℝ) in Ι a b, ‖f x‖ ∂μ

Tactic:
calc
    ‖∫ x in a..b, f x ∂μ‖ = ‖∫ x in Ι a b, f x ∂μ‖ := norm_integral_eq_norm_integral_uIoc f
    _ ≤ ∫ x in Ι a b, ‖f x‖ ∂μ := norm_integral_le_integral_norm f

Premises used: Trans.trans, MeasureTheory.norm_integral_le_integral_norm, intervalIntegral.norm_integral_eq_norm_integral_uIoc
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
Goal:
E : Type u_5
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
a b : ℝ
f : ℝ → E
μ : Measure ℝ
simp : norm.{u_5} (E := E) (∫ (x : ℝ) in Ι a b, f x ∂μ) ≤ norm (E := ℝ) (∫ (x : ℝ) in Ι a b, ‖f x‖ ∂μ)
⊢ norm.{u_5} (E := E) (∫ (x : ℝ) in a..b, f x ∂μ) ≤ |∫ (x : ℝ) in a..b, ‖f x‖ ∂μ|

Tactic:
simp only [← Real.norm_eq_abs, norm_integral_eq_norm_integral_uIoc]

Premises used: intervalIntegral.norm_integral_eq_norm_integral_uIoc, Real.norm_eq_abs
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
Goal:
E : Type u_5
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
a b : ℝ
f : ℝ → E
μ : Measure ℝ
⊢ norm.{u_5} (E := E) (∫ (x : ℝ) in Ι a b, f x ∂μ) ≤ norm (E := ℝ) (∫ (x : ℝ) in Ι a b, ‖f x‖ ∂μ)

Tactic:
le_trans (norm_integral_le_integral_norm _) (le_abs_self _)

Premises used: le_abs_self, MeasureTheory.norm_integral_le_integral_norm, le_trans
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
Goal:
E : Type u_5
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
a b : ℝ
f : ℝ → E
μ : Measure ℝ
⊢ norm.{u_5} (E := E) (∫ (x : ℝ) in Ι a b, f x ∂μ) ≤ norm (E := ℝ) (∫ (x : ℝ) in Ι a b, ‖f x‖ ∂μ)

Tactic:
exact le_trans (norm_integral_le_integral_norm _) (le_abs_self _)

Premises used: le_abs_self, MeasureTheory.norm_integral_le_integral_norm, le_trans
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
Goal:
E : Type u_5
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
a b : ℝ
f : ℝ → E
μ : Measure ℝ
h : a ≤ b
rw : Eq (α := ℝ) (∫ (x : ℝ) in Ioc a b, ‖f x‖ ∂μ) (∫ (x : ℝ) in a..b, ‖f x‖ ∂μ)
rw₁ rw₂ : Eq (α := ℝ) (∫ (x : ℝ) in Ioc a b, ‖f x‖ ∂μ) (∫ (x : ℝ) in Ioc a b, ‖f x‖ ∂μ)
⊢ Eq (α := ℝ) (∫ (x : ℝ) in Ι a b, ‖f x‖ ∂μ) (∫ (x : ℝ) in a..b, ‖f x‖ ∂μ)

Tactic:
rw [uIoc_of_le h, integral_of_le h]

Premises used: intervalIntegral.integral_of_le, Set.uIoc_of_le
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
Goal:
E : Type u_5
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
a b : ℝ
f : ℝ → E
μ : Measure ℝ
g : ℝ → ℝ
h : ∀ᵐ (t : ℝ) ∂μ.restrict (Ι a b), ‖f t‖ ≤ g t
hbound : IntervalIntegrable g μ a b
rw : norm.{u_5} (E := E) (∫ (x : ℝ) in Ι a b, f x ∂μ) ≤ |∫ (x : ℝ) in Ι a b, g x ∂μ|
⊢ norm.{u_5} (E := E) (∫ (t : ℝ) in a..b, f t ∂μ) ≤ |∫ (t : ℝ) in a..b, g t ∂μ|

Tactic:
rw [norm_intervalIntegral_eq, abs_intervalIntegral_eq]

Premises used: intervalIntegral.abs_intervalIntegral_eq, intervalIntegral.norm_intervalIntegral_eq
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
Goal:
E : Type u_5
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
a b : ℝ
f : ℝ → E
μ : Measure ℝ
g : ℝ → ℝ
h : ∀ᵐ (t : ℝ) ∂μ.restrict (Ι a b), ‖f t‖ ≤ g t
hbound : IntervalIntegrable g μ a b
⊢ norm.{u_5} (E := E) (∫ (x : ℝ) in Ι a b, f x ∂μ) ≤ |∫ (x : ℝ) in Ι a b, g x ∂μ|

Tactic:
(norm_integral_le_of_norm_le hbound.def' h).trans (le_abs_self _)

Premises used: le_abs_self, MeasureTheory.norm_integral_le_of_norm_le, IntervalIntegrable.def', LE.le.trans
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
Goal:
E : Type u_5
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
a b : ℝ
f : ℝ → E
μ : Measure ℝ
g : ℝ → ℝ
h : ∀ᵐ (t : ℝ) ∂μ.restrict (Ι a b), ‖f t‖ ≤ g t
hbound : IntervalIntegrable g μ a b
⊢ norm.{u_5} (E := E) (∫ (x : ℝ) in Ι a b, f x ∂μ) ≤ |∫ (x : ℝ) in Ι a b, g x ∂μ|

Tactic:
exact (norm_integral_le_of_norm_le hbound.def' h).trans (le_abs_self _)

Premises used: le_abs_self, MeasureTheory.norm_integral_le_of_norm_le, IntervalIntegrable.def', LE.le.trans
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
Goal:
E : Type u_5
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
a b : ℝ
f : ℝ → E
μ : Measure ℝ
g : ℝ → ℝ
hab : a ≤ b
h : ∀ᵐ (t : ℝ) ∂μ, t ∈ Ioc a b → ‖f t‖ ≤ g t
hbound : IntervalIntegrable g μ a b
simp :
  ∀ (h : ∀ᵐ (x : ℝ) ∂μ.restrict (Ioc a b), ‖f x‖ ≤ g x),
    norm.{u_5} (E := E) (∫ (t : ℝ) in Ioc a b, f t ∂μ) ≤ ∫ (t : ℝ) in Ioc a b, g t ∂μ
⊢ norm.{u_5} (E := E) (∫ (t : ℝ) in a..b, f t ∂μ) ≤ ∫ (t : ℝ) in a..b, g t ∂μ

Tactic:
simp only [integral_of_le hab, ← ae_restrict_iff' measurableSet_Ioc] at *

Premises used: intervalIntegral.integral_of_le, MeasureTheory.ae_restrict_iff', measurableSet_Ioc
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
Goal:
E : Type u_5
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
a b : ℝ
f : ℝ → E
μ : Measure ℝ
g : ℝ → ℝ
hab : a ≤ b
hbound : IntervalIntegrable g μ a b
h : ∀ᵐ (x : ℝ) ∂μ.restrict (Ioc a b), ‖f x‖ ≤ g x
⊢ norm.{u_5} (E := E) (∫ (t : ℝ) in Ioc a b, f t ∂μ) ≤ ∫ (t : ℝ) in Ioc a b, g t ∂μ

Tactic:
MeasureTheory.norm_integral_le_of_norm_le hbound.1 h

Premises used: MeasureTheory.norm_integral_le_of_norm_le, And.left
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
Goal:
E : Type u_5
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
a b : ℝ
f : ℝ → E
μ : Measure ℝ
g : ℝ → ℝ
hab : a ≤ b
hbound : IntervalIntegrable g μ a b
h : ∀ᵐ (x : ℝ) ∂μ.restrict (Ioc a b), ‖f x‖ ≤ g x
⊢ norm.{u_5} (E := E) (∫ (t : ℝ) in Ioc a b, f t ∂μ) ≤ ∫ (t : ℝ) in Ioc a b, g t ∂μ

Tactic:
exact MeasureTheory.norm_integral_le_of_norm_le hbound.1 h

Premises used: MeasureTheory.norm_integral_le_of_norm_le, And.left
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
Goal:
E : Type u_5
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
a b C : ℝ
f : ℝ → E
h : ∀ᵐ (x : ℝ), x ∈ Ι a b → ‖f x‖ ≤ C
rw :
  norm.{u_5} (E := E) (@integral _ _ _ _ Real.measurableSpace (Measure.restrict volume (Ι a b)) fun (x : ℝ) ↦ f x) ≤
    C * |b - a|
⊢ norm.{u_5} (E := E) (∫ (x : ℝ) in a..b, f x) ≤ C * |b - a|

Tactic:
rw [norm_integral_eq_norm_integral_uIoc]

Premises used: intervalIntegral.norm_integral_eq_norm_integral_uIoc
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
Goal:
E : Type u_5
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
a b C : ℝ
f : ℝ → E
h : ∀ᵐ (x : ℝ), x ∈ Ι a b → ‖f x‖ ≤ C
⊢ norm.{u_5} (E := E)
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ι a b)) fun (x : ℝ) ↦ f x) ≤
    C * Measure.real (m := MeasureSpace.toMeasurableSpace) volume (Ι a b)

Tactic:
norm_setIntegral_le_of_norm_le_const_ae' _ h

Premises used: MeasureTheory.norm_setIntegral_le_of_norm_le_const_ae'
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
Goal:
E : Type u_5
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
a b C : ℝ
f : ℝ → E
h : ∀ᵐ (x : ℝ), x ∈ Ι a b → ‖f x‖ ≤ C
h₁ : C * |b - a| = C * Measure.real (m := MeasureSpace.toMeasurableSpace) volume (Ι a b)
convert! : LT.lt (α := ℝ≥0∞) ((volume : (a : Set ℝ) → ℝ≥0∞) (Ι a b) : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ norm.{u_5} (E := E) (@integral _ _ _ _ Real.measurableSpace (Measure.restrict volume (Ι a b)) fun (x : ℝ) ↦ f x) ≤
    C * |b - a|

Tactic:
convert! norm_setIntegral_le_of_norm_le_const_ae' _ h using 1

Premises used: MeasureTheory.norm_setIntegral_le_of_norm_le_const_ae'
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
Goal:
E : Type u_5
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
a b C : ℝ
f : ℝ → E
h : ∀ᵐ (x : ℝ), x ∈ Ι a b → ‖f x‖ ≤ C
h₁ : C * |b - a| = C * Measure.real (m := MeasureSpace.toMeasurableSpace) volume (Ioc (min a b) (max a b))
h₂ : C * |b - a| = C * (max a b - min a b)
h₃ h₄ : C * |b - a| = C * |b - a|
⊢ C * |b - a| = C * Measure.real (m := MeasureSpace.toMeasurableSpace) volume (Ι a b)

Tactic:
rw [uIoc, Real.volume_real_Ioc_of_le inf_le_sup, max_sub_min_eq_abs]

Premises used: Set.uIoc, Real.volume_real_Ioc_of_le, inf_le_sup, max_sub_min_eq_abs
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
Goal:
E : Type u_5
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
a b C : ℝ
f : ℝ → E
h : ∀ᵐ (x : ℝ), x ∈ Ι a b → ‖f x‖ ≤ C
⊢ LT.lt (α := ℝ≥0∞) ((volume : (a : Set ℝ) → ℝ≥0∞) (Ι a b) : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
simp [uIoc, Real.volume_Ioc]

Premises used: Set.uIoc, Real.volume_Ioc
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
Goal:
E : Type u_5
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
a b C : ℝ
f : ℝ → E
h : ∀ x ∈ Ι a b, ‖f x‖ ≤ C
⊢ norm.{u_5} (E := E) (∫ (x : ℝ) in a..b, f x) ≤ C * |b - a|

Tactic:
norm_integral_le_of_norm_le_const_ae <| Eventually.of_forall h

Premises used: Filter.Eventually.of_forall, intervalIntegral.norm_integral_le_of_norm_le_const_ae
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
Goal:
E : Type u_5
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
a b : ℝ
f g : ℝ → E
μ : Measure ℝ
hf : IntervalIntegrable f μ a b
hg : IntervalIntegrable g μ a b
⊢ ∫ (x : ℝ) in a..b, f x + g x ∂μ = HAdd.hAdd (α := E) (∫ (x : ℝ) in a..b, f x ∂μ) (∫ (x : ℝ) in a..b, g x ∂μ)

Tactic:
simp only [intervalIntegral_eq_integral_uIoc, integral_add hf.def' hg.def', smul_add]

Premises used: intervalIntegral.intervalIntegral_eq_integral_uIoc, smul_add
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
Goal:
E : Type u_5
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
a b : ℝ
μ : Measure ℝ
ι : Type u_8
s : Finset ι
f : ι → ℝ → E
h : ∀ i ∈ s, IntervalIntegrable (f i) μ a b
⊢ Eq.{u_5 + 1} (α := E) (∫ (x : ℝ) in a..b, ∑ i ∈ s, f i x ∂μ) (∑ i ∈ s, ∫ (x : ℝ) in a..b, f i x ∂μ)

Tactic:
simp only [intervalIntegral_eq_integral_uIoc, integral_finsetSum s fun i hi => (h i hi).def',
    Finset.smul_sum]

Premises used: intervalIntegral.intervalIntegral_eq_integral_uIoc, Finset.smul_sum
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
Goal:
E : Type u_5
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
a b : ℝ
f : ℝ → E
μ : Measure ℝ
simp :
  HSub.hSub (α := E) (-∫ (a : ℝ) in Ioc a b, f a ∂μ) (-∫ (a : ℝ) in Ioc b a, f a ∂μ) =
    -HSub.hSub (α := E) (∫ (a : ℝ) in Ioc a b, f a ∂μ) (∫ (a : ℝ) in Ioc b a, f a ∂μ)
⊢ Eq.{u_5 + 1} (α := E) (∫ (x : ℝ) in a..b, -f x ∂μ) (-∫ (x : ℝ) in a..b, f x ∂μ)

Tactic:
simp only [intervalIntegral, integral_neg]

Premises used: intervalIntegral, intervalIntegral.integral_neg
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
Goal:
E : Type u_5
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
a b : ℝ
f : ℝ → E
μ : Measure ℝ
⊢ HSub.hSub (α := E) (-∫ (a : ℝ) in Ioc a b, f a ∂μ) (-∫ (a : ℝ) in Ioc b a, f a ∂μ) =
    -HSub.hSub (α := E) (∫ (a : ℝ) in Ioc a b, f a ∂μ) (∫ (a : ℝ) in Ioc b a, f a ∂μ)

Tactic:
abel
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
Goal:
E : Type u_5
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
a b : ℝ
f g : ℝ → E
μ : Measure ℝ
hf : IntervalIntegrable f μ a b
hg : IntervalIntegrable g μ a b
⊢ ∫ (x : ℝ) in a..b, f x - g x ∂μ = HSub.hSub (α := E) (∫ (x : ℝ) in a..b, f x ∂μ) (∫ (x : ℝ) in a..b, g x ∂μ)

Tactic:
simpa only [sub_eq_add_neg] using (integral_add hf hg.neg).trans (congr_arg _ integral_neg)

Premises used: IntervalIntegrable.neg, sub_eq_add_neg, congr_arg, intervalIntegral.integral_add, intervalIntegral.integral_neg, Eq.trans
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
Goal:
𝕜 : Type u_2
E : Type u_5
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
a b : ℝ
μ : Measure ℝ
inst_2 : NormedDivisionRing 𝕜
inst_3 : Module 𝕜 E
inst_4 : NormSMulClass 𝕜 E
inst_5 : SMulCommClass ℝ 𝕜 E
r : 𝕜
f : ℝ → E
⊢ ∫ (x : ℝ) in a..b, r • f x ∂μ = HSMul.hSMul (β := E) r (∫ (x : ℝ) in a..b, f x ∂μ)

Tactic:
simp only [intervalIntegral, integral_smul, smul_sub]

Premises used: intervalIntegral, intervalIntegral.integral_smul, smul_sub
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
Goal:
E : Type u_5
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
a b : ℝ
μ : Measure ℝ
R : Type u_8
inst_2 : NormedRing R
inst_3 : Module R E
inst_4 : IsBoundedSMul R E
inst_5 : SMulCommClass ℝ R E
f : ℝ → E
r : R
hf : IntervalIntegrable f μ a b
⊢ ∫ (x : ℝ) in a..b, r • f x ∂μ = HSMul.hSMul (β := E) r (∫ (x : ℝ) in a..b, f x ∂μ)

Tactic:
simp only [intervalIntegral, smul_sub, hf.1.integral_smul, hf.2.integral_smul]

Premises used: intervalIntegral, smul_sub, And.right, And.left, MeasureTheory.Integrable.integral_smul
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
Goal:
E : Type u_5
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
a b : ℝ
μ : Measure ℝ
inst_2 : CompleteSpace E
𝕜 : Type u_8
inst_3 : RCLike 𝕜
inst_4 : NormedSpace 𝕜 E
f : ℝ → 𝕜
c : E
⊢ ∫ (x : ℝ) in a..b, f x • c ∂μ = HSMul.hSMul.{u_8, u_5, u_5} (α := 𝕜) (∫ (x : ℝ) in a..b, f x ∂μ) c

Tactic:
simp only [intervalIntegral_eq_integral_uIoc, integral_smul_const, smul_assoc]

Premises used: intervalIntegral.intervalIntegral_eq_integral_uIoc, smul_assoc, intervalIntegral.integral_smul_const
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
Goal:
𝕜 : Type u_2
a b : ℝ
μ : Measure ℝ
inst : NormedDivisionRing 𝕜
inst_1 : NormedAlgebra ℝ 𝕜
r : 𝕜
f : ℝ → 𝕜
⊢ ∫ (x : ℝ) in a..b, r * f x ∂μ = r * ∫ (x : ℝ) in a..b, f x ∂μ

Tactic:
integral_smul r f

Premises used: intervalIntegral.integral_smul
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
Goal:
a b : ℝ
μ : Measure ℝ
𝕜 : Type u_8
inst : RCLike 𝕜
r : 𝕜
f : ℝ → 𝕜
⊢ ∫ (x : ℝ) in a..b, f x * r ∂μ = (∫ (x : ℝ) in a..b, f x ∂μ) * r

Tactic:
simpa only [mul_comm r] using integral_const_mul r f

Premises used: mul_comm, intervalIntegral.integral_const_mul
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
Goal:
a b : ℝ
μ : Measure ℝ
𝕜 : Type u_8
inst : RCLike 𝕜
r : 𝕜
f : ℝ → 𝕜
⊢ ∫ (x : ℝ) in a..b, f x / r ∂μ = (∫ (x : ℝ) in a..b, f x ∂μ) / r

Tactic:
simpa only [div_eq_mul_inv] using integral_mul_const r⁻¹ f

Premises used: div_eq_mul_inv, Inv.inv, intervalIntegral.integral_mul_const
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
Goal:
E : Type u_5
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
a b : ℝ
μ : Measure ℝ
inst_2 : CompleteSpace E
c : E
⊢ ∫ (x : ℝ) in a..b, c ∂μ = (μ.real (Ioc a b) - μ.real (Ioc b a)) • c

Tactic:
simp only [measureReal_def, intervalIntegral, setIntegral_const, sub_smul]

Premises used: intervalIntegral, sub_smul, MeasureTheory.measureReal_def, MeasureTheory.setIntegral_const