awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic (goal)
Goal:
E : Type u_5
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
a b c : ℝ
f : ℝ → E
μ : 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 ∂μ
⊢ HAdd.hAdd (α := E) (∫ (x : ℝ) in Ioc a b ∪ Ioc b c, f x ∂μ) (∫ (x : ℝ) in Ioc c a, f x ∂μ) =
    HAdd.hAdd (α := E) (∫ (x : ℝ) in Ioc b a, f x ∂μ) (∫ (x : ℝ) in Ioc c b, f x ∂μ) + ∫ (x : ℝ) in Ioc a c, f x ∂μ
have hst : Disjoint (Ioc a b ∪ Ioc b c) (Ioc c a)
Tactic: rw [← setIntegral_union]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic (goal)
Goal:
E : Type u_5
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
a b c : ℝ
f : ℝ → E
μ : Measure ℝ
hab : IntervalIntegrable f μ a b
hbc : IntervalIntegrable f μ b c
hac : IntervalIntegrable f μ a c
rw :
  ∫ (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)
⊢ HAdd.hAdd (α := E) (∫ (x : ℝ) in Ioc a b ∪ Ioc b c, f x ∂μ) (∫ (x : ℝ) in Ioc c a, f x ∂μ) =
    HAdd.hAdd (α := E) (∫ (x : ℝ) in Ioc b a, f x ∂μ) (∫ (x : ℝ) in Ioc c b, f x ∂μ) + ∫ (x : ℝ) in Ioc a c, f x ∂μ
have ht : MeasurableSet (Ioc c a)
Tactic: rw [← setIntegral_union]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic (goal)
Goal:
E : Type u_5
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
a b c : ℝ
f : ℝ → E
μ : Measure ℝ
hab : IntervalIntegrable f μ a b
hbc : IntervalIntegrable f μ b c
hac : IntervalIntegrable f μ a c
rw :
  ∫ (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)
⊢ HAdd.hAdd (α := E) (∫ (x : ℝ) in Ioc a b ∪ Ioc b c, f x ∂μ) (∫ (x : ℝ) in Ioc c a, f x ∂μ) =
    HAdd.hAdd (α := E) (∫ (x : ℝ) in Ioc b a, f x ∂μ) (∫ (x : ℝ) in Ioc c b, f x ∂μ) + ∫ (x : ℝ) in Ioc a c, f x ∂μ
have hfs : IntegrableOn f (Ioc a b ∪ Ioc b c) μ
Tactic: rw [← setIntegral_union]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic (goal)
Goal:
E : Type u_5
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
a b c : ℝ
f : ℝ → E
μ : Measure ℝ
hab : IntervalIntegrable f μ a b
hbc : IntervalIntegrable f μ b c
hac : IntervalIntegrable f μ a c
rw :
  ∫ (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) μ
⊢ HAdd.hAdd (α := E) (∫ (x : ℝ) in Ioc a b ∪ Ioc b c, f x ∂μ) (∫ (x : ℝ) in Ioc c a, f x ∂μ) =
    HAdd.hAdd (α := E) (∫ (x : ℝ) in Ioc b a, f x ∂μ) (∫ (x : ℝ) in Ioc c b, f x ∂μ) + ∫ (x : ℝ) in Ioc a c, f x ∂μ
have hft : IntegrableOn f (Ioc c a) μ
Tactic: rw [← setIntegral_union]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic (goal)
Goal:
E : Type u_5
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
a b c : ℝ
f : ℝ → E
μ : Measure ℝ
hab : IntervalIntegrable f μ a b
hbc : IntervalIntegrable f μ b c
hac : IntervalIntegrable f μ a c
⊢ ∫ (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 ∂μ
have 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 ∂μ)
Tactic: rw [← setIntegral_union]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic (goal)
Goal:
E : Type u_5
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
a b c : ℝ
f : ℝ → E
μ : Measure ℝ
hab : IntervalIntegrable f μ a b
hbc : IntervalIntegrable f μ b c
hac : IntervalIntegrable f μ a c
rw :
  ∫ (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 ∂μ)
⊢ ∫ (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 ∂μ
have hst : Disjoint (Ioc b a) (Ioc c b)
Tactic: rw [← setIntegral_union]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic (goal)
Goal:
E : Type u_5
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
a b c : ℝ
f : ℝ → E
μ : Measure ℝ
hab : IntervalIntegrable f μ a b
hbc : IntervalIntegrable f μ b c
hac : IntervalIntegrable f μ a c
rw :
  ∫ (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)
⊢ ∫ (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 ∂μ
have ht : MeasurableSet (Ioc c b)
Tactic: rw [← setIntegral_union]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic (goal)
Goal:
E : Type u_5
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
a b c : ℝ
f : ℝ → E
μ : Measure ℝ
hab : IntervalIntegrable f μ a b
hbc : IntervalIntegrable f μ b c
hac : IntervalIntegrable f μ a c
rw :
  ∫ (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)
⊢ ∫ (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 ∂μ
have hfs : IntegrableOn f (Ioc b a) μ
Tactic: rw [← setIntegral_union]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic (goal)
Goal:
E : Type u_5
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
a b c : ℝ
f : ℝ → E
μ : Measure ℝ
hab : IntervalIntegrable f μ a b
hbc : IntervalIntegrable f μ b c
hac : IntervalIntegrable f μ a c
rw :
  ∫ (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) μ
⊢ ∫ (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 ∂μ
have hft : IntegrableOn f (Ioc c b) μ
Tactic: rw [← setIntegral_union]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic (goal)
Goal:
E : Type u_5
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
a b c : ℝ
f : ℝ → E
μ : Measure ℝ
hab : IntervalIntegrable f μ a b
hbc : IntervalIntegrable f μ b c
hac : IntervalIntegrable f μ a c
⊢ ∫ (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 ∂μ)
have 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 ∂μ)
Tactic: rw [← setIntegral_union]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic (goal)
Goal:
E : Type u_5
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
a b c : ℝ
f : ℝ → E
μ : Measure ℝ
hab : IntervalIntegrable f μ a b
hbc : IntervalIntegrable f μ b c
hac : IntervalIntegrable f μ a c
rw :
  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 ∂μ)
⊢ ∫ (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 ∂μ)
have hst : Disjoint (Ioc b a ∪ Ioc c b) (Ioc a c)
Tactic: rw [← setIntegral_union]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic (goal)
Goal:
E : Type u_5
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
a b c : ℝ
f : ℝ → E
μ : Measure ℝ
hab : IntervalIntegrable f μ a b
hbc : IntervalIntegrable f μ b c
hac : IntervalIntegrable f μ a c
rw :
  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)
⊢ ∫ (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 ∂μ)
have ht : MeasurableSet (Ioc a c)
Tactic: rw [← setIntegral_union]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic (goal)
Goal:
E : Type u_5
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
a b c : ℝ
f : ℝ → E
μ : Measure ℝ
hab : IntervalIntegrable f μ a b
hbc : IntervalIntegrable f μ b c
hac : IntervalIntegrable f μ a c
rw :
  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)
⊢ ∫ (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 ∂μ)
have hfs : IntegrableOn f (Ioc b a ∪ Ioc c b) μ
Tactic: rw [← setIntegral_union]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic (goal)
Goal:
E : Type u_5
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
a b c : ℝ
f : ℝ → E
μ : Measure ℝ
hab : IntervalIntegrable f μ a b
hbc : IntervalIntegrable f μ b c
hac : IntervalIntegrable f μ a c
rw :
  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) μ
⊢ ∫ (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 ∂μ)
have hft : IntegrableOn f (Ioc a c) μ
Tactic: rw [← setIntegral_union]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic (goal)
Goal:
E : Type u_5
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
a b c : ℝ
f : ℝ → E
μ : Measure ℝ
hab : IntervalIntegrable f μ a b
hbc : IntervalIntegrable f μ b c
hac : IntervalIntegrable f μ a c
⊢ HAdd.hAdd (α := E) (∫ (x : ℝ) in Ioc a b, f x ∂μ) (∫ (x : ℝ) in Ioc b c, f x ∂μ) + ∫ (x : ℝ) in Ioc c a, f x ∂μ =
    HAdd.hAdd (α := E) (∫ (x : ℝ) in Ioc b a, f x ∂μ) (∫ (x : ℝ) in Ioc c b, f x ∂μ) + ∫ (x : ℝ) in Ioc a c, f x ∂μ
have 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 ∂μ)
Tactic: iterate 4 rw [← setIntegral_union]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic (goal)
Goal:
E : Type u_5
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
a b c : ℝ
f : ℝ → E
μ : Measure ℝ
hab : IntervalIntegrable f μ a b
hbc : IntervalIntegrable f μ b c
hac : IntervalIntegrable f μ a c
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 ∂μ)
⊢ HAdd.hAdd (α := E) (∫ (x : ℝ) in Ioc a b, f x ∂μ) (∫ (x : ℝ) in Ioc b c, f x ∂μ) + ∫ (x : ℝ) in Ioc c a, f x ∂μ =
    HAdd.hAdd (α := E) (∫ (x : ℝ) in Ioc b a, f x ∂μ) (∫ (x : ℝ) in Ioc c b, f x ∂μ) + ∫ (x : ℝ) in Ioc a c, f x ∂μ
have hst : Disjoint (Ioc b a ∪ Ioc c b) (Ioc a c)
Tactic: iterate 4 rw [← setIntegral_union]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic (goal)
Goal:
E : Type u_5
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
a b c : ℝ
f : ℝ → E
μ : Measure ℝ
hab : IntervalIntegrable f μ a b
hbc : IntervalIntegrable f μ b c
hac : IntervalIntegrable f μ a c
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)
⊢ HAdd.hAdd (α := E) (∫ (x : ℝ) in Ioc a b, f x ∂μ) (∫ (x : ℝ) in Ioc b c, f x ∂μ) + ∫ (x : ℝ) in Ioc c a, f x ∂μ =
    HAdd.hAdd (α := E) (∫ (x : ℝ) in Ioc b a, f x ∂μ) (∫ (x : ℝ) in Ioc c b, f x ∂μ) + ∫ (x : ℝ) in Ioc a c, f x ∂μ
have ht : MeasurableSet (Ioc a c)
Tactic: iterate 4 rw [← setIntegral_union]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic (goal)
Goal:
E : Type u_5
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
a b c : ℝ
f : ℝ → E
μ : Measure ℝ
hab : IntervalIntegrable f μ a b
hbc : IntervalIntegrable f μ b c
hac : IntervalIntegrable f μ a c
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)
⊢ HAdd.hAdd (α := E) (∫ (x : ℝ) in Ioc a b, f x ∂μ) (∫ (x : ℝ) in Ioc b c, f x ∂μ) + ∫ (x : ℝ) in Ioc c a, f x ∂μ =
    HAdd.hAdd (α := E) (∫ (x : ℝ) in Ioc b a, f x ∂μ) (∫ (x : ℝ) in Ioc c b, f x ∂μ) + ∫ (x : ℝ) in Ioc a c, f x ∂μ
have hfs : IntegrableOn f (Ioc b a ∪ Ioc c b) μ
Tactic: iterate 4 rw [← setIntegral_union]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic (goal)
Goal:
E : Type u_5
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
a b c : ℝ
f : ℝ → E
μ : Measure ℝ
hab : IntervalIntegrable f μ a b
hbc : IntervalIntegrable f μ b c
hac : IntervalIntegrable f μ a c
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) μ
⊢ HAdd.hAdd (α := E) (∫ (x : ℝ) in Ioc a b, f x ∂μ) (∫ (x : ℝ) in Ioc b c, f x ∂μ) + ∫ (x : ℝ) in Ioc c a, f x ∂μ =
    HAdd.hAdd (α := E) (∫ (x : ℝ) in Ioc b a, f x ∂μ) (∫ (x : ℝ) in Ioc c b, f x ∂μ) + ∫ (x : ℝ) in Ioc a c, f x ∂μ
have hft : IntegrableOn f (Ioc a c) μ
Tactic: iterate 4 rw [← setIntegral_union]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic (goal)
Goal:
E : Type u_5
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
a b c : ℝ
f : ℝ → E
μ : Measure ℝ
hab : IntervalIntegrable f μ a b
hbc : IntervalIntegrable f μ b c
hac : IntervalIntegrable f μ a c
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) μ
⊢ HAdd.hAdd (α := E) (∫ (x : ℝ) in Ioc a b, f x ∂μ) (∫ (x : ℝ) in Ioc b c, f x ∂μ) + ∫ (x : ℝ) in Ioc c a, f x ∂μ =
    HAdd.hAdd (α := E) (∫ (x : ℝ) in Ioc b a, f x ∂μ) (∫ (x : ℝ) in Ioc c b, f x ∂μ) + ∫ (x : ℝ) in Ioc a c, f x ∂μ
have hst₁ : Disjoint (Ioc b a) (Ioc c b)
Tactic: iterate 4 rw [← setIntegral_union]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic (goal)
Goal:
E : Type u_5
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
a b c : ℝ
f : ℝ → E
μ : Measure ℝ
hab : IntervalIntegrable f μ a b
hbc : IntervalIntegrable f μ b c
hac : IntervalIntegrable f μ a c
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)
⊢ HAdd.hAdd (α := E) (∫ (x : ℝ) in Ioc a b, f x ∂μ) (∫ (x : ℝ) in Ioc b c, f x ∂μ) + ∫ (x : ℝ) in Ioc c a, f x ∂μ =
    HAdd.hAdd (α := E) (∫ (x : ℝ) in Ioc b a, f x ∂μ) (∫ (x : ℝ) in Ioc c b, f x ∂μ) + ∫ (x : ℝ) in Ioc a c, f x ∂μ
have ht₁ : MeasurableSet (Ioc c b)
Tactic: iterate 4 rw [← setIntegral_union]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic (goal)
Goal:
E : Type u_5
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
a b c : ℝ
f : ℝ → E
μ : Measure ℝ
hab : IntervalIntegrable f μ a b
hbc : IntervalIntegrable f μ b c
hac : IntervalIntegrable f μ a c
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)
⊢ HAdd.hAdd (α := E) (∫ (x : ℝ) in Ioc a b, f x ∂μ) (∫ (x : ℝ) in Ioc b c, f x ∂μ) + ∫ (x : ℝ) in Ioc c a, f x ∂μ =
    HAdd.hAdd (α := E) (∫ (x : ℝ) in Ioc b a, f x ∂μ) (∫ (x : ℝ) in Ioc c b, f x ∂μ) + ∫ (x : ℝ) in Ioc a c, f x ∂μ
have hfs₁ : IntegrableOn f (Ioc b a) μ
Tactic: iterate 4 rw [← setIntegral_union]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic (goal)
Goal:
E : Type u_5
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
a b c : ℝ
f : ℝ → E
μ : Measure ℝ
hab : IntervalIntegrable f μ a b
hbc : IntervalIntegrable f μ b c
hac : IntervalIntegrable f μ a c
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) μ
⊢ HAdd.hAdd (α := E) (∫ (x : ℝ) in Ioc a b, f x ∂μ) (∫ (x : ℝ) in Ioc b c, f x ∂μ) + ∫ (x : ℝ) in Ioc c a, f x ∂μ =
    HAdd.hAdd (α := E) (∫ (x : ℝ) in Ioc b a, f x ∂μ) (∫ (x : ℝ) in Ioc c b, f x ∂μ) + ∫ (x : ℝ) in Ioc a c, f x ∂μ
have hft₁ : IntegrableOn f (Ioc c b) μ
Tactic: iterate 4 rw [← setIntegral_union]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic (goal)
Goal:
E : Type u_5
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
a b c : ℝ
f : ℝ → E
μ : Measure ℝ
hab : IntervalIntegrable f μ a b
hbc : IntervalIntegrable f μ b c
hac : IntervalIntegrable f μ a c
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) μ
⊢ HAdd.hAdd (α := E) (∫ (x : ℝ) in Ioc a b, f x ∂μ) (∫ (x : ℝ) in Ioc b c, f x ∂μ) + ∫ (x : ℝ) in Ioc c a, f x ∂μ =
    HAdd.hAdd (α := E) (∫ (x : ℝ) in Ioc b a, f x ∂μ) (∫ (x : ℝ) in Ioc c b, f x ∂μ) + ∫ (x : ℝ) in Ioc a c, f x ∂μ
have hst₂ : Disjoint (Ioc a b ∪ Ioc b c) (Ioc c a)
Tactic: iterate 4 rw [← setIntegral_union]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic (goal)
Goal:
E : Type u_5
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
a b c : ℝ
f : ℝ → E
μ : Measure ℝ
hab : IntervalIntegrable f μ a b
hbc : IntervalIntegrable f μ b c
hac : IntervalIntegrable f μ a c
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)
⊢ HAdd.hAdd (α := E) (∫ (x : ℝ) in Ioc a b, f x ∂μ) (∫ (x : ℝ) in Ioc b c, f x ∂μ) + ∫ (x : ℝ) in Ioc c a, f x ∂μ =
    HAdd.hAdd (α := E) (∫ (x : ℝ) in Ioc b a, f x ∂μ) (∫ (x : ℝ) in Ioc c b, f x ∂μ) + ∫ (x : ℝ) in Ioc a c, f x ∂μ
have ht₂ : MeasurableSet (Ioc c a)
Tactic: iterate 4 rw [← setIntegral_union]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic (goal)
Goal:
E : Type u_5
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
a b c : ℝ
f : ℝ → E
μ : Measure ℝ
hab : IntervalIntegrable f μ a b
hbc : IntervalIntegrable f μ b c
hac : IntervalIntegrable f μ a c
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)
⊢ HAdd.hAdd (α := E) (∫ (x : ℝ) in Ioc a b, f x ∂μ) (∫ (x : ℝ) in Ioc b c, f x ∂μ) + ∫ (x : ℝ) in Ioc c a, f x ∂μ =
    HAdd.hAdd (α := E) (∫ (x : ℝ) in Ioc b a, f x ∂μ) (∫ (x : ℝ) in Ioc c b, f x ∂μ) + ∫ (x : ℝ) in Ioc a c, f x ∂μ
have hfs₂ : IntegrableOn f (Ioc a b ∪ Ioc b c) μ
Tactic: iterate 4 rw [← setIntegral_union]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic (goal)
Goal:
E : Type u_5
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
a b c : ℝ
f : ℝ → E
μ : Measure ℝ
hab : IntervalIntegrable f μ a b
hbc : IntervalIntegrable f μ b c
hac : IntervalIntegrable f μ a c
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) μ
⊢ HAdd.hAdd (α := E) (∫ (x : ℝ) in Ioc a b, f x ∂μ) (∫ (x : ℝ) in Ioc b c, f x ∂μ) + ∫ (x : ℝ) in Ioc c a, f x ∂μ =
    HAdd.hAdd (α := E) (∫ (x : ℝ) in Ioc b a, f x ∂μ) (∫ (x : ℝ) in Ioc c b, f x ∂μ) + ∫ (x : ℝ) in Ioc a c, f x ∂μ
have hft₂ : IntegrableOn f (Ioc c a) μ
Tactic: iterate 4 rw [← setIntegral_union]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic (goal)
Goal:
E : Type u_5
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
a b c : ℝ
f : ℝ → E
μ : Measure ℝ
hab : IntervalIntegrable f μ a b
hbc : IntervalIntegrable f μ b c
hac : IntervalIntegrable f μ a c
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) μ
⊢ HAdd.hAdd (α := E) (∫ (x : ℝ) in Ioc a b, f x ∂μ) (∫ (x : ℝ) in Ioc b c, f x ∂μ) + ∫ (x : ℝ) in Ioc c a, f x ∂μ =
    HAdd.hAdd (α := E) (∫ (x : ℝ) in Ioc b a, f x ∂μ) (∫ (x : ℝ) in Ioc c b, f x ∂μ) + ∫ (x : ℝ) in Ioc a c, f x ∂μ
have hst₃ : Disjoint (Ioc a b) (Ioc b c)
Tactic: iterate 4 rw [← setIntegral_union]