awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntegralEqImproper (goal)
Goal:
A : Type u_1
inst : NormedRing A
inst_1 : NormedAlgebra ℝ A
a : ℝ
a' b' : A
u v u' v' : ℝ → A
inst_2 : CompleteSpace A
hu : ∀ x ∈ Iio a, HasDerivAt u (u' x) x
hv : ∀ x ∈ Iio a, HasDerivAt v (v' x) x
huv : IntegrableOn (mα := MeasureSpace.toMeasurableSpace) (u' * v + u * v') (Iic a) volume
h_zero : Tendsto (u * v) (𝓝[Iic a \ {a}] a) (𝓝 a')
h_infty : Tendsto (u * v) atBot (𝓝 b')
f : (a : ℝ) → A := Function.update (β := fun (a : ℝ) ↦ A) (u * v) a a'
hderiv : ∀ x ∈ Iio a, HasDerivAt f (u' x * v x + u x * v' x) x
⊢ u * v =ᶠ[atBot] f
have h : ∀ (x : ℝ) (hx : x < a), (u * v) x = f x
Tactic: filter_upwards [Iio_mem_atBot a] with x (hx : x < a)
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntegralEqImproper (hypothesis)
Goal:
A : Type u_1
inst : NormedRing A
inst_1 : NormedAlgebra ℝ A
a : ℝ
a' b' : A
u v u' v' : ℝ → A
inst_2 : CompleteSpace A
hu : ∀ x ∈ Iio a, HasDerivAt u (u' x) x
hv : ∀ x ∈ Iio a, HasDerivAt v (v' x) x
huv : IntegrableOn (mα := MeasureSpace.toMeasurableSpace) (u' * v + u * v') (Iic a) volume
h_zero : Tendsto (u * v) (𝓝[Iic a \ {a}] a) (𝓝 a')
h_infty : Tendsto (u * v) atBot (𝓝 b')
f : (a : ℝ) → A := Function.update (β := fun (a : ℝ) ↦ A) (u * v) a a'
hderiv : ∀ x ∈ Iio a, HasDerivAt f (u' x * v x + u x * v' x) x
⊢ (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Iic a)) fun (x : ℝ) ↦
      u' x * v x + u x * v' x) =
    a' - b'
have htendsto : Tendsto f atBot (𝓝 b')
Tactic: have htendsto : Tendsto f atBot (𝓝 b') := by
    apply h_infty.congr'
    filter_upwards [Iio_mem_atBot a] with x (hx : x < a)
    exact (Function.update_of_ne (ne_of_lt hx) a' (u * v)).symm
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntegralEqImproper (hypothesis)
Goal:
A : Type u_1
inst : NormedRing A
inst_1 : NormedAlgebra ℝ A
a : ℝ
a' b' : A
u v u' v' : ℝ → A
inst_2 : CompleteSpace A
hu : ∀ x ∈ Iio a, HasDerivAt u (u' x) x
hv : ∀ x ∈ Iio a, HasDerivAt v (v' x) x
huv' : IntegrableOn (mα := MeasureSpace.toMeasurableSpace) (u * v') (Iic a) volume
hu'v : IntegrableOn (mα := MeasureSpace.toMeasurableSpace) (u' * v) (Iic a) volume
h_zero : Tendsto (u * v) (𝓝[<] a) (𝓝 a')
h_infty : Tendsto (u * v) atBot (𝓝 b')
⊢ (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Iic a)) fun (x : ℝ) ↦ u x * v' x) =
    a' - b' -
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Iic a)) fun (x : ℝ) ↦ u' x * v x
have huv'₁ : IntegrableOn.{0, u_1} (ε := A) (mα := MeasureSpace.toMeasurableSpace) (fun (i : ℝ) ↦ u i * v' i) (Iic a) volume
Tactic: rw [Pi.mul_def] at huv' hu'v
Cleared hypotheses: huv', hu'v, h_zero, h_infty
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntegralEqImproper (hypothesis)
Goal:
A : Type u_1
inst : NormedRing A
inst_1 : NormedAlgebra ℝ A
a : ℝ
a' b' : A
u v u' v' : ℝ → A
inst_2 : CompleteSpace A
hu : ∀ x ∈ Iio a, HasDerivAt u (u' x) x
hv : ∀ x ∈ Iio a, HasDerivAt v (v' x) x
huv' : IntegrableOn (mα := MeasureSpace.toMeasurableSpace) (u * v') (Iic a) volume
hu'v : IntegrableOn (mα := MeasureSpace.toMeasurableSpace) (u' * v) (Iic a) volume
h_zero : Tendsto (u * v) (𝓝[<] a) (𝓝 a')
h_infty : Tendsto (u * v) atBot (𝓝 b')
huv'₁ : IntegrableOn.{0, u_1} (ε := A) (mα := MeasureSpace.toMeasurableSpace) (fun (i : ℝ) ↦ u i * v' i) (Iic a) volume
⊢ (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Iic a)) fun (x : ℝ) ↦ u x * v' x) =
    a' - b' -
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Iic a)) fun (x : ℝ) ↦ u' x * v x
have hu'v₁ : IntegrableOn.{0, u_1} (ε := A) (mα := MeasureSpace.toMeasurableSpace) (fun (i : ℝ) ↦ u' i * v i) (Iic a) volume
Tactic: rw [Pi.mul_def] at huv' hu'v
Cleared hypotheses: huv', hu'v, h_zero, h_infty
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntegralEqImproper (goal)
Goal:
A : Type u_1
inst : NormedRing A
inst_1 : NormedAlgebra ℝ A
a : ℝ
a' b' : A
u v u' v' : ℝ → A
inst_2 : CompleteSpace A
hu : ∀ x ∈ Iio a, HasDerivAt u (u' x) x
hv : ∀ x ∈ Iio a, HasDerivAt v (v' x) x
huv' : IntegrableOn.{0, u_1} (ε := A) (mα := MeasureSpace.toMeasurableSpace) (fun (i : ℝ) ↦ u i * v' i) (Iic a) volume
hu'v : IntegrableOn.{0, u_1} (ε := A) (mα := MeasureSpace.toMeasurableSpace) (fun (i : ℝ) ↦ u' i * v i) (Iic a) volume
h_zero : Tendsto (u * v) (𝓝[<] a) (𝓝 a')
h_infty : Tendsto (u * v) atBot (𝓝 b')
⊢ (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Iic a)) fun (x : ℝ) ↦ u x * v' x) =
    a' - b' -
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Iic a)) fun (x : ℝ) ↦ u' x * v x
have rw : (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Iic a)) fun (a : ℝ) ↦
    u a * v' a + u' a * v a) =
  a' - b'
Tactic: rw [eq_sub_iff_add_eq, ← integral_add huv' hu'v]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalAverage (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
⊢ Eq.{u_1 + 1} (α := E) (⨍ (x : ℝ) in a..b, f x) (⨍ (x : ℝ) in b..a, f x)
have rw : HSMul.hSMul (β := E) (Measure.real (m := MeasureSpace.toMeasurableSpace) volume (Ι a b))⁻¹
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ι a b)) fun (x : ℝ) ↦ f x) =
  ⨍ (x : ℝ) in b..a, f x
Tactic: rw [setAverage_eq, setAverage_eq, uIoc_comm]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalAverage (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
rw :
  HSMul.hSMul (β := E) (Measure.real (m := MeasureSpace.toMeasurableSpace) volume (Ι a b))⁻¹
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ι a b)) fun (x : ℝ) ↦ f x) =
    ⨍ (x : ℝ) in b..a, f x
⊢ Eq.{u_1 + 1} (α := E) (⨍ (x : ℝ) in a..b, f x) (⨍ (x : ℝ) in b..a, f x)
have rw₁ : HSMul.hSMul (β := E) (Measure.real (m := MeasureSpace.toMeasurableSpace) volume (Ι a b))⁻¹
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ι a b)) fun (x : ℝ) ↦ f x) =
  HSMul.hSMul (β := E) (Measure.real (m := MeasureSpace.toMeasurableSpace) volume (Ι b a))⁻¹
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ι b a)) fun (x : ℝ) ↦ f x)
Tactic: rw [setAverage_eq, setAverage_eq, uIoc_comm]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalAverage (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
rw :
  HSMul.hSMul (β := E) (Measure.real (m := MeasureSpace.toMeasurableSpace) volume (Ι a b))⁻¹
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ι a b)) fun (x : ℝ) ↦ f x) =
    ⨍ (x : ℝ) in b..a, f x
rw₁ :
  HSMul.hSMul (β := E) (Measure.real (m := MeasureSpace.toMeasurableSpace) volume (Ι a b))⁻¹
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ι a b)) fun (x : ℝ) ↦ f x) =
    HSMul.hSMul (β := E) (Measure.real (m := MeasureSpace.toMeasurableSpace) volume (Ι b a))⁻¹
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ι b a)) fun (x : ℝ) ↦ f x)
⊢ Eq.{u_1 + 1} (α := E) (⨍ (x : ℝ) in a..b, f x) (⨍ (x : ℝ) in b..a, f x)
have rw₂ : HSMul.hSMul (β := E) (Measure.real (m := MeasureSpace.toMeasurableSpace) volume (Ι b a))⁻¹
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ι b a)) fun (x : ℝ) ↦ f x) =
  HSMul.hSMul (β := E) (Measure.real (m := MeasureSpace.toMeasurableSpace) volume (Ι b a))⁻¹
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ι b a)) fun (x : ℝ) ↦ f x)
Tactic: rw [setAverage_eq, setAverage_eq, uIoc_comm]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalAverage (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
⊢ ⨍ (x : ℝ) in a..b, f x = HSMul.hSMul (β := E) (b - a)⁻¹ (∫ (x : ℝ) in a..b, f x)
have inl : ∀ (h : a ≤ b), ⨍ (x : ℝ) in a..b, f x = HSMul.hSMul (β := E) (b - a)⁻¹ (∫ (x : ℝ) in a..b, f x)
Tactic: rcases le_or_gt a b with h | h
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalAverage (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
inl : ∀ (h : a ≤ b), ⨍ (x : ℝ) in a..b, f x = HSMul.hSMul (β := E) (b - a)⁻¹ (∫ (x : ℝ) in a..b, f x)
⊢ ⨍ (x : ℝ) in a..b, f x = HSMul.hSMul (β := E) (b - a)⁻¹ (∫ (x : ℝ) in a..b, f x)
have inr : ∀ (h : b < a), ⨍ (x : ℝ) in a..b, f x = HSMul.hSMul (β := E) (b - a)⁻¹ (∫ (x : ℝ) in a..b, f x)
Tactic: rcases le_or_gt a b with h | h
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalAverage (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
h : a ≤ b
⊢ ⨍ (x : ℝ) in a..b, f x = HSMul.hSMul (β := E) (b - a)⁻¹ (∫ (x : ℝ) in a..b, f x)
have inl : HSMul.hSMul (β := E) (Measure.real (m := MeasureSpace.toMeasurableSpace) volume (Ι a b))⁻¹
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ι a b)) fun (x : ℝ) ↦ f x) =
  HSMul.hSMul (β := E) (b - a)⁻¹ (∫ (x : ℝ) in a..b, f x)
Tactic: rw [setAverage_eq, uIoc_of_le h, Real.volume_real_Ioc_of_le h, integral_of_le h]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalAverage (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
h : a ≤ b
inl :
  HSMul.hSMul (β := E) (Measure.real (m := MeasureSpace.toMeasurableSpace) volume (Ι a b))⁻¹
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ι a b)) fun (x : ℝ) ↦ f x) =
    HSMul.hSMul (β := E) (b - a)⁻¹ (∫ (x : ℝ) in a..b, f x)
⊢ ⨍ (x : ℝ) in a..b, f x = HSMul.hSMul (β := E) (b - a)⁻¹ (∫ (x : ℝ) in a..b, f x)
have inl₁ : HSMul.hSMul (β := E) (Measure.real (m := MeasureSpace.toMeasurableSpace) volume (Ioc a b))⁻¹
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioc a b)) fun (x : ℝ) ↦ f x) =
  HSMul.hSMul (β := E) (b - a)⁻¹ (∫ (x : ℝ) in a..b, f x)
Tactic: rw [setAverage_eq, uIoc_of_le h, Real.volume_real_Ioc_of_le h, integral_of_le h]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalAverage (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
h : a ≤ b
inl :
  HSMul.hSMul (β := E) (Measure.real (m := MeasureSpace.toMeasurableSpace) volume (Ι a b))⁻¹
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ι a b)) fun (x : ℝ) ↦ f x) =
    HSMul.hSMul (β := E) (b - a)⁻¹ (∫ (x : ℝ) in a..b, f x)
inl₁ :
  HSMul.hSMul (β := E) (Measure.real (m := MeasureSpace.toMeasurableSpace) volume (Ioc a b))⁻¹
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioc a b)) fun (x : ℝ) ↦ f x) =
    HSMul.hSMul (β := E) (b - a)⁻¹ (∫ (x : ℝ) in a..b, f x)
⊢ ⨍ (x : ℝ) in a..b, f x = HSMul.hSMul (β := E) (b - a)⁻¹ (∫ (x : ℝ) in a..b, f x)
have inl₂ : HSMul.hSMul (β := E) (b - a)⁻¹
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioc a b)) fun (x : ℝ) ↦ f x) =
  HSMul.hSMul (β := E) (b - a)⁻¹ (∫ (x : ℝ) in a..b, f x)
Tactic: rw [setAverage_eq, uIoc_of_le h, Real.volume_real_Ioc_of_le h, integral_of_le h]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalAverage (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
h : a ≤ b
inl :
  HSMul.hSMul (β := E) (Measure.real (m := MeasureSpace.toMeasurableSpace) volume (Ι a b))⁻¹
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ι a b)) fun (x : ℝ) ↦ f x) =
    HSMul.hSMul (β := E) (b - a)⁻¹ (∫ (x : ℝ) in a..b, f x)
inl₁ :
  HSMul.hSMul (β := E) (Measure.real (m := MeasureSpace.toMeasurableSpace) volume (Ioc a b))⁻¹
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioc a b)) fun (x : ℝ) ↦ f x) =
    HSMul.hSMul (β := E) (b - a)⁻¹ (∫ (x : ℝ) in a..b, f x)
inl₂ :
  HSMul.hSMul (β := E) (b - a)⁻¹
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioc a b)) fun (x : ℝ) ↦ f x) =
    HSMul.hSMul (β := E) (b - a)⁻¹ (∫ (x : ℝ) in a..b, f x)
⊢ ⨍ (x : ℝ) in a..b, f x = HSMul.hSMul (β := E) (b - a)⁻¹ (∫ (x : ℝ) in a..b, f x)
have inl₃ : HSMul.hSMul (β := E) (b - a)⁻¹
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioc a b)) fun (x : ℝ) ↦ f x) =
  HSMul.hSMul (β := E) (b - a)⁻¹
    (@integral _ _ _ _ Real.measurableSpace (Measure.restrict volume (Ioc a b)) fun (x : ℝ) ↦ f x)
Tactic: rw [setAverage_eq, uIoc_of_le h, Real.volume_real_Ioc_of_le h, integral_of_le h]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalAverage (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
h : b < a
⊢ ⨍ (x : ℝ) in a..b, f x = HSMul.hSMul (β := E) (b - a)⁻¹ (∫ (x : ℝ) in a..b, f x)
have inr : HSMul.hSMul (β := E) (Measure.real (m := MeasureSpace.toMeasurableSpace) volume (Ι a b))⁻¹
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ι a b)) fun (x : ℝ) ↦ f x) =
  HSMul.hSMul (β := E) (b - a)⁻¹ (∫ (x : ℝ) in a..b, f x)
Tactic: rw [setAverage_eq, uIoc_of_ge h.le, Real.volume_real_Ioc_of_le h.le, integral_of_ge h.le,
      smul_neg, ← neg_smul, ← inv_neg, neg_sub]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalAverage (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
h : b < a
inr :
  HSMul.hSMul (β := E) (Measure.real (m := MeasureSpace.toMeasurableSpace) volume (Ι a b))⁻¹
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ι a b)) fun (x : ℝ) ↦ f x) =
    HSMul.hSMul (β := E) (b - a)⁻¹ (∫ (x : ℝ) in a..b, f x)
⊢ ⨍ (x : ℝ) in a..b, f x = HSMul.hSMul (β := E) (b - a)⁻¹ (∫ (x : ℝ) in a..b, f x)
have inr₁ : HSMul.hSMul (β := E) (Measure.real (m := MeasureSpace.toMeasurableSpace) volume (Ioc b a))⁻¹
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioc b a)) fun (x : ℝ) ↦ f x) =
  HSMul.hSMul (β := E) (b - a)⁻¹ (∫ (x : ℝ) in a..b, f x)
Tactic: rw [setAverage_eq, uIoc_of_ge h.le, Real.volume_real_Ioc_of_le h.le, integral_of_ge h.le,
      smul_neg, ← neg_smul, ← inv_neg, neg_sub]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalAverage (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
h : b < a
inr :
  HSMul.hSMul (β := E) (Measure.real (m := MeasureSpace.toMeasurableSpace) volume (Ι a b))⁻¹
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ι a b)) fun (x : ℝ) ↦ f x) =
    HSMul.hSMul (β := E) (b - a)⁻¹ (∫ (x : ℝ) in a..b, f x)
inr₁ :
  HSMul.hSMul (β := E) (Measure.real (m := MeasureSpace.toMeasurableSpace) volume (Ioc b a))⁻¹
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioc b a)) fun (x : ℝ) ↦ f x) =
    HSMul.hSMul (β := E) (b - a)⁻¹ (∫ (x : ℝ) in a..b, f x)
⊢ ⨍ (x : ℝ) in a..b, f x = HSMul.hSMul (β := E) (b - a)⁻¹ (∫ (x : ℝ) in a..b, f x)
have inr₂ : HSMul.hSMul (β := E) (a - b)⁻¹
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioc b a)) fun (x : ℝ) ↦ f x) =
  HSMul.hSMul (β := E) (b - a)⁻¹ (∫ (x : ℝ) in a..b, f x)
Tactic: rw [setAverage_eq, uIoc_of_ge h.le, Real.volume_real_Ioc_of_le h.le, integral_of_ge h.le,
      smul_neg, ← neg_smul, ← inv_neg, neg_sub]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalAverage (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
h : b < a
inr :
  HSMul.hSMul (β := E) (Measure.real (m := MeasureSpace.toMeasurableSpace) volume (Ι a b))⁻¹
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ι a b)) fun (x : ℝ) ↦ f x) =
    HSMul.hSMul (β := E) (b - a)⁻¹ (∫ (x : ℝ) in a..b, f x)
inr₁ :
  HSMul.hSMul (β := E) (Measure.real (m := MeasureSpace.toMeasurableSpace) volume (Ioc b a))⁻¹
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioc b a)) fun (x : ℝ) ↦ f x) =
    HSMul.hSMul (β := E) (b - a)⁻¹ (∫ (x : ℝ) in a..b, f x)
inr₂ :
  HSMul.hSMul (β := E) (a - b)⁻¹
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioc b a)) fun (x : ℝ) ↦ f x) =
    HSMul.hSMul (β := E) (b - a)⁻¹ (∫ (x : ℝ) in a..b, f x)
⊢ ⨍ (x : ℝ) in a..b, f x = HSMul.hSMul (β := E) (b - a)⁻¹ (∫ (x : ℝ) in a..b, f x)
have inr₃ : HSMul.hSMul (β := E) (a - b)⁻¹
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioc b a)) fun (x : ℝ) ↦ f x) =
  HSMul.hSMul (β := E) (b - a)⁻¹
    (-@integral _ _ _ _ Real.measurableSpace (Measure.restrict volume (Ioc b a)) fun (x : ℝ) ↦ f x)
Tactic: rw [setAverage_eq, uIoc_of_ge h.le, Real.volume_real_Ioc_of_le h.le, integral_of_ge h.le,
      smul_neg, ← neg_smul, ← inv_neg, neg_sub]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalAverage (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
h : b < a
inr :
  HSMul.hSMul (β := E) (Measure.real (m := MeasureSpace.toMeasurableSpace) volume (Ι a b))⁻¹
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ι a b)) fun (x : ℝ) ↦ f x) =
    HSMul.hSMul (β := E) (b - a)⁻¹ (∫ (x : ℝ) in a..b, f x)
inr₁ :
  HSMul.hSMul (β := E) (Measure.real (m := MeasureSpace.toMeasurableSpace) volume (Ioc b a))⁻¹
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioc b a)) fun (x : ℝ) ↦ f x) =
    HSMul.hSMul (β := E) (b - a)⁻¹ (∫ (x : ℝ) in a..b, f x)
inr₂ :
  HSMul.hSMul (β := E) (a - b)⁻¹
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioc b a)) fun (x : ℝ) ↦ f x) =
    HSMul.hSMul (β := E) (b - a)⁻¹ (∫ (x : ℝ) in a..b, f x)
inr₃ :
  HSMul.hSMul (β := E) (a - b)⁻¹
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioc b a)) fun (x : ℝ) ↦ f x) =
    HSMul.hSMul (β := E) (b - a)⁻¹
      (-@integral _ _ _ _ Real.measurableSpace (Measure.restrict volume (Ioc b a)) fun (x : ℝ) ↦ f x)
⊢ ⨍ (x : ℝ) in a..b, f x = HSMul.hSMul (β := E) (b - a)⁻¹ (∫ (x : ℝ) in a..b, f x)
have inr₄ : HSMul.hSMul (β := E) (a - b)⁻¹
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioc b a)) fun (x : ℝ) ↦ f x) =
  -HSMul.hSMul (β := E) (b - a)⁻¹
      (@integral _ _ _ _ Real.measurableSpace (Measure.restrict volume (Ioc b a)) fun (x : ℝ) ↦ f x)
Tactic: rw [setAverage_eq, uIoc_of_ge h.le, Real.volume_real_Ioc_of_le h.le, integral_of_ge h.le,
      smul_neg, ← neg_smul, ← inv_neg, neg_sub]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalAverage (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
h : b < a
inr :
  HSMul.hSMul (β := E) (Measure.real (m := MeasureSpace.toMeasurableSpace) volume (Ι a b))⁻¹
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ι a b)) fun (x : ℝ) ↦ f x) =
    HSMul.hSMul (β := E) (b - a)⁻¹ (∫ (x : ℝ) in a..b, f x)
inr₁ :
  HSMul.hSMul (β := E) (Measure.real (m := MeasureSpace.toMeasurableSpace) volume (Ioc b a))⁻¹
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioc b a)) fun (x : ℝ) ↦ f x) =
    HSMul.hSMul (β := E) (b - a)⁻¹ (∫ (x : ℝ) in a..b, f x)
inr₂ :
  HSMul.hSMul (β := E) (a - b)⁻¹
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioc b a)) fun (x : ℝ) ↦ f x) =
    HSMul.hSMul (β := E) (b - a)⁻¹ (∫ (x : ℝ) in a..b, f x)
inr₃ :
  HSMul.hSMul (β := E) (a - b)⁻¹
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioc b a)) fun (x : ℝ) ↦ f x) =
    HSMul.hSMul (β := E) (b - a)⁻¹
      (-@integral _ _ _ _ Real.measurableSpace (Measure.restrict volume (Ioc b a)) fun (x : ℝ) ↦ f x)
inr₄ :
  HSMul.hSMul (β := E) (a - b)⁻¹
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioc b a)) fun (x : ℝ) ↦ f x) =
    -HSMul.hSMul (β := E) (b - a)⁻¹
        (@integral _ _ _ _ Real.measurableSpace (Measure.restrict volume (Ioc b a)) fun (x : ℝ) ↦ f x)
⊢ ⨍ (x : ℝ) in a..b, f x = HSMul.hSMul (β := E) (b - a)⁻¹ (∫ (x : ℝ) in a..b, f x)
have inr₅ : HSMul.hSMul (β := E) (a - b)⁻¹
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioc b a)) fun (x : ℝ) ↦ f x) =
  HSMul.hSMul (β := E) (-(b - a)⁻¹)
    (@integral _ _ _ _ Real.measurableSpace (Measure.restrict volume (Ioc b a)) fun (x : ℝ) ↦ f x)
Tactic: rw [setAverage_eq, uIoc_of_ge h.le, Real.volume_real_Ioc_of_le h.le, integral_of_ge h.le,
      smul_neg, ← neg_smul, ← inv_neg, neg_sub]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalAverage (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
h : b < a
inr :
  HSMul.hSMul (β := E) (Measure.real (m := MeasureSpace.toMeasurableSpace) volume (Ι a b))⁻¹
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ι a b)) fun (x : ℝ) ↦ f x) =
    HSMul.hSMul (β := E) (b - a)⁻¹ (∫ (x : ℝ) in a..b, f x)
inr₁ :
  HSMul.hSMul (β := E) (Measure.real (m := MeasureSpace.toMeasurableSpace) volume (Ioc b a))⁻¹
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioc b a)) fun (x : ℝ) ↦ f x) =
    HSMul.hSMul (β := E) (b - a)⁻¹ (∫ (x : ℝ) in a..b, f x)
inr₂ :
  HSMul.hSMul (β := E) (a - b)⁻¹
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioc b a)) fun (x : ℝ) ↦ f x) =
    HSMul.hSMul (β := E) (b - a)⁻¹ (∫ (x : ℝ) in a..b, f x)
inr₃ :
  HSMul.hSMul (β := E) (a - b)⁻¹
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioc b a)) fun (x : ℝ) ↦ f x) =
    HSMul.hSMul (β := E) (b - a)⁻¹
      (-@integral _ _ _ _ Real.measurableSpace (Measure.restrict volume (Ioc b a)) fun (x : ℝ) ↦ f x)
inr₄ :
  HSMul.hSMul (β := E) (a - b)⁻¹
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioc b a)) fun (x : ℝ) ↦ f x) =
    -HSMul.hSMul (β := E) (b - a)⁻¹
        (@integral _ _ _ _ Real.measurableSpace (Measure.restrict volume (Ioc b a)) fun (x : ℝ) ↦ f x)
inr₅ :
  HSMul.hSMul (β := E) (a - b)⁻¹
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioc b a)) fun (x : ℝ) ↦ f x) =
    HSMul.hSMul (β := E) (-(b - a)⁻¹)
      (@integral _ _ _ _ Real.measurableSpace (Measure.restrict volume (Ioc b a)) fun (x : ℝ) ↦ f x)
⊢ ⨍ (x : ℝ) in a..b, f x = HSMul.hSMul (β := E) (b - a)⁻¹ (∫ (x : ℝ) in a..b, f x)
have inr₆ : HSMul.hSMul (β := E) (a - b)⁻¹
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioc b a)) fun (x : ℝ) ↦ f x) =
  HSMul.hSMul (β := E) (-(b - a))⁻¹
    (@integral _ _ _ _ Real.measurableSpace (Measure.restrict volume (Ioc b a)) fun (x : ℝ) ↦ f x)
Tactic: rw [setAverage_eq, uIoc_of_ge h.le, Real.volume_real_Ioc_of_le h.le, integral_of_ge h.le,
      smul_neg, ← neg_smul, ← inv_neg, neg_sub]