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 c : ℝ
f : ℝ → E
μ : Measure ℝ
hab : IntervalIntegrable f μ a b
hbc : IntervalIntegrable f μ b c
hac : IntervalIntegrable f μ a c
⊢ MeasurableSet (Ioc c a)

Tactic:
simp [*, hab.1, hab.2, hbc.1, hbc.2, hac.1, hac.2]

Premises used: And.right, And.left
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
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
⊢ IntegrableOn f (Ioc a b ∪ Ioc b c) μ

Tactic:
simp [*, hab.1, hab.2, hbc.1, hbc.2, hac.1, hac.2]

Premises used: And.right, And.left
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
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
⊢ IntegrableOn f (Ioc c a) μ

Tactic:
simp [*, hab.1, hab.2, hbc.1, hbc.2, hac.1, hac.2]

Premises used: And.right, And.left
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
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
⊢ Disjoint (Ioc a b) (Ioc b c)

Tactic:
simp [*, hab.1, hab.2, hbc.1, hbc.2, hac.1, hac.2]

Premises used: And.right, And.left
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
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
⊢ MeasurableSet (Ioc b c)

Tactic:
simp [*, hab.1, hab.2, hbc.1, hbc.2, hac.1, hac.2]

Premises used: And.right, And.left
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
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
⊢ IntegrableOn f (Ioc a b) μ

Tactic:
simp [*, hab.1, hab.2, hbc.1, hbc.2, hac.1, hac.2]

Premises used: And.right, And.left
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
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
⊢ IntegrableOn f (Ioc b c) μ

Tactic:
simp [*, hab.1, hab.2, hbc.1, hbc.2, hac.1, hac.2]

Premises used: And.right, And.left
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
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
rw : HAdd.hAdd (α := E) (∫ (x : ℝ) in a..b, f x ∂μ) (∫ (x : ℝ) in b..c, f x ∂μ) + -∫ (x : ℝ) in a..c, f x ∂μ = 0
rw₁ : HAdd.hAdd (α := E) (∫ (x : ℝ) in a..b, f x ∂μ) (∫ (x : ℝ) in b..c, f x ∂μ) + ∫ (x : ℝ) in c..a, f x ∂μ = 0
rw₂ rw₃ : Eq.{u_5 + 1} (α := E) 0 0
⊢ HAdd.hAdd (α := E) (∫ (x : ℝ) in a..b, f x ∂μ) (∫ (x : ℝ) in b..c, f x ∂μ) = ∫ (x : ℝ) in a..c, f x ∂μ

Tactic:
rw [← add_neg_eq_zero, ← integral_symm, integral_add_adjacent_intervals_cancel hab hbc]

Premises used: add_neg_eq_zero, intervalIntegral.integral_symm, intervalIntegral.integral_add_adjacent_intervals_cancel
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
Goal:
E : Type u_5
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℝ → E
μ : Measure ℝ
a : ℕ → ℝ
m n : ℕ
hmn : m ≤ n
hint : ∀ k ∈ Ico m n, IntervalIntegrable f μ (a k) (a (k + 1))
revert :
  ∀ (hint : ∀ k ∈ Ico m n, IntervalIntegrable f μ (a k) (a (k + 1))),
    Eq.{u_5 + 1} (α := E) (∑ k ∈ Finset.Ico m n, ∫ (x : ℝ) in a k..a (k + 1), f x ∂μ) (∫ (x : ℝ) in a m..a n, f x ∂μ)
⊢ Eq.{u_5 + 1} (α := E) (∑ k ∈ Finset.Ico m n, ∫ (x : ℝ) in a k..a (k + 1), f x ∂μ) (∫ (x : ℝ) in a m..a n, f x ∂μ)

Tactic:
revert hint
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
Goal:
E : Type u_5
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℝ → E
μ : Measure ℝ
a : ℕ → ℝ
m n : ℕ
hmn : m ≤ n
⊢ ∀ (hint : ∀ k ∈ Ico m n, IntervalIntegrable f μ (a k) (a (k + 1))),
    Eq.{u_5 + 1} (α := E) (∑ k ∈ Finset.Ico m n, ∫ (x : ℝ) in a k..a (k + 1), f x ∂μ) (∫ (x : ℝ) in a m..a n, f x ∂μ)

Tactic:
Nat.le_induction ?_ ?_ n hmn

Premises used: Nat.le_induction
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
Goal:
E : Type u_5
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℝ → E
μ : Measure ℝ
a : ℕ → ℝ
m n : ℕ
hmn : m ≤ n
refine_1 :
  ∀ (hint : ∀ k ∈ Ico m m, IntervalIntegrable f μ (a k) (a (k + 1))),
    Eq.{u_5 + 1} (α := E) (∑ k ∈ Finset.Ico m m, ∫ (x : ℝ) in a k..a (k + 1), f x ∂μ) (∫ (x : ℝ) in a m..a m, f x ∂μ)
refine_2 :
  ∀ (n : ℕ) (hmn : m ≤ n),
    (∀ (hint : ∀ k ∈ Ico m n, IntervalIntegrable f μ (a k) (a (k + 1))),
        Eq.{u_5 + 1} (α := E) (∑ k ∈ Finset.Ico m n, ∫ (x : ℝ) in a k..a (k + 1), f x ∂μ)
          (∫ (x : ℝ) in a m..a n, f x ∂μ)) →
      ∀ (hint : ∀ k ∈ Ico m (n + 1), IntervalIntegrable f μ (a k) (a (k + 1))),
        Eq.{u_5 + 1} (α := E) (∑ k ∈ Finset.Ico m (n + 1), ∫ (x : ℝ) in a k..a (k + 1), f x ∂μ)
          (∫ (x : ℝ) in a m..a (n + 1), f x ∂μ)
⊢ ∀ (hint : ∀ k ∈ Ico m n, IntervalIntegrable f μ (a k) (a (k + 1))),
    Eq.{u_5 + 1} (α := E) (∑ k ∈ Finset.Ico m n, ∫ (x : ℝ) in a k..a (k + 1), f x ∂μ) (∫ (x : ℝ) in a m..a n, f x ∂μ)

Tactic:
refine Nat.le_induction ?_ ?_ n hmn
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
Goal:
E : Type u_5
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℝ → E
μ : Measure ℝ
a : ℕ → ℝ
m n : ℕ
hmn : m ≤ n
⊢ ∀ (hint : ∀ k ∈ Ico m m, IntervalIntegrable f μ (a k) (a (k + 1))),
    Eq.{u_5 + 1} (α := E) (∑ k ∈ Finset.Ico m m, ∫ (x : ℝ) in a k..a (k + 1), f x ∂μ) (∫ (x : ℝ) in a m..a m, f x ∂μ)

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
Goal:
E : Type u_5
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℝ → E
μ : Measure ℝ
a : ℕ → ℝ
m n : ℕ
hmn : m ≤ n
p : ℕ
hmp : m ≤ p
IH :
  ∀ (hint : ∀ k ∈ Ico m p, IntervalIntegrable f μ (a k) (a (k + 1))),
    Eq.{u_5 + 1} (α := E) (∑ k ∈ Finset.Ico m p, ∫ (x : ℝ) in a k..a (k + 1), f x ∂μ) (∫ (x : ℝ) in a m..a p, f x ∂μ)
h : ∀ k ∈ Ico m (p + 1), IntervalIntegrable f μ (a k) (a (k + 1))
refine_2 : IntervalIntegrable f μ (a m) (a p)
refine_2₁ : IntervalIntegrable f μ (a p) (a (p + 1))
refine_2₂ : ∀ k ∈ Ico m p, IntervalIntegrable f μ (a k) (a (k + 1))
⊢ Eq.{u_5 + 1} (α := E) (∑ k ∈ Finset.Ico m (p + 1), ∫ (x : ℝ) in a k..a (k + 1), f x ∂μ)
    (∫ (x : ℝ) in a m..a (p + 1), f x ∂μ)

Tactic:
rw [Finset.sum_Ico_succ_top hmp, IH, integral_add_adjacent_intervals]

Premises used: intervalIntegral.integral_add_adjacent_intervals, Finset.sum_Ico_succ_top
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
Goal:
E : Type u_5
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℝ → E
μ : Measure ℝ
a : ℕ → ℝ
m n : ℕ
hmn : m ≤ n
p : ℕ
hmp : m ≤ p
IH :
  ∀ (hint : ∀ k ∈ Ico m p, IntervalIntegrable f μ (a k) (a (k + 1))),
    Eq.{u_5 + 1} (α := E) (∑ k ∈ Finset.Ico m p, ∫ (x : ℝ) in a k..a (k + 1), f x ∂μ) (∫ (x : ℝ) in a m..a p, f x ∂μ)
h : ∀ k ∈ Ico m (p + 1), IntervalIntegrable f μ (a k) (a (k + 1))
⊢ IntervalIntegrable f μ (a m) (a p)

Tactic:
IntervalIntegrable.trans_iterate_Ico hmp fun k hk => h k ?_

Premises used: IntervalIntegrable.trans_iterate_Ico
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
Goal:
E : Type u_5
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℝ → E
μ : Measure ℝ
a : ℕ → ℝ
m n : ℕ
hmn : m ≤ n
p : ℕ
hmp : m ≤ p
IH :
  ∀ (hint : ∀ k ∈ Ico m p, IntervalIntegrable f μ (a k) (a (k + 1))),
    Eq.{u_5 + 1} (α := E) (∑ k ∈ Finset.Ico m p, ∫ (x : ℝ) in a k..a (k + 1), f x ∂μ) (∫ (x : ℝ) in a m..a p, f x ∂μ)
h : ∀ k ∈ Ico m (p + 1), IntervalIntegrable f μ (a k) (a (k + 1))
refine_2 : ∀ (k : ℕ) (hk : k ∈ Ico m p), k ∈ Ico m (p + 1)
⊢ IntervalIntegrable f μ (a m) (a p)

Tactic:
refine IntervalIntegrable.trans_iterate_Ico hmp fun k hk => h k ?_

Premises used: IntervalIntegrable.trans_iterate_Ico
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
Goal:
E : Type u_5
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℝ → E
μ : Measure ℝ
a : ℕ → ℝ
m n : ℕ
hmn : m ≤ n
p : ℕ
hmp : m ≤ p
IH :
  ∀ (hint : ∀ k ∈ Ico m p, IntervalIntegrable f μ (a k) (a (k + 1))),
    Eq.{u_5 + 1} (α := E) (∑ k ∈ Finset.Ico m p, ∫ (x : ℝ) in a k..a (k + 1), f x ∂μ) (∫ (x : ℝ) in a m..a p, f x ∂μ)
h : ∀ k ∈ Ico m (p + 1), IntervalIntegrable f μ (a k) (a (k + 1))
k : ℕ
hk : k ∈ Ico m p
⊢ k ∈ Ico m (p + 1)

Tactic:
(Ico_subset_Ico le_rfl (Nat.le_succ _)) hk

Premises used: le_rfl, Set.Mem, Nat.le_succ, Set.Ico_subset_Ico
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
Goal:
E : Type u_5
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℝ → E
μ : Measure ℝ
a : ℕ → ℝ
m n : ℕ
hmn : m ≤ n
p : ℕ
hmp : m ≤ p
IH :
  ∀ (hint : ∀ k ∈ Ico m p, IntervalIntegrable f μ (a k) (a (k + 1))),
    Eq.{u_5 + 1} (α := E) (∑ k ∈ Finset.Ico m p, ∫ (x : ℝ) in a k..a (k + 1), f x ∂μ) (∫ (x : ℝ) in a m..a p, f x ∂μ)
h : ∀ k ∈ Ico m (p + 1), IntervalIntegrable f μ (a k) (a (k + 1))
k : ℕ
hk : k ∈ Ico m p
⊢ k ∈ Ico m (p + 1)

Tactic:
exact (Ico_subset_Ico le_rfl (Nat.le_succ _)) hk

Premises used: le_rfl, Nat.le_succ, Set.Ico_subset_Ico
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
Goal:
E : Type u_5
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℝ → E
μ : Measure ℝ
a : ℕ → ℝ
m n : ℕ
hmn : m ≤ n
p : ℕ
hmp : m ≤ p
IH :
  ∀ (hint : ∀ k ∈ Ico m p, IntervalIntegrable f μ (a k) (a (k + 1))),
    Eq.{u_5 + 1} (α := E) (∑ k ∈ Finset.Ico m p, ∫ (x : ℝ) in a k..a (k + 1), f x ∂μ) (∫ (x : ℝ) in a m..a p, f x ∂μ)
h : ∀ k ∈ Ico m (p + 1), IntervalIntegrable f μ (a k) (a (k + 1))
refine_2 : p ∈ Ico m (p + 1)
⊢ IntervalIntegrable f μ (a p) (a (p + 1))

Tactic:
apply h
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
Goal:
E : Type u_5
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℝ → E
μ : Measure ℝ
a : ℕ → ℝ
m n : ℕ
hmn : m ≤ n
p : ℕ
hmp : m ≤ p
IH :
  ∀ (hint : ∀ k ∈ Ico m p, IntervalIntegrable f μ (a k) (a (k + 1))),
    Eq.{u_5 + 1} (α := E) (∑ k ∈ Finset.Ico m p, ∫ (x : ℝ) in a k..a (k + 1), f x ∂μ) (∫ (x : ℝ) in a m..a p, f x ∂μ)
h : ∀ k ∈ Ico m (p + 1), IntervalIntegrable f μ (a k) (a (k + 1))
⊢ p ∈ Ico m (p + 1)

Tactic:
simp [hmp]
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
Goal:
E : Type u_5
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℝ → E
μ : Measure ℝ
a : ℕ → ℝ
m n : ℕ
hmn : m ≤ n
p : ℕ
hmp : m ≤ p
IH :
  ∀ (hint : ∀ k ∈ Ico m p, IntervalIntegrable f μ (a k) (a (k + 1))),
    Eq.{u_5 + 1} (α := E) (∑ k ∈ Finset.Ico m p, ∫ (x : ℝ) in a k..a (k + 1), f x ∂μ) (∫ (x : ℝ) in a m..a p, f x ∂μ)
h : ∀ k ∈ Ico m (p + 1), IntervalIntegrable f μ (a k) (a (k + 1))
k : ℕ
hk : k ∈ Ico m p
⊢ IntervalIntegrable f μ (a k) (a (k + 1))

Tactic:
h _ (Ico_subset_Ico_right p.le_succ hk)

Premises used: Nat.le_succ, Set.Ico_subset_Ico_right
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
Goal:
E : Type u_5
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℝ → E
μ : Measure ℝ
a : ℕ → ℝ
m n : ℕ
hmn : m ≤ n
p : ℕ
hmp : m ≤ p
IH :
  ∀ (hint : ∀ k ∈ Ico m p, IntervalIntegrable f μ (a k) (a (k + 1))),
    Eq.{u_5 + 1} (α := E) (∑ k ∈ Finset.Ico m p, ∫ (x : ℝ) in a k..a (k + 1), f x ∂μ) (∫ (x : ℝ) in a m..a p, f x ∂μ)
h : ∀ k ∈ Ico m (p + 1), IntervalIntegrable f μ (a k) (a (k + 1))
k : ℕ
hk : k ∈ Ico m p
⊢ IntervalIntegrable f μ (a k) (a (k + 1))

Tactic:
exact h _ (Ico_subset_Ico_right p.le_succ hk)

Premises used: Nat.le_succ, Set.Ico_subset_Ico_right
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
Goal:
E : Type u_5
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℝ → E
μ : Measure ℝ
a : ℕ → ℝ
n : ℕ
hint : ∀ k < n, IntervalIntegrable f μ (a k) (a (k + 1))
rw : Eq.{u_5 + 1} (α := E) (∑ k ∈ Finset.Ico 0 n, ∫ (x : ℝ) in a k..a (k + 1), f x ∂μ) (∫ (x : ℝ) in a 0..a n, f x ∂μ)
⊢ Eq.{u_5 + 1} (α := E) (∑ k ∈ Finset.range n, ∫ (x : ℝ) in a k..a (k + 1), f x ∂μ) (∫ (x : ℝ) in a 0..a n, f x ∂μ)

Tactic:
rw [← Nat.Ico_zero_eq_range]

Premises used: Nat.Ico_zero_eq_range
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
Goal:
E : Type u_5
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℝ → E
μ : Measure ℝ
a : ℕ → ℝ
n : ℕ
hint : ∀ k < n, IntervalIntegrable f μ (a k) (a (k + 1))
⊢ Eq.{u_5 + 1} (α := E) (∑ k ∈ Finset.Ico 0 n, ∫ (x : ℝ) in a k..a (k + 1), f x ∂μ) (∫ (x : ℝ) in a 0..a n, f x ∂μ)

Tactic:
sum_integral_adjacent_intervals_Ico zero_le fun k hk => hint k hk.2

Premises used: zero_le, intervalIntegral.sum_integral_adjacent_intervals_Ico, And.right
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
Goal:
E : Type u_5
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℝ → E
μ : Measure ℝ
a : ℕ → ℝ
n : ℕ
hint : ∀ k < n, IntervalIntegrable f μ (a k) (a (k + 1))
⊢ Eq.{u_5 + 1} (α := E) (∑ k ∈ Finset.Ico 0 n, ∫ (x : ℝ) in a k..a (k + 1), f x ∂μ) (∫ (x : ℝ) in a 0..a n, f x ∂μ)

Tactic:
exact sum_integral_adjacent_intervals_Ico zero_le fun k hk => hint k hk.2

Premises used: zero_le, intervalIntegral.sum_integral_adjacent_intervals_Ico, And.right
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
Goal:
E : Type u_5
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
a b c : ℝ
f : ℝ → E
μ : Measure ℝ
hab : IntervalIntegrable f μ a b
hac : IntervalIntegrable f μ a c
⊢ HSub.hSub (α := E) (∫ (x : ℝ) in a..b, f x ∂μ) (∫ (x : ℝ) in a..c, f x ∂μ) = ∫ (x : ℝ) in c..b, f x ∂μ

Tactic:
sub_eq_of_eq_add' <| Eq.symm <| integral_add_adjacent_intervals hac (hac.symm.trans hab)

Premises used: sub_eq_of_eq_add', intervalIntegral.integral_add_adjacent_intervals, IntervalIntegrable.symm, IntervalIntegrable.trans, Eq.symm
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
Goal:
E : Type u_5
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
a b c d : ℝ
f : ℝ → E
μ : Measure ℝ
hab : IntervalIntegrable f μ a b
hcd : IntervalIntegrable f μ c d
hac : IntervalIntegrable f μ a c
rw :
  HAdd.hAdd (α := E) (∫ (x : ℝ) in a..b, f x ∂μ) (∫ (x : ℝ) in c..d, f x ∂μ) =
    HAdd.hAdd (α := E) (∫ (x : ℝ) in a..c, f x ∂μ) (∫ (x : ℝ) in c..d, f x ∂μ) + ∫ (x : ℝ) in c..b, f x ∂μ
rw₁ :
  HAdd.hAdd (α := E) (∫ (x : ℝ) in a..b, f x ∂μ) (∫ (x : ℝ) in c..d, f x ∂μ) =
    ∫ (x : ℝ) in a..c, f x ∂μ + HAdd.hAdd (α := E) (∫ (x : ℝ) in c..d, f x ∂μ) (∫ (x : ℝ) in c..b, f x ∂μ)
rw₂ :
  HAdd.hAdd (α := E) (∫ (x : ℝ) in a..b, f x ∂μ) (∫ (x : ℝ) in c..d, f x ∂μ) =
    ∫ (x : ℝ) in c..d, f x ∂μ + HAdd.hAdd (α := E) (∫ (x : ℝ) in a..c, f x ∂μ) (∫ (x : ℝ) in c..b, f x ∂μ)
rw₃ :
  HAdd.hAdd (α := E) (∫ (x : ℝ) in a..b, f x ∂μ) (∫ (x : ℝ) in c..d, f x ∂μ) =
    HAdd.hAdd (α := E) (∫ (x : ℝ) in c..d, f x ∂μ) (∫ (x : ℝ) in a..b, f x ∂μ)
rw₄ rw₅ :
  HAdd.hAdd (α := E) (∫ (x : ℝ) in c..d, f x ∂μ) (∫ (x : ℝ) in a..b, f x ∂μ) =
    HAdd.hAdd (α := E) (∫ (x : ℝ) in c..d, f x ∂μ) (∫ (x : ℝ) in a..b, f x ∂μ)
⊢ HAdd.hAdd (α := E) (∫ (x : ℝ) in a..b, f x ∂μ) (∫ (x : ℝ) in c..d, f x ∂μ) =
    HAdd.hAdd (α := E) (∫ (x : ℝ) in a..d, f x ∂μ) (∫ (x : ℝ) in c..b, f x ∂μ)

Tactic:
rw [← integral_add_adjacent_intervals hac hcd, add_assoc, add_left_comm,
    integral_add_adjacent_intervals hac (hac.symm.trans hab), add_comm]

Premises used: add_left_comm, add_assoc, intervalIntegral.integral_add_adjacent_intervals, add_comm, IntervalIntegrable.symm, IntervalIntegrable.trans
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
Goal:
E : Type u_5
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
a b c d : ℝ
f : ℝ → E
μ : Measure ℝ
hab : IntervalIntegrable f μ a b
hcd : IntervalIntegrable f μ c d
hac : IntervalIntegrable f μ a c
⊢ HSub.hSub (α := E) (∫ (x : ℝ) in a..b, f x ∂μ) (∫ (x : ℝ) in c..d, f x ∂μ) =
    HSub.hSub (α := E) (∫ (x : ℝ) in a..c, f x ∂μ) (∫ (x : ℝ) in b..d, f x ∂μ)

Tactic:
simp only [sub_eq_add_neg, ← integral_symm,
    integral_interval_add_interval_comm hab hcd.symm (hac.trans hcd)]

Premises used: sub_eq_add_neg, intervalIntegral.integral_symm, IntervalIntegrable.symm, IntervalIntegrable.trans, intervalIntegral.integral_interval_add_interval_comm
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
Goal:
E : Type u_5
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
a b c d : ℝ
f : ℝ → E
μ : Measure ℝ
hab : IntervalIntegrable f μ a b
hcd : IntervalIntegrable f μ c d
hac : IntervalIntegrable f μ a c
rw :
  HSub.hSub (α := E) (∫ (x : ℝ) in a..c, f x ∂μ) (∫ (x : ℝ) in b..d, f x ∂μ) =
    HSub.hSub (α := E) (∫ (x : ℝ) in d..b, f x ∂μ) (∫ (x : ℝ) in c..a, f x ∂μ)
rw₁ :
  HSub.hSub (α := E) (∫ (x : ℝ) in a..c, f x ∂μ) (∫ (x : ℝ) in b..d, f x ∂μ) =
    HSub.hSub (α := E) (-∫ (x : ℝ) in b..d, f x ∂μ) (∫ (x : ℝ) in c..a, f x ∂μ)
rw₂ :
  HSub.hSub (α := E) (∫ (x : ℝ) in a..c, f x ∂μ) (∫ (x : ℝ) in b..d, f x ∂μ) =
    HSub.hSub (α := E) (-∫ (x : ℝ) in b..d, f x ∂μ) (-∫ (x : ℝ) in a..c, f x ∂μ)
rw₃ :
  HSub.hSub (α := E) (∫ (x : ℝ) in a..c, f x ∂μ) (∫ (x : ℝ) in b..d, f x ∂μ) =
    HAdd.hAdd (α := E) (-∫ (x : ℝ) in b..d, f x ∂μ) (∫ (x : ℝ) in a..c, f x ∂μ)
rw₄ rw₅ :
  HAdd.hAdd (α := E) (-∫ (x : ℝ) in b..d, f x ∂μ) (∫ (x : ℝ) in a..c, f x ∂μ) =
    HAdd.hAdd (α := E) (-∫ (x : ℝ) in b..d, f x ∂μ) (∫ (x : ℝ) in a..c, f x ∂μ)
⊢ HSub.hSub (α := E) (∫ (x : ℝ) in a..b, f x ∂μ) (∫ (x : ℝ) in c..d, f x ∂μ) =
    HSub.hSub (α := E) (∫ (x : ℝ) in d..b, f x ∂μ) (∫ (x : ℝ) in c..a, f x ∂μ)

Tactic:
rw [integral_interval_sub_interval_comm hab hcd hac, integral_symm b d, integral_symm a c,
    sub_neg_eq_add, sub_eq_neg_add]

Premises used: sub_eq_neg_add, intervalIntegral.integral_symm, intervalIntegral.integral_interval_sub_interval_comm, sub_neg_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 ℝ
ha : IntegrableOn f (Iic a) μ
hb : IntegrableOn f (Iic b) μ
inr :
  ∀
    (this :
      ∀ {a b : ℝ} (ha : IntegrableOn f (Iic a) μ) (hb : IntegrableOn f (Iic b) μ) (hab : a ≤ b),
        HSub.hSub (α := E) (∫ (x : ℝ) in Iic b, f x ∂μ) (∫ (x : ℝ) in Iic a, f x ∂μ) = ∫ (x : ℝ) in a..b, f x ∂μ)
    (hab : ¬a ≤ b),
    HSub.hSub (α := E) (∫ (x : ℝ) in Iic b, f x ∂μ) (∫ (x : ℝ) in Iic a, f x ∂μ) = ∫ (x : ℝ) in a..b, f x ∂μ
wlog :
  ∀ {a b : ℝ} (ha : IntegrableOn f (Iic a) μ) (hb : IntegrableOn f (Iic b) μ) (hab : a ≤ b),
    HSub.hSub (α := E) (∫ (x : ℝ) in Iic b, f x ∂μ) (∫ (x : ℝ) in Iic a, f x ∂μ) = ∫ (x : ℝ) in a..b, f x ∂μ
⊢ HSub.hSub (α := E) (∫ (x : ℝ) in Iic b, f x ∂μ) (∫ (x : ℝ) in Iic 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 ℝ
ha : IntegrableOn f (Iic a) μ
hb : IntegrableOn f (Iic b) μ
this :
  ∀ {a b : ℝ} (ha : IntegrableOn f (Iic a) μ) (hb : IntegrableOn f (Iic b) μ) (hab : a ≤ b),
    HSub.hSub (α := E) (∫ (x : ℝ) in Iic b, f x ∂μ) (∫ (x : ℝ) in Iic a, f x ∂μ) = ∫ (x : ℝ) in a..b, f x ∂μ
hab : ¬a ≤ b
inr : HSub.hSub (α := E) (∫ (x : ℝ) in Iic b, f x ∂μ) (∫ (x : ℝ) in Iic a, f x ∂μ) = -∫ (x : ℝ) in b..a, f x ∂μ
inr₁ :
  HSub.hSub (α := E) (∫ (x : ℝ) in Iic b, f x ∂μ) (∫ (x : ℝ) in Iic a, f x ∂μ) =
    -HSub.hSub (α := E) (∫ (x : ℝ) in Iic a, f x ∂μ) (∫ (x : ℝ) in Iic b, f x ∂μ)
inr₂ inr₃ :
  HSub.hSub (α := E) (∫ (x : ℝ) in Iic b, f x ∂μ) (∫ (x : ℝ) in Iic a, f x ∂μ) =
    HSub.hSub (α := E) (∫ (x : ℝ) in Iic b, f x ∂μ) (∫ (x : ℝ) in Iic a, f x ∂μ)
⊢ HSub.hSub (α := E) (∫ (x : ℝ) in Iic b, f x ∂μ) (∫ (x : ℝ) in Iic a, f x ∂μ) = ∫ (x : ℝ) in a..b, f x ∂μ

Tactic:
rw [integral_symm, ← this hb ha (le_of_not_ge hab), neg_sub]

Premises used: neg_sub, le_of_not_ge, 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 : ℝ
ha : IntegrableOn f (Iic a) μ
hb : IntegrableOn f (Iic b) μ
hab : a ≤ b
ht : MeasurableSet (Ioc a b)
hfs : IntegrableOn f (Iic a) μ
hft : IntegrableOn f (Ioc a b) μ
⊢ HSub.hSub (α := E) (∫ (x : ℝ) in Iic b, f x ∂μ) (∫ (x : ℝ) in Iic a, f x ∂μ) = ∫ (x : ℝ) in a..b, f x ∂μ

Tactic:
rw [sub_eq_iff_eq_add', integral_of_le hab, ← setIntegral_union (Iic_disjoint_Ioc le_rfl),
    Iic_union_Ioc_eq_Iic hab]

Premises used: MeasureTheory.setIntegral_union, le_rfl, Set.Iic_union_Ioc_eq_Iic, intervalIntegral.integral_of_le, Set.Iic_disjoint_Ioc, sub_eq_iff_eq_add'
-- 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 (Iic a) μ
hb : IntegrableOn f (Iic b) μ
hab : a ≤ b
⊢ MeasurableSet (Ioc a b)

Tactic:
measurableSet_Ioc

Premises used: measurableSet_Ioc
-- 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 (Iic a) μ
hb : IntegrableOn f (Iic b) μ
hab : a ≤ b
⊢ IntegrableOn f (Iic a) μ

Tactic:
ha
-- 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 (Iic a) μ
hb : IntegrableOn f (Iic b) μ
hab : a ≤ b
⊢ IntegrableOn f (Ioc a b) μ

Tactic:
hb.mono_set fun _ => And.right

Premises used: MeasureTheory.IntegrableOn.mono_set, And.right
-- 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 (Iic a) μ
hb : IntegrableOn f (Iic b) μ
hab : a ≤ b
⊢ MeasurableSet (Ioc a b)

Tactic:
exacts [measurableSet_Ioc, ha, hb.mono_set fun _ => And.right]

Premises used: MeasureTheory.IntegrableOn.mono_set, And.right, measurableSet_Ioc
-- 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) μ
inr :
  ∀
    (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),
    HAdd.hAdd (α := E) (∫ (x : ℝ) in a..b, f x ∂μ) (∫ (x : ℝ) in Ioi b, f x ∂μ) = ∫ (x : ℝ) in Ioi a, f x ∂μ
wlog :
  ∀ {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 ∂μ
⊢ HAdd.hAdd (α := E) (∫ (x : ℝ) in a..b, f x ∂μ) (∫ (x : ℝ) in Ioi b, f x ∂μ) = ∫ (x : ℝ) in Ioi a, 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 ℝ
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
inr :
  -∫ (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 ∂μ
⊢ HAdd.hAdd (α := E) (∫ (x : ℝ) in a..b, f x ∂μ) (∫ (x : ℝ) in Ioi b, f x ∂μ) = ∫ (x : ℝ) in Ioi a, f x ∂μ

Tactic:
rw [integral_symm, ← this hb ha (le_of_not_ge hab)]

Premises used: le_of_not_ge, intervalIntegral.integral_symm