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
hc : c ≠ 0
d : ℝ
⊢ ∫ (x : ℝ) in a..b, f (d + x / c) = HSMul.hSMul (β := E) c (∫ (x : ℝ) in d + a / c..d + b / c, f x)

Tactic:
simpa only [div_eq_inv_mul, inv_inv] using integral_comp_add_mul f (inv_ne_zero hc) d

Premises used: intervalIntegral.integral_comp_add_mul, inv_inv, inv_ne_zero, div_eq_inv_mul
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
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
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
⊢ 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
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
Goal:
E : Type u_5
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
a b : ℝ
f : ℝ → E
c d : ℝ
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:
simp [hc, integral_comp_add_div]

Premises used: intervalIntegral.integral_comp_add_div
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
Goal:
E : Type u_5
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
a b : ℝ
f : ℝ → E
c d : ℝ
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:
simp [hc, integral_comp_add_div]

Premises used: intervalIntegral.integral_comp_add_div
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
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)

Tactic:
simpa only [sub_eq_add_neg] using integral_comp_mul_add f hc (-d)

Premises used: sub_eq_add_neg, intervalIntegral.integral_comp_mul_add, Neg.neg
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
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
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
⊢ 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
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
Goal:
E : Type u_5
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
a b : ℝ
f : ℝ → E
c d : ℝ
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:
simp [hc, integral_comp_mul_sub]

Premises used: intervalIntegral.integral_comp_mul_sub
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
Goal:
E : Type u_5
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
a b : ℝ
f : ℝ → E
c d : ℝ
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:
simp [hc, integral_comp_mul_sub]

Premises used: intervalIntegral.integral_comp_mul_sub
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
Goal:
E : Type u_5
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
a b c : ℝ
f : ℝ → E
hc : c ≠ 0
d : ℝ
simp : ∫ (x : ℝ) in a..b, f (d + -c * x) = HSMul.hSMul (β := E) c⁻¹ (∫ (x : ℝ) in d + -c * b..d + -c * a, f x)
⊢ ∫ (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]

Premises used: sub_eq_add_neg, neg_mul_eq_neg_mul
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
Goal:
E : Type u_5
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
a b c : ℝ
f : ℝ → E
hc : c ≠ 0
d : ℝ
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)
⊢ ∫ (x : ℝ) in a..b, f (d + -c * 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]

Premises used: Iff.mpr, intervalIntegral.integral_comp_add_mul, intervalIntegral.integral_symm, neg_ne_zero
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
Goal:
E : Type u_5
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
a b c : ℝ
f : ℝ → E
hc : c ≠ 0
d : ℝ
⊢ 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:
simp only [inv_neg, smul_neg, neg_neg, neg_smul]

Premises used: neg_smul, inv_neg, neg_neg, smul_neg
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
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
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
⊢ 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
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
Goal:
E : Type u_5
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
a b : ℝ
f : ℝ → E
c d : ℝ
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:
simp [hc, integral_comp_sub_mul]

Premises used: intervalIntegral.integral_comp_sub_mul
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
Goal:
E : Type u_5
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
a b : ℝ
f : ℝ → E
c d : ℝ
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:
simp [hc, integral_comp_sub_mul]

Premises used: intervalIntegral.integral_comp_sub_mul
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
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 (x / c - d) = HSMul.hSMul (β := E) c (∫ (x : ℝ) in a / c - d..b / c - d, f x)

Tactic:
simpa only [div_eq_inv_mul, inv_inv] using integral_comp_mul_sub f (inv_ne_zero hc) d

Premises used: intervalIntegral.integral_comp_mul_sub, inv_inv, inv_ne_zero, div_eq_inv_mul
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
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
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
⊢ 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
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
Goal:
E : Type u_5
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
a b : ℝ
f : ℝ → E
c d : ℝ
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:
simp [hc, integral_comp_div_sub]

Premises used: intervalIntegral.integral_comp_div_sub
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
Goal:
E : Type u_5
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
a b : ℝ
f : ℝ → E
c d : ℝ
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:
simp [hc, integral_comp_div_sub]

Premises used: intervalIntegral.integral_comp_div_sub
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
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 - x / c) = HSMul.hSMul (β := E) c (∫ (x : ℝ) in d - b / c..d - a / c, f x)

Tactic:
simpa only [div_eq_inv_mul, inv_inv] using integral_comp_sub_mul f (inv_ne_zero hc) d

Premises used: intervalIntegral.integral_comp_sub_mul, inv_inv, inv_ne_zero, div_eq_inv_mul
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
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
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
⊢ 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
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
Goal:
E : Type u_5
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
a b : ℝ
f : ℝ → E
c d : ℝ
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:
simp [hc, integral_comp_sub_div]

Premises used: intervalIntegral.integral_comp_sub_div
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
Goal:
E : Type u_5
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
a b : ℝ
f : ℝ → E
c d : ℝ
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:
simp [hc, integral_comp_sub_div]

Premises used: intervalIntegral.integral_comp_sub_div
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
Goal:
E : Type u_5
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
a b : ℝ
f : ℝ → E
d : ℝ
⊢ Eq.{u_5 + 1} (α := E) (∫ (x : ℝ) in a..b, f (x - d)) (∫ (x : ℝ) in a - d..b - d, f x)

Tactic:
simpa only [sub_eq_add_neg] using integral_comp_add_right f (-d)

Premises used: sub_eq_add_neg, intervalIntegral.integral_comp_add_right, Neg.neg
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
Goal:
E : Type u_5
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
a b : ℝ
f : ℝ → E
d : ℝ
⊢ Eq.{u_5 + 1} (α := E) (∫ (x : ℝ) in a..b, f (d - x)) (∫ (x : ℝ) in d - b..d - a, f x)

Tactic:
simpa only [one_mul, one_smul, inv_one] using integral_comp_sub_mul f one_ne_zero d

Premises used: inv_one, one_smul, intervalIntegral.integral_comp_sub_mul, one_ne_zero, one_mul
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
Goal:
E : Type u_5
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
a b : ℝ
f : ℝ → E
⊢ Eq.{u_5 + 1} (α := E) (∫ (x : ℝ) in a..b, f (-x)) (∫ (x : ℝ) in -b..-a, f x)

Tactic:
simpa only [zero_sub] using integral_comp_sub_left f 0

Premises used: intervalIntegral.integral_comp_sub_left, OfNat.ofNat, zero_sub
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
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 ∂μ)
inr : ∀ (hab : b ≤ a), 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 ∂μ)

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 g : ℝ → E
μ : Measure ℝ
a b : ℝ
h : EqOn f g [[a, b]]
hab : a ≤ b
⊢ Eq.{u_5 + 1} (α := E) (∫ (x : ℝ) in a..b, f x ∂μ) (∫ (x : ℝ) in a..b, g x ∂μ)

Tactic:
simpa [hab, integral_of_le, integral_of_ge] using
      setIntegral_congr_fun measurableSet_Ioc (h.mono Ioc_subset_Icc_self)

Premises used: Set.Ioc_subset_Icc_self, intervalIntegral.integral_of_ge, intervalIntegral.integral_of_le, MeasureTheory.setIntegral_congr_fun, measurableSet_Ioc, Set.EqOn.mono
-- Module: Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
Goal:
E : Type u_5
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f g : ℝ → E
μ : Measure ℝ
a b : ℝ
h : EqOn f g [[a, b]]
hab : b ≤ a
⊢ Eq.{u_5 + 1} (α := E) (∫ (x : ℝ) in a..b, f x ∂μ) (∫ (x : ℝ) in a..b, g x ∂μ)

Tactic:
simpa [hab, integral_of_le, integral_of_ge] using
      setIntegral_congr_fun measurableSet_Ioc (h.mono Ioc_subset_Icc_self)

Premises used: Set.Ioc_subset_Icc_self, intervalIntegral.integral_of_ge, intervalIntegral.integral_of_le, MeasureTheory.setIntegral_congr_fun, measurableSet_Ioc, Set.EqOn.mono
-- 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
⊢ IntervalIntegrable f μ a c

Tactic:
have hac := hab.trans hbc
-- 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
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 ∂μ
⊢ HAdd.hAdd (α := E) (∫ (x : ℝ) in a..b, f x ∂μ) (∫ (x : ℝ) in b..c, f x ∂μ) + ∫ (x : ℝ) in c..a, f x ∂μ = 0

Tactic:
simp only [intervalIntegral, sub_add_sub_comm, sub_eq_zero]

Premises used: sub_eq_zero, intervalIntegral, sub_add_sub_comm
-- 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
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) μ
hft : IntegrableOn f (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 ∂μ

Tactic:
rw [← setIntegral_union]

Premises used: MeasureTheory.setIntegral_union
-- 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
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 ∂μ
hst : Disjoint (Ioc a b ∪ Ioc b c) (Ioc c a)
ht : MeasurableSet (Ioc c a)
hfs : IntegrableOn f (Ioc a b ∪ Ioc b c) μ
hft : IntegrableOn f (Ioc c a) μ
⊢ 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]

Premises used: MeasureTheory.setIntegral_union
-- 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
rw :
  ∫ (x : ℝ) in Ioc a b ∪ Ioc b c ∪ Ioc c a, f x ∂μ =
    HAdd.hAdd (α := E) (∫ (x : ℝ) in Ioc b a ∪ Ioc c b, f x ∂μ) (∫ (x : ℝ) in Ioc a c, f x ∂μ)
hst : Disjoint (Ioc b a) (Ioc c b)
ht : MeasurableSet (Ioc c b)
hfs : IntegrableOn f (Ioc b a) μ
hft : IntegrableOn f (Ioc c b) μ
⊢ ∫ (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]

Premises used: MeasureTheory.setIntegral_union
-- 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
rw :
  Eq.{u_5 + 1} (α := E) (∫ (x : ℝ) in Ioc a b ∪ Ioc b c ∪ Ioc c a, f x ∂μ)
    (∫ (x : ℝ) in Ioc b a ∪ Ioc c b ∪ Ioc a c, f x ∂μ)
hst : Disjoint (Ioc b a ∪ Ioc c b) (Ioc a c)
ht : MeasurableSet (Ioc a c)
hfs : IntegrableOn f (Ioc b a ∪ Ioc c b) μ
hft : IntegrableOn f (Ioc a c) μ
⊢ ∫ (x : ℝ) in Ioc a b ∪ Ioc b c ∪ Ioc c a, f x ∂μ =
    HAdd.hAdd (α := E) (∫ (x : ℝ) in Ioc b a ∪ Ioc c b, f x ∂μ) (∫ (x : ℝ) in Ioc a c, f x ∂μ)

Tactic:
rw [← setIntegral_union]

Premises used: MeasureTheory.setIntegral_union
-- 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
iterate :
  Eq.{u_5 + 1} (α := E) (∫ (x : ℝ) in Ioc a b ∪ Ioc b c ∪ Ioc c a, f x ∂μ)
    (∫ (x : ℝ) in Ioc b a ∪ Ioc c b ∪ Ioc a c, f x ∂μ)
hst : Disjoint (Ioc b a ∪ Ioc c b) (Ioc a c)
ht : MeasurableSet (Ioc a c)
hfs : IntegrableOn f (Ioc b a ∪ Ioc c b) μ
hft : IntegrableOn f (Ioc a c) μ
hst₁ : Disjoint (Ioc b a) (Ioc c b)
ht₁ : MeasurableSet (Ioc c b)
hfs₁ : IntegrableOn f (Ioc b a) μ
hft₁ : IntegrableOn f (Ioc c b) μ
hst₂ : Disjoint (Ioc a b ∪ Ioc b c) (Ioc c a)
ht₂ : MeasurableSet (Ioc c a)
hfs₂ : IntegrableOn f (Ioc a b ∪ Ioc b c) μ
hft₂ : IntegrableOn f (Ioc c a) μ
hst₃ : Disjoint (Ioc a b) (Ioc b c)
ht₃ : MeasurableSet (Ioc b c)
hfs₃ : IntegrableOn f (Ioc a b) μ
hft₃ : IntegrableOn f (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 ∂μ

Tactic:
iterate 4 rw [← setIntegral_union]

Premises used: MeasureTheory.setIntegral_union
-- 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
this : Ioc a b ∪ Ioc b c ∪ Ioc c a = Ioc b a ∪ Ioc c b ∪ Ioc a c
rw rw₁ :
  Eq.{u_5 + 1} (α := E) (∫ (x : ℝ) in Ioc b a ∪ Ioc c b ∪ Ioc a c, f x ∂μ)
    (∫ (x : ℝ) in Ioc b a ∪ Ioc c b ∪ Ioc a c, f x ∂μ)
⊢ Eq.{u_5 + 1} (α := E) (∫ (x : ℝ) in Ioc a b ∪ Ioc b c ∪ Ioc c a, f x ∂μ)
    (∫ (x : ℝ) in Ioc b a ∪ Ioc c b ∪ Ioc a c, f x ∂μ)

Tactic:
rw [this]
-- 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
suffices : Ioc a b ∪ Ioc b c ∪ Ioc c a = Ioc b a ∪ Ioc c b ∪ Ioc a c
⊢ Eq.{u_5 + 1} (α := E) (∫ (x : ℝ) in Ioc a b ∪ Ioc b c ∪ Ioc c a, f x ∂μ)
    (∫ (x : ℝ) in Ioc b a ∪ Ioc c b ∪ Ioc a c, f x ∂μ)

Tactic:
suffices Ioc a b ∪ Ioc b c ∪ Ioc c a = Ioc b a ∪ Ioc c b ∪ Ioc a c by rw [this]
-- 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
rw : Ioc (min a (min b c)) (max a (max b c)) = Ioc b a ∪ Ioc c b ∪ Ioc a c
rw₁ : Ioc (min a (min b c)) (max a (max b c)) = Ioc b a ∪ Ioc a c ∪ Ioc c b
rw₂ : Ioc (min a (min b c)) (max a (max b c)) = Ioc (min b (min a c)) (max b (max a c))
rw₃ : Ioc (min b (min a c)) (max a (max b c)) = Ioc (min b (min a c)) (max b (max a c))
rw₄ rw₅ : Ioc (min b (min a c)) (max b (max a c)) = Ioc (min b (min a c)) (max b (max a c))
⊢ Ioc a b ∪ Ioc b c ∪ Ioc c a = Ioc b a ∪ Ioc c b ∪ Ioc a c

Tactic:
rw [Ioc_union_Ioc_union_Ioc_cycle, union_right_comm, Ioc_union_Ioc_union_Ioc_cycle,
      min_left_comm, max_left_comm]

Premises used: max_left_comm, Set.Ioc_union_Ioc_union_Ioc_cycle, min_left_comm, Set.union_right_comm
-- 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 b a ∪ Ioc c b) (Ioc a 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 a 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 b a ∪ Ioc c 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 a 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
⊢ Disjoint (Ioc b a) (Ioc c 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
⊢ MeasurableSet (Ioc c 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 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 c 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
⊢ Disjoint (Ioc a b ∪ Ioc b c) (Ioc c a)

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

Premises used: And.right, And.left