awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic (goal)
Goal:
ε : Type u_3
inst : TopologicalSpace ε
inst_1 : ENormedAddMonoid ε
inst_2 : PseudoMetrizableSpace ε
f : ℝ → ε
a b : ℝ
μ : Measure ℝ
inst_3 : NoAtoms μ
h : ‖f (min a b)‖ₑ ≠ ∞
⊢ IntervalIntegrable f μ a b ↔ IntegrableOn f [[a, b]] μ
have rw : IntegrableOn f (Ι a b) μ ↔ IntegrableOn f [[a, b]] μ
Tactic: rw [intervalIntegrable_iff, ← Icc_min_max, uIoc, integrableOn_Icc_iff_integrableOn_Ioc h]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic (goal)
Goal:
ε : Type u_3
inst : TopologicalSpace ε
inst_1 : ENormedAddMonoid ε
inst_2 : PseudoMetrizableSpace ε
f : ℝ → ε
a b : ℝ
μ : Measure ℝ
inst_3 : NoAtoms μ
h : ‖f (min a b)‖ₑ ≠ ∞
rw : IntegrableOn f (Ι a b) μ ↔ IntegrableOn f [[a, b]] μ
⊢ IntervalIntegrable f μ a b ↔ IntegrableOn f [[a, b]] μ
have rw₁ : IntegrableOn f (Ι a b) μ ↔ IntegrableOn f (Icc (min a b) (max a b)) μ
Tactic: rw [intervalIntegrable_iff, ← Icc_min_max, uIoc, integrableOn_Icc_iff_integrableOn_Ioc h]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic (goal)
Goal:
ε : Type u_3
inst : TopologicalSpace ε
inst_1 : ENormedAddMonoid ε
inst_2 : PseudoMetrizableSpace ε
f : ℝ → ε
a b : ℝ
μ : Measure ℝ
inst_3 : NoAtoms μ
h : ‖f (min a b)‖ₑ ≠ ∞
rw : IntegrableOn f (Ι a b) μ ↔ IntegrableOn f [[a, b]] μ
rw₁ : IntegrableOn f (Ι a b) μ ↔ IntegrableOn f (Icc (min a b) (max a b)) μ
⊢ IntervalIntegrable f μ a b ↔ IntegrableOn f [[a, b]] μ
have rw₂ : IntegrableOn f (Ioc (min a b) (max a b)) μ ↔ IntegrableOn f (Icc (min a b) (max a b)) μ
Tactic: rw [intervalIntegrable_iff, ← Icc_min_max, uIoc, integrableOn_Icc_iff_integrableOn_Ioc h]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic (goal)
Goal:
ε : Type u_3
inst : TopologicalSpace ε
inst_1 : ENormedAddMonoid ε
inst_2 : PseudoMetrizableSpace ε
f : ℝ → ε
a b : ℝ
μ : Measure ℝ
inst_3 : NoAtoms μ
h : ‖f (min a b)‖ₑ ≠ ∞
rw : IntegrableOn f (Ι a b) μ ↔ IntegrableOn f [[a, b]] μ
rw₁ : IntegrableOn f (Ι a b) μ ↔ IntegrableOn f (Icc (min a b) (max a b)) μ
rw₂ : IntegrableOn f (Ioc (min a b) (max a b)) μ ↔ IntegrableOn f (Icc (min a b) (max a b)) μ
⊢ IntervalIntegrable f μ a b ↔ IntegrableOn f [[a, b]] μ
have rw₃ : IntegrableOn f (Ioc (min a b) (max a b)) μ ↔ IntegrableOn f (Ioc (min a b) (max a b)) μ
Tactic: rw [intervalIntegrable_iff, ← Icc_min_max, uIoc, integrableOn_Icc_iff_integrableOn_Ioc h]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic (goal)
Goal:
ε : Type u_3
inst : TopologicalSpace ε
inst_1 : ENormedAddMonoid ε
inst_2 : PseudoMetrizableSpace ε
f : ℝ → ε
a b : ℝ
μ : Measure ℝ
inst_3 : NoAtoms μ
hab : a ≤ b
ha : ‖f a‖ₑ ≠ ∞
⊢ IntervalIntegrable f μ a b ↔ IntegrableOn f (Icc a b) μ
have rw : IntegrableOn f (Ioc a b) μ ↔ IntegrableOn f (Icc a b) μ
Tactic: rw [intervalIntegrable_iff_integrableOn_Ioc_of_le hab, integrableOn_Icc_iff_integrableOn_Ioc ha]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic (goal)
Goal:
ε : Type u_3
inst : TopologicalSpace ε
inst_1 : ENormedAddMonoid ε
inst_2 : PseudoMetrizableSpace ε
f : ℝ → ε
a b : ℝ
μ : Measure ℝ
inst_3 : NoAtoms μ
hab : a ≤ b
ha : ‖f a‖ₑ ≠ ∞
rw : IntegrableOn f (Ioc a b) μ ↔ IntegrableOn f (Icc a b) μ
⊢ IntervalIntegrable f μ a b ↔ IntegrableOn f (Icc a b) μ
have rw₁ : IntegrableOn f (Ioc a b) μ ↔ IntegrableOn f (Ioc a b) μ
Tactic: rw [intervalIntegrable_iff_integrableOn_Ioc_of_le hab, integrableOn_Icc_iff_integrableOn_Ioc ha]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic (goal)
Goal:
ε : Type u_3
inst : TopologicalSpace ε
inst_1 : ENormedAddMonoid ε
inst_2 : PseudoMetrizableSpace ε
f : ℝ → ε
a b : ℝ
μ : Measure ℝ
inst_3 : NoAtoms μ
hab : a ≤ b
ha : ‖f a‖ₑ ≠ ∞
hb : ‖f b‖ₑ ≠ ∞
⊢ IntervalIntegrable f μ a b ↔ IntegrableOn f (Ico a b) μ
have rw : IntegrableOn f (Icc a b) μ ↔ IntegrableOn f (Ico a b) μ
Tactic: rw [intervalIntegrable_iff_integrableOn_Icc_of_le hab ha,
    integrableOn_Icc_iff_integrableOn_Ico hb]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic (goal)
Goal:
ε : Type u_3
inst : TopologicalSpace ε
inst_1 : ENormedAddMonoid ε
inst_2 : PseudoMetrizableSpace ε
f : ℝ → ε
a b : ℝ
μ : Measure ℝ
inst_3 : NoAtoms μ
hab : a ≤ b
ha : ‖f a‖ₑ ≠ ∞
hb : ‖f b‖ₑ ≠ ∞
rw : IntegrableOn f (Icc a b) μ ↔ IntegrableOn f (Ico a b) μ
⊢ IntervalIntegrable f μ a b ↔ IntegrableOn f (Ico a b) μ
have rw₁ : IntegrableOn f (Ico a b) μ ↔ IntegrableOn f (Ico a b) μ
Tactic: rw [intervalIntegrable_iff_integrableOn_Icc_of_le hab ha,
    integrableOn_Icc_iff_integrableOn_Ico hb]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic (goal)
Goal:
ε : Type u_3
inst : TopologicalSpace ε
inst_1 : ENormedAddMonoid ε
inst_2 : PseudoMetrizableSpace ε
f : ℝ → ε
a b : ℝ
μ : Measure ℝ
inst_3 : NoAtoms μ
hab : a ≤ b
ha : ‖f a‖ₑ ≠ ∞
hb : ‖f b‖ₑ ≠ ∞
⊢ IntervalIntegrable f μ a b ↔ IntegrableOn f (Ioo a b) μ
have rw : IntegrableOn f (Icc a b) μ ↔ IntegrableOn f (Ioo a b) μ
Tactic: rw [intervalIntegrable_iff_integrableOn_Icc_of_le hab ha,
    integrableOn_Icc_iff_integrableOn_Ioo ha hb]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic (goal)
Goal:
ε : Type u_3
inst : TopologicalSpace ε
inst_1 : ENormedAddMonoid ε
inst_2 : PseudoMetrizableSpace ε
f : ℝ → ε
a b : ℝ
μ : Measure ℝ
inst_3 : NoAtoms μ
hab : a ≤ b
ha : ‖f a‖ₑ ≠ ∞
hb : ‖f b‖ₑ ≠ ∞
rw : IntegrableOn f (Icc a b) μ ↔ IntegrableOn f (Ioo a b) μ
⊢ IntervalIntegrable f μ a b ↔ IntegrableOn f (Ioo a b) μ
have rw₁ : IntegrableOn f (Ioo a b) μ ↔ IntegrableOn f (Ioo a b) μ
Tactic: rw [intervalIntegrable_iff_integrableOn_Icc_of_le hab ha,
    integrableOn_Icc_iff_integrableOn_Ioo ha hb]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic (goal)
Goal:
ε : Type u_3
inst : TopologicalSpace ε
inst_1 : ENormedAddMonoid ε
f : ℝ → ε
a : ℝ
μ : Measure ℝ
⊢ IntervalIntegrable f μ a a
have left : IntegrableOn f (Ioc a a) μ
Tactic: constructor
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic (goal)
Goal:
ε : Type u_3
inst : TopologicalSpace ε
inst_1 : ENormedAddMonoid ε
f : ℝ → ε
μ : Measure ℝ
inst_2 : PseudoMetrizableSpace ε
a : ℕ → ℝ
m n : ℕ
hmn : m ≤ n
hint : ∀ k ∈ Ico m n, IntervalIntegrable f μ (a k) (a (k + 1))
⊢ IntervalIntegrable f μ (a m) (a n)
have revert : ∀ (hint : ∀ k ∈ Ico m n, IntervalIntegrable f μ (a k) (a (k + 1))), IntervalIntegrable f μ (a m) (a n)
Tactic: revert hint
Cleared hypotheses: hint
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic (goal)
Goal:
ε : Type u_3
inst : TopologicalSpace ε
inst_1 : ENormedAddMonoid ε
f : ℝ → ε
μ : Measure ℝ
inst_2 : PseudoMetrizableSpace ε
a : ℕ → ℝ
m n : ℕ
hmn : m ≤ n
⊢ ∀ (hint : ∀ k ∈ Ico m n, IntervalIntegrable f μ (a k) (a (k + 1))), IntervalIntegrable f μ (a m) (a n)
have refine_1 : ∀ (hint : ∀ k ∈ Ico m m, IntervalIntegrable f μ (a k) (a (k + 1))), IntervalIntegrable f μ (a m) (a m)
Tactic: refine Nat.le_induction ?_ ?_ n hmn
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic (goal)
Goal:
ε : Type u_3
inst : TopologicalSpace ε
inst_1 : ENormedAddMonoid ε
f : ℝ → ε
μ : Measure ℝ
inst_2 : PseudoMetrizableSpace ε
a : ℕ → ℝ
m n : ℕ
hmn : m ≤ n
refine_1 : ∀ (hint : ∀ k ∈ Ico m m, IntervalIntegrable f μ (a k) (a (k + 1))), IntervalIntegrable f μ (a m) (a m)
⊢ ∀ (hint : ∀ k ∈ Ico m n, IntervalIntegrable f μ (a k) (a (k + 1))), IntervalIntegrable f μ (a m) (a n)
have refine_2 : ∀ (n : ℕ) (hmn : m ≤ n),
  (∀ (hint : ∀ k ∈ Ico m n, IntervalIntegrable f μ (a k) (a (k + 1))), IntervalIntegrable f μ (a m) (a n)) →
    ∀ (hint : ∀ k ∈ Ico m (n + 1), IntervalIntegrable f μ (a k) (a (k + 1))), IntervalIntegrable f μ (a m) (a (n + 1))
Tactic: refine Nat.le_induction ?_ ?_ n hmn
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic (goal)
Goal:
ε : Type u_3
inst : TopologicalSpace ε
inst_1 : ENormedAddMonoid ε
f : ℝ → ε
inst_2 : PseudoMetrizableSpace ε
μ : Measure ℝ
a b : ℝ
hf : AEStronglyMeasurable f (μ.restrict (Ι a b))
⊢ IntervalIntegrable (ε := ℝ≥0∞) (fun (t : ℝ) ↦ ‖f t‖ₑ) μ a b ↔ IntervalIntegrable f μ a b
have simp_rw : IntegrableOn (ε := ℝ≥0∞) (fun (t : ℝ) ↦ ‖f t‖ₑ) (Ι a b) μ ↔ IntegrableOn f (Ι a b) μ
Tactic: simp_rw [intervalIntegrable_iff, IntegrableOn, integrable_enorm_iff hf]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic (goal)
Goal:
ε : Type u_3
inst : TopologicalSpace ε
inst_1 : ENormedAddMonoid ε
f : ℝ → ε
inst_2 : PseudoMetrizableSpace ε
μ : Measure ℝ
a b : ℝ
hf : AEStronglyMeasurable f (μ.restrict (Ι a b))
simp_rw : IntegrableOn (ε := ℝ≥0∞) (fun (t : ℝ) ↦ ‖f t‖ₑ) (Ι a b) μ ↔ IntegrableOn f (Ι a b) μ
⊢ IntervalIntegrable (ε := ℝ≥0∞) (fun (t : ℝ) ↦ ‖f t‖ₑ) μ a b ↔ IntervalIntegrable f μ a b
have simp_rw₁ : Integrable (ε := ℝ≥0∞) (fun (t : ℝ) ↦ ‖f t‖ₑ) (μ.restrict (Ι a b)) ↔ Integrable f (μ.restrict (Ι a b))
Tactic: simp_rw [intervalIntegrable_iff, IntegrableOn, integrable_enorm_iff hf]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic (goal)
Goal:
E : Type u_5
inst : NormedAddCommGroup E
f : ℝ → E
μ : Measure ℝ
a b : ℝ
hf : AEStronglyMeasurable f (μ.restrict (Ι a b))
⊢ IntervalIntegrable (ε := ℝ) (fun (t : ℝ) ↦ ‖f t‖) μ a b ↔ IntervalIntegrable f μ a b
have simp_rw : IntegrableOn (ε := ℝ) (fun (t : ℝ) ↦ ‖f t‖) (Ι a b) μ ↔ IntegrableOn f (Ι a b) μ
Tactic: simp_rw [intervalIntegrable_iff, IntegrableOn, integrable_norm_iff hf]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic (goal)
Goal:
E : Type u_5
inst : NormedAddCommGroup E
f : ℝ → E
μ : Measure ℝ
a b : ℝ
hf : AEStronglyMeasurable f (μ.restrict (Ι a b))
simp_rw : IntegrableOn (ε := ℝ) (fun (t : ℝ) ↦ ‖f t‖) (Ι a b) μ ↔ IntegrableOn f (Ι a b) μ
⊢ IntervalIntegrable (ε := ℝ) (fun (t : ℝ) ↦ ‖f t‖) μ a b ↔ IntervalIntegrable f μ a b
have simp_rw₁ : Integrable (ε := ℝ) (fun (t : ℝ) ↦ ‖f t‖) (μ.restrict (Ι a b)) ↔ Integrable f (μ.restrict (Ι a b))
Tactic: simp_rw [intervalIntegrable_iff, IntegrableOn, integrable_norm_iff hf]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic (goal)
Goal:
ε : Type u_3
inst : TopologicalSpace ε
inst_1 : ENormedAddMonoid ε
f : ℝ → ε
a b : ℝ
μ : Measure ℝ
h : IntervalIntegrable f μ a b
⊢ AEStronglyMeasurable f (μ.restrict (Ι a b))
have pos : ∀ (hab : a ≤ b), AEStronglyMeasurable f (μ.restrict (Ι a b))
Tactic: by_cases hab : a ≤ b
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic (goal)
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))
⊢ AEStronglyMeasurable f (μ.restrict (Ι a b))
have neg : ∀ (hab : ¬a ≤ b), AEStronglyMeasurable f (μ.restrict (Ι a b))
Tactic: by_cases hab : a ≤ b
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic (goal)
Goal:
ε : Type u_3
inst : TopologicalSpace ε
inst_1 : ENormedAddMonoid ε
f : ℝ → ε
a b : ℝ
μ : Measure ℝ
h : IntervalIntegrable f μ a b
hab : a ≤ b
⊢ AEStronglyMeasurable f (μ.restrict (Ι a b))
have pos : AEStronglyMeasurable f (μ.restrict (Ioc a b))
Tactic: rw [uIoc_of_le hab]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic (goal)
Goal:
ε : Type u_3
inst : TopologicalSpace ε
inst_1 : ENormedAddMonoid ε
f : ℝ → ε
a b : ℝ
μ : Measure ℝ
h : IntervalIntegrable f μ a b
hab : ¬a ≤ b
⊢ b ≤ a
have linarith : a < b → b - a + (a - b) = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic (goal)
Goal:
ε : Type u_3
inst : TopologicalSpace ε
inst_1 : ENormedAddMonoid ε
f : ℝ → ε
a b : ℝ
μ : Measure ℝ
h : IntervalIntegrable f μ a b
hab : ¬a ≤ b
⊢ AEStronglyMeasurable f (μ.restrict (Ι a b))
have neg : AEStronglyMeasurable f (μ.restrict (Ioc b a))
Tactic: rw [uIoc_of_ge (by linarith)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic (goal)
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
⊢ IntervalIntegrable.{u_8} (ε := ε) (∑ᶠ (i : ι), f i) μ a b
have pos : ∀ (h₁ : (support f).Finite), IntervalIntegrable.{u_8} (ε := ε) (∑ᶠ (i : ι), f i) μ a b
Tactic: by_cases h₁ : f.support.Finite
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic (goal)
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
⊢ IntervalIntegrable.{u_8} (ε := ε) (∑ᶠ (i : ι), f i) μ a b
have neg : ∀ (h₁ : ¬(support f).Finite), IntervalIntegrable.{u_8} (ε := ε) (∑ᶠ (i : ι), f i) μ a b
Tactic: by_cases h₁ : f.support.Finite
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic (goal)
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
have neg : IntervalIntegrable.{u_8} (ε := ε) 0 μ a b
Tactic: rw [finsum_of_infinite_support h₁]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic (goal)
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} (ε := ε) 0 μ a b
have neg : Eq.{u_8 + 1} (α := ε) 0 0 ∨ LT.lt (α := ℝ≥0∞) ((μ : (a : Set ℝ) → ℝ≥0∞) (Ι a b) : ℝ≥0∞) (∞ : ℝ≥0∞)
Tactic: apply intervalIntegrable_const_iff (c := 0) (by simp) |>.2
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic (goal)
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
⊢ Eq.{u_8 + 1} (α := ε) 0 0 ∨ LT.lt (α := ℝ≥0∞) ((μ : (a : Set ℝ) → ℝ≥0∞) (Ι a b) : ℝ≥0∞) (∞ : ℝ≥0∞)
have neg : ¬Eq.{u_8 + 1} (α := ε) 0 0 → LT.lt (α := ℝ≥0∞) ((μ : (a : Set ℝ) → ℝ≥0∞) (Ι a b) : ℝ≥0∞) (∞ : ℝ≥0∞)
Tactic: tauto
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic (goal)
Goal:
A : Type u_7
inst : NormedRing A
a b : ℝ
μ : Measure ℝ
f g : ℝ → A
hf : IntervalIntegrable f μ a b
hg : ContinuousOn g [[a, b]]
⊢ IntervalIntegrable.{u_7} (ε := A) (fun (x : ℝ) ↦ f x * g x) μ a b
have rw : ∀ (hf : IntegrableOn f (Ι a b) μ) (hg : ContinuousOn g [[a, b]]),
  IntegrableOn.{0, u_7} (ε := A) (fun (x : ℝ) ↦ f x * g x) (Ι a b) μ
Tactic: rw [intervalIntegrable_iff] at hf ⊢
Cleared hypotheses: hf, hg
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic (goal)
Goal:
A : Type u_7
inst : NormedRing A
a b : ℝ
μ : Measure ℝ
f g : ℝ → A
hf : IntervalIntegrable f μ a b
hg : ContinuousOn g [[a, b]]
⊢ IntervalIntegrable.{u_7} (ε := A) (fun (x : ℝ) ↦ g x * f x) μ a b
have rw : ∀ (hf : IntegrableOn f (Ι a b) μ) (hg : ContinuousOn g [[a, b]]),
  IntegrableOn.{0, u_7} (ε := A) (fun (x : ℝ) ↦ g x * f x) (Ι a b) μ
Tactic: rw [intervalIntegrable_iff] at hf ⊢
Cleared hypotheses: hf, hg
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic (goal)
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]]
⊢ IntervalIntegrable.{u_5} (ε := E) (fun (x : ℝ) ↦ f x • g x) μ a b
have rw : ∀ (hf : IntegrableOn f (Ι a b) μ) (hg : ContinuousOn g [[a, b]]),
  IntegrableOn.{0, u_5} (ε := E) (fun (x : ℝ) ↦ f x • g x) (Ι a b) μ
Tactic: rw [intervalIntegrable_iff] at hf ⊢
Cleared hypotheses: hf, hg
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic (goal)
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]]
⊢ IntervalIntegrable.{u_5} (ε := E) (fun (x : ℝ) ↦ f x • g x) μ a b
have rw : ∀ (hg : IntegrableOn g (Ι a b) μ) (hf : ContinuousOn f [[a, b]]),
  IntegrableOn.{0, u_5} (ε := E) (fun (x : ℝ) ↦ f x • g x) (Ι a b) μ
Tactic: rw [intervalIntegrable_iff] at hg ⊢
Cleared hypotheses: hg, hf
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic (goal)
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))‖ₑ ≠ ∞
⊢ IntervalIntegrable.{u_3} (ε := ε) (fun (x : ℝ) ↦ f (c * x)) volume (a / c) (b / c)
have inl : ∀ (hc : c = 0), IntervalIntegrable.{u_3} (ε := ε) (fun (x : ℝ) ↦ f (c * x)) volume (a / c) (b / c)
Tactic: rcases eq_or_ne c 0 with (hc | hc)
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic (goal)
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)
⊢ IntervalIntegrable.{u_3} (ε := ε) (fun (x : ℝ) ↦ f (c * x)) volume (a / c) (b / c)
have inr : ∀ (hc : c ≠ 0), IntervalIntegrable.{u_3} (ε := ε) (fun (x : ℝ) ↦ f (c * x)) volume (a / c) (b / c)
Tactic: rcases eq_or_ne c 0 with (hc | hc)
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic (goal)
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 (c * x)) volume (a / c) (b / c)
have inl : IntervalIntegrable.{u_3} (ε := ε) (fun (x : ℝ) ↦ f (0 * x)) volume (a / 0) (b / 0)
Tactic: rw [hc]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic (goal)
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 (c * x)) volume (a / c) (b / c)
have 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)
Tactic: rw [intervalIntegrable_iff' h] at hf
Cleared hypotheses: hf, c, h, h', hc
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic (goal)
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
⊢ IntervalIntegrable.{u_3} (ε := ε) (fun (x : ℝ) ↦ f (c * x)) volume (a / c) (b / c)
have inr : IntegrableOn.{0, u_3} (ε := ε) (mα := Real.measurableSpace) (fun (x : ℝ) ↦ f (c * x)) [[a / c, b / c]] volume
Tactic: rw [intervalIntegrable_iff' h'] at ⊢
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic (hypothesis)
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
⊢ IntegrableOn.{0, u_3} (ε := ε) (mα := Real.measurableSpace) (fun (x : ℝ) ↦ f (c * x)) [[a / c, b / c]] volume
have A : MeasurableEmbedding (β := ℝ) fun (x : ℝ) ↦ x * c⁻¹
Tactic: have A : MeasurableEmbedding fun x => x * c⁻¹ :=
    (Homeomorph.mulRight₀ _ (inv_ne_zero hc)).isClosedEmbedding.measurableEmbedding
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic (goal)
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⁻¹
⊢ IntegrableOn.{0, u_3} (ε := ε) (mα := Real.measurableSpace) (fun (x : ℝ) ↦ f (c * x)) [[a / c, b / c]] volume
have inr : IntegrableOn.{0, u_3} (α := ℝ) (ε := ε) (mα := Real.measurableSpace) ((fun (x : ℝ) ↦ f (c * x)) ∘ fun (x : ℝ) ↦ x * c⁻¹)
  ((fun (x : ℝ) ↦ x * c⁻¹) ⁻¹' [[a / c, b / c]]) volume
Tactic: rw [← Real.smul_map_volume_mul_right (inv_ne_zero hc), IntegrableOn, Measure.restrict_smul,
    integrable_smul_measure (by simpa : ENNReal.ofReal |c⁻¹| ≠ 0) ENNReal.ofReal_ne_top,
    ← IntegrableOn, MeasurableEmbedding.integrableOn_map_iff A]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic (goal)
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⁻¹
⊢ IntegrableOn.{0, u_3} (α := ℝ) (ε := ε) (mα := Real.measurableSpace)
    ((fun (x : ℝ) ↦ f (c * x)) ∘ fun (x : ℝ) ↦ x * c⁻¹) ((fun (x : ℝ) ↦ x * c⁻¹) ⁻¹' [[a / c, b / c]]) volume
have h₁ : ((fun (x : ℝ) ↦ f (c * x)) ∘ fun (x : ℝ) ↦ x * c⁻¹) = f
Tactic: convert! hf using 1
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic (goal)
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⁻¹
h₁ : ((fun (x : ℝ) ↦ f (c * x)) ∘ fun (x : ℝ) ↦ x * c⁻¹) = f
⊢ IntegrableOn.{0, u_3} (α := ℝ) (ε := ε) (mα := Real.measurableSpace)
    ((fun (x : ℝ) ↦ f (c * x)) ∘ fun (x : ℝ) ↦ x * c⁻¹) ((fun (x : ℝ) ↦ x * c⁻¹) ⁻¹' [[a / c, b / c]]) volume
have h₂ : (fun (x : ℝ) ↦ x * c⁻¹) ⁻¹' [[a / c, b / c]] = [[a, b]]
Tactic: convert! hf using 1
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic (goal)
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⁻¹
⊢ ((fun (x : ℝ) ↦ f (c * x)) ∘ fun (x : ℝ) ↦ x * c⁻¹) = f
have h₁ : ∀ (x : ℝ), ((fun (x : ℝ) ↦ f (c * x)) ∘ fun (x : ℝ) ↦ x * c⁻¹) x = f x
Tactic: ext
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic (goal)
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⁻¹
x : ℝ
⊢ ((fun (x : ℝ) ↦ f (c * x)) ∘ fun (x : ℝ) ↦ x * c⁻¹) x = f x
have h₁ : f (c * (x * c⁻¹)) = f x
Tactic: simp only [comp_apply]