awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
Goal:
E : Type u_5
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
a b : ℝ
f : ℝ → E
μ : Measure ℝ
ha : IntegrableOn f (Ioi a) μ
hb : IntegrableOn f (Ioi b) μ
this :
  ∀ {a b : ℝ} (ha : IntegrableOn f (Ioi a) μ) (hb : IntegrableOn f (Ioi b) μ) (hab : a ≤ b),
    HAdd.hAdd (α := E) (∫ (x : ℝ) in a..b, f x ∂μ) (∫ (x : ℝ) in Ioi b, f x ∂μ) = ∫ (x : ℝ) in Ioi a, f x ∂μ
hab : ¬a ≤ b
⊢ -∫ (x : ℝ) in b..a, f x ∂μ + HAdd.hAdd (α := E) (∫ (x : ℝ) in b..a, f x ∂μ) (∫ (x : ℝ) in Ioi a, f x ∂μ) =
    ∫ (x : ℝ) in Ioi a, f x ∂μ

Tactic:
grind
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
Goal:
E : Type u_5
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
a_1 b_1 : ℝ
f : ℝ → E
μ : Measure ℝ
a b : ℝ
ha : IntegrableOn f (Ioi a) μ
hb : IntegrableOn f (Ioi b) μ
hab : a ≤ b
rw : HAdd.hAdd (α := E) (∫ (x : ℝ) in Ioc a b, f x ∂μ) (∫ (x : ℝ) in Ioi b, f x ∂μ) = ∫ (x : ℝ) in Ioi a, f x ∂μ
rw₁ : Eq.{u_5 + 1} (α := E) (∫ (x : ℝ) in Ioc a b ∪ Ioi b, f x ∂μ) (∫ (x : ℝ) in Ioi a, f x ∂μ)
rw₂ rw₃ : Eq.{u_5 + 1} (α := E) (∫ (x : ℝ) in Ioi a, f x ∂μ) (∫ (x : ℝ) in Ioi a, f x ∂μ)
⊢ HAdd.hAdd (α := E) (∫ (x : ℝ) in a..b, f x ∂μ) (∫ (x : ℝ) in Ioi b, f x ∂μ) = ∫ (x : ℝ) in Ioi a, f x ∂μ

Tactic:
rw [integral_of_le hab, ← setIntegral_union Ioc_disjoint_Ioi_same measurableSet_Ioi
    (ha.mono_set Ioc_subset_Ioi_self) hb, Ioc_union_Ioi_eq_Ioi hab]

Premises used: MeasureTheory.setIntegral_union, Set.Ioc_union_Ioi_eq_Ioi, measurableSet_Ioi, Set.Ioc_subset_Ioi_self, intervalIntegral.integral_of_le, MeasureTheory.IntegrableOn.mono_set, Set.Ioc_disjoint_Ioi_same
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
Goal:
E : Type u_5
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
a b : ℝ
f : ℝ → E
μ : Measure ℝ
ha : IntervalIntegrable f μ a b
hb : IntegrableOn f (Ioi b) μ
rw : IntegrableOn f (Ioi a) μ
⊢ HAdd.hAdd (α := E) (∫ (x : ℝ) in a..b, f x ∂μ) (∫ (x : ℝ) in Ioi b, f x ∂μ) = ∫ (x : ℝ) in Ioi a, f x ∂μ

Tactic:
rw [integral_interval_add_Ioi _ hb]

Premises used: intervalIntegral.integral_interval_add_Ioi
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
Goal:
E : Type u_5
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
a b : ℝ
f : ℝ → E
μ : Measure ℝ
ha : IntervalIntegrable f μ a b
hb : IntegrableOn f (Ioi b) μ
pos : ∀ (h : a ≤ b), IntegrableOn f (Ioi a) μ
neg : ∀ (h : b < a), IntegrableOn f (Ioi a) μ
⊢ IntegrableOn f (Ioi a) μ

Tactic:
by_cases! h : a ≤ b
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
Goal:
E : Type u_5
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
a b : ℝ
f : ℝ → E
μ : Measure ℝ
ha : IntervalIntegrable f μ a b
hb : IntegrableOn f (Ioi b) μ
h : a ≤ b
⊢ IntegrableOn f (Ioi a) μ

Tactic:
(Ioc_union_Ioi_eq_Ioi h) ▸ IntegrableOn.union
      ((intervalIntegrable_iff_integrableOn_Ioc_of_le h).1 ha) hb

Premises used: Set.Ioc_union_Ioi_eq_Ioi, intervalIntegrable_iff_integrableOn_Ioc_of_le, Eq.rec, MeasureTheory.IntegrableOn.union, Iff.mp
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
Goal:
E : Type u_5
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
a b : ℝ
f : ℝ → E
μ : Measure ℝ
ha : IntervalIntegrable f μ a b
hb : IntegrableOn f (Ioi b) μ
h : a ≤ b
⊢ IntegrableOn f (Ioi a) μ

Tactic:
exact (Ioc_union_Ioi_eq_Ioi h) ▸ IntegrableOn.union
      ((intervalIntegrable_iff_integrableOn_Ioc_of_le h).1 ha) hb
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
Goal:
E : Type u_5
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
a b : ℝ
f : ℝ → E
μ : Measure ℝ
ha : IntervalIntegrable f μ a b
hb : IntegrableOn f (Ioi b) μ
h : b < a
⊢ IntegrableOn f (Ioi a) μ

Tactic:
hb.mono_set <| Ioi_subset_Ioi h.le

Premises used: LT.lt.le, MeasureTheory.IntegrableOn.mono_set, Set.Ioi_subset_Ioi
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
Goal:
E : Type u_5
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
a b : ℝ
f : ℝ → E
μ : Measure ℝ
ha : IntervalIntegrable f μ a b
hb : IntegrableOn f (Ioi b) μ
h : b < a
⊢ IntegrableOn f (Ioi a) μ

Tactic:
exact hb.mono_set <| Ioi_subset_Ioi h.le

Premises used: LT.lt.le, MeasureTheory.IntegrableOn.mono_set, Set.Ioi_subset_Ioi
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
Goal:
E : Type u_5
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
a b : ℝ
f : ℝ → E
μ : Measure ℝ
hf : IntegrableOn f (Ioi a) μ
hab : a ≤ b
⊢ HSub.hSub (α := E) (∫ (x : ℝ) in Ioi a, f x ∂μ) (∫ (x : ℝ) in Ioi b, f x ∂μ) = ∫ (x : ℝ) in a..b, f x ∂μ

Tactic:
sub_eq_of_eq_add (integral_interval_add_Ioi hf (hf.mono_set (Ioi_subset_Ioi hab))).symm

Premises used: MeasureTheory.IntegrableOn.mono_set, Set.Ioi_subset_Ioi, sub_eq_of_eq_add, intervalIntegral.integral_interval_add_Ioi, Eq.symm
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
Goal:
E : Type u_5
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
a b : ℝ
f : ℝ → E
μ : Measure ℝ
hf : IntegrableOn f (Ioi a) μ
hg : IntegrableOn f (Ioi b) μ
inr :
  ∀
    (this :
      ∀ {a b : ℝ} (hf : IntegrableOn f (Ioi a) μ) (hg : IntegrableOn f (Ioi b) μ) (hab : a ≤ b),
        HSub.hSub (α := E) (∫ (x : ℝ) in Ioi a, f x ∂μ) (∫ (x : ℝ) in Ioi b, f x ∂μ) = ∫ (x : ℝ) in a..b, f x ∂μ)
    (hab : b < a),
    HSub.hSub (α := E) (∫ (x : ℝ) in Ioi a, f x ∂μ) (∫ (x : ℝ) in Ioi b, f x ∂μ) = ∫ (x : ℝ) in a..b, f x ∂μ
wlog! :
  ∀ {a b : ℝ} (hf : IntegrableOn f (Ioi a) μ) (hg : IntegrableOn f (Ioi b) μ) (hab : a ≤ b),
    HSub.hSub (α := E) (∫ (x : ℝ) in Ioi a, f x ∂μ) (∫ (x : ℝ) in Ioi b, f x ∂μ) = ∫ (x : ℝ) in a..b, f x ∂μ
⊢ HSub.hSub (α := E) (∫ (x : ℝ) in Ioi a, f x ∂μ) (∫ (x : ℝ) in Ioi b, f x ∂μ) = ∫ (x : ℝ) in a..b, f x ∂μ

Tactic:
wlog! hab : a ≤ b generalizing a b
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
Goal:
E : Type u_5
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
a b : ℝ
f : ℝ → E
μ : Measure ℝ
hf : IntegrableOn f (Ioi a) μ
hg : IntegrableOn f (Ioi b) μ
this :
  ∀ {a b : ℝ} (hf : IntegrableOn f (Ioi a) μ) (hg : IntegrableOn f (Ioi b) μ) (hab : a ≤ b),
    HSub.hSub (α := E) (∫ (x : ℝ) in Ioi a, f x ∂μ) (∫ (x : ℝ) in Ioi b, f x ∂μ) = ∫ (x : ℝ) in a..b, f x ∂μ
hab : b < a
inr : HSub.hSub (α := E) (∫ (x : ℝ) in Ioi a, f x ∂μ) (∫ (x : ℝ) in Ioi b, f x ∂μ) = -∫ (x : ℝ) in b..a, f x ∂μ
inr₁ :
  HSub.hSub (α := E) (∫ (x : ℝ) in Ioi a, f x ∂μ) (∫ (x : ℝ) in Ioi b, f x ∂μ) =
    -HSub.hSub (α := E) (∫ (x : ℝ) in Ioi b, f x ∂μ) (∫ (x : ℝ) in Ioi a, f x ∂μ)
inr₂ inr₃ :
  HSub.hSub (α := E) (∫ (x : ℝ) in Ioi a, f x ∂μ) (∫ (x : ℝ) in Ioi b, f x ∂μ) =
    HSub.hSub (α := E) (∫ (x : ℝ) in Ioi a, f x ∂μ) (∫ (x : ℝ) in Ioi b, f x ∂μ)
⊢ HSub.hSub (α := E) (∫ (x : ℝ) in Ioi a, f x ∂μ) (∫ (x : ℝ) in Ioi b, f x ∂μ) = ∫ (x : ℝ) in a..b, f x ∂μ

Tactic:
rw [integral_symm, ← this hg hf hab.le, neg_sub]

Premises used: neg_sub, LT.lt.le, intervalIntegral.integral_symm
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
Goal:
E : Type u_5
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
a_1 b_1 : ℝ
f : ℝ → E
μ : Measure ℝ
a b : ℝ
hf : IntegrableOn f (Ioi a) μ
hg : IntegrableOn f (Ioi b) μ
hab : a ≤ b
⊢ HSub.hSub (α := E) (∫ (x : ℝ) in Ioi a, f x ∂μ) (∫ (x : ℝ) in Ioi b, f x ∂μ) = ∫ (x : ℝ) in a..b, f x ∂μ

Tactic:
integral_Ioi_sub_Ioi hf hab

Premises used: intervalIntegral.integral_Ioi_sub_Ioi
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
Goal:
E : Type u_5
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
a_1 b_1 : ℝ
f : ℝ → E
μ : Measure ℝ
a b : ℝ
hf : IntegrableOn f (Ioi a) μ
hg : IntegrableOn f (Ioi b) μ
hab : a ≤ b
⊢ HSub.hSub (α := E) (∫ (x : ℝ) in Ioi a, f x ∂μ) (∫ (x : ℝ) in Ioi b, f x ∂μ) = ∫ (x : ℝ) in a..b, f x ∂μ

Tactic:
exact integral_Ioi_sub_Ioi hf hab

Premises used: intervalIntegral.integral_Ioi_sub_Ioi
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
Goal:
E : Type u_5
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
a b : ℝ
f : ℝ → E
μ : Measure ℝ
hf : IntegrableOn f (Iio b) μ
hab : a ≤ b
⊢ IntegrableOn f (Iio a) μ

Tactic:
have ha : IntegrableOn f (Iio a) μ := hf.mono_set (Iio_subset_Iio hab)
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
Goal:
E : Type u_5
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
a b : ℝ
f : ℝ → E
μ : Measure ℝ
hf : IntegrableOn f (Iio b) μ
hab : a ≤ b
ha : IntegrableOn f (Iio a) μ
⊢ IntegrableOn f (Ico a b) μ

Tactic:
have h : IntegrableOn f (Ico a b) μ := hf.mono_set Ico_subset_Iio_self
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
Goal:
E : Type u_5
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
a b : ℝ
f : ℝ → E
μ : Measure ℝ
hf : IntegrableOn f (Iio b) μ
hab : a ≤ b
ha : IntegrableOn f (Iio a) μ
h : IntegrableOn f (Ico a b) μ
⊢ Disjoint (Iio a) (Ico a b)

Tactic:
grind
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
Goal:
E : Type u_5
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
a b : ℝ
f : ℝ → E
μ : Measure ℝ
hf : IntegrableOn f (Iio b) μ
hab : a ≤ b
ha : IntegrableOn f (Iio a) μ
h : IntegrableOn f (Ico a b) μ
rw : ∫ (x : ℝ) in Iio b, f x ∂μ = HAdd.hAdd (α := E) (∫ (x : ℝ) in Iio a, f x ∂μ) (∫ (x : ℝ) in Ico a b, f x ∂μ)
rw₁ : Eq.{u_5 + 1} (α := E) (∫ (x : ℝ) in Iio b, f x ∂μ) (∫ (x : ℝ) in Iio a ∪ Ico a b, f x ∂μ)
rw₂ rw₃ : Eq.{u_5 + 1} (α := E) (∫ (x : ℝ) in Iio b, 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 Ico a b, f x ∂μ

Tactic:
rw [sub_eq_iff_eq_add', ← setIntegral_union (by grind) measurableSet_Ico ha h,
      Iio_union_Ico_eq_Iio hab]

Premises used: MeasureTheory.setIntegral_union, measurableSet_Ico, Set.Iio_union_Ico_eq_Iio, sub_eq_iff_eq_add'
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
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 ∂μ
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 ∂μ
⊢ 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
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
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 ∂μ)
inr₂ 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 ∂μ)
⊢ HSub.hSub (α := E) (∫ (x : ℝ) in Iio b, f x ∂μ) (∫ (x : ℝ) in Iio a, f x ∂μ) = ∫ (x : ℝ) in a..b, f x ∂μ

Tactic:
rw [integral_symm, ← this hg hf hab.le, neg_sub]

Premises used: neg_sub, LT.lt.le, intervalIntegral.integral_symm
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
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 ∂μ)
rw₂ rw₃ : Eq.{u_5 + 1} (α := E) (∫ (t : ℝ) in Ioc a b, f t ∂μ) (∫ (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 ∂μ

Tactic:
rw [integral_Iio_sub_Iio hf hab, integral_of_le hab, integral_Ico_eq_integral_Ioc]

Premises used: MeasureTheory.integral_Ico_eq_integral_Ioc, intervalIntegral.integral_of_le, intervalIntegral.integral_Iio_sub_Iio
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
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
⊢ IntegrableOn f (Ici b) μ

Tactic:
have ha : IntegrableOn f (Ici b) μ := hf.mono_set (Ici_subset_Ici.2 hab)
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
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) μ
⊢ IntegrableOn f (Ico a b) μ

Tactic:
have h : IntegrableOn f (Ico a b) μ := hf.mono_set Ico_subset_Ici_self
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
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) μ
⊢ Disjoint (Ici b) (Ico a b)

Tactic:
grind
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
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 ∂μ)
rw₃ rw₄ : Eq.{u_5 + 1} (α := E) (∫ (x : ℝ) in Ici a, 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 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]

Premises used: MeasureTheory.setIntegral_union, Set.Ico_union_Ici_eq_Ici, measurableSet_Ico, Set.union_comm, sub_eq_iff_eq_add'
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
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 ∂μ
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 ∂μ
⊢ 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
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
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 ∂μ)
inr₂ 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 ∂μ)
⊢ HSub.hSub (α := E) (∫ (x : ℝ) in Ici a, f x ∂μ) (∫ (x : ℝ) in Ici b, f x ∂μ) = ∫ (x : ℝ) in a..b, f x ∂μ

Tactic:
rw [integral_symm, ← this hg hf hab.le, neg_sub]

Premises used: neg_sub, LT.lt.le, intervalIntegral.integral_symm
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
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 ∂μ)
rw₂ rw₃ : Eq.{u_5 + 1} (α := E) (∫ (t : ℝ) in Ioc a b, f t ∂μ) (∫ (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 ∂μ

Tactic:
rw [integral_Ici_sub_Ici hf hab, integral_of_le hab, integral_Ico_eq_integral_Ioc]

Premises used: MeasureTheory.integral_Ico_eq_integral_Ioc, intervalIntegral.integral_of_le, intervalIntegral.integral_Ici_sub_Ici
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
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 : ℝ) in Iic b ∪ Ioi b, f x ∂μ

Tactic:
(setIntegral_union (Iic_disjoint_Ioi <| Eq.le rfl) measurableSet_Ioi h_left h_right).symm

Premises used: MeasureTheory.setIntegral_union, Set.Iic_disjoint_Ioi, Eq.le, measurableSet_Ioi, Eq.symm, rfl
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
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 (Iic b ∪ Ioi b)
⊢ HAdd.hAdd (α := E) (∫ (x : ℝ) in Iic b, f x ∂μ) (∫ (x : ℝ) in Ioi b, f x ∂μ) = ∫ (x : ℝ), f x ∂μ

Tactic:
convert! (setIntegral_union (Iic_disjoint_Ioi <| Eq.le rfl) measurableSet_Ioi h_left h_right).symm

Premises used: MeasureTheory.setIntegral_union, Set.Iic_disjoint_Ioi, Eq.le, measurableSet_Ioi, Eq.symm, rfl
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
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
h₁ h₂ : μ = μ
⊢ μ = μ.restrict (Iic b ∪ Ioi b)

Tactic:
rw [Iic_union_Ioi, Measure.restrict_univ]

Premises used: Set.Iic_union_Ioi, MeasureTheory.Measure.restrict_univ
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
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 : ℝ) in Iio b ∪ Ici b, f x ∂μ

Tactic:
(setIntegral_union (Iio_disjoint_Ici <| Eq.le rfl) measurableSet_Ici h_left h_right).symm

Premises used: MeasureTheory.setIntegral_union, Eq.le, Set.Iio_disjoint_Ici, Eq.symm, measurableSet_Ici, rfl
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
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 (Iio b ∪ Ici b)
⊢ HAdd.hAdd (α := E) (∫ (x : ℝ) in Iio b, f x ∂μ) (∫ (x : ℝ) in Ici b, f x ∂μ) = ∫ (x : ℝ), f x ∂μ

Tactic:
convert! (setIntegral_union (Iio_disjoint_Ici <| Eq.le rfl) measurableSet_Ici h_left h_right).symm

Premises used: MeasureTheory.setIntegral_union, Eq.le, Set.Iio_disjoint_Ici, Eq.symm, measurableSet_Ici, rfl
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
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
h₁ h₂ : μ = μ
⊢ μ = μ.restrict (Iio b ∪ Ici b)

Tactic:
rw [Iio_union_Ici, Measure.restrict_univ]

Premises used: Set.Iio_union_Ici, MeasureTheory.Measure.restrict_univ
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
Goal:
E : Type u_5
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
a b : ℝ
μ : Measure ℝ
inst_2 : CompleteSpace E
inst_3 : IsFiniteMeasure μ
c : E
simp : ∫ (x : ℝ) in a..b, c ∂μ = HSub.hSub (α := E) (∫ (x : ℝ) in Iic b, c ∂μ) (∫ (x : ℝ) in Iic a, c ∂μ)
⊢ ∫ (x : ℝ) in a..b, c ∂μ = (μ.real (Iic b) - μ.real (Iic a)) • c

Tactic:
simp only [sub_smul, ← setIntegral_const]

Premises used: sub_smul, MeasureTheory.setIntegral_const
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
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 ∂μ)

Tactic:
(integral_Iic_sub_Iic ?_ ?_).symm

Premises used: intervalIntegral.integral_Iic_sub_Iic, Eq.symm
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
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) μ
refine_2 : IntegrableOn.{0, u_5} (ε := E) (fun (x : ℝ) ↦ c) (Iic b) μ
⊢ ∫ (x : ℝ) in a..b, c ∂μ = HSub.hSub (α := E) (∫ (x : ℝ) in Iic b, c ∂μ) (∫ (x : ℝ) in Iic a, c ∂μ)

Tactic:
refine (integral_Iic_sub_Iic ?_ ?_).symm

Premises used: intervalIntegral.integral_Iic_sub_Iic, Eq.symm
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
Goal:
E : Type u_5
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
a b : ℝ
μ : Measure ℝ
inst_2 : CompleteSpace E
inst_3 : IsFiniteMeasure μ
c : E
⊢ IntegrableOn.{0, u_5} (ε := E) (fun (x : ℝ) ↦ c) (Iic a) μ

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
Goal:
E : Type u_5
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
a b : ℝ
μ : Measure ℝ
inst_2 : CompleteSpace E
inst_3 : IsFiniteMeasure μ
c : E
⊢ IntegrableOn.{0, u_5} (ε := E) (fun (x : ℝ) ↦ c) (Iic b) μ

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
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 ∂μ)
inr : ∀ (hab : b ≤ a), 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 ∂μ)

Tactic:
rcases le_total a b with hab | hab

Premises used: le_total
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
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 ∂μ)
inl₂ inl₃ : Eq.{u_5 + 1} (α := E) (∫ (x : ℝ), f x ∂μ) (∫ (x : ℝ), f x ∂μ)
⊢ Eq.{u_5 + 1} (α := E) (∫ (x : ℝ) in a..b, f x ∂μ) (∫ (x : ℝ), f x ∂μ)

Tactic:
rw [integral_of_le hab, ← integral_indicator measurableSet_Ioc, indicator_eq_self.2 h]

Premises used: Iff.mpr, MeasureTheory.integral_indicator, Set.indicator_eq_self, intervalIntegral.integral_of_le, measurableSet_Ioc