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
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)
⊢ 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 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) μ
hft₂ : IntegrableOn f (Ioc c a) μ
hst₃ : Disjoint (Ioc a b) (Ioc b c)
ht₃ : MeasurableSet (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 hfs₃ : IntegrableOn f (Ioc a 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) μ
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) μ
⊢ 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 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
this : 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 ∂μ)
have 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 ∂μ)
Tactic: rw [this]
-- 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
⊢ 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 ∂μ)
have suffices : Ioc a b ∪ Ioc b c ∪ Ioc c a = Ioc b a ∪ Ioc c b ∪ Ioc a c
Tactic: suffices Ioc a b ∪ Ioc b c ∪ Ioc c a = Ioc b a ∪ Ioc c b ∪ Ioc a c by rw [this]
-- 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
⊢ Ioc a b ∪ Ioc b c ∪ Ioc c a = Ioc b a ∪ Ioc c b ∪ Ioc a c
have rw : Ioc (min a (min b c)) (max a (max b c)) = 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]
-- 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 : Ioc (min a (min b c)) (max a (max b c)) = Ioc b a ∪ Ioc c b ∪ Ioc a c
⊢ Ioc a b ∪ Ioc b c ∪ Ioc c a = Ioc b a ∪ Ioc c b ∪ Ioc a c
have rw₁ : Ioc (min a (min b c)) (max a (max b c)) = Ioc b a ∪ Ioc a c ∪ Ioc c b
Tactic: rw [Ioc_union_Ioc_union_Ioc_cycle, union_right_comm, Ioc_union_Ioc_union_Ioc_cycle,
      min_left_comm, max_left_comm]
-- 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 : 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
⊢ Ioc a b ∪ Ioc b c ∪ Ioc c a = Ioc b a ∪ Ioc c b ∪ Ioc a c
have rw₂ : Ioc (min a (min b c)) (max a (max b c)) = Ioc (min b (min a c)) (max b (max 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]
-- 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 : 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))
⊢ Ioc a b ∪ Ioc b c ∪ Ioc c a = Ioc b a ∪ Ioc c b ∪ Ioc a c
have rw₃ : Ioc (min b (min a c)) (max a (max b c)) = Ioc (min b (min a c)) (max b (max 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]
-- 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 : 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))
⊢ Ioc a b ∪ Ioc b c ∪ Ioc c a = Ioc b a ∪ Ioc c b ∪ Ioc a c
have rw₄ : Ioc (min b (min a c)) (max b (max a c)) = Ioc (min b (min a c)) (max b (max 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]
-- 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
⊢ HAdd.hAdd (α := E) (∫ (x : ℝ) in a..b, f x ∂μ) (∫ (x : ℝ) in b..c, f x ∂μ) = ∫ (x : ℝ) in a..c, f x ∂μ
have rw : HAdd.hAdd (α := E) (∫ (x : ℝ) in a..b, f x ∂μ) (∫ (x : ℝ) in b..c, f x ∂μ) + -∫ (x : ℝ) in a..c, f x ∂μ = 0
Tactic: rw [← add_neg_eq_zero, ← integral_symm, integral_add_adjacent_intervals_cancel hab hbc]
-- 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
rw : HAdd.hAdd (α := E) (∫ (x : ℝ) in a..b, f x ∂μ) (∫ (x : ℝ) in b..c, f x ∂μ) + -∫ (x : ℝ) in a..c, f x ∂μ = 0
⊢ HAdd.hAdd (α := E) (∫ (x : ℝ) in a..b, f x ∂μ) (∫ (x : ℝ) in b..c, f x ∂μ) = ∫ (x : ℝ) in a..c, f x ∂μ
have rw₁ : HAdd.hAdd (α := E) (∫ (x : ℝ) in a..b, f x ∂μ) (∫ (x : ℝ) in b..c, f x ∂μ) + ∫ (x : ℝ) in c..a, f x ∂μ = 0
Tactic: rw [← add_neg_eq_zero, ← integral_symm, integral_add_adjacent_intervals_cancel hab hbc]
-- 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
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
⊢ HAdd.hAdd (α := E) (∫ (x : ℝ) in a..b, f x ∂μ) (∫ (x : ℝ) in b..c, f x ∂μ) = ∫ (x : ℝ) in a..c, f x ∂μ
have rw₂ : Eq.{u_5 + 1} (α := E) 0 0
Tactic: rw [← add_neg_eq_zero, ← integral_symm, integral_add_adjacent_intervals_cancel hab hbc]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic (goal)
Goal:
E : Type u_5
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℝ → E
μ : Measure ℝ
a : ℕ → ℝ
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 ∂μ)
have 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 ∂μ)
Tactic: revert hint
Cleared hypotheses: hint
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic (goal)
Goal:
E : Type u_5
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℝ → E
μ : Measure ℝ
a : ℕ → ℝ
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 ∂μ)
have 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 ∂μ)
Tactic: refine Nat.le_induction ?_ ?_ n hmn
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic (goal)
Goal:
E : Type u_5
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℝ → E
μ : Measure ℝ
a : ℕ → ℝ
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 ∂μ)
⊢ ∀ (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 ∂μ)
have 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 ∂μ)
Tactic: refine Nat.le_induction ?_ ?_ n hmn
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic (goal)
Goal:
E : Type u_5
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℝ → E
μ : Measure ℝ
a : ℕ → ℝ
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))
⊢ 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 ∂μ)
have refine_2 : IntervalIntegrable f μ (a m) (a p)
Tactic: rw [Finset.sum_Ico_succ_top hmp, IH, integral_add_adjacent_intervals]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic (goal)
Goal:
E : Type u_5
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℝ → E
μ : Measure ℝ
a : ℕ → ℝ
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)
⊢ 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 ∂μ)
have refine_2₁ : IntervalIntegrable f μ (a p) (a (p + 1))
Tactic: rw [Finset.sum_Ico_succ_top hmp, IH, integral_add_adjacent_intervals]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic (goal)
Goal:
E : Type u_5
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℝ → E
μ : Measure ℝ
a : ℕ → ℝ
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))
⊢ 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 ∂μ)
have refine_2₂ : ∀ k ∈ Ico m p, IntervalIntegrable f μ (a k) (a (k + 1))
Tactic: rw [Finset.sum_Ico_succ_top hmp, IH, integral_add_adjacent_intervals]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic (goal)
Goal:
E : Type u_5
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℝ → E
μ : Measure ℝ
a : ℕ → ℝ
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)
have refine_2 : ∀ (k : ℕ) (hk : k ∈ Ico m p), k ∈ Ico m (p + 1)
Tactic: refine IntervalIntegrable.trans_iterate_Ico hmp fun k hk => h k ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic (goal)
Goal:
E : Type u_5
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℝ → E
μ : Measure ℝ
a : ℕ → ℝ
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 p) (a (p + 1))
have refine_2 : p ∈ Ico m (p + 1)
Tactic: apply h
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic (goal)
Goal:
E : Type u_5
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : ℝ → E
μ : Measure ℝ
a : ℕ → ℝ
n : ℕ
hint : ∀ k < n, IntervalIntegrable f μ (a k) (a (k + 1))
⊢ 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 ∂μ)
have 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 ∂μ)
Tactic: rw [← Nat.Ico_zero_eq_range]
-- 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 d : ℝ
f : ℝ → E
μ : Measure ℝ
hab : IntervalIntegrable f μ a b
hcd : IntervalIntegrable f μ c d
hac : IntervalIntegrable f μ a c
⊢ 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 ∂μ)
have 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 ∂μ
Tactic: rw [← integral_add_adjacent_intervals hac hcd, add_assoc, add_left_comm,
    integral_add_adjacent_intervals hac (hac.symm.trans hab), add_comm]
-- 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 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 ∂μ
⊢ 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 ∂μ)
have 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 ∂μ)
Tactic: rw [← integral_add_adjacent_intervals hac hcd, add_assoc, add_left_comm,
    integral_add_adjacent_intervals hac (hac.symm.trans hab), add_comm]
-- 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 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 ∂μ)
⊢ 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 ∂μ)
have 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 ∂μ)
Tactic: rw [← integral_add_adjacent_intervals hac hcd, add_assoc, add_left_comm,
    integral_add_adjacent_intervals hac (hac.symm.trans hab), add_comm]
-- 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 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 ∂μ)
⊢ 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 ∂μ)
have 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 ∂μ)
Tactic: rw [← integral_add_adjacent_intervals hac hcd, add_assoc, add_left_comm,
    integral_add_adjacent_intervals hac (hac.symm.trans hab), add_comm]
-- 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 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 ∂μ)
⊢ 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 ∂μ)
have 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 ∂μ)
Tactic: rw [← integral_add_adjacent_intervals hac hcd, add_assoc, add_left_comm,
    integral_add_adjacent_intervals hac (hac.symm.trans hab), add_comm]
-- 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 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 d..b, f x ∂μ) (∫ (x : ℝ) in c..a, f x ∂μ)
have 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 ∂μ)
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]