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 : ℝ
f : ℝ → E
μ : Measure ℝ
inst_2 : NoAtoms μ
hf : IntegrableOn f (Iio b) μ
hg : IntegrableOn f (Iio a) μ
⊢ HSub.hSub (α := E) (∫ (x : ℝ) in Iio b, f x ∂μ) (∫ (x : ℝ) in Iio a, f x ∂μ) = ∫ (x : ℝ) in a..b, f x ∂μ
have inr : ∀
  (this :
    ∀ {a b : ℝ} (hf : IntegrableOn f (Iio b) μ) (hg : IntegrableOn f (Iio a) μ) (hab : a ≤ b),
      HSub.hSub (α := E) (∫ (x : ℝ) in Iio b, f x ∂μ) (∫ (x : ℝ) in Iio a, f x ∂μ) = ∫ (x : ℝ) in a..b, f x ∂μ)
  (hab : b < a),
  HSub.hSub (α := E) (∫ (x : ℝ) in Iio b, f x ∂μ) (∫ (x : ℝ) in Iio a, f x ∂μ) = ∫ (x : ℝ) in a..b, f x ∂μ
Tactic: wlog! hab : a ≤ b generalizing 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 : ℝ
f : ℝ → E
μ : Measure ℝ
inst_2 : NoAtoms μ
hf : IntegrableOn f (Iio b) μ
hg : IntegrableOn f (Iio a) μ
inr :
  ∀
    (this :
      ∀ {a b : ℝ} (hf : IntegrableOn f (Iio b) μ) (hg : IntegrableOn f (Iio a) μ) (hab : a ≤ b),
        HSub.hSub (α := E) (∫ (x : ℝ) in Iio b, f x ∂μ) (∫ (x : ℝ) in Iio a, f x ∂μ) = ∫ (x : ℝ) in a..b, f x ∂μ)
    (hab : b < a),
    HSub.hSub (α := E) (∫ (x : ℝ) in Iio b, f x ∂μ) (∫ (x : ℝ) in Iio a, f x ∂μ) = ∫ (x : ℝ) in a..b, f x ∂μ
⊢ HSub.hSub (α := E) (∫ (x : ℝ) in Iio b, f x ∂μ) (∫ (x : ℝ) in Iio a, f x ∂μ) = ∫ (x : ℝ) in a..b, f x ∂μ
have wlog! : ∀ {a b : ℝ} (hf : IntegrableOn f (Iio b) μ) (hg : IntegrableOn f (Iio a) μ) (hab : a ≤ b),
  HSub.hSub (α := E) (∫ (x : ℝ) in Iio b, f x ∂μ) (∫ (x : ℝ) in Iio a, f x ∂μ) = ∫ (x : ℝ) in a..b, f x ∂μ
Tactic: wlog! hab : a ≤ b generalizing a b
Cleared hypotheses: hf, hg
-- 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 ℝ
inst_2 : NoAtoms μ
hf : IntegrableOn f (Iio b) μ
hg : IntegrableOn f (Iio a) μ
this :
  ∀ {a b : ℝ} (hf : IntegrableOn f (Iio b) μ) (hg : IntegrableOn f (Iio a) μ) (hab : a ≤ b),
    HSub.hSub (α := E) (∫ (x : ℝ) in Iio b, f x ∂μ) (∫ (x : ℝ) in Iio a, f x ∂μ) = ∫ (x : ℝ) in a..b, f x ∂μ
hab : b < a
⊢ HSub.hSub (α := E) (∫ (x : ℝ) in Iio b, f x ∂μ) (∫ (x : ℝ) in Iio a, f x ∂μ) = ∫ (x : ℝ) in a..b, f x ∂μ
have inr : HSub.hSub (α := E) (∫ (x : ℝ) in Iio b, f x ∂μ) (∫ (x : ℝ) in Iio a, f x ∂μ) = -∫ (x : ℝ) in b..a, f x ∂μ
Tactic: rw [integral_symm, ← this hg hf hab.le, neg_sub]
-- 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 ℝ
inst_2 : NoAtoms μ
hf : IntegrableOn f (Iio b) μ
hg : IntegrableOn f (Iio a) μ
this :
  ∀ {a b : ℝ} (hf : IntegrableOn f (Iio b) μ) (hg : IntegrableOn f (Iio a) μ) (hab : a ≤ b),
    HSub.hSub (α := E) (∫ (x : ℝ) in Iio b, f x ∂μ) (∫ (x : ℝ) in Iio a, f x ∂μ) = ∫ (x : ℝ) in a..b, f x ∂μ
hab : b < a
inr : HSub.hSub (α := E) (∫ (x : ℝ) in Iio b, f x ∂μ) (∫ (x : ℝ) in Iio a, f x ∂μ) = -∫ (x : ℝ) in b..a, f x ∂μ
⊢ HSub.hSub (α := E) (∫ (x : ℝ) in Iio b, f x ∂μ) (∫ (x : ℝ) in Iio a, f x ∂μ) = ∫ (x : ℝ) in a..b, f x ∂μ
have inr₁ : HSub.hSub (α := E) (∫ (x : ℝ) in Iio b, f x ∂μ) (∫ (x : ℝ) in Iio a, f x ∂μ) =
  -HSub.hSub (α := E) (∫ (x : ℝ) in Iio a, f x ∂μ) (∫ (x : ℝ) in Iio b, f x ∂μ)
Tactic: rw [integral_symm, ← this hg hf hab.le, neg_sub]
-- 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 ℝ
inst_2 : NoAtoms μ
hf : IntegrableOn f (Iio b) μ
hg : IntegrableOn f (Iio a) μ
this :
  ∀ {a b : ℝ} (hf : IntegrableOn f (Iio b) μ) (hg : IntegrableOn f (Iio a) μ) (hab : a ≤ b),
    HSub.hSub (α := E) (∫ (x : ℝ) in Iio b, f x ∂μ) (∫ (x : ℝ) in Iio a, f x ∂μ) = ∫ (x : ℝ) in a..b, f x ∂μ
hab : b < a
inr : HSub.hSub (α := E) (∫ (x : ℝ) in Iio b, f x ∂μ) (∫ (x : ℝ) in Iio a, f x ∂μ) = -∫ (x : ℝ) in b..a, f x ∂μ
inr₁ :
  HSub.hSub (α := E) (∫ (x : ℝ) in Iio b, f x ∂μ) (∫ (x : ℝ) in Iio a, f x ∂μ) =
    -HSub.hSub (α := E) (∫ (x : ℝ) in Iio a, f x ∂μ) (∫ (x : ℝ) in Iio b, f x ∂μ)
⊢ HSub.hSub (α := E) (∫ (x : ℝ) in Iio b, f x ∂μ) (∫ (x : ℝ) in Iio a, f x ∂μ) = ∫ (x : ℝ) in a..b, f x ∂μ
have inr₂ : HSub.hSub (α := E) (∫ (x : ℝ) in Iio b, f x ∂μ) (∫ (x : ℝ) in Iio a, f x ∂μ) =
  HSub.hSub (α := E) (∫ (x : ℝ) in Iio b, f x ∂μ) (∫ (x : ℝ) in Iio a, f x ∂μ)
Tactic: rw [integral_symm, ← this hg hf hab.le, neg_sub]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic (goal)
Goal:
E : Type u_5
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
a_1 b_1 : ℝ
f : ℝ → E
μ : Measure ℝ
inst_2 : NoAtoms μ
a b : ℝ
hf : IntegrableOn f (Iio b) μ
hg : IntegrableOn f (Iio a) μ
hab : a ≤ b
⊢ HSub.hSub (α := E) (∫ (x : ℝ) in Iio b, f x ∂μ) (∫ (x : ℝ) in Iio a, f x ∂μ) = ∫ (x : ℝ) in a..b, f x ∂μ
have rw : Eq.{u_5 + 1} (α := E) (∫ (x : ℝ) in Ico a b, f x ∂μ) (∫ (x : ℝ) in a..b, f x ∂μ)
Tactic: rw [integral_Iio_sub_Iio hf hab, integral_of_le hab, integral_Ico_eq_integral_Ioc]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic (goal)
Goal:
E : Type u_5
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
a_1 b_1 : ℝ
f : ℝ → E
μ : Measure ℝ
inst_2 : NoAtoms μ
a b : ℝ
hf : IntegrableOn f (Iio b) μ
hg : IntegrableOn f (Iio a) μ
hab : a ≤ b
rw : Eq.{u_5 + 1} (α := E) (∫ (x : ℝ) in Ico a b, f x ∂μ) (∫ (x : ℝ) in a..b, f x ∂μ)
⊢ HSub.hSub (α := E) (∫ (x : ℝ) in Iio b, f x ∂μ) (∫ (x : ℝ) in Iio a, f x ∂μ) = ∫ (x : ℝ) in a..b, f x ∂μ
have rw₁ : Eq.{u_5 + 1} (α := E) (∫ (x : ℝ) in Ico a b, f x ∂μ) (∫ (x : ℝ) in Ioc a b, f x ∂μ)
Tactic: rw [integral_Iio_sub_Iio hf hab, integral_of_le hab, integral_Ico_eq_integral_Ioc]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic (goal)
Goal:
E : Type u_5
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
a_1 b_1 : ℝ
f : ℝ → E
μ : Measure ℝ
inst_2 : NoAtoms μ
a b : ℝ
hf : IntegrableOn f (Iio b) μ
hg : IntegrableOn f (Iio a) μ
hab : a ≤ b
rw : Eq.{u_5 + 1} (α := E) (∫ (x : ℝ) in Ico a b, f x ∂μ) (∫ (x : ℝ) in a..b, f x ∂μ)
rw₁ : Eq.{u_5 + 1} (α := E) (∫ (x : ℝ) in Ico a b, f x ∂μ) (∫ (x : ℝ) in Ioc a b, f x ∂μ)
⊢ HSub.hSub (α := E) (∫ (x : ℝ) in Iio b, f x ∂μ) (∫ (x : ℝ) in Iio a, f x ∂μ) = ∫ (x : ℝ) in a..b, f x ∂μ
have rw₂ : Eq.{u_5 + 1} (α := E) (∫ (t : ℝ) in Ioc a b, f t ∂μ) (∫ (x : ℝ) in Ioc a b, f x ∂μ)
Tactic: rw [integral_Iio_sub_Iio hf hab, integral_of_le hab, integral_Ico_eq_integral_Ioc]
-- 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 ℝ
hf : IntegrableOn f (Ici a) μ
hab : a ≤ b
⊢ HSub.hSub (α := E) (∫ (x : ℝ) in Ici a, f x ∂μ) (∫ (x : ℝ) in Ici b, f x ∂μ) = ∫ (x : ℝ) in Ico a b, f x ∂μ
have ha : IntegrableOn f (Ici b) μ
Tactic: have ha : IntegrableOn f (Ici b) μ := hf.mono_set (Ici_subset_Ici.2 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 : ℝ
f : ℝ → E
μ : Measure ℝ
hf : IntegrableOn f (Ici a) μ
hab : a ≤ b
ha : IntegrableOn f (Ici b) μ
⊢ HSub.hSub (α := E) (∫ (x : ℝ) in Ici a, f x ∂μ) (∫ (x : ℝ) in Ici b, f x ∂μ) = ∫ (x : ℝ) in Ico a b, f x ∂μ
have h : IntegrableOn f (Ico a b) μ
Tactic: have h : IntegrableOn f (Ico a b) μ := hf.mono_set Ico_subset_Ici_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 : ℝ
f : ℝ → E
μ : Measure ℝ
hf : IntegrableOn f (Ici a) μ
hab : a ≤ b
ha : IntegrableOn f (Ici b) μ
h : IntegrableOn f (Ico a b) μ
⊢ HSub.hSub (α := E) (∫ (x : ℝ) in Ici a, f x ∂μ) (∫ (x : ℝ) in Ici b, f x ∂μ) = ∫ (x : ℝ) in Ico a b, f x ∂μ
have rw : ∫ (x : ℝ) in Ici a, f x ∂μ = HAdd.hAdd (α := E) (∫ (x : ℝ) in Ici b, f x ∂μ) (∫ (x : ℝ) in Ico a b, f x ∂μ)
Tactic: rw [sub_eq_iff_eq_add', ← setIntegral_union (by grind) measurableSet_Ico ha h, union_comm,
    Ico_union_Ici_eq_Ici hab]
-- 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 : IntegrableOn f (Ici a) μ
hab : a ≤ b
ha : IntegrableOn f (Ici b) μ
h : IntegrableOn f (Ico a b) μ
rw : ∫ (x : ℝ) in Ici a, f x ∂μ = HAdd.hAdd (α := E) (∫ (x : ℝ) in Ici b, f x ∂μ) (∫ (x : ℝ) in Ico a b, f x ∂μ)
⊢ HSub.hSub (α := E) (∫ (x : ℝ) in Ici a, f x ∂μ) (∫ (x : ℝ) in Ici b, f x ∂μ) = ∫ (x : ℝ) in Ico a b, f x ∂μ
have rw₁ : Eq.{u_5 + 1} (α := E) (∫ (x : ℝ) in Ici a, f x ∂μ) (∫ (x : ℝ) in Ici b ∪ Ico a b, f x ∂μ)
Tactic: rw [sub_eq_iff_eq_add', ← setIntegral_union (by grind) measurableSet_Ico ha h, union_comm,
    Ico_union_Ici_eq_Ici hab]
-- 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 : IntegrableOn f (Ici a) μ
hab : a ≤ b
ha : IntegrableOn f (Ici b) μ
h : IntegrableOn f (Ico a b) μ
rw : ∫ (x : ℝ) in Ici a, f x ∂μ = HAdd.hAdd (α := E) (∫ (x : ℝ) in Ici b, f x ∂μ) (∫ (x : ℝ) in Ico a b, f x ∂μ)
rw₁ : Eq.{u_5 + 1} (α := E) (∫ (x : ℝ) in Ici a, f x ∂μ) (∫ (x : ℝ) in Ici b ∪ Ico a b, f x ∂μ)
⊢ HSub.hSub (α := E) (∫ (x : ℝ) in Ici a, f x ∂μ) (∫ (x : ℝ) in Ici b, f x ∂μ) = ∫ (x : ℝ) in Ico a b, f x ∂μ
have rw₂ : Eq.{u_5 + 1} (α := E) (∫ (x : ℝ) in Ici a, f x ∂μ) (∫ (x : ℝ) in Ico a b ∪ Ici b, f x ∂μ)
Tactic: rw [sub_eq_iff_eq_add', ← setIntegral_union (by grind) measurableSet_Ico ha h, union_comm,
    Ico_union_Ici_eq_Ici hab]
-- 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 : IntegrableOn f (Ici a) μ
hab : a ≤ b
ha : IntegrableOn f (Ici b) μ
h : IntegrableOn f (Ico a b) μ
rw : ∫ (x : ℝ) in Ici a, f x ∂μ = HAdd.hAdd (α := E) (∫ (x : ℝ) in Ici b, f x ∂μ) (∫ (x : ℝ) in Ico a b, f x ∂μ)
rw₁ : Eq.{u_5 + 1} (α := E) (∫ (x : ℝ) in Ici a, f x ∂μ) (∫ (x : ℝ) in Ici b ∪ Ico a b, f x ∂μ)
rw₂ : Eq.{u_5 + 1} (α := E) (∫ (x : ℝ) in Ici a, f x ∂μ) (∫ (x : ℝ) in Ico a b ∪ Ici b, f x ∂μ)
⊢ HSub.hSub (α := E) (∫ (x : ℝ) in Ici a, f x ∂μ) (∫ (x : ℝ) in Ici b, f x ∂μ) = ∫ (x : ℝ) in Ico a b, f x ∂μ
have rw₃ : Eq.{u_5 + 1} (α := E) (∫ (x : ℝ) in Ici a, f x ∂μ) (∫ (x : ℝ) in Ici a, f x ∂μ)
Tactic: rw [sub_eq_iff_eq_add', ← setIntegral_union (by grind) measurableSet_Ico ha h, union_comm,
    Ico_union_Ici_eq_Ici hab]
-- 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 ℝ
inst_2 : NoAtoms μ
hf : IntegrableOn f (Ici a) μ
hg : IntegrableOn f (Ici b) μ
⊢ HSub.hSub (α := E) (∫ (x : ℝ) in Ici a, f x ∂μ) (∫ (x : ℝ) in Ici b, f x ∂μ) = ∫ (x : ℝ) in a..b, f x ∂μ
have inr : ∀
  (this :
    ∀ {a b : ℝ} (hf : IntegrableOn f (Ici a) μ) (hg : IntegrableOn f (Ici b) μ) (hab : a ≤ b),
      HSub.hSub (α := E) (∫ (x : ℝ) in Ici a, f x ∂μ) (∫ (x : ℝ) in Ici b, f x ∂μ) = ∫ (x : ℝ) in a..b, f x ∂μ)
  (hab : b < a),
  HSub.hSub (α := E) (∫ (x : ℝ) in Ici a, f x ∂μ) (∫ (x : ℝ) in Ici b, f x ∂μ) = ∫ (x : ℝ) in a..b, f x ∂μ
Tactic: wlog! hab : a ≤ b generalizing 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 : ℝ
f : ℝ → E
μ : Measure ℝ
inst_2 : NoAtoms μ
hf : IntegrableOn f (Ici a) μ
hg : IntegrableOn f (Ici b) μ
inr :
  ∀
    (this :
      ∀ {a b : ℝ} (hf : IntegrableOn f (Ici a) μ) (hg : IntegrableOn f (Ici b) μ) (hab : a ≤ b),
        HSub.hSub (α := E) (∫ (x : ℝ) in Ici a, f x ∂μ) (∫ (x : ℝ) in Ici b, f x ∂μ) = ∫ (x : ℝ) in a..b, f x ∂μ)
    (hab : b < a),
    HSub.hSub (α := E) (∫ (x : ℝ) in Ici a, f x ∂μ) (∫ (x : ℝ) in Ici b, f x ∂μ) = ∫ (x : ℝ) in a..b, f x ∂μ
⊢ HSub.hSub (α := E) (∫ (x : ℝ) in Ici a, f x ∂μ) (∫ (x : ℝ) in Ici b, f x ∂μ) = ∫ (x : ℝ) in a..b, f x ∂μ
have wlog! : ∀ {a b : ℝ} (hf : IntegrableOn f (Ici a) μ) (hg : IntegrableOn f (Ici b) μ) (hab : a ≤ b),
  HSub.hSub (α := E) (∫ (x : ℝ) in Ici a, f x ∂μ) (∫ (x : ℝ) in Ici b, f x ∂μ) = ∫ (x : ℝ) in a..b, f x ∂μ
Tactic: wlog! hab : a ≤ b generalizing a b
Cleared hypotheses: hf, hg
-- 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 ℝ
inst_2 : NoAtoms μ
hf : IntegrableOn f (Ici a) μ
hg : IntegrableOn f (Ici b) μ
this :
  ∀ {a b : ℝ} (hf : IntegrableOn f (Ici a) μ) (hg : IntegrableOn f (Ici b) μ) (hab : a ≤ b),
    HSub.hSub (α := E) (∫ (x : ℝ) in Ici a, f x ∂μ) (∫ (x : ℝ) in Ici b, f x ∂μ) = ∫ (x : ℝ) in a..b, f x ∂μ
hab : b < a
⊢ HSub.hSub (α := E) (∫ (x : ℝ) in Ici a, f x ∂μ) (∫ (x : ℝ) in Ici b, f x ∂μ) = ∫ (x : ℝ) in a..b, f x ∂μ
have inr : HSub.hSub (α := E) (∫ (x : ℝ) in Ici a, f x ∂μ) (∫ (x : ℝ) in Ici b, f x ∂μ) = -∫ (x : ℝ) in b..a, f x ∂μ
Tactic: rw [integral_symm, ← this hg hf hab.le, neg_sub]
-- 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 ℝ
inst_2 : NoAtoms μ
hf : IntegrableOn f (Ici a) μ
hg : IntegrableOn f (Ici b) μ
this :
  ∀ {a b : ℝ} (hf : IntegrableOn f (Ici a) μ) (hg : IntegrableOn f (Ici b) μ) (hab : a ≤ b),
    HSub.hSub (α := E) (∫ (x : ℝ) in Ici a, f x ∂μ) (∫ (x : ℝ) in Ici b, f x ∂μ) = ∫ (x : ℝ) in a..b, f x ∂μ
hab : b < a
inr : HSub.hSub (α := E) (∫ (x : ℝ) in Ici a, f x ∂μ) (∫ (x : ℝ) in Ici b, f x ∂μ) = -∫ (x : ℝ) in b..a, f x ∂μ
⊢ HSub.hSub (α := E) (∫ (x : ℝ) in Ici a, f x ∂μ) (∫ (x : ℝ) in Ici b, f x ∂μ) = ∫ (x : ℝ) in a..b, f x ∂μ
have inr₁ : HSub.hSub (α := E) (∫ (x : ℝ) in Ici a, f x ∂μ) (∫ (x : ℝ) in Ici b, f x ∂μ) =
  -HSub.hSub (α := E) (∫ (x : ℝ) in Ici b, f x ∂μ) (∫ (x : ℝ) in Ici a, f x ∂μ)
Tactic: rw [integral_symm, ← this hg hf hab.le, neg_sub]
-- 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 ℝ
inst_2 : NoAtoms μ
hf : IntegrableOn f (Ici a) μ
hg : IntegrableOn f (Ici b) μ
this :
  ∀ {a b : ℝ} (hf : IntegrableOn f (Ici a) μ) (hg : IntegrableOn f (Ici b) μ) (hab : a ≤ b),
    HSub.hSub (α := E) (∫ (x : ℝ) in Ici a, f x ∂μ) (∫ (x : ℝ) in Ici b, f x ∂μ) = ∫ (x : ℝ) in a..b, f x ∂μ
hab : b < a
inr : HSub.hSub (α := E) (∫ (x : ℝ) in Ici a, f x ∂μ) (∫ (x : ℝ) in Ici b, f x ∂μ) = -∫ (x : ℝ) in b..a, f x ∂μ
inr₁ :
  HSub.hSub (α := E) (∫ (x : ℝ) in Ici a, f x ∂μ) (∫ (x : ℝ) in Ici b, f x ∂μ) =
    -HSub.hSub (α := E) (∫ (x : ℝ) in Ici b, f x ∂μ) (∫ (x : ℝ) in Ici a, f x ∂μ)
⊢ HSub.hSub (α := E) (∫ (x : ℝ) in Ici a, f x ∂μ) (∫ (x : ℝ) in Ici b, f x ∂μ) = ∫ (x : ℝ) in a..b, f x ∂μ
have inr₂ : HSub.hSub (α := E) (∫ (x : ℝ) in Ici a, f x ∂μ) (∫ (x : ℝ) in Ici b, f x ∂μ) =
  HSub.hSub (α := E) (∫ (x : ℝ) in Ici a, f x ∂μ) (∫ (x : ℝ) in Ici b, f x ∂μ)
Tactic: rw [integral_symm, ← this hg hf hab.le, neg_sub]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic (goal)
Goal:
E : Type u_5
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
a_1 b_1 : ℝ
f : ℝ → E
μ : Measure ℝ
inst_2 : NoAtoms μ
a b : ℝ
hf : IntegrableOn f (Ici a) μ
hg : IntegrableOn f (Ici b) μ
hab : a ≤ b
⊢ HSub.hSub (α := E) (∫ (x : ℝ) in Ici a, f x ∂μ) (∫ (x : ℝ) in Ici b, f x ∂μ) = ∫ (x : ℝ) in a..b, f x ∂μ
have rw : Eq.{u_5 + 1} (α := E) (∫ (x : ℝ) in Ico a b, f x ∂μ) (∫ (x : ℝ) in a..b, f x ∂μ)
Tactic: rw [integral_Ici_sub_Ici hf hab, integral_of_le hab, integral_Ico_eq_integral_Ioc]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic (goal)
Goal:
E : Type u_5
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
a_1 b_1 : ℝ
f : ℝ → E
μ : Measure ℝ
inst_2 : NoAtoms μ
a b : ℝ
hf : IntegrableOn f (Ici a) μ
hg : IntegrableOn f (Ici b) μ
hab : a ≤ b
rw : Eq.{u_5 + 1} (α := E) (∫ (x : ℝ) in Ico a b, f x ∂μ) (∫ (x : ℝ) in a..b, f x ∂μ)
⊢ HSub.hSub (α := E) (∫ (x : ℝ) in Ici a, f x ∂μ) (∫ (x : ℝ) in Ici b, f x ∂μ) = ∫ (x : ℝ) in a..b, f x ∂μ
have rw₁ : Eq.{u_5 + 1} (α := E) (∫ (x : ℝ) in Ico a b, f x ∂μ) (∫ (x : ℝ) in Ioc a b, f x ∂μ)
Tactic: rw [integral_Ici_sub_Ici hf hab, integral_of_le hab, integral_Ico_eq_integral_Ioc]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic (goal)
Goal:
E : Type u_5
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
a_1 b_1 : ℝ
f : ℝ → E
μ : Measure ℝ
inst_2 : NoAtoms μ
a b : ℝ
hf : IntegrableOn f (Ici a) μ
hg : IntegrableOn f (Ici b) μ
hab : a ≤ b
rw : Eq.{u_5 + 1} (α := E) (∫ (x : ℝ) in Ico a b, f x ∂μ) (∫ (x : ℝ) in a..b, f x ∂μ)
rw₁ : Eq.{u_5 + 1} (α := E) (∫ (x : ℝ) in Ico a b, f x ∂μ) (∫ (x : ℝ) in Ioc a b, f x ∂μ)
⊢ HSub.hSub (α := E) (∫ (x : ℝ) in Ici a, f x ∂μ) (∫ (x : ℝ) in Ici b, f x ∂μ) = ∫ (x : ℝ) in a..b, f x ∂μ
have rw₂ : Eq.{u_5 + 1} (α := E) (∫ (t : ℝ) in Ioc a b, f t ∂μ) (∫ (x : ℝ) in Ioc a b, f x ∂μ)
Tactic: rw [integral_Ici_sub_Ici hf hab, integral_of_le hab, integral_Ico_eq_integral_Ioc]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic (goal)
Goal:
E : Type u_5
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
b : ℝ
f : ℝ → E
μ : Measure ℝ
h_left : IntegrableOn f (Iic b) μ
h_right : IntegrableOn f (Ioi b) μ
⊢ HAdd.hAdd (α := E) (∫ (x : ℝ) in Iic b, f x ∂μ) (∫ (x : ℝ) in Ioi b, f x ∂μ) = ∫ (x : ℝ), f x ∂μ
have h : μ = μ.restrict (Iic b ∪ Ioi b)
Tactic: convert! (setIntegral_union (Iic_disjoint_Ioi <| Eq.le rfl) measurableSet_Ioi h_left h_right).symm
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic (goal)
Goal:
E : Type u_5
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
b : ℝ
f : ℝ → E
μ : Measure ℝ
h_left : IntegrableOn f (Iic b) μ
h_right : IntegrableOn f (Ioi b) μ
⊢ μ = μ.restrict (Iic b ∪ Ioi b)
have h : μ = μ.restrict univ
Tactic: rw [Iic_union_Ioi, Measure.restrict_univ]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic (goal)
Goal:
E : Type u_5
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
b : ℝ
f : ℝ → E
μ : Measure ℝ
h_left : IntegrableOn f (Iic b) μ
h_right : IntegrableOn f (Ioi b) μ
h : μ = μ.restrict univ
⊢ μ = μ.restrict (Iic b ∪ Ioi b)
have h₁ : μ = μ
Tactic: rw [Iic_union_Ioi, Measure.restrict_univ]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic (goal)
Goal:
E : Type u_5
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
b : ℝ
f : ℝ → E
μ : Measure ℝ
h_left : IntegrableOn f (Iio b) μ
h_right : IntegrableOn f (Ici b) μ
⊢ HAdd.hAdd (α := E) (∫ (x : ℝ) in Iio b, f x ∂μ) (∫ (x : ℝ) in Ici b, f x ∂μ) = ∫ (x : ℝ), f x ∂μ
have h : μ = μ.restrict (Iio b ∪ Ici b)
Tactic: convert! (setIntegral_union (Iio_disjoint_Ici <| Eq.le rfl) measurableSet_Ici h_left h_right).symm
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic (goal)
Goal:
E : Type u_5
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
b : ℝ
f : ℝ → E
μ : Measure ℝ
h_left : IntegrableOn f (Iio b) μ
h_right : IntegrableOn f (Ici b) μ
⊢ μ = μ.restrict (Iio b ∪ Ici b)
have h : μ = μ.restrict univ
Tactic: rw [Iio_union_Ici, Measure.restrict_univ]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic (goal)
Goal:
E : Type u_5
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
b : ℝ
f : ℝ → E
μ : Measure ℝ
h_left : IntegrableOn f (Iio b) μ
h_right : IntegrableOn f (Ici b) μ
h : μ = μ.restrict univ
⊢ μ = μ.restrict (Iio b ∪ Ici b)
have h₁ : μ = μ
Tactic: rw [Iio_union_Ici, Measure.restrict_univ]
-- 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 ℝ
inst_2 : CompleteSpace E
inst_3 : IsFiniteMeasure μ
c : E
⊢ ∫ (x : ℝ) in a..b, c ∂μ = (μ.real (Iic b) - μ.real (Iic a)) • c
have simp : ∫ (x : ℝ) in a..b, c ∂μ = HSub.hSub (α := E) (∫ (x : ℝ) in Iic b, c ∂μ) (∫ (x : ℝ) in Iic a, c ∂μ)
Tactic: simp only [sub_smul, ← setIntegral_const]
-- 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 ℝ
inst_2 : CompleteSpace E
inst_3 : IsFiniteMeasure μ
c : E
⊢ ∫ (x : ℝ) in a..b, c ∂μ = HSub.hSub (α := E) (∫ (x : ℝ) in Iic b, c ∂μ) (∫ (x : ℝ) in Iic a, c ∂μ)
have refine_1 : IntegrableOn.{0, u_5} (ε := E) (fun (x : ℝ) ↦ c) (Iic a) μ
Tactic: refine (integral_Iic_sub_Iic ?_ ?_).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 : ℝ
μ : Measure ℝ
inst_2 : CompleteSpace E
inst_3 : IsFiniteMeasure μ
c : E
refine_1 : IntegrableOn.{0, u_5} (ε := E) (fun (x : ℝ) ↦ c) (Iic a) μ
⊢ ∫ (x : ℝ) in a..b, c ∂μ = HSub.hSub (α := E) (∫ (x : ℝ) in Iic b, c ∂μ) (∫ (x : ℝ) in Iic a, c ∂μ)
have refine_2 : IntegrableOn.{0, u_5} (ε := E) (fun (x : ℝ) ↦ c) (Iic b) μ
Tactic: refine (integral_Iic_sub_Iic ?_ ?_).symm
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic (goal)
Goal:
E : Type u_5
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℝ → E
μ : Measure ℝ
a b : ℝ
h : support f ⊆ Ioc a b
⊢ Eq.{u_5 + 1} (α := E) (∫ (x : ℝ) in a..b, f x ∂μ) (∫ (x : ℝ), f x ∂μ)
have inl : ∀ (hab : a ≤ b), Eq.{u_5 + 1} (α := E) (∫ (x : ℝ) in a..b, f x ∂μ) (∫ (x : ℝ), f 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 : ℝ → E
μ : Measure ℝ
a b : ℝ
h : support f ⊆ Ioc a b
inl : ∀ (hab : a ≤ b), Eq.{u_5 + 1} (α := E) (∫ (x : ℝ) in a..b, f x ∂μ) (∫ (x : ℝ), f x ∂μ)
⊢ Eq.{u_5 + 1} (α := E) (∫ (x : ℝ) in a..b, f x ∂μ) (∫ (x : ℝ), f x ∂μ)
have inr : ∀ (hab : b ≤ a), Eq.{u_5 + 1} (α := E) (∫ (x : ℝ) in a..b, f x ∂μ) (∫ (x : ℝ), f 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 : ℝ → E
μ : Measure ℝ
a b : ℝ
h : support f ⊆ Ioc a b
hab : a ≤ b
⊢ Eq.{u_5 + 1} (α := E) (∫ (x : ℝ) in a..b, f x ∂μ) (∫ (x : ℝ), f x ∂μ)
have inl : Eq.{u_5 + 1} (α := E) (∫ (x : ℝ) in Ioc a b, f x ∂μ) (∫ (x : ℝ), f x ∂μ)
Tactic: rw [integral_of_le hab, ← integral_indicator measurableSet_Ioc, indicator_eq_self.2 h]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic (goal)
Goal:
E : Type u_5
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℝ → E
μ : Measure ℝ
a b : ℝ
h : support f ⊆ Ioc a b
hab : a ≤ b
inl : Eq.{u_5 + 1} (α := E) (∫ (x : ℝ) in Ioc a b, f x ∂μ) (∫ (x : ℝ), f x ∂μ)
⊢ Eq.{u_5 + 1} (α := E) (∫ (x : ℝ) in a..b, f x ∂μ) (∫ (x : ℝ), f x ∂μ)
have inl₁ : Eq.{u_5 + 1} (α := E) (∫ (x : ℝ), (Ioc a b).indicator f x ∂μ) (∫ (x : ℝ), f x ∂μ)
Tactic: rw [integral_of_le hab, ← integral_indicator measurableSet_Ioc, indicator_eq_self.2 h]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic (goal)
Goal:
E : Type u_5
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℝ → E
μ : Measure ℝ
a b : ℝ
h : support f ⊆ Ioc a b
hab : a ≤ b
inl : Eq.{u_5 + 1} (α := E) (∫ (x : ℝ) in Ioc a b, f x ∂μ) (∫ (x : ℝ), f x ∂μ)
inl₁ : Eq.{u_5 + 1} (α := E) (∫ (x : ℝ), (Ioc a b).indicator f x ∂μ) (∫ (x : ℝ), f x ∂μ)
⊢ Eq.{u_5 + 1} (α := E) (∫ (x : ℝ) in a..b, f x ∂μ) (∫ (x : ℝ), f x ∂μ)
have inl₂ : Eq.{u_5 + 1} (α := E) (∫ (x : ℝ), f x ∂μ) (∫ (x : ℝ), f x ∂μ)
Tactic: rw [integral_of_le hab, ← integral_indicator measurableSet_Ioc, indicator_eq_self.2 h]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic (hypothesis)
Goal:
E : Type u_5
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℝ → E
μ : Measure ℝ
a b : ℝ
h : support f ⊆ Ioc a b
hab : b ≤ a
⊢ Eq.{u_5 + 1} (α := E) (∫ (x : ℝ) in a..b, f x ∂μ) (∫ (x : ℝ), f x ∂μ)
have h₁ : f = 0
Tactic: rw [Ioc_eq_empty hab.not_gt, subset_empty_iff, support_eq_empty_iff] at h
Cleared hypotheses: h, hab