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
a b c : ℝ
f : ℝ → E
hc : c ≠ 0
A : MeasurableEmbedding (β := ℝ) fun (x : ℝ) ↦ x * c
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))
⊢ 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 inr : ∀ (h : 0 < 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))
Tactic: rcases hc.lt_or_gt with h | 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
c : ℝ
⊢ HSMul.hSMul (β := E) c (∫ (x : ℝ) in a..b, f (x * c)) = ∫ (x : ℝ) in a * c..b * c, f x
have pos : ∀ (hc : c = 0), HSMul.hSMul (β := E) c (∫ (x : ℝ) in a..b, f (x * c)) = ∫ (x : ℝ) in a * c..b * c, f x
Tactic: by_cases hc : c = 0
-- 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
c : ℝ
pos : ∀ (hc : c = 0), HSMul.hSMul (β := E) c (∫ (x : ℝ) in a..b, f (x * c)) = ∫ (x : ℝ) in a * c..b * c, f x
⊢ HSMul.hSMul (β := E) c (∫ (x : ℝ) in a..b, f (x * c)) = ∫ (x : ℝ) in a * c..b * c, f x
have neg : ∀ (hc : ¬c = 0), HSMul.hSMul (β := E) c (∫ (x : ℝ) in a..b, f (x * c)) = ∫ (x : ℝ) in a * c..b * c, f x
Tactic: by_cases hc : c = 0
-- 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
c : ℝ
⊢ HSMul.hSMul (β := E) c (∫ (x : ℝ) in a..b, f (c * x)) = ∫ (x : ℝ) in c * a..c * b, f x
have pos : ∀ (hc : c = 0), HSMul.hSMul (β := E) c (∫ (x : ℝ) in a..b, f (c * x)) = ∫ (x : ℝ) in c * a..c * b, f x
Tactic: by_cases hc : c = 0
-- 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
c : ℝ
pos : ∀ (hc : c = 0), HSMul.hSMul (β := E) c (∫ (x : ℝ) in a..b, f (c * x)) = ∫ (x : ℝ) in c * a..c * b, f x
⊢ HSMul.hSMul (β := E) c (∫ (x : ℝ) in a..b, f (c * x)) = ∫ (x : ℝ) in c * a..c * b, f x
have neg : ∀ (hc : ¬c = 0), HSMul.hSMul (β := E) c (∫ (x : ℝ) in a..b, f (c * x)) = ∫ (x : ℝ) in c * a..c * b, f x
Tactic: by_cases hc : c = 0
-- 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
c : ℝ
⊢ HSMul.hSMul (β := E) c⁻¹ (∫ (x : ℝ) in a..b, f (x / c)) = ∫ (x : ℝ) in a / c..b / c, f x
have pos : ∀ (hc : c = 0), HSMul.hSMul (β := E) c⁻¹ (∫ (x : ℝ) in a..b, f (x / c)) = ∫ (x : ℝ) in a / c..b / c, f x
Tactic: by_cases hc : c = 0
-- 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
c : ℝ
pos : ∀ (hc : c = 0), HSMul.hSMul (β := E) c⁻¹ (∫ (x : ℝ) in a..b, f (x / c)) = ∫ (x : ℝ) in a / c..b / c, f x
⊢ HSMul.hSMul (β := E) c⁻¹ (∫ (x : ℝ) in a..b, f (x / c)) = ∫ (x : ℝ) in a / c..b / c, f x
have neg : ∀ (hc : ¬c = 0), HSMul.hSMul (β := E) c⁻¹ (∫ (x : ℝ) in a..b, f (x / c)) = ∫ (x : ℝ) in a / c..b / c, f x
Tactic: by_cases hc : c = 0
-- 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
d : ℝ
A : MeasurableEmbedding (β := ℝ) fun (x : ℝ) ↦ x + d
⊢ Eq.{u_5 + 1} (α := E) (∫ (x : ℝ) in a + d..b + d, f x ∂Measure.map (fun (x : ℝ) ↦ x + d) volume)
    (∫ (x : ℝ) in a + d..b + d, f x)
have rw : Eq.{u_5 + 1} (α := E) (∫ (x : ℝ) in a + d..b + d, f x) (∫ (x : ℝ) in a + d..b + d, f x)
Tactic: rw [map_add_right_eq_self]
-- 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
d : ℝ
⊢ ∫ (x : ℝ) in a..b, f (c * x + d) = HSMul.hSMul (β := E) c⁻¹ (∫ (x : ℝ) in c * a + d..c * b + d, f x)
have rw : ∫ (x : ℝ) in a..b, f (c * x + d) = HSMul.hSMul (β := E) c⁻¹ (∫ (x : ℝ) in c * a..c * b, f (x + d))
Tactic: rw [← integral_comp_add_right, ← integral_comp_mul_left _ 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
d : ℝ
rw : ∫ (x : ℝ) in a..b, f (c * x + d) = HSMul.hSMul (β := E) c⁻¹ (∫ (x : ℝ) in c * a..c * b, f (x + d))
⊢ ∫ (x : ℝ) in a..b, f (c * x + d) = HSMul.hSMul (β := E) c⁻¹ (∫ (x : ℝ) in c * a + d..c * b + d, f x)
have rw₁ : Eq.{u_5 + 1} (α := E) (∫ (x : ℝ) in a..b, f (c * x + d)) (∫ (x : ℝ) in a..b, f (c * x + d))
Tactic: rw [← integral_comp_add_right, ← integral_comp_mul_left _ 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 : ℝ
f : ℝ → E
c d : ℝ
⊢ HSMul.hSMul (β := E) c (∫ (x : ℝ) in a..b, f (c * x + d)) = ∫ (x : ℝ) in c * a + d..c * b + d, f x
have pos : ∀ (hc : c = 0), HSMul.hSMul (β := E) c (∫ (x : ℝ) in a..b, f (c * x + d)) = ∫ (x : ℝ) in c * a + d..c * b + d, f x
Tactic: by_cases hc : c = 0
-- 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
c d : ℝ
pos : ∀ (hc : c = 0), HSMul.hSMul (β := E) c (∫ (x : ℝ) in a..b, f (c * x + d)) = ∫ (x : ℝ) in c * a + d..c * b + d, f x
⊢ HSMul.hSMul (β := E) c (∫ (x : ℝ) in a..b, f (c * x + d)) = ∫ (x : ℝ) in c * a + d..c * b + d, f x
have neg : ∀ (hc : ¬c = 0), HSMul.hSMul (β := E) c (∫ (x : ℝ) in a..b, f (c * x + d)) = ∫ (x : ℝ) in c * a + d..c * b + d, f x
Tactic: by_cases hc : c = 0
-- 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
d : ℝ
⊢ ∫ (x : ℝ) in a..b, f (d + c * x) = HSMul.hSMul (β := E) c⁻¹ (∫ (x : ℝ) in d + c * a..d + c * b, f x)
have rw : ∫ (x : ℝ) in a..b, f (d + c * x) = HSMul.hSMul (β := E) c⁻¹ (∫ (x : ℝ) in c * a..c * b, f (d + x))
Tactic: rw [← integral_comp_add_left, ← integral_comp_mul_left _ 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
d : ℝ
rw : ∫ (x : ℝ) in a..b, f (d + c * x) = HSMul.hSMul (β := E) c⁻¹ (∫ (x : ℝ) in c * a..c * b, f (d + x))
⊢ ∫ (x : ℝ) in a..b, f (d + c * x) = HSMul.hSMul (β := E) c⁻¹ (∫ (x : ℝ) in d + c * a..d + c * b, f x)
have rw₁ : Eq.{u_5 + 1} (α := E) (∫ (x : ℝ) in a..b, f (d + c * x)) (∫ (x : ℝ) in a..b, f (d + c * x))
Tactic: rw [← integral_comp_add_left, ← integral_comp_mul_left _ 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 : ℝ
f : ℝ → E
c d : ℝ
⊢ HSMul.hSMul (β := E) c (∫ (x : ℝ) in a..b, f (d + c * x)) = ∫ (x : ℝ) in d + c * a..d + c * b, f x
have pos : ∀ (hc : c = 0), HSMul.hSMul (β := E) c (∫ (x : ℝ) in a..b, f (d + c * x)) = ∫ (x : ℝ) in d + c * a..d + c * b, f x
Tactic: by_cases hc : c = 0
-- 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
c d : ℝ
pos : ∀ (hc : c = 0), HSMul.hSMul (β := E) c (∫ (x : ℝ) in a..b, f (d + c * x)) = ∫ (x : ℝ) in d + c * a..d + c * b, f x
⊢ HSMul.hSMul (β := E) c (∫ (x : ℝ) in a..b, f (d + c * x)) = ∫ (x : ℝ) in d + c * a..d + c * b, f x
have neg : ∀ (hc : ¬c = 0), HSMul.hSMul (β := E) c (∫ (x : ℝ) in a..b, f (d + c * x)) = ∫ (x : ℝ) in d + c * a..d + c * b, f x
Tactic: by_cases hc : c = 0
-- 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
c d : ℝ
⊢ HSMul.hSMul (β := E) c⁻¹ (∫ (x : ℝ) in a..b, f (x / c + d)) = ∫ (x : ℝ) in a / c + d..b / c + d, f x
have pos : ∀ (hc : c = 0), HSMul.hSMul (β := E) c⁻¹ (∫ (x : ℝ) in a..b, f (x / c + d)) = ∫ (x : ℝ) in a / c + d..b / c + d, f x
Tactic: by_cases hc : c = 0
-- 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
c d : ℝ
pos :
  ∀ (hc : c = 0), HSMul.hSMul (β := E) c⁻¹ (∫ (x : ℝ) in a..b, f (x / c + d)) = ∫ (x : ℝ) in a / c + d..b / c + d, f x
⊢ HSMul.hSMul (β := E) c⁻¹ (∫ (x : ℝ) in a..b, f (x / c + d)) = ∫ (x : ℝ) in a / c + d..b / c + d, f x
have neg : ∀ (hc : ¬c = 0), HSMul.hSMul (β := E) c⁻¹ (∫ (x : ℝ) in a..b, f (x / c + d)) = ∫ (x : ℝ) in a / c + d..b / c + d, f x
Tactic: by_cases hc : c = 0
-- 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
c d : ℝ
⊢ HSMul.hSMul (β := E) c⁻¹ (∫ (x : ℝ) in a..b, f (d + x / c)) = ∫ (x : ℝ) in d + a / c..d + b / c, f x
have pos : ∀ (hc : c = 0), HSMul.hSMul (β := E) c⁻¹ (∫ (x : ℝ) in a..b, f (d + x / c)) = ∫ (x : ℝ) in d + a / c..d + b / c, f x
Tactic: by_cases hc : c = 0
-- 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
c d : ℝ
pos :
  ∀ (hc : c = 0), HSMul.hSMul (β := E) c⁻¹ (∫ (x : ℝ) in a..b, f (d + x / c)) = ∫ (x : ℝ) in d + a / c..d + b / c, f x
⊢ HSMul.hSMul (β := E) c⁻¹ (∫ (x : ℝ) in a..b, f (d + x / c)) = ∫ (x : ℝ) in d + a / c..d + b / c, f x
have neg : ∀ (hc : ¬c = 0), HSMul.hSMul (β := E) c⁻¹ (∫ (x : ℝ) in a..b, f (d + x / c)) = ∫ (x : ℝ) in d + a / c..d + b / c, f x
Tactic: by_cases hc : c = 0
-- 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
c d : ℝ
⊢ HSMul.hSMul (β := E) c (∫ (x : ℝ) in a..b, f (c * x - d)) = ∫ (x : ℝ) in c * a - d..c * b - d, f x
have pos : ∀ (hc : c = 0), HSMul.hSMul (β := E) c (∫ (x : ℝ) in a..b, f (c * x - d)) = ∫ (x : ℝ) in c * a - d..c * b - d, f x
Tactic: by_cases hc : c = 0
-- 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
c d : ℝ
pos : ∀ (hc : c = 0), HSMul.hSMul (β := E) c (∫ (x : ℝ) in a..b, f (c * x - d)) = ∫ (x : ℝ) in c * a - d..c * b - d, f x
⊢ HSMul.hSMul (β := E) c (∫ (x : ℝ) in a..b, f (c * x - d)) = ∫ (x : ℝ) in c * a - d..c * b - d, f x
have neg : ∀ (hc : ¬c = 0), HSMul.hSMul (β := E) c (∫ (x : ℝ) in a..b, f (c * x - d)) = ∫ (x : ℝ) in c * a - d..c * b - d, f x
Tactic: by_cases hc : c = 0
-- 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
d : ℝ
⊢ ∫ (x : ℝ) in a..b, f (d - c * x) = HSMul.hSMul (β := E) c⁻¹ (∫ (x : ℝ) in d - c * b..d - c * a, f x)
have simp : ∫ (x : ℝ) in a..b, f (d + -c * x) = HSMul.hSMul (β := E) c⁻¹ (∫ (x : ℝ) in d + -c * b..d + -c * a, f x)
Tactic: simp only [sub_eq_add_neg, neg_mul_eq_neg_mul]
-- 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
d : ℝ
⊢ ∫ (x : ℝ) in a..b, f (d + -c * x) = HSMul.hSMul (β := E) c⁻¹ (∫ (x : ℝ) in d + -c * b..d + -c * a, f x)
have rw : HSMul.hSMul (β := E) (-c)⁻¹ (-∫ (x : ℝ) in d + -c * b..d + -c * a, f x) =
  HSMul.hSMul (β := E) c⁻¹ (∫ (x : ℝ) in d + -c * b..d + -c * a, f x)
Tactic: rw [integral_comp_add_mul f (neg_ne_zero.mpr hc) d, integral_symm]
-- 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
c d : ℝ
⊢ HSMul.hSMul (β := E) c (∫ (x : ℝ) in a..b, f (d - c * x)) = ∫ (x : ℝ) in d - c * b..d - c * a, f x
have pos : ∀ (hc : c = 0), HSMul.hSMul (β := E) c (∫ (x : ℝ) in a..b, f (d - c * x)) = ∫ (x : ℝ) in d - c * b..d - c * a, f x
Tactic: by_cases hc : c = 0
-- 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
c d : ℝ
pos : ∀ (hc : c = 0), HSMul.hSMul (β := E) c (∫ (x : ℝ) in a..b, f (d - c * x)) = ∫ (x : ℝ) in d - c * b..d - c * a, f x
⊢ HSMul.hSMul (β := E) c (∫ (x : ℝ) in a..b, f (d - c * x)) = ∫ (x : ℝ) in d - c * b..d - c * a, f x
have neg : ∀ (hc : ¬c = 0), HSMul.hSMul (β := E) c (∫ (x : ℝ) in a..b, f (d - c * x)) = ∫ (x : ℝ) in d - c * b..d - c * a, f x
Tactic: by_cases hc : c = 0
-- 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
c d : ℝ
⊢ HSMul.hSMul (β := E) c⁻¹ (∫ (x : ℝ) in a..b, f (x / c - d)) = ∫ (x : ℝ) in a / c - d..b / c - d, f x
have pos : ∀ (hc : c = 0), HSMul.hSMul (β := E) c⁻¹ (∫ (x : ℝ) in a..b, f (x / c - d)) = ∫ (x : ℝ) in a / c - d..b / c - d, f x
Tactic: by_cases hc : c = 0
-- 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
c d : ℝ
pos :
  ∀ (hc : c = 0), HSMul.hSMul (β := E) c⁻¹ (∫ (x : ℝ) in a..b, f (x / c - d)) = ∫ (x : ℝ) in a / c - d..b / c - d, f x
⊢ HSMul.hSMul (β := E) c⁻¹ (∫ (x : ℝ) in a..b, f (x / c - d)) = ∫ (x : ℝ) in a / c - d..b / c - d, f x
have neg : ∀ (hc : ¬c = 0), HSMul.hSMul (β := E) c⁻¹ (∫ (x : ℝ) in a..b, f (x / c - d)) = ∫ (x : ℝ) in a / c - d..b / c - d, f x
Tactic: by_cases hc : c = 0
-- 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
c d : ℝ
⊢ HSMul.hSMul (β := E) c⁻¹ (∫ (x : ℝ) in a..b, f (d - x / c)) = ∫ (x : ℝ) in d - b / c..d - a / c, f x
have pos : ∀ (hc : c = 0), HSMul.hSMul (β := E) c⁻¹ (∫ (x : ℝ) in a..b, f (d - x / c)) = ∫ (x : ℝ) in d - b / c..d - a / c, f x
Tactic: by_cases hc : c = 0
-- 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
c d : ℝ
pos :
  ∀ (hc : c = 0), HSMul.hSMul (β := E) c⁻¹ (∫ (x : ℝ) in a..b, f (d - x / c)) = ∫ (x : ℝ) in d - b / c..d - a / c, f x
⊢ HSMul.hSMul (β := E) c⁻¹ (∫ (x : ℝ) in a..b, f (d - x / c)) = ∫ (x : ℝ) in d - b / c..d - a / c, f x
have neg : ∀ (hc : ¬c = 0), HSMul.hSMul (β := E) c⁻¹ (∫ (x : ℝ) in a..b, f (d - x / c)) = ∫ (x : ℝ) in d - b / c..d - a / c, f x
Tactic: by_cases hc : c = 0
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic (goal)
Goal:
E : Type u_5
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f g : ℝ → E
μ : Measure ℝ
a b : ℝ
h : EqOn f g [[a, b]]
⊢ Eq.{u_5 + 1} (α := E) (∫ (x : ℝ) in a..b, f x ∂μ) (∫ (x : ℝ) in a..b, g x ∂μ)
have inl : ∀ (hab : a ≤ b), Eq.{u_5 + 1} (α := E) (∫ (x : ℝ) in a..b, f x ∂μ) (∫ (x : ℝ) in a..b, g x ∂μ)
Tactic: rcases le_total a b with hab | hab
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic (goal)
Goal:
E : Type u_5
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f g : ℝ → E
μ : Measure ℝ
a b : ℝ
h : EqOn f g [[a, b]]
inl : ∀ (hab : a ≤ b), Eq.{u_5 + 1} (α := E) (∫ (x : ℝ) in a..b, f x ∂μ) (∫ (x : ℝ) in a..b, g x ∂μ)
⊢ Eq.{u_5 + 1} (α := E) (∫ (x : ℝ) in a..b, f x ∂μ) (∫ (x : ℝ) in a..b, g x ∂μ)
have inr : ∀ (hab : b ≤ a), Eq.{u_5 + 1} (α := E) (∫ (x : ℝ) in a..b, f x ∂μ) (∫ (x : ℝ) in a..b, g x ∂μ)
Tactic: rcases le_total a b with hab | hab
-- 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
μ : Measure ℝ
hab : IntervalIntegrable f μ a b
hbc : IntervalIntegrable f μ b c
⊢ HAdd.hAdd (α := E) (∫ (x : ℝ) in a..b, f x ∂μ) (∫ (x : ℝ) in b..c, f x ∂μ) + ∫ (x : ℝ) in c..a, f x ∂μ = 0
have hac : IntervalIntegrable f μ a c
Tactic: have hac := hab.trans hbc
-- 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
μ : Measure ℝ
hab : IntervalIntegrable f μ a b
hbc : IntervalIntegrable f μ b c
hac : IntervalIntegrable f μ a c
⊢ HAdd.hAdd (α := E) (∫ (x : ℝ) in a..b, f x ∂μ) (∫ (x : ℝ) in b..c, f x ∂μ) + ∫ (x : ℝ) in c..a, f x ∂μ = 0
have simp : HAdd.hAdd (α := E) (∫ (x : ℝ) in Ioc a b, f x ∂μ) (∫ (x : ℝ) in Ioc b c, f x ∂μ) + ∫ (x : ℝ) in Ioc c a, f x ∂μ =
  HAdd.hAdd (α := E) (∫ (x : ℝ) in Ioc b a, f x ∂μ) (∫ (x : ℝ) in Ioc c b, f x ∂μ) + ∫ (x : ℝ) in Ioc a c, f x ∂μ
Tactic: simp only [intervalIntegral, sub_add_sub_comm, sub_eq_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 c : ℝ
f : ℝ → E
μ : Measure ℝ
hab : IntervalIntegrable f μ a b
hbc : IntervalIntegrable f μ b c
hac : IntervalIntegrable f μ a c
⊢ HAdd.hAdd (α := E) (∫ (x : ℝ) in Ioc a b, f x ∂μ) (∫ (x : ℝ) in Ioc b c, f x ∂μ) + ∫ (x : ℝ) in Ioc c a, f x ∂μ =
    HAdd.hAdd (α := E) (∫ (x : ℝ) in Ioc b a, f x ∂μ) (∫ (x : ℝ) in Ioc c b, f x ∂μ) + ∫ (x : ℝ) in Ioc a c, f x ∂μ
have rw : HAdd.hAdd (α := E) (∫ (x : ℝ) in Ioc a b ∪ Ioc b c, f x ∂μ) (∫ (x : ℝ) in Ioc c a, f x ∂μ) =
  HAdd.hAdd (α := E) (∫ (x : ℝ) in Ioc b a, f x ∂μ) (∫ (x : ℝ) in Ioc c b, f x ∂μ) + ∫ (x : ℝ) in Ioc a c, f x ∂μ
Tactic: rw [← setIntegral_union]
-- 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
μ : Measure ℝ
hab : IntervalIntegrable f μ a b
hbc : IntervalIntegrable f μ b c
hac : IntervalIntegrable f μ a c
rw :
  HAdd.hAdd (α := E) (∫ (x : ℝ) in Ioc a b ∪ Ioc b c, f x ∂μ) (∫ (x : ℝ) in Ioc c a, f x ∂μ) =
    HAdd.hAdd (α := E) (∫ (x : ℝ) in Ioc b a, f x ∂μ) (∫ (x : ℝ) in Ioc c b, f x ∂μ) + ∫ (x : ℝ) in Ioc a c, f x ∂μ
⊢ HAdd.hAdd (α := E) (∫ (x : ℝ) in Ioc a b, f x ∂μ) (∫ (x : ℝ) in Ioc b c, f x ∂μ) + ∫ (x : ℝ) in Ioc c a, f x ∂μ =
    HAdd.hAdd (α := E) (∫ (x : ℝ) in Ioc b a, f x ∂μ) (∫ (x : ℝ) in Ioc c b, f x ∂μ) + ∫ (x : ℝ) in Ioc a c, f x ∂μ
have hst : Disjoint (Ioc a b) (Ioc b c)
Tactic: rw [← setIntegral_union]
-- 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
μ : Measure ℝ
hab : IntervalIntegrable f μ a b
hbc : IntervalIntegrable f μ b c
hac : IntervalIntegrable f μ a c
rw :
  HAdd.hAdd (α := E) (∫ (x : ℝ) in Ioc a b ∪ Ioc b c, f x ∂μ) (∫ (x : ℝ) in Ioc c a, f x ∂μ) =
    HAdd.hAdd (α := E) (∫ (x : ℝ) in Ioc b a, f x ∂μ) (∫ (x : ℝ) in Ioc c b, f x ∂μ) + ∫ (x : ℝ) in Ioc a c, f x ∂μ
hst : Disjoint (Ioc a b) (Ioc b c)
⊢ HAdd.hAdd (α := E) (∫ (x : ℝ) in Ioc a b, f x ∂μ) (∫ (x : ℝ) in Ioc b c, f x ∂μ) + ∫ (x : ℝ) in Ioc c a, f x ∂μ =
    HAdd.hAdd (α := E) (∫ (x : ℝ) in Ioc b a, f x ∂μ) (∫ (x : ℝ) in Ioc c b, f x ∂μ) + ∫ (x : ℝ) in Ioc a c, f x ∂μ
have ht : MeasurableSet (Ioc b c)
Tactic: rw [← setIntegral_union]
-- 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
μ : Measure ℝ
hab : IntervalIntegrable f μ a b
hbc : IntervalIntegrable f μ b c
hac : IntervalIntegrable f μ a c
rw :
  HAdd.hAdd (α := E) (∫ (x : ℝ) in Ioc a b ∪ Ioc b c, f x ∂μ) (∫ (x : ℝ) in Ioc c a, f x ∂μ) =
    HAdd.hAdd (α := E) (∫ (x : ℝ) in Ioc b a, f x ∂μ) (∫ (x : ℝ) in Ioc c b, f x ∂μ) + ∫ (x : ℝ) in Ioc a c, f x ∂μ
hst : Disjoint (Ioc a b) (Ioc b c)
ht : MeasurableSet (Ioc b c)
⊢ HAdd.hAdd (α := E) (∫ (x : ℝ) in Ioc a b, f x ∂μ) (∫ (x : ℝ) in Ioc b c, f x ∂μ) + ∫ (x : ℝ) in Ioc c a, f x ∂μ =
    HAdd.hAdd (α := E) (∫ (x : ℝ) in Ioc b a, f x ∂μ) (∫ (x : ℝ) in Ioc c b, f x ∂μ) + ∫ (x : ℝ) in Ioc a c, f x ∂μ
have hfs : IntegrableOn f (Ioc a b) μ
Tactic: rw [← setIntegral_union]
-- 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
μ : Measure ℝ
hab : IntervalIntegrable f μ a b
hbc : IntervalIntegrable f μ b c
hac : IntervalIntegrable f μ a c
rw :
  HAdd.hAdd (α := E) (∫ (x : ℝ) in Ioc a b ∪ Ioc b c, f x ∂μ) (∫ (x : ℝ) in Ioc c a, f x ∂μ) =
    HAdd.hAdd (α := E) (∫ (x : ℝ) in Ioc b a, f x ∂μ) (∫ (x : ℝ) in Ioc c b, f x ∂μ) + ∫ (x : ℝ) in Ioc a c, f x ∂μ
hst : Disjoint (Ioc a b) (Ioc b c)
ht : MeasurableSet (Ioc b c)
hfs : IntegrableOn f (Ioc a b) μ
⊢ HAdd.hAdd (α := E) (∫ (x : ℝ) in Ioc a b, f x ∂μ) (∫ (x : ℝ) in Ioc b c, f x ∂μ) + ∫ (x : ℝ) in Ioc c a, f x ∂μ =
    HAdd.hAdd (α := E) (∫ (x : ℝ) in Ioc b a, f x ∂μ) (∫ (x : ℝ) in Ioc c b, f x ∂μ) + ∫ (x : ℝ) in Ioc a c, f x ∂μ
have hft : IntegrableOn f (Ioc b c) μ
Tactic: rw [← setIntegral_union]
-- 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
μ : Measure ℝ
hab : IntervalIntegrable f μ a b
hbc : IntervalIntegrable f μ b c
hac : IntervalIntegrable f μ a c
⊢ HAdd.hAdd (α := E) (∫ (x : ℝ) in Ioc a b ∪ Ioc b c, f x ∂μ) (∫ (x : ℝ) in Ioc c a, f x ∂μ) =
    HAdd.hAdd (α := E) (∫ (x : ℝ) in Ioc b a, f x ∂μ) (∫ (x : ℝ) in Ioc c b, f x ∂μ) + ∫ (x : ℝ) in Ioc a c, f x ∂μ
have rw : ∫ (x : ℝ) in Ioc a b ∪ Ioc b c ∪ Ioc c a, f x ∂μ =
  HAdd.hAdd (α := E) (∫ (x : ℝ) in Ioc b a, f x ∂μ) (∫ (x : ℝ) in Ioc c b, f x ∂μ) + ∫ (x : ℝ) in Ioc a c, f x ∂μ
Tactic: rw [← setIntegral_union]