awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
Goal:
ε : Type u_3
inst : TopologicalSpace ε
inst_1 : ENormedAddMonoid ε
f : ℝ → ε
a b : ℝ
μ ν : Measure ℝ
inst_2 : PseudoMetrizableSpace ε
hf : IntervalIntegrable f ν a b
h : μ ≤ ν
⊢ IntervalIntegrable f μ a b

Tactic:
hf.mono Subset.rfl h

Premises used: IntervalIntegrable.mono, Set.Subset.rfl
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
Goal:
ε : Type u_3
inst : TopologicalSpace ε
inst_1 : ENormedAddMonoid ε
f : ℝ → ε
a b c d : ℝ
μ : Measure ℝ
inst_2 : PseudoMetrizableSpace ε
hf : IntervalIntegrable f μ a b
h : [[c, d]] ⊆ [[a, b]]
⊢ IntervalIntegrable f μ c d

Tactic:
hf.mono h le_rfl

Premises used: le_rfl, IntervalIntegrable.mono
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
Goal:
ε : Type u_3
inst : TopologicalSpace ε
inst_1 : ENormedAddMonoid ε
f : ℝ → ε
a b c d : ℝ
μ : Measure ℝ
inst_2 : PseudoMetrizableSpace ε
hf : IntervalIntegrable f μ a b
h : Ι c d ≤ᶠ[ae μ] Ι a b
⊢ IntervalIntegrable f μ c d

Tactic:
intervalIntegrable_iff.mpr <| hf.def'.mono_set_ae h

Premises used: Iff.mpr, intervalIntegrable_iff, MeasureTheory.IntegrableOn.mono_set_ae, IntervalIntegrable.def'
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
Goal:
ε : Type u_3
inst : TopologicalSpace ε
inst_1 : ENormedAddMonoid ε
f : ℝ → ε
a b c d : ℝ
μ : Measure ℝ
inst_2 : PseudoMetrizableSpace ε
hf : IntervalIntegrable f μ a b
hsub : Ι c d ⊆ Ι a b
⊢ IntervalIntegrable f μ c d

Tactic:
hf.mono_set_ae <| Eventually.of_forall hsub

Premises used: IntervalIntegrable.mono_set_ae, Filter.Eventually.of_forall
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
Goal:
ε : Type u_3
ε' : Type u_4
inst : TopologicalSpace ε
inst_1 : ENormedAddMonoid ε
inst_2 : TopologicalSpace ε'
inst_3 : ENormedAddMonoid ε'
f : ℝ → ε
a b : ℝ
μ : Measure ℝ
inst_4 : PseudoMetrizableSpace ε
inst_5 : PseudoMetrizableSpace ε'
g : ℝ → ε'
hf : IntervalIntegrable f μ a b
hgm : AEStronglyMeasurable g (μ.restrict (Ι a b))
hle : (ae (μ.restrict (Ι a b))).EventuallyLE (β := ℝ≥0∞) (fun (x : ℝ) ↦ ‖g x‖ₑ) fun (x : ℝ) ↦ ‖f x‖ₑ
⊢ IntervalIntegrable g μ a b

Tactic:
intervalIntegrable_iff.2 <| hf.def'.integrable.mono_enorm hgm hle

Premises used: Iff.mpr, intervalIntegrable_iff, MeasureTheory.Integrable.mono_enorm, IntervalIntegrable.def', MeasureTheory.IntegrableOn.integrable
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
Goal:
E : Type u_5
F : Type u_6
inst : NormedAddCommGroup E
a b : ℝ
μ : Measure ℝ
f : ℝ → E
inst_1 : NormedAddCommGroup F
g : ℝ → F
hf : IntervalIntegrable f μ a b
hgm : AEStronglyMeasurable g (μ.restrict (Ι a b))
hle : (ae (μ.restrict (Ι a b))).EventuallyLE (β := ℝ) (fun (x : ℝ) ↦ ‖g x‖) fun (x : ℝ) ↦ ‖f x‖
⊢ IntervalIntegrable g μ a b

Tactic:
intervalIntegrable_iff.2 <| hf.def'.integrable.mono hgm hle

Premises used: Iff.mpr, intervalIntegrable_iff, MeasureTheory.Integrable.mono, IntervalIntegrable.def', MeasureTheory.IntegrableOn.integrable
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
Goal:
ε : Type u_3
inst : TopologicalSpace ε
inst_1 : ENormedAddMonoid ε
a b : ℝ
μ : Measure ℝ
inst_2 : PseudoMetrizableSpace ε
f : ℝ → ε
g : ℝ → ℝ≥0∞
hg : IntervalIntegrable g μ a b
hfm : AEStronglyMeasurable f (μ.restrict (Ι a b))
hle : (fun (x : ℝ) ↦ ‖f x‖ₑ) ≤ᶠ[ae (μ.restrict (Ι a b))] g
⊢ IntervalIntegrable f μ a b

Tactic:
intervalIntegrable_iff.2 <| hg.def'.integrable.mono_enorm hfm hle

Premises used: Iff.mpr, intervalIntegrable_iff, MeasureTheory.Integrable.mono_enorm, IntervalIntegrable.def', MeasureTheory.IntegrableOn.integrable
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
Goal:
E : Type u_5
inst : NormedAddCommGroup E
a b : ℝ
μ : Measure ℝ
f : ℝ → E
g : ℝ → ℝ
hg : IntervalIntegrable g μ a b
hfm : AEStronglyMeasurable f (μ.restrict (Ι a b))
hle : (fun (x : ℝ) ↦ ‖f x‖) ≤ᶠ[ae (μ.restrict (Ι a b))] g
⊢ IntervalIntegrable f μ a b

Tactic:
intervalIntegrable_iff.2 <| hg.def'.integrable.mono' hfm hle

Premises used: Iff.mpr, intervalIntegrable_iff, MeasureTheory.Integrable.mono', IntervalIntegrable.def', MeasureTheory.IntegrableOn.integrable
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
Goal:
ε : Type u_3
inst : TopologicalSpace ε
inst_1 : ENormedAddMonoid ε
f : ℝ → ε
a b : ℝ
μ : Measure ℝ
h : IntervalIntegrable f μ a b
⊢ AEStronglyMeasurable f (μ.restrict (Ioc a b))

Tactic:
h.1.aestronglyMeasurable

Premises used: MeasureTheory.Integrable.aestronglyMeasurable, And.left
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
Goal:
ε : Type u_3
inst : TopologicalSpace ε
inst_1 : ENormedAddMonoid ε
f : ℝ → ε
a b : ℝ
μ : Measure ℝ
h : IntervalIntegrable f μ a b
⊢ AEStronglyMeasurable f (μ.restrict (Ioc b a))

Tactic:
h.2.aestronglyMeasurable

Premises used: MeasureTheory.Integrable.aestronglyMeasurable, And.right
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
Goal:
ε : Type u_3
inst : TopologicalSpace ε
inst_1 : ENormedAddMonoid ε
f : ℝ → ε
a b : ℝ
μ : Measure ℝ
h : IntervalIntegrable f μ a b
pos : ∀ (hab : a ≤ b), AEStronglyMeasurable f (μ.restrict (Ι a b))
neg : ∀ (hab : ¬a ≤ b), AEStronglyMeasurable f (μ.restrict (Ι a b))
⊢ AEStronglyMeasurable f (μ.restrict (Ι a b))

Tactic:
by_cases hab : a ≤ b
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
Goal:
ε : Type u_3
inst : TopologicalSpace ε
inst_1 : ENormedAddMonoid ε
f : ℝ → ε
a b : ℝ
μ : Measure ℝ
h : IntervalIntegrable f μ a b
hab : a ≤ b
pos : AEStronglyMeasurable f (μ.restrict (Ioc a b))
⊢ AEStronglyMeasurable f (μ.restrict (Ι a b))

Tactic:
rw [uIoc_of_le hab]

Premises used: Set.uIoc_of_le
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
Goal:
ε : Type u_3
inst : TopologicalSpace ε
inst_1 : ENormedAddMonoid ε
f : ℝ → ε
a b : ℝ
μ : Measure ℝ
h : IntervalIntegrable f μ a b
hab : a ≤ b
⊢ AEStronglyMeasurable f (μ.restrict (Ioc a b))

Tactic:
h.aestronglyMeasurable

Premises used: IntervalIntegrable.aestronglyMeasurable
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
Goal:
ε : Type u_3
inst : TopologicalSpace ε
inst_1 : ENormedAddMonoid ε
f : ℝ → ε
a b : ℝ
μ : Measure ℝ
h : IntervalIntegrable f μ a b
hab : a ≤ b
⊢ AEStronglyMeasurable f (μ.restrict (Ioc a b))

Tactic:
exact h.aestronglyMeasurable

Premises used: IntervalIntegrable.aestronglyMeasurable
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
Goal:
ε : Type u_3
inst : TopologicalSpace ε
inst_1 : ENormedAddMonoid ε
f : ℝ → ε
a b : ℝ
μ : Measure ℝ
h : IntervalIntegrable f μ a b
hab : ¬a ≤ b
linarith : a < b → b - a + (a - b) = 0
⊢ b ≤ a

Tactic:
linarith
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
Goal:
ε : Type u_3
inst : TopologicalSpace ε
inst_1 : ENormedAddMonoid ε
f : ℝ → ε
a b : ℝ
μ : Measure ℝ
h : IntervalIntegrable f μ a b
hab : ¬a ≤ b
neg : AEStronglyMeasurable f (μ.restrict (Ioc b a))
⊢ AEStronglyMeasurable f (μ.restrict (Ι a b))

Tactic:
rw [uIoc_of_ge (by linarith)]

Premises used: Set.uIoc_of_ge
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
Goal:
ε : Type u_3
inst : TopologicalSpace ε
inst_1 : ENormedAddMonoid ε
f : ℝ → ε
a b : ℝ
μ : Measure ℝ
h : IntervalIntegrable f μ a b
hab : ¬a ≤ b
⊢ AEStronglyMeasurable f (μ.restrict (Ioc b a))

Tactic:
h.aestronglyMeasurable'

Premises used: IntervalIntegrable.aestronglyMeasurable'
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
Goal:
ε : Type u_3
inst : TopologicalSpace ε
inst_1 : ENormedAddMonoid ε
f : ℝ → ε
a b : ℝ
μ : Measure ℝ
h : IntervalIntegrable f μ a b
hab : ¬a ≤ b
⊢ AEStronglyMeasurable f (μ.restrict (Ioc b a))

Tactic:
exact h.aestronglyMeasurable'

Premises used: IntervalIntegrable.aestronglyMeasurable'
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
Goal:
E : Type u_5
inst : NormedAddCommGroup E
a b : ℝ
μ : Measure ℝ
R : Type u_8
inst_1 : NormedAddCommGroup R
inst_2 : SMulZeroClass R E
inst_3 : IsBoundedSMul R E
f : ℝ → E
h : IntervalIntegrable f μ a b
r : R
⊢ IntervalIntegrable (r • f) μ a b

Tactic:
⟨h.1.smul r, h.2.smul r⟩

Premises used: IntervalIntegrable, MeasureTheory.Integrable.smul, And.right, And.left, And.intro
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
Goal:
ε : Type u_3
inst : TopologicalSpace ε
inst_1 : ENormedAddMonoid ε
f g : ℝ → ε
a b : ℝ
μ : Measure ℝ
inst_2 : ContinuousAdd ε
hf : IntervalIntegrable f μ a b
hg : IntervalIntegrable g μ a b
⊢ IntervalIntegrable.{u_3} (ε := ε) (fun (x : ℝ) ↦ f x + g x) μ a b

Tactic:
⟨hf.1.add hg.1, hf.2.add hg.2⟩

Premises used: IntervalIntegrable, MeasureTheory.IntegrableOn.add, And.right, And.left, And.intro
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
Goal:
E : Type u_5
inst : NormedAddCommGroup E
a b : ℝ
μ : Measure ℝ
f g : ℝ → E
hf : IntervalIntegrable f μ a b
hg : IntervalIntegrable g μ a b
⊢ IntervalIntegrable.{u_5} (ε := E) (fun (x : ℝ) ↦ f x - g x) μ a b

Tactic:
⟨hf.1.sub hg.1, hf.2.sub hg.2⟩

Premises used: MeasureTheory.IntegrableOn.sub, IntervalIntegrable, And.right, And.left, And.intro
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
Goal:
ι : Type u_1
a b : ℝ
μ : Measure ℝ
ε : Type u_8
inst : TopologicalSpace ε
inst_1 : ENormedAddCommMonoid ε
inst_2 : ContinuousAdd ε
s : Finset ι
f : ι → ℝ → ε
h : ∀ i ∈ s, IntervalIntegrable (f i) μ a b
⊢ IntervalIntegrable.{u_8} (ε := ε) (∑ i ∈ s, f i) μ a b

Tactic:
⟨integrable_finsetSum' s fun i hi => (h i hi).1, integrable_finsetSum' s fun i hi => (h i hi).2⟩

Premises used: IntervalIntegrable, MeasureTheory.integrable_finsetSum', And.right, And.left, And.intro
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
Goal:
ι : Type u_1
a b : ℝ
μ : Measure ℝ
ε : Type u_8
inst : TopologicalSpace ε
inst_1 : ENormedAddCommMonoid ε
inst_2 : ContinuousAdd ε
inst_3 : PseudoMetrizableSpace ε
f : ι → ℝ → ε
h : ∀ (i : ι), IntervalIntegrable (f i) μ a b
pos : ∀ (h₁ : (support f).Finite), IntervalIntegrable.{u_8} (ε := ε) (∑ᶠ (i : ι), f i) μ a b
neg : ∀ (h₁ : ¬(support f).Finite), IntervalIntegrable.{u_8} (ε := ε) (∑ᶠ (i : ι), f i) μ a b
⊢ IntervalIntegrable.{u_8} (ε := ε) (∑ᶠ (i : ι), f i) μ a b

Tactic:
by_cases h₁ : f.support.Finite

Premises used: Set.Finite, Function.support
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
Goal:
ι : Type u_1
a b : ℝ
μ : Measure ℝ
ε : Type u_8
inst : TopologicalSpace ε
inst_1 : ENormedAddCommMonoid ε
inst_2 : ContinuousAdd ε
inst_3 : PseudoMetrizableSpace ε
f : ι → ℝ → ε
h : ∀ (i : ι), IntervalIntegrable (f i) μ a b
h₁ : (support f).Finite
⊢ IntervalIntegrable.{u_8} (ε := ε) (∑ᶠ (i : ι), f i) μ a b

Tactic:
simp [finsum_eq_sum _ h₁, IntervalIntegrable.sum h₁.toFinset (fun i _ ↦ h i)]

Premises used: IntervalIntegrable.sum, finsum_eq_sum, Set.Finite.toFinset
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
Goal:
ι : Type u_1
a b : ℝ
μ : Measure ℝ
ε : Type u_8
inst : TopologicalSpace ε
inst_1 : ENormedAddCommMonoid ε
inst_2 : ContinuousAdd ε
inst_3 : PseudoMetrizableSpace ε
f : ι → ℝ → ε
h : ∀ (i : ι), IntervalIntegrable (f i) μ a b
h₁ : ¬(support f).Finite
neg : IntervalIntegrable.{u_8} (ε := ε) 0 μ a b
⊢ IntervalIntegrable.{u_8} (ε := ε) (∑ᶠ (i : ι), f i) μ a b

Tactic:
rw [finsum_of_infinite_support h₁]

Premises used: finsum_of_infinite_support
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
Goal:
ι : Type u_1
a b : ℝ
μ : Measure ℝ
ε : Type u_8
inst : TopologicalSpace ε
inst_1 : ENormedAddCommMonoid ε
inst_2 : ContinuousAdd ε
inst_3 : PseudoMetrizableSpace ε
f : ι → ℝ → ε
h : ∀ (i : ι), IntervalIntegrable (f i) μ a b
h₁ : ¬(support f).Finite
⊢ ENorm.enorm.{u_8} (E := ε) 0 ≠ ∞

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
Goal:
ι : Type u_1
a b : ℝ
μ : Measure ℝ
ε : Type u_8
inst : TopologicalSpace ε
inst_1 : ENormedAddCommMonoid ε
inst_2 : ContinuousAdd ε
inst_3 : PseudoMetrizableSpace ε
f : ι → ℝ → ε
h : ∀ (i : ι), IntervalIntegrable (f i) μ a b
h₁ : ¬(support f).Finite
neg : Eq.{u_8 + 1} (α := ε) 0 0 ∨ LT.lt (α := ℝ≥0∞) ((μ : (a : Set ℝ) → ℝ≥0∞) (Ι a b) : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ IntervalIntegrable.{u_8} (ε := ε) 0 μ a b

Tactic:
apply intervalIntegrable_const_iff (c := 0) (by simp) |>.2

Premises used: Iff.mpr, intervalIntegrable_const_iff
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
Goal:
ι : Type u_1
a b : ℝ
μ : Measure ℝ
ε : Type u_8
inst : TopologicalSpace ε
inst_1 : ENormedAddCommMonoid ε
inst_2 : ContinuousAdd ε
inst_3 : PseudoMetrizableSpace ε
f : ι → ℝ → ε
h : ∀ (i : ι), IntervalIntegrable (f i) μ a b
h₁ : ¬(support f).Finite
neg neg₁ : ¬Eq.{u_8 + 1} (α := ε) 0 0 → LT.lt (α := ℝ≥0∞) ((μ : (a : Set ℝ) → ℝ≥0∞) (Ι a b) : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ Eq.{u_8 + 1} (α := ε) 0 0 ∨ LT.lt (α := ℝ≥0∞) ((μ : (a : Set ℝ) → ℝ≥0∞) (Ι a b) : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
tauto
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
Goal:
A : Type u_7
inst : NormedRing A
a b : ℝ
μ : Measure ℝ
f g : ℝ → A
hf : IntervalIntegrable f μ a b
hg : ContinuousOn g [[a, b]]
rw :
  ∀ (hf : IntegrableOn f (Ι a b) μ) (hg : ContinuousOn g [[a, b]]),
    IntegrableOn.{0, u_7} (ε := A) (fun (x : ℝ) ↦ f x * g x) (Ι a b) μ
⊢ IntervalIntegrable.{u_7} (ε := A) (fun (x : ℝ) ↦ f x * g x) μ a b

Tactic:
rw [intervalIntegrable_iff] at hf ⊢

Premises used: intervalIntegrable_iff
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
Goal:
A : Type u_7
inst : NormedRing A
a b : ℝ
μ : Measure ℝ
f g : ℝ → A
hf : IntegrableOn f (Ι a b) μ
hg : ContinuousOn g [[a, b]]
⊢ IntegrableOn.{0, u_7} (ε := A) (fun (x : ℝ) ↦ f x * g x) (Ι a b) μ

Tactic:
hf.mul_continuousOn_of_subset hg measurableSet_Ioc isCompact_uIcc Ioc_subset_Icc_self

Premises used: isCompact_uIcc, Set.Ioc_subset_Icc_self, MeasureTheory.IntegrableOn.mul_continuousOn_of_subset, measurableSet_Ioc
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
Goal:
A : Type u_7
inst : NormedRing A
a b : ℝ
μ : Measure ℝ
f g : ℝ → A
hf : IntegrableOn f (Ι a b) μ
hg : ContinuousOn g [[a, b]]
⊢ IntegrableOn.{0, u_7} (ε := A) (fun (x : ℝ) ↦ f x * g x) (Ι a b) μ

Tactic:
exact hf.mul_continuousOn_of_subset hg measurableSet_Ioc isCompact_uIcc Ioc_subset_Icc_self

Premises used: isCompact_uIcc, Set.Ioc_subset_Icc_self, MeasureTheory.IntegrableOn.mul_continuousOn_of_subset, measurableSet_Ioc
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
Goal:
A : Type u_7
inst : NormedRing A
a b : ℝ
μ : Measure ℝ
f g : ℝ → A
hf : IntervalIntegrable f μ a b
hg : ContinuousOn g [[a, b]]
rw :
  ∀ (hf : IntegrableOn f (Ι a b) μ) (hg : ContinuousOn g [[a, b]]),
    IntegrableOn.{0, u_7} (ε := A) (fun (x : ℝ) ↦ g x * f x) (Ι a b) μ
⊢ IntervalIntegrable.{u_7} (ε := A) (fun (x : ℝ) ↦ g x * f x) μ a b

Tactic:
rw [intervalIntegrable_iff] at hf ⊢

Premises used: intervalIntegrable_iff
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
Goal:
A : Type u_7
inst : NormedRing A
a b : ℝ
μ : Measure ℝ
f g : ℝ → A
hf : IntegrableOn f (Ι a b) μ
hg : ContinuousOn g [[a, b]]
⊢ IntegrableOn.{0, u_7} (ε := A) (fun (x : ℝ) ↦ g x * f x) (Ι a b) μ

Tactic:
hf.continuousOn_mul_of_subset hg isCompact_uIcc measurableSet_Ioc Ioc_subset_Icc_self

Premises used: isCompact_uIcc, Set.Ioc_subset_Icc_self, MeasureTheory.IntegrableOn.continuousOn_mul_of_subset, measurableSet_Ioc
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
Goal:
A : Type u_7
inst : NormedRing A
a b : ℝ
μ : Measure ℝ
f g : ℝ → A
hf : IntegrableOn f (Ι a b) μ
hg : ContinuousOn g [[a, b]]
⊢ IntegrableOn.{0, u_7} (ε := A) (fun (x : ℝ) ↦ g x * f x) (Ι a b) μ

Tactic:
exact hf.continuousOn_mul_of_subset hg isCompact_uIcc measurableSet_Ioc Ioc_subset_Icc_self

Premises used: isCompact_uIcc, Set.Ioc_subset_Icc_self, MeasureTheory.IntegrableOn.continuousOn_mul_of_subset, measurableSet_Ioc
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
Goal:
A : Type u_7
inst : NormedRing A
a b : ℝ
μ : Measure ℝ
f : ℝ → A
hf : IntervalIntegrable f μ a b
c : A
⊢ IntervalIntegrable.{u_7} (ε := A) (fun (x : ℝ) ↦ c * f x) μ a b

Tactic:
hf.continuousOn_mul continuousOn_const

Premises used: continuousOn_const, IntervalIntegrable.continuousOn_mul
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
Goal:
A : Type u_7
inst : NormedRing A
a b : ℝ
μ : Measure ℝ
f : ℝ → A
hf : IntervalIntegrable f μ a b
c : A
⊢ IntervalIntegrable.{u_7} (ε := A) (fun (x : ℝ) ↦ f x * c) μ a b

Tactic:
hf.mul_continuousOn continuousOn_const

Premises used: IntervalIntegrable.mul_continuousOn, continuousOn_const
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
Goal:
𝕜 : Type u_2
E : Type u_5
inst : NormedAddCommGroup E
a b : ℝ
μ : Measure ℝ
f : ℝ → 𝕜
g : ℝ → E
inst_1 : NormedRing 𝕜
inst_2 : Module 𝕜 E
inst_3 : NormSMulClass 𝕜 E
hf : IntervalIntegrable f μ a b
hg : ContinuousOn g [[a, b]]
rw :
  ∀ (hf : IntegrableOn f (Ι a b) μ) (hg : ContinuousOn g [[a, b]]),
    IntegrableOn.{0, u_5} (ε := E) (fun (x : ℝ) ↦ f x • g x) (Ι a b) μ
⊢ IntervalIntegrable.{u_5} (ε := E) (fun (x : ℝ) ↦ f x • g x) μ a b

Tactic:
rw [intervalIntegrable_iff] at hf ⊢

Premises used: intervalIntegrable_iff
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
Goal:
𝕜 : Type u_2
E : Type u_5
inst : NormedAddCommGroup E
a b : ℝ
μ : Measure ℝ
f : ℝ → 𝕜
g : ℝ → E
inst_1 : NormedRing 𝕜
inst_2 : Module 𝕜 E
inst_3 : NormSMulClass 𝕜 E
hf : IntegrableOn f (Ι a b) μ
hg : ContinuousOn g [[a, b]]
⊢ IntegrableOn.{0, u_5} (ε := E) (fun (x : ℝ) ↦ f x • g x) (Ι a b) μ

Tactic:
hf.smul_continuousOn_of_subset hg measurableSet_Ioc isCompact_uIcc Ioc_subset_Icc_self

Premises used: isCompact_uIcc, Set.Ioc_subset_Icc_self, measurableSet_Ioc, MeasureTheory.IntegrableOn.smul_continuousOn_of_subset
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
Goal:
𝕜 : Type u_2
E : Type u_5
inst : NormedAddCommGroup E
a b : ℝ
μ : Measure ℝ
f : ℝ → 𝕜
g : ℝ → E
inst_1 : NormedRing 𝕜
inst_2 : Module 𝕜 E
inst_3 : NormSMulClass 𝕜 E
hf : IntegrableOn f (Ι a b) μ
hg : ContinuousOn g [[a, b]]
⊢ IntegrableOn.{0, u_5} (ε := E) (fun (x : ℝ) ↦ f x • g x) (Ι a b) μ

Tactic:
exact hf.smul_continuousOn_of_subset hg measurableSet_Ioc isCompact_uIcc Ioc_subset_Icc_self

Premises used: isCompact_uIcc, Set.Ioc_subset_Icc_self, measurableSet_Ioc, MeasureTheory.IntegrableOn.smul_continuousOn_of_subset
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
Goal:
𝕜 : Type u_2
E : Type u_5
inst : NormedAddCommGroup E
a b : ℝ
μ : Measure ℝ
f : ℝ → 𝕜
g : ℝ → E
inst_1 : NormedRing 𝕜
inst_2 : Module 𝕜 E
inst_3 : NormSMulClass 𝕜 E
hg : IntervalIntegrable g μ a b
hf : ContinuousOn f [[a, b]]
rw :
  ∀ (hg : IntegrableOn g (Ι a b) μ) (hf : ContinuousOn f [[a, b]]),
    IntegrableOn.{0, u_5} (ε := E) (fun (x : ℝ) ↦ f x • g x) (Ι a b) μ
⊢ IntervalIntegrable.{u_5} (ε := E) (fun (x : ℝ) ↦ f x • g x) μ a b

Tactic:
rw [intervalIntegrable_iff] at hg ⊢

Premises used: intervalIntegrable_iff
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
Goal:
𝕜 : Type u_2
E : Type u_5
inst : NormedAddCommGroup E
a b : ℝ
μ : Measure ℝ
f : ℝ → 𝕜
g : ℝ → E
inst_1 : NormedRing 𝕜
inst_2 : Module 𝕜 E
inst_3 : NormSMulClass 𝕜 E
hg : IntegrableOn g (Ι a b) μ
hf : ContinuousOn f [[a, b]]
⊢ IntegrableOn.{0, u_5} (ε := E) (fun (x : ℝ) ↦ f x • g x) (Ι a b) μ

Tactic:
hg.continuousOn_smul_of_subset hf isCompact_uIcc measurableSet_Ioc Ioc_subset_Icc_self

Premises used: isCompact_uIcc, Set.Ioc_subset_Icc_self, measurableSet_Ioc, MeasureTheory.IntegrableOn.continuousOn_smul_of_subset
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
Goal:
𝕜 : Type u_2
E : Type u_5
inst : NormedAddCommGroup E
a b : ℝ
μ : Measure ℝ
f : ℝ → 𝕜
g : ℝ → E
inst_1 : NormedRing 𝕜
inst_2 : Module 𝕜 E
inst_3 : NormSMulClass 𝕜 E
hg : IntegrableOn g (Ι a b) μ
hf : ContinuousOn f [[a, b]]
⊢ IntegrableOn.{0, u_5} (ε := E) (fun (x : ℝ) ↦ f x • g x) (Ι a b) μ

Tactic:
exact hg.continuousOn_smul_of_subset hf isCompact_uIcc measurableSet_Ioc Ioc_subset_Icc_self

Premises used: isCompact_uIcc, Set.Ioc_subset_Icc_self, measurableSet_Ioc, MeasureTheory.IntegrableOn.continuousOn_smul_of_subset
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
Goal:
a b : ℝ
μ : Measure ℝ
𝕜 : Type u_8
f : ℝ → 𝕜
inst : NormedDivisionRing 𝕜
h : IntervalIntegrable f μ a b
c : 𝕜
⊢ IntervalIntegrable.{u_8} (ε := 𝕜) (fun (x : ℝ) ↦ f x / c) μ a b

Tactic:
simpa only [div_eq_mul_inv] using mul_const h c⁻¹

Premises used: IntervalIntegrable.mul_const, div_eq_mul_inv, Inv.inv
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
Goal:
ε : Type u_3
inst : TopologicalSpace ε
inst_1 : ENormedAddMonoid ε
f : ℝ → ε
a b : ℝ
inst_2 : PseudoMetrizableSpace ε
hf : IntervalIntegrable f volume a b
c : ℝ
h : ‖f (min a b)‖ₑ ≠ ∞
h' : ‖f (c * min (a / c) (b / c))‖ₑ ≠ ∞
inl : ∀ (hc : c = 0), IntervalIntegrable.{u_3} (ε := ε) (fun (x : ℝ) ↦ f (c * x)) volume (a / c) (b / c)
inr : ∀ (hc : c ≠ 0), IntervalIntegrable.{u_3} (ε := ε) (fun (x : ℝ) ↦ f (c * x)) volume (a / c) (b / c)
⊢ IntervalIntegrable.{u_3} (ε := ε) (fun (x : ℝ) ↦ f (c * x)) volume (a / c) (b / c)

Tactic:
rcases eq_or_ne c 0 with (hc | hc)

Premises used: eq_or_ne, OfNat.ofNat
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
Goal:
ε : Type u_3
inst : TopologicalSpace ε
inst_1 : ENormedAddMonoid ε
f : ℝ → ε
a b : ℝ
inst_2 : PseudoMetrizableSpace ε
hf : IntervalIntegrable f volume a b
c : ℝ
h : ‖f (min a b)‖ₑ ≠ ∞
h' : ‖f (c * min (a / c) (b / c))‖ₑ ≠ ∞
hc : c = 0
inl : IntervalIntegrable.{u_3} (ε := ε) (fun (x : ℝ) ↦ f (0 * x)) volume (a / 0) (b / 0)
⊢ IntervalIntegrable.{u_3} (ε := ε) (fun (x : ℝ) ↦ f (c * x)) volume (a / c) (b / c)

Tactic:
rw [hc]
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
Goal:
ε : Type u_3
inst : TopologicalSpace ε
inst_1 : ENormedAddMonoid ε
f : ℝ → ε
a b : ℝ
inst_2 : PseudoMetrizableSpace ε
hf : IntervalIntegrable f volume a b
c : ℝ
h : ‖f (min a b)‖ₑ ≠ ∞
h' : ‖f (c * min (a / c) (b / c))‖ₑ ≠ ∞
hc : c = 0
⊢ IntervalIntegrable.{u_3} (ε := ε) (fun (x : ℝ) ↦ f (0 * x)) volume (a / 0) (b / 0)

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
Goal:
ε : Type u_3
inst : TopologicalSpace ε
inst_1 : ENormedAddMonoid ε
f : ℝ → ε
a b : ℝ
inst_2 : PseudoMetrizableSpace ε
hf : IntervalIntegrable f volume a b
c : ℝ
h : ‖f (min a b)‖ₑ ≠ ∞
h' : ‖f (c * min (a / c) (b / c))‖ₑ ≠ ∞
hc : c ≠ 0
inr :
  ∀ (hf : IntegrableOn (mα := Real.measurableSpace) f [[a, b]] volume) {c : ℝ} (h : ‖f (min a b)‖ₑ ≠ ∞)
    (h' : ‖f (c * min (a / c) (b / c))‖ₑ ≠ ∞) (hc : c ≠ 0),
    IntervalIntegrable.{u_3} (ε := ε) (fun (x : ℝ) ↦ f (c * x)) volume (a / c) (b / c)
⊢ IntervalIntegrable.{u_3} (ε := ε) (fun (x : ℝ) ↦ f (c * x)) volume (a / c) (b / c)

Tactic:
rw [intervalIntegrable_iff' h] at hf

Premises used: intervalIntegrable_iff'
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
Goal:
ε : Type u_3
inst : TopologicalSpace ε
inst_1 : ENormedAddMonoid ε
f : ℝ → ε
a b : ℝ
inst_2 : PseudoMetrizableSpace ε
hf : IntegrableOn (mα := Real.measurableSpace) f [[a, b]] volume
c : ℝ
h : ‖f (min a b)‖ₑ ≠ ∞
h' : ‖f (c * min (a / c) (b / c))‖ₑ ≠ ∞
hc : c ≠ 0
inr : IntegrableOn.{0, u_3} (ε := ε) (mα := Real.measurableSpace) (fun (x : ℝ) ↦ f (c * x)) [[a / c, b / c]] volume
⊢ IntervalIntegrable.{u_3} (ε := ε) (fun (x : ℝ) ↦ f (c * x)) volume (a / c) (b / c)

Tactic:
rw [intervalIntegrable_iff' h'] at ⊢

Premises used: intervalIntegrable_iff'
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
Goal:
ε : Type u_3
inst : TopologicalSpace ε
inst_1 : ENormedAddMonoid ε
f : ℝ → ε
a b : ℝ
inst_2 : PseudoMetrizableSpace ε
hf : IntegrableOn (mα := Real.measurableSpace) f [[a, b]] volume
c : ℝ
h : ‖f (min a b)‖ₑ ≠ ∞
h' : ‖f (c * min (a / c) (b / c))‖ₑ ≠ ∞
hc : c ≠ 0
⊢ MeasurableEmbedding (β := ℝ) fun (x : ℝ) ↦ x * c⁻¹

Tactic:
have A : MeasurableEmbedding fun x => x * c⁻¹ :=
    (Homeomorph.mulRight₀ _ (inv_ne_zero hc)).isClosedEmbedding.measurableEmbedding
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
Goal:
ε : Type u_3
inst : TopologicalSpace ε
inst_1 : ENormedAddMonoid ε
f : ℝ → ε
a b : ℝ
inst_2 : PseudoMetrizableSpace ε
hf : IntegrableOn (mα := Real.measurableSpace) f [[a, b]] volume
c : ℝ
h : ‖f (min a b)‖ₑ ≠ ∞
h' : ‖f (c * min (a / c) (b / c))‖ₑ ≠ ∞
hc : c ≠ 0
A : MeasurableEmbedding (β := ℝ) fun (x : ℝ) ↦ x * c⁻¹
⊢ ENNReal.ofReal |c⁻¹| ≠ 0

Tactic:
simpa