awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic (goal)
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 ∂μ))
⊢ 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 ∂μ))
have 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 ∂μ))
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic (hypothesis)
Goal:
E : Type u_5
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
a b : ℝ
f : ℝ → E
μ : Measure ℝ
h : ¬IntervalIntegrable f μ a b
⊢ Eq.{u_5 + 1} (α := E) (∫ (x : ℝ) in a..b, f x ∂μ) 0
have h₁ : ¬IntegrableOn f (Ι a b) μ
Tactic: rw [intervalIntegrable_iff] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic (goal)
Goal:
E : Type u_5
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
a b : ℝ
f : ℝ → E
μ : Measure ℝ
h : ¬IntegrableOn f (Ι a b) μ
⊢ Eq.{u_5 + 1} (α := E) (∫ (x : ℝ) in a..b, f x ∂μ) 0
have rw : HSMul.hSMul (α := ℝ) (β := E) (if a ≤ b then 1 else -1) (∫ (x : ℝ) in Ι a b, f x ∂μ) = 0
Tactic: rw [intervalIntegral_eq_integral_uIoc, integral_undef h, smul_zero]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic (goal)
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
⊢ Eq.{u_5 + 1} (α := E) (∫ (x : ℝ) in a..b, f x ∂μ) 0
have rw₁ : HSMul.hSMul (α := ℝ) (β := E) (if a ≤ b then 1 else -1) 0 = 0
Tactic: rw [intervalIntegral_eq_integral_uIoc, integral_undef h, smul_zero]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic (goal)
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
⊢ Eq.{u_5 + 1} (α := E) (∫ (x : ℝ) in a..b, f x ∂μ) 0
have rw₂ : Eq.{u_5 + 1} (α := E) 0 0
Tactic: rw [intervalIntegral_eq_integral_uIoc, integral_undef h, smul_zero]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic (goal)
Goal:
E : Type u_5
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
a b : ℝ
f : ℝ → E
μ : Measure ℝ
hf : ¬AEStronglyMeasurable f (μ.restrict (Ι a b))
⊢ Eq.{u_5 + 1} (α := E) (∫ (x : ℝ) in a..b, f x ∂μ) 0
have rw : HSMul.hSMul (α := ℝ) (β := E) (if a ≤ b then 1 else -1) (∫ (x : ℝ) in Ι a b, f x ∂μ) = 0
Tactic: rw [intervalIntegral_eq_integral_uIoc, integral_non_aestronglyMeasurable hf, smul_zero]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic (goal)
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
⊢ Eq.{u_5 + 1} (α := E) (∫ (x : ℝ) in a..b, f x ∂μ) 0
have rw₁ : HSMul.hSMul (α := ℝ) (β := E) (if a ≤ b then 1 else -1) 0 = 0
Tactic: rw [intervalIntegral_eq_integral_uIoc, integral_non_aestronglyMeasurable hf, smul_zero]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic (goal)
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
⊢ Eq.{u_5 + 1} (α := E) (∫ (x : ℝ) in a..b, f x ∂μ) 0
have rw₂ : Eq.{u_5 + 1} (α := E) 0 0
Tactic: rw [intervalIntegral_eq_integral_uIoc, integral_non_aestronglyMeasurable hf, smul_zero]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic (goal)
Goal:
E : Type u_5
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
a b : ℝ
μ : Measure ℝ
f : ℝ → E
⊢ 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 ∂μ)
have 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 ∂μ)
Tactic: cases le_total a b
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic (goal)
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 ∂μ)
⊢ 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 ∂μ)
have 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 ∂μ)
Tactic: cases le_total a b
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic (goal)
Goal:
E : Type u_5
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
a b : ℝ
μ : Measure ℝ
f : ℝ → E
⊢ norm.{u_5} (E := E) (∫ (x : ℝ) in a..b, f x ∂μ) = norm.{u_5} (E := E) (∫ (x : ℝ) in Ι a b, f x ∂μ)
have 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 ∂μ)
Tactic: rw [← norm_integral_min_max, integral_of_le min_le_max, uIoc]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic (goal)
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 ∂μ)
⊢ norm.{u_5} (E := E) (∫ (x : ℝ) in a..b, f x ∂μ) = norm.{u_5} (E := E) (∫ (x : ℝ) in Ι a b, f x ∂μ)
have 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 ∂μ)
Tactic: rw [← norm_integral_min_max, integral_of_le min_le_max, uIoc]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic (goal)
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 ∂μ)
⊢ norm.{u_5} (E := E) (∫ (x : ℝ) in a..b, f x ∂μ) = norm.{u_5} (E := E) (∫ (x : ℝ) in Ι a b, f x ∂μ)
have 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 ∂μ)
Tactic: rw [← norm_integral_min_max, integral_of_le min_le_max, uIoc]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic (goal)
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‖ ∂μ|
have simp : norm.{u_5} (E := E) (∫ (x : ℝ) in Ι a b, f x ∂μ) ≤ norm (E := ℝ) (∫ (x : ℝ) in Ι a b, ‖f x‖ ∂μ)
Tactic: simp only [← Real.norm_eq_abs, norm_integral_eq_norm_integral_uIoc]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic (goal)
Goal:
E : Type u_5
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
a b : ℝ
f : ℝ → E
μ : Measure ℝ
h : a ≤ b
⊢ Eq (α := ℝ) (∫ (x : ℝ) in Ι a b, ‖f x‖ ∂μ) (∫ (x : ℝ) in a..b, ‖f x‖ ∂μ)
have rw : Eq (α := ℝ) (∫ (x : ℝ) in Ioc a b, ‖f x‖ ∂μ) (∫ (x : ℝ) in a..b, ‖f x‖ ∂μ)
Tactic: rw [uIoc_of_le h, integral_of_le h]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic (goal)
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‖ ∂μ)
⊢ Eq (α := ℝ) (∫ (x : ℝ) in Ι a b, ‖f x‖ ∂μ) (∫ (x : ℝ) in a..b, ‖f x‖ ∂μ)
have rw₁ : Eq (α := ℝ) (∫ (x : ℝ) in Ioc a b, ‖f x‖ ∂μ) (∫ (x : ℝ) in Ioc a b, ‖f x‖ ∂μ)
Tactic: rw [uIoc_of_le h, integral_of_le h]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic (goal)
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) (∫ (t : ℝ) in a..b, f t ∂μ) ≤ |∫ (t : ℝ) in a..b, g t ∂μ|
have rw : norm.{u_5} (E := E) (∫ (x : ℝ) in Ι a b, f x ∂μ) ≤ |∫ (x : ℝ) in Ι a b, g x ∂μ|
Tactic: rw [norm_intervalIntegral_eq, abs_intervalIntegral_eq]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic (goal)
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
⊢ norm.{u_5} (E := E) (∫ (t : ℝ) in a..b, f t ∂μ) ≤ ∫ (t : ℝ) in a..b, g t ∂μ
have 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 ∂μ
Tactic: simp only [integral_of_le hab, ← ae_restrict_iff' measurableSet_Ioc] at *
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic (goal)
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) (∫ (x : ℝ) in a..b, f x) ≤ C * |b - a|
have rw : norm.{u_5} (E := E) (@integral _ _ _ _ Real.measurableSpace (Measure.restrict volume (Ι a b)) fun (x : ℝ) ↦ f x) ≤
  C * |b - a|
Tactic: rw [norm_integral_eq_norm_integral_uIoc]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic (goal)
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 _ _ _ _ Real.measurableSpace (Measure.restrict volume (Ι a b)) fun (x : ℝ) ↦ f x) ≤
    C * |b - a|
have h₁ : C * |b - a| = C * Measure.real (m := MeasureSpace.toMeasurableSpace) volume (Ι a b)
Tactic: convert! norm_setIntegral_le_of_norm_le_const_ae' _ h using 1
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic (goal)
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)
⊢ norm.{u_5} (E := E) (@integral _ _ _ _ Real.measurableSpace (Measure.restrict volume (Ι a b)) fun (x : ℝ) ↦ f x) ≤
    C * |b - a|
have convert! : LT.lt (α := ℝ≥0∞) ((volume : (a : Set ℝ) → ℝ≥0∞) (Ι a b) : ℝ≥0∞) (∞ : ℝ≥0∞)
Tactic: convert! norm_setIntegral_le_of_norm_le_const_ae' _ h using 1
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic (goal)
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
⊢ C * |b - a| = C * Measure.real (m := MeasureSpace.toMeasurableSpace) volume (Ι a b)
have h₁ : C * |b - a| = C * Measure.real (m := MeasureSpace.toMeasurableSpace) volume (Ioc (min a b) (max a b))
Tactic: rw [uIoc, Real.volume_real_Ioc_of_le inf_le_sup, max_sub_min_eq_abs]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic (goal)
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))
⊢ C * |b - a| = C * Measure.real (m := MeasureSpace.toMeasurableSpace) volume (Ι a b)
have h₂ : C * |b - a| = C * (max a b - min a b)
Tactic: rw [uIoc, Real.volume_real_Ioc_of_le inf_le_sup, max_sub_min_eq_abs]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic (goal)
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)
⊢ C * |b - a| = C * Measure.real (m := MeasureSpace.toMeasurableSpace) volume (Ι a b)
have h₃ : C * |b - a| = C * |b - a|
Tactic: rw [uIoc, Real.volume_real_Ioc_of_le inf_le_sup, max_sub_min_eq_abs]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic (goal)
Goal:
E : Type u_5
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
a b : ℝ
f : ℝ → E
μ : Measure ℝ
⊢ Eq.{u_5 + 1} (α := E) (∫ (x : ℝ) in a..b, -f x ∂μ) (-∫ (x : ℝ) in a..b, f x ∂μ)
have 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 ∂μ)
Tactic: simp only [intervalIntegral, integral_neg]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic (goal)
Goal:
𝕜 : Type u_2
E : Type u_5
F : Type u_6
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
μ : Measure ℝ
inst_2 : RCLike 𝕜
inst_3 : NormedSpace 𝕜 E
inst_4 : NormedAddCommGroup F
inst_5 : NormedSpace 𝕜 F
a b : ℝ
φ : ℝ → F →L[𝕜] E
hφ : IntervalIntegrable φ μ a b
v : F
⊢ Eq.{u_5 + 1} (α := E) ((∫ (x : ℝ) in a..b, φ x ∂μ : (a : F) → E) v : E)
    (∫ (x : ℝ) in a..b, (φ x : (a : F) → E) v ∂μ : E)
have simp_rw : (HSMul.hSMul (α := ℝ) (β := F →L[𝕜] E) (if a ≤ b then 1 else -1) (∫ (x : ℝ) in Ι a b, φ x ∂μ) : (a : F) → E) v =
  HSMul.hSMul (α := ℝ) (β := E) (if a ≤ b then 1 else -1) (∫ (x : ℝ) in Ι a b, (φ x : (a : F) → E) v ∂μ)
Tactic: simp_rw [intervalIntegral_eq_integral_uIoc, ← integral_apply hφ.def' v, coe_smul', Pi.smul_apply]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic (goal)
Goal:
𝕜 : Type u_2
E : Type u_5
F : Type u_6
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
μ : Measure ℝ
inst_2 : RCLike 𝕜
inst_3 : NormedSpace 𝕜 E
inst_4 : NormedAddCommGroup F
inst_5 : NormedSpace 𝕜 F
a b : ℝ
φ : ℝ → F →L[𝕜] E
hφ : IntervalIntegrable φ μ a b
v : F
simp_rw :
  (HSMul.hSMul (α := ℝ) (β := F →L[𝕜] E) (if a ≤ b then 1 else -1) (∫ (x : ℝ) in Ι a b, φ x ∂μ) : (a : F) → E) v =
    HSMul.hSMul (α := ℝ) (β := E) (if a ≤ b then 1 else -1) (∫ (x : ℝ) in Ι a b, (φ x : (a : F) → E) v ∂μ)
⊢ Eq.{u_5 + 1} (α := E) ((∫ (x : ℝ) in a..b, φ x ∂μ : (a : F) → E) v : E)
    (∫ (x : ℝ) in a..b, (φ x : (a : F) → E) v ∂μ : E)
have simp_rw₁ : (HSMul.hSMul (α := ℝ) (β := F →L[𝕜] E) (if a ≤ b then 1 else -1) (∫ (x : ℝ) in Ι a b, φ x ∂μ) : (a : F) → E) v =
  HSMul.hSMul (α := ℝ) (β := E) (if a ≤ b then 1 else -1) ((∫ (x : ℝ) in Ι a b, φ x ∂μ : (a : F) → E) v : E)
Tactic: simp_rw [intervalIntegral_eq_integral_uIoc, ← integral_apply hφ.def' v, coe_smul', Pi.smul_apply]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic (goal)
Goal:
𝕜 : Type u_2
E : Type u_5
F : Type u_6
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
μ : Measure ℝ
inst_2 : RCLike 𝕜
inst_3 : NormedSpace 𝕜 E
inst_4 : NormedAddCommGroup F
inst_5 : NormedSpace 𝕜 F
a b : ℝ
φ : ℝ → F →L[𝕜] E
hφ : IntervalIntegrable φ μ a b
v : F
simp_rw :
  (HSMul.hSMul (α := ℝ) (β := F →L[𝕜] E) (if a ≤ b then 1 else -1) (∫ (x : ℝ) in Ι a b, φ x ∂μ) : (a : F) → E) v =
    HSMul.hSMul (α := ℝ) (β := E) (if a ≤ b then 1 else -1) (∫ (x : ℝ) in Ι a b, (φ x : (a : F) → E) v ∂μ)
simp_rw₁ :
  (HSMul.hSMul (α := ℝ) (β := F →L[𝕜] E) (if a ≤ b then 1 else -1) (∫ (x : ℝ) in Ι a b, φ x ∂μ) : (a : F) → E) v =
    HSMul.hSMul (α := ℝ) (β := E) (if a ≤ b then 1 else -1) ((∫ (x : ℝ) in Ι a b, φ x ∂μ : (a : F) → E) v : E)
⊢ Eq.{u_5 + 1} (α := E) ((∫ (x : ℝ) in a..b, φ x ∂μ : (a : F) → E) v : E)
    (∫ (x : ℝ) in a..b, (φ x : (a : F) → E) v ∂μ : E)
have simp_rw₂ : HSMul.hSMul (α := ℝ) (β := (a : F) → E) (if a ≤ b then 1 else -1) (⇑(∫ (x : ℝ) in Ι a b, φ x ∂μ) : (a : F) → E) v =
  HSMul.hSMul (α := ℝ) (β := E) (if a ≤ b then 1 else -1) ((∫ (x : ℝ) in Ι a b, φ x ∂μ : (a : F) → E) v : E)
Tactic: simp_rw [intervalIntegral_eq_integral_uIoc, ← integral_apply hφ.def' v, coe_smul', Pi.smul_apply]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic (goal)
Goal:
𝕜 : Type u_2
E : Type u_5
F : Type u_6
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
a b : ℝ
μ : Measure ℝ
f : ℝ → E
inst_2 : RCLike 𝕜
inst_3 : NormedSpace 𝕜 E
inst_4 : NormedAddCommGroup F
inst_5 : NormedSpace 𝕜 F
inst_6 : NormedSpace ℝ F
inst_7 : CompleteSpace F
inst_8 : CompleteSpace E
L : E →L[𝕜] F
hf : IntervalIntegrable f μ a b
⊢ Eq.{u_6 + 1} (α := F) (∫ (x : ℝ) in a..b, (L : (a : E) → F) (f x) ∂μ : F)
    ((L : (a : E) → F) (∫ (x : ℝ) in a..b, f x ∂μ) : F)
have simp_rw : HSub.hSub (α := F) (∫ (x : ℝ) in Ioc a b, (L : (a : E) → F) (f x) ∂μ)
    (∫ (x : ℝ) in Ioc b a, (L : (a : E) → F) (f x) ∂μ) =
  (L : (a : E) → F) (HSub.hSub (α := E) (∫ (x : ℝ) in Ioc a b, f x ∂μ) (∫ (x : ℝ) in Ioc b a, f x ∂μ))
Tactic: simp_rw [intervalIntegral, L.integral_comp_comm hf.1, L.integral_comp_comm hf.2, L.map_sub]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic (goal)
Goal:
𝕜 : Type u_2
E : Type u_5
F : Type u_6
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
a b : ℝ
μ : Measure ℝ
f : ℝ → E
inst_2 : RCLike 𝕜
inst_3 : NormedSpace 𝕜 E
inst_4 : NormedAddCommGroup F
inst_5 : NormedSpace 𝕜 F
inst_6 : NormedSpace ℝ F
inst_7 : CompleteSpace F
inst_8 : CompleteSpace E
L : E →L[𝕜] F
hf : IntervalIntegrable f μ a b
simp_rw :
  HSub.hSub (α := F) (∫ (x : ℝ) in Ioc a b, (L : (a : E) → F) (f x) ∂μ)
      (∫ (x : ℝ) in Ioc b a, (L : (a : E) → F) (f x) ∂μ) =
    (L : (a : E) → F) (HSub.hSub (α := E) (∫ (x : ℝ) in Ioc a b, f x ∂μ) (∫ (x : ℝ) in Ioc b a, f x ∂μ))
⊢ Eq.{u_6 + 1} (α := F) (∫ (x : ℝ) in a..b, (L : (a : E) → F) (f x) ∂μ : F)
    ((L : (a : E) → F) (∫ (x : ℝ) in a..b, f x ∂μ) : F)
have simp_rw₁ : HSub.hSub (α := F) (β := F) ((L : (a : E) → F) (∫ (x : ℝ) in Ioc a b, f x ∂μ) : F)
    (∫ (x : ℝ) in Ioc b a, (L : (a : E) → F) (f x) ∂μ : F) =
  (L : (a : E) → F) (HSub.hSub (α := E) (∫ (x : ℝ) in Ioc a b, f x ∂μ) (∫ (x : ℝ) in Ioc b a, f x ∂μ))
Tactic: simp_rw [intervalIntegral, L.integral_comp_comm hf.1, L.integral_comp_comm hf.2, L.map_sub]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic (goal)
Goal:
𝕜 : Type u_2
E : Type u_5
F : Type u_6
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
a b : ℝ
μ : Measure ℝ
f : ℝ → E
inst_2 : RCLike 𝕜
inst_3 : NormedSpace 𝕜 E
inst_4 : NormedAddCommGroup F
inst_5 : NormedSpace 𝕜 F
inst_6 : NormedSpace ℝ F
inst_7 : CompleteSpace F
inst_8 : CompleteSpace E
L : E →L[𝕜] F
hf : IntervalIntegrable f μ a b
simp_rw :
  HSub.hSub (α := F) (∫ (x : ℝ) in Ioc a b, (L : (a : E) → F) (f x) ∂μ)
      (∫ (x : ℝ) in Ioc b a, (L : (a : E) → F) (f x) ∂μ) =
    (L : (a : E) → F) (HSub.hSub (α := E) (∫ (x : ℝ) in Ioc a b, f x ∂μ) (∫ (x : ℝ) in Ioc b a, f x ∂μ))
simp_rw₁ :
  HSub.hSub (α := F) (β := F) ((L : (a : E) → F) (∫ (x : ℝ) in Ioc a b, f x ∂μ) : F)
      (∫ (x : ℝ) in Ioc b a, (L : (a : E) → F) (f x) ∂μ : F) =
    (L : (a : E) → F) (HSub.hSub (α := E) (∫ (x : ℝ) in Ioc a b, f x ∂μ) (∫ (x : ℝ) in Ioc b a, f x ∂μ))
⊢ Eq.{u_6 + 1} (α := F) (∫ (x : ℝ) in a..b, (L : (a : E) → F) (f x) ∂μ : F)
    ((L : (a : E) → F) (∫ (x : ℝ) in a..b, f x ∂μ) : F)
have simp_rw₂ : HSub.hSub (α := F) (β := F) ((L : (a : E) → F) (∫ (x : ℝ) in Ioc a b, f x ∂μ) : F)
    ((L : (a : E) → F) (∫ (x : ℝ) in Ioc b a, f x ∂μ) : F) =
  (L : (a : E) → F) (HSub.hSub (α := E) (∫ (x : ℝ) in Ioc a b, f x ∂μ) (∫ (x : ℝ) in Ioc b a, f x ∂μ))
Tactic: simp_rw [intervalIntegral, L.integral_comp_comm hf.1, L.integral_comp_comm hf.2, L.map_sub]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic (hypothesis)
Goal:
E : Type u_5
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
a b c : ℝ
f : ℝ → E
hc : c ≠ 0
⊢ ∫ (x : ℝ) in a..b, f (x * c) = HSMul.hSMul (β := E) c⁻¹ (∫ (x : ℝ) in a * c..b * c, f x)
have A : MeasurableEmbedding (β := ℝ) fun (x : ℝ) ↦ x * c
Tactic: have A : MeasurableEmbedding fun x => x * c :=
    (Homeomorph.mulRight₀ c hc).isClosedEmbedding.measurableEmbedding
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic (goal)
Goal:
E : Type u_5
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
a b c : ℝ
f : ℝ → E
hc : c ≠ 0
A : MeasurableEmbedding (β := ℝ) fun (x : ℝ) ↦ x * c
| HSMul.hSMul (β := E) c⁻¹ (∫ (x : ℝ) in a * c..b * c, f x)
have rw : HSMul.hSMul (β := E) c⁻¹
  (∫ (x : ℝ) in a * c..b * c,
    f x ∂HSMul.hSMul (β := Measure ℝ) (ENNReal.ofReal |c|) (Measure.map (fun (x : ℝ) ↦ x * c) volume))
Tactic: rw [← Real.smul_map_volume_mul_right hc]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic (goal)
Goal:
E : Type u_5
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
a b c : ℝ
f : ℝ → E
hc : c ≠ 0
A : MeasurableEmbedding (β := ℝ) fun (x : ℝ) ↦ x * c
⊢ ∫ (x : ℝ) in a..b, f (x * c) = HSMul.hSMul (β := E) c⁻¹ (∫ (x : ℝ) in a * c..b * c, f x)
have conv_rhs : ∫ (x : ℝ) in a..b, f (x * c) =
  HSMul.hSMul (β := E) c⁻¹
    (∫ (x : ℝ) in a * c..b * c,
      f x ∂HSMul.hSMul (β := Measure ℝ) (ENNReal.ofReal |c|) (Measure.map (fun (x : ℝ) ↦ x * c) volume))
Tactic: conv_rhs => rw [← Real.smul_map_volume_mul_right hc]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic (goal)
Goal:
E : Type u_5
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
a b c : ℝ
f : ℝ → E
hc : c ≠ 0
A : MeasurableEmbedding (β := ℝ) fun (x : ℝ) ↦ x * c
⊢ ∫ (x : ℝ) in a..b, f (x * c) =
    HSMul.hSMul (β := E) c⁻¹
      (∫ (x : ℝ) in a * c..b * c,
        f x ∂HSMul.hSMul (β := Measure ℝ) (ENNReal.ofReal |c|) (Measure.map (fun (x : ℝ) ↦ x * c) volume))
have simp_rw : HSub.hSub (α := E) (@integral _ _ _ _ Real.measurableSpace (Measure.restrict volume (Ioc a b)) fun (x : ℝ) ↦ f (x * c))
    (@integral _ _ _ _ Real.measurableSpace (Measure.restrict volume (Ioc b a)) fun (x : ℝ) ↦ f (x * c)) =
  c⁻¹ •
    |c| •
      HSub.hSub (α := E)
        (@integral _ _ _ _ Real.measurableSpace
          (Measure.restrict volume ((fun (x : ℝ) ↦ x * c) ⁻¹' Ioc (a * c) (b * c))) fun (x : ℝ) ↦ f (x * c))
        (@integral _ _ _ _ Real.measurableSpace
          (Measure.restrict volume ((fun (x : ℝ) ↦ x * c) ⁻¹' Ioc (b * c) (a * c))) fun (x : ℝ) ↦ f (x * c))
Tactic: simp_rw [integral_smul_measure, intervalIntegral, A.setIntegral_map,
    ENNReal.toReal_ofReal (abs_nonneg c)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic (goal)
Goal:
E : Type u_5
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
a b c : ℝ
f : ℝ → E
hc : c ≠ 0
A : MeasurableEmbedding (β := ℝ) fun (x : ℝ) ↦ x * c
⊢ HSub.hSub (α := E)
      (@integral _ _ _ _ Real.measurableSpace (Measure.restrict volume (Ioc a b)) fun (x : ℝ) ↦ f (x * c))
      (@integral _ _ _ _ Real.measurableSpace (Measure.restrict volume (Ioc b a)) fun (x : ℝ) ↦ f (x * c)) =
    c⁻¹ •
      |c| •
        HSub.hSub (α := E)
          (@integral _ _ _ _ Real.measurableSpace
            (Measure.restrict volume ((fun (x : ℝ) ↦ x * c) ⁻¹' Ioc (a * c) (b * c))) fun (x : ℝ) ↦ f (x * c))
          (@integral _ _ _ _ Real.measurableSpace
            (Measure.restrict volume ((fun (x : ℝ) ↦ x * c) ⁻¹' Ioc (b * c) (a * c))) fun (x : ℝ) ↦ f (x * c))
have inl : ∀ (h : c < 0),
  HSub.hSub (α := E)
      (@integral _ _ _ _ Real.measurableSpace (Measure.restrict volume (Ioc a b)) fun (x : ℝ) ↦ f (x * c))
      (@integral _ _ _ _ Real.measurableSpace (Measure.restrict volume (Ioc b a)) fun (x : ℝ) ↦ f (x * c)) =
    c⁻¹ •
      |c| •
        HSub.hSub (α := E)
          (@integral _ _ _ _ Real.measurableSpace
            (Measure.restrict volume ((fun (x : ℝ) ↦ x * c) ⁻¹' Ioc (a * c) (b * c))) fun (x : ℝ) ↦ f (x * c))
          (@integral _ _ _ _ Real.measurableSpace
            (Measure.restrict volume ((fun (x : ℝ) ↦ x * c) ⁻¹' Ioc (b * c) (a * c))) fun (x : ℝ) ↦ f (x * c))
Tactic: rcases hc.lt_or_gt with h | h