awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.NumberTheory.AbelSummation (goal)
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
c : ℕ → 𝕜
f : ℝ → 𝕜
a b : ℝ
ha : 0 ≤ a
hab : a ≤ b
hf_diff : ∀ t ∈ Set.Icc a b, DifferentiableAt ℝ f t
hf_int : IntegrableOn (mα := MeasureSpace.toMeasurableSpace) (deriv f) (Set.Icc a b) volume
aux1 : (↑⌊a⌋₊ : ℝ) ≤ a
aux2 : b ≤ HAdd.hAdd (α := ℝ) (↑⌊b⌋₊ : ℝ) 1
hb : ⌊a⌋₊ = ⌊b⌋₊
inl :
  ∑ k ∈ Ioc ⌊b⌋₊ ⌊b⌋₊, f (↑k : ℝ) * c k =
    f b * ∑ k ∈ Icc 0 ⌊b⌋₊, c k - f a * ∑ k ∈ Icc 0 ⌊b⌋₊, c k - ∫ (x : ℝ) in a..b, deriv f x * ∑ k ∈ Icc 0 ⌊x⌋₊, c k
inl₁ :
  ∑ k ∈ ∅, f (↑k : ℝ) * c k =
    f b * ∑ k ∈ Icc 0 ⌊b⌋₊, c k - f a * ∑ k ∈ Icc 0 ⌊b⌋₊, c k - ∫ (x : ℝ) in a..b, deriv f x * ∑ k ∈ Icc 0 ⌊x⌋₊, c k
inl₂ :
  0 = f b * ∑ k ∈ Icc 0 ⌊b⌋₊, c k - f a * ∑ k ∈ Icc 0 ⌊b⌋₊, c k - ∫ (x : ℝ) in a..b, deriv f x * ∑ k ∈ Icc 0 ⌊x⌋₊, c k
inl₃ : 0 = (f b - f a) * ∑ k ∈ Icc 0 ⌊b⌋₊, c k - ∫ (x : ℝ) in a..b, deriv f x * ∑ k ∈ Icc 0 ⌊x⌋₊, c k
⊢ ∑ k ∈ Ioc ⌊a⌋₊ ⌊b⌋₊, f (↑k : ℝ) * c k =
    f b * ∑ k ∈ Icc 0 ⌊b⌋₊, c k - f a * ∑ k ∈ Icc 0 ⌊a⌋₊, c k - ∫ (x : ℝ) in a..b, deriv f x * ∑ k ∈ Icc 0 ⌊x⌋₊, c k
have inl₄ : 0 = (f b - f a) * ∑ k ∈ Icc 0 ⌊b⌋₊, c k - (f b - f a) * ∑ k ∈ Icc 0 ⌊b⌋₊, c k
Tactic: rw [hb, Ioc_eq_empty_of_le le_rfl, sum_empty, ← sub_mul,
      integralmulsum c hf_diff hf_int _ _ ⌊b⌋₊ hab (hb ▸ aux1) aux2 le_rfl le_rfl, sub_self]
-- Lean 4 proof step from Mathlib.NumberTheory.AbelSummation (goal)
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
c : ℕ → 𝕜
f : ℝ → 𝕜
a b : ℝ
ha : 0 ≤ a
hab : a ≤ b
hf_diff : ∀ t ∈ Set.Icc a b, DifferentiableAt ℝ f t
hf_int : IntegrableOn (mα := MeasureSpace.toMeasurableSpace) (deriv f) (Set.Icc a b) volume
aux1 : (↑⌊a⌋₊ : ℝ) ≤ a
aux2 : b ≤ HAdd.hAdd (α := ℝ) (↑⌊b⌋₊ : ℝ) 1
hb : ⌊a⌋₊ = ⌊b⌋₊
inl :
  ∑ k ∈ Ioc ⌊b⌋₊ ⌊b⌋₊, f (↑k : ℝ) * c k =
    f b * ∑ k ∈ Icc 0 ⌊b⌋₊, c k - f a * ∑ k ∈ Icc 0 ⌊b⌋₊, c k - ∫ (x : ℝ) in a..b, deriv f x * ∑ k ∈ Icc 0 ⌊x⌋₊, c k
inl₁ :
  ∑ k ∈ ∅, f (↑k : ℝ) * c k =
    f b * ∑ k ∈ Icc 0 ⌊b⌋₊, c k - f a * ∑ k ∈ Icc 0 ⌊b⌋₊, c k - ∫ (x : ℝ) in a..b, deriv f x * ∑ k ∈ Icc 0 ⌊x⌋₊, c k
inl₂ :
  0 = f b * ∑ k ∈ Icc 0 ⌊b⌋₊, c k - f a * ∑ k ∈ Icc 0 ⌊b⌋₊, c k - ∫ (x : ℝ) in a..b, deriv f x * ∑ k ∈ Icc 0 ⌊x⌋₊, c k
inl₃ : 0 = (f b - f a) * ∑ k ∈ Icc 0 ⌊b⌋₊, c k - ∫ (x : ℝ) in a..b, deriv f x * ∑ k ∈ Icc 0 ⌊x⌋₊, c k
inl₄ : 0 = (f b - f a) * ∑ k ∈ Icc 0 ⌊b⌋₊, c k - (f b - f a) * ∑ k ∈ Icc 0 ⌊b⌋₊, c k
⊢ ∑ k ∈ Ioc ⌊a⌋₊ ⌊b⌋₊, f (↑k : ℝ) * c k =
    f b * ∑ k ∈ Icc 0 ⌊b⌋₊, c k - f a * ∑ k ∈ Icc 0 ⌊a⌋₊, c k - ∫ (x : ℝ) in a..b, deriv f x * ∑ k ∈ Icc 0 ⌊x⌋₊, c k
have inl₅ : Eq.{u_1 + 1} (α := 𝕜) 0 0
Tactic: rw [hb, Ioc_eq_empty_of_le le_rfl, sum_empty, ← sub_mul,
      integralmulsum c hf_diff hf_int _ _ ⌊b⌋₊ hab (hb ▸ aux1) aux2 le_rfl le_rfl, sub_self]
-- Lean 4 proof step from Mathlib.NumberTheory.AbelSummation (hypothesis)
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
c : ℕ → 𝕜
f : ℝ → 𝕜
a b : ℝ
ha : 0 ≤ a
hab : a ≤ b
hf_diff : ∀ t ∈ Set.Icc a b, DifferentiableAt ℝ f t
hf_int : IntegrableOn (mα := MeasureSpace.toMeasurableSpace) (deriv f) (Set.Icc a b) volume
aux1 : (↑⌊a⌋₊ : ℝ) ≤ a
aux2 : b ≤ HAdd.hAdd (α := ℝ) (↑⌊b⌋₊ : ℝ) 1
hb : ⌊a⌋₊ < ⌊b⌋₊
⊢ ∑ k ∈ Ioc ⌊a⌋₊ ⌊b⌋₊, f (↑k : ℝ) * c k =
    f b * ∑ k ∈ Icc 0 ⌊b⌋₊, c k - f a * ∑ k ∈ Icc 0 ⌊a⌋₊, c k - ∫ (x : ℝ) in a..b, deriv f x * ∑ k ∈ Icc 0 ⌊x⌋₊, c k
have aux3 : a ≤ HAdd.hAdd (α := ℝ) (↑⌊a⌋₊ : ℝ) 1
Tactic: have aux3 : a ≤ ⌊a⌋₊ + 1 := (Nat.lt_floor_add_one _).le
-- Lean 4 proof step from Mathlib.NumberTheory.AbelSummation (goal)
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
c : ℕ → 𝕜
f : ℝ → 𝕜
a b : ℝ
ha : 0 ≤ a
hab : a ≤ b
hf_diff : ∀ t ∈ Set.Icc a b, DifferentiableAt ℝ f t
hf_int : IntegrableOn (mα := MeasureSpace.toMeasurableSpace) (deriv f) (Set.Icc a b) volume
aux1 : (↑⌊a⌋₊ : ℝ) ≤ a
aux2 : b ≤ HAdd.hAdd (α := ℝ) (↑⌊b⌋₊ : ℝ) 1
hb : ⌊a⌋₊ < ⌊b⌋₊
aux3 : a ≤ HAdd.hAdd (α := ℝ) (↑⌊a⌋₊ : ℝ) 1
⊢ HAdd.hAdd (α := ℝ) (↑⌊a⌋₊ : ℝ) 1 ≤ b
have rwa : (↑(⌊a⌋₊ + 1) : ℝ) ≤ b
Tactic: rwa [← Nat.cast_add_one, ← Nat.le_floor_iff (ha.trans hab)]
-- Lean 4 proof step from Mathlib.NumberTheory.AbelSummation (goal)
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
c : ℕ → 𝕜
f : ℝ → 𝕜
a b : ℝ
ha : 0 ≤ a
hab : a ≤ b
hf_diff : ∀ t ∈ Set.Icc a b, DifferentiableAt ℝ f t
hf_int : IntegrableOn (mα := MeasureSpace.toMeasurableSpace) (deriv f) (Set.Icc a b) volume
aux1 : (↑⌊a⌋₊ : ℝ) ≤ a
aux2 : b ≤ HAdd.hAdd (α := ℝ) (↑⌊b⌋₊ : ℝ) 1
hb : ⌊a⌋₊ < ⌊b⌋₊
aux3 : a ≤ HAdd.hAdd (α := ℝ) (↑⌊a⌋₊ : ℝ) 1
rwa : (↑(⌊a⌋₊ + 1) : ℝ) ≤ b
⊢ HAdd.hAdd (α := ℝ) (↑⌊a⌋₊ : ℝ) 1 ≤ b
have rwa₁ : ⌊a⌋₊ + 1 ≤ ⌊b⌋₊
Tactic: rwa [← Nat.cast_add_one, ← Nat.le_floor_iff (ha.trans hab)]
-- Lean 4 proof step from Mathlib.NumberTheory.AbelSummation (hypothesis)
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
c : ℕ → 𝕜
f : ℝ → 𝕜
a b : ℝ
ha : 0 ≤ a
hab : a ≤ b
hf_diff : ∀ t ∈ Set.Icc a b, DifferentiableAt ℝ f t
hf_int : IntegrableOn (mα := MeasureSpace.toMeasurableSpace) (deriv f) (Set.Icc a b) volume
aux1 : (↑⌊a⌋₊ : ℝ) ≤ a
aux2 : b ≤ HAdd.hAdd (α := ℝ) (↑⌊b⌋₊ : ℝ) 1
hb : ⌊a⌋₊ < ⌊b⌋₊
aux3 : a ≤ HAdd.hAdd (α := ℝ) (↑⌊a⌋₊ : ℝ) 1
⊢ ∑ k ∈ Ioc ⌊a⌋₊ ⌊b⌋₊, f (↑k : ℝ) * c k =
    f b * ∑ k ∈ Icc 0 ⌊b⌋₊, c k - f a * ∑ k ∈ Icc 0 ⌊a⌋₊, c k - ∫ (x : ℝ) in a..b, deriv f x * ∑ k ∈ Icc 0 ⌊x⌋₊, c k
have aux4 : HAdd.hAdd (α := ℝ) (↑⌊a⌋₊ : ℝ) 1 ≤ b
Tactic: have aux4 : ⌊a⌋₊ + 1 ≤ b := by rwa [← Nat.cast_add_one, ← Nat.le_floor_iff (ha.trans hab)]
-- Lean 4 proof step from Mathlib.NumberTheory.AbelSummation (hypothesis)
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
c : ℕ → 𝕜
f : ℝ → 𝕜
a b : ℝ
ha : 0 ≤ a
hab : a ≤ b
hf_diff : ∀ t ∈ Set.Icc a b, DifferentiableAt ℝ f t
hf_int : IntegrableOn (mα := MeasureSpace.toMeasurableSpace) (deriv f) (Set.Icc a b) volume
aux1 : (↑⌊a⌋₊ : ℝ) ≤ a
aux2 : b ≤ HAdd.hAdd (α := ℝ) (↑⌊b⌋₊ : ℝ) 1
hb : ⌊a⌋₊ < ⌊b⌋₊
aux3 : a ≤ HAdd.hAdd (α := ℝ) (↑⌊a⌋₊ : ℝ) 1
aux4 : HAdd.hAdd (α := ℝ) (↑⌊a⌋₊ : ℝ) 1 ≤ b
⊢ ∑ k ∈ Ioc ⌊a⌋₊ ⌊b⌋₊, f (↑k : ℝ) * c k =
    f b * ∑ k ∈ Icc 0 ⌊b⌋₊, c k - f a * ∑ k ∈ Icc 0 ⌊a⌋₊, c k - ∫ (x : ℝ) in a..b, deriv f x * ∑ k ∈ Icc 0 ⌊x⌋₊, c k
have aux5 : (↑⌊b⌋₊ : ℝ) ≤ b
Tactic: have aux5 : ⌊b⌋₊ ≤ b := Nat.floor_le (ha.trans hab)
-- Lean 4 proof step from Mathlib.NumberTheory.AbelSummation (hypothesis)
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
c : ℕ → 𝕜
f : ℝ → 𝕜
a b : ℝ
ha : 0 ≤ a
hab : a ≤ b
hf_diff : ∀ t ∈ Set.Icc a b, DifferentiableAt ℝ f t
hf_int : IntegrableOn (mα := MeasureSpace.toMeasurableSpace) (deriv f) (Set.Icc a b) volume
aux1 : (↑⌊a⌋₊ : ℝ) ≤ a
aux2 : b ≤ HAdd.hAdd (α := ℝ) (↑⌊b⌋₊ : ℝ) 1
hb : ⌊a⌋₊ < ⌊b⌋₊
aux3 : a ≤ HAdd.hAdd (α := ℝ) (↑⌊a⌋₊ : ℝ) 1
aux4 : HAdd.hAdd (α := ℝ) (↑⌊a⌋₊ : ℝ) 1 ≤ b
aux5 : (↑⌊b⌋₊ : ℝ) ≤ b
⊢ ∑ k ∈ Ioc ⌊a⌋₊ ⌊b⌋₊, f (↑k : ℝ) * c k =
    f b * ∑ k ∈ Icc 0 ⌊b⌋₊, c k - f a * ∑ k ∈ Icc 0 ⌊a⌋₊, c k - ∫ (x : ℝ) in a..b, deriv f x * ∑ k ∈ Icc 0 ⌊x⌋₊, c k
have aux6 : a ≤ (↑⌊b⌋₊ : ℝ)
Tactic: have aux6 : a ≤ ⌊b⌋₊ := Nat.floor_lt ha |>.mp hb |>.le
-- Lean 4 proof step from Mathlib.NumberTheory.AbelSummation (goal)
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
c : ℕ → 𝕜
f : ℝ → 𝕜
a b : ℝ
ha : 0 ≤ a
hab : a ≤ b
hf_diff : ∀ t ∈ Set.Icc a b, DifferentiableAt ℝ f t
hf_int : IntegrableOn (mα := MeasureSpace.toMeasurableSpace) (deriv f) (Set.Icc a b) volume
aux1 : (↑⌊a⌋₊ : ℝ) ≤ a
aux2 : b ≤ HAdd.hAdd (α := ℝ) (↑⌊b⌋₊ : ℝ) 1
hb : ⌊a⌋₊ < ⌊b⌋₊
aux3 : a ≤ HAdd.hAdd (α := ℝ) (↑⌊a⌋₊ : ℝ) 1
aux4 : HAdd.hAdd (α := ℝ) (↑⌊a⌋₊ : ℝ) 1 ≤ b
aux5 : (↑⌊b⌋₊ : ℝ) ≤ b
aux6 : a ≤ (↑⌊b⌋₊ : ℝ)
⊢ ∑ k ∈ Ioc ⌊a⌋₊ ⌊b⌋₊, f (↑k : ℝ) * c k =
    f b * ∑ k ∈ Icc 0 ⌊b⌋₊, c k - f a * ∑ k ∈ Icc 0 ⌊a⌋₊, c k - ∫ (x : ℝ) in a..b, deriv f x * ∑ k ∈ Icc 0 ⌊x⌋₊, c k
have inr : f (↑⌊b⌋₊ : ℝ) * ∑ x ∈ Icc 0 ⌊b⌋₊, c x - f (↑(⌊a⌋₊ + 1) : ℝ) * ∑ x ∈ Icc 0 ⌊a⌋₊, c x -
    ∑ x ∈ Ioc ⌊a⌋₊ (⌊b⌋₊ - 1), (f (↑(x + 1) : ℝ) - f (↑x : ℝ)) * ∑ x ∈ Icc 0 x, c x =
  f b * ∑ x ∈ Icc 0 ⌊b⌋₊, c x - f a * ∑ x ∈ Icc 0 ⌊a⌋₊, c x - ∫ (x : ℝ) in a..b, deriv f x * ∑ x ∈ Icc 0 ⌊x⌋₊, c x
Tactic: simp_rw [← smul_eq_mul, sum_Ioc_by_parts (fun k ↦ f k) _ hb, range_eq_Ico,
    Ico_add_one_right_eq_Icc, smul_eq_mul]
-- Lean 4 proof step from Mathlib.NumberTheory.AbelSummation (goal)
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
c : ℕ → 𝕜
f : ℝ → 𝕜
a b : ℝ
ha : 0 ≤ a
hab : a ≤ b
hf_diff : ∀ t ∈ Set.Icc a b, DifferentiableAt ℝ f t
hf_int : IntegrableOn (mα := MeasureSpace.toMeasurableSpace) (deriv f) (Set.Icc a b) volume
aux1 : (↑⌊a⌋₊ : ℝ) ≤ a
aux2 : b ≤ HAdd.hAdd (α := ℝ) (↑⌊b⌋₊ : ℝ) 1
hb : ⌊a⌋₊ < ⌊b⌋₊
aux3 : a ≤ HAdd.hAdd (α := ℝ) (↑⌊a⌋₊ : ℝ) 1
aux4 : HAdd.hAdd (α := ℝ) (↑⌊a⌋₊ : ℝ) 1 ≤ b
aux5 : (↑⌊b⌋₊ : ℝ) ≤ b
aux6 : a ≤ (↑⌊b⌋₊ : ℝ)
⊢ Eq.{u_1 + 1} (α := 𝕜) (∑ k ∈ Ioc ⌊a⌋₊ (⌊b⌋₊ - 1), (f (↑(k + 1) : ℝ) - f (↑k : ℝ)) * ∑ n ∈ Icc 0 k, c n)
    (∑ k ∈ Ico (⌊a⌋₊ + 1) ⌊b⌋₊, ∫ (t : ℝ) in (↑k : ℝ)..(↑(k + 1) : ℝ), deriv f t * ∑ n ∈ Icc 0 ⌊t⌋₊, c n)
have rw : Eq.{u_1 + 1} (α := 𝕜)
  (∑ k ∈ Ico (⌊a⌋₊ + 1) ⌊b⌋₊, ∫ (t : ℝ) in (↑k : ℝ)..(↑(k + 1) : ℝ), deriv f t * ∑ n ∈ Icc 0 ⌊t⌋₊, c n)
  (∑ k ∈ Ico (⌊a⌋₊ + 1) ⌊b⌋₊, (f (↑(k + 1) : ℝ) - f (↑k : ℝ)) * ∑ n ∈ Icc 0 k, c n)
Tactic: rw [← Ico_add_one_add_one_eq_Ioc, Nat.sub_add_cancel (by lia), Eq.comm]
-- Lean 4 proof step from Mathlib.NumberTheory.AbelSummation (hypothesis)
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
c : ℕ → 𝕜
f : ℝ → 𝕜
a b : ℝ
ha : 0 ≤ a
hab : a ≤ b
hf_diff : ∀ t ∈ Set.Icc a b, DifferentiableAt ℝ f t
hf_int : IntegrableOn (mα := MeasureSpace.toMeasurableSpace) (deriv f) (Set.Icc a b) volume
aux1 : (↑⌊a⌋₊ : ℝ) ≤ a
aux2 : b ≤ HAdd.hAdd (α := ℝ) (↑⌊b⌋₊ : ℝ) 1
hb : ⌊a⌋₊ < ⌊b⌋₊
aux3 : a ≤ HAdd.hAdd (α := ℝ) (↑⌊a⌋₊ : ℝ) 1
aux4 : HAdd.hAdd (α := ℝ) (↑⌊a⌋₊ : ℝ) 1 ≤ b
aux5 : (↑⌊b⌋₊ : ℝ) ≤ b
aux6 : a ≤ (↑⌊b⌋₊ : ℝ)
⊢ f (↑⌊b⌋₊ : ℝ) * ∑ x ∈ Icc 0 ⌊b⌋₊, c x - f (↑(⌊a⌋₊ + 1) : ℝ) * ∑ x ∈ Icc 0 ⌊a⌋₊, c x -
      ∑ x ∈ Ioc ⌊a⌋₊ (⌊b⌋₊ - 1), (f (↑(x + 1) : ℝ) - f (↑x : ℝ)) * ∑ x ∈ Icc 0 x, c x =
    f b * ∑ x ∈ Icc 0 ⌊b⌋₊, c x - f a * ∑ x ∈ Icc 0 ⌊a⌋₊, c x - ∫ (x : ℝ) in a..b, deriv f x * ∑ x ∈ Icc 0 ⌊x⌋₊, c x
have this : Eq.{u_1 + 1} (α := 𝕜) (∑ k ∈ Ioc ⌊a⌋₊ (⌊b⌋₊ - 1), (f (↑(k + 1) : ℝ) - f (↑k : ℝ)) * ∑ n ∈ Icc 0 k, c n)
  (∑ k ∈ Ico (⌊a⌋₊ + 1) ⌊b⌋₊, ∫ (t : ℝ) in (↑k : ℝ)..(↑(k + 1) : ℝ), deriv f t * ∑ n ∈ Icc 0 ⌊t⌋₊, c n)
Tactic: have : ∑ k ∈ Ioc ⌊a⌋₊ (⌊b⌋₊ - 1), (f ↑(k + 1) - f k) * ∑ n ∈ Icc 0 k, c n =
        ∑ k ∈ Ico (⌊a⌋₊ + 1) ⌊b⌋₊, ∫ t in k..↑(k + 1), deriv f t * ∑ n ∈ Icc 0 ⌊t⌋₊, c n := by
    rw [← Ico_add_one_add_one_eq_Ioc, Nat.sub_add_cancel (by lia), Eq.comm]
    exact sum_congr rfl fun k hk ↦ (integralmulsum c hf_diff hf_int _ _ _ (mod_cast k.le_succ)
      le_rfl (mod_cast le_rfl) (ineqofmemIco' hk).1 <| mod_cast (ineqofmemIco' hk).2)
-- Lean 4 proof step from Mathlib.NumberTheory.AbelSummation (goal)
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
c : ℕ → 𝕜
f : ℝ → 𝕜
a b : ℝ
ha : 0 ≤ a
hab : a ≤ b
hf_diff : ∀ t ∈ Set.Icc a b, DifferentiableAt ℝ f t
hf_int : IntegrableOn (mα := MeasureSpace.toMeasurableSpace) (deriv f) (Set.Icc a b) volume
aux1 : (↑⌊a⌋₊ : ℝ) ≤ a
aux2 : b ≤ HAdd.hAdd (α := ℝ) (↑⌊b⌋₊ : ℝ) 1
hb : ⌊a⌋₊ < ⌊b⌋₊
aux3 : a ≤ HAdd.hAdd (α := ℝ) (↑⌊a⌋₊ : ℝ) 1
aux4 : HAdd.hAdd (α := ℝ) (↑⌊a⌋₊ : ℝ) 1 ≤ b
aux5 : (↑⌊b⌋₊ : ℝ) ≤ b
aux6 : a ≤ (↑⌊b⌋₊ : ℝ)
this :
  Eq.{u_1 + 1} (α := 𝕜) (∑ k ∈ Ioc ⌊a⌋₊ (⌊b⌋₊ - 1), (f (↑(k + 1) : ℝ) - f (↑k : ℝ)) * ∑ n ∈ Icc 0 k, c n)
    (∑ k ∈ Ico (⌊a⌋₊ + 1) ⌊b⌋₊, ∫ (t : ℝ) in (↑k : ℝ)..(↑(k + 1) : ℝ), deriv f t * ∑ n ∈ Icc 0 ⌊t⌋₊, c n)
⊢ f (↑⌊b⌋₊ : ℝ) * ∑ x ∈ Icc 0 ⌊b⌋₊, c x - f (↑(⌊a⌋₊ + 1) : ℝ) * ∑ x ∈ Icc 0 ⌊a⌋₊, c x -
      ∑ x ∈ Ioc ⌊a⌋₊ (⌊b⌋₊ - 1), (f (↑(x + 1) : ℝ) - f (↑x : ℝ)) * ∑ x ∈ Icc 0 x, c x =
    f b * ∑ x ∈ Icc 0 ⌊b⌋₊, c x - f a * ∑ x ∈ Icc 0 ⌊a⌋₊, c x - ∫ (x : ℝ) in a..b, deriv f x * ∑ x ∈ Icc 0 ⌊x⌋₊, c x
have inr : f (↑⌊b⌋₊ : ℝ) * ∑ x ∈ Icc 0 ⌊b⌋₊, c x - f (HAdd.hAdd (α := ℝ) (↑⌊a⌋₊ : ℝ) 1) * ∑ x ∈ Icc 0 ⌊a⌋₊, c x -
    ((∫ (x : ℝ) in a..(↑⌊b⌋₊ : ℝ), deriv f x * ∑ n ∈ Icc 0 ⌊x⌋₊, c n) -
      (f (HAdd.hAdd (α := ℝ) (↑⌊a⌋₊ : ℝ) 1) - f a) * ∑ k ∈ Icc 0 ⌊a⌋₊, c k) =
  f b * ∑ x ∈ Icc 0 ⌊b⌋₊, c x - f a * ∑ x ∈ Icc 0 ⌊a⌋₊, c x -
    ((∫ (x : ℝ) in a..(↑⌊b⌋₊ : ℝ), deriv f x * ∑ x ∈ Icc 0 ⌊x⌋₊, c x) + (f b - f (↑⌊b⌋₊ : ℝ)) * ∑ k ∈ Icc 0 ⌊b⌋₊, c k)
Tactic: rw [this, sum_integral_adjacent_intervals_Ico hb, Nat.cast_add, Nat.cast_one,
    ← integral_interval_sub_left (a := a) (c := ⌊a⌋₊ + 1),
    ← integral_add_adjacent_intervals (b := ⌊b⌋₊) (c := b),
    integralmulsum c hf_diff hf_int _ _ _ aux3 aux1 le_rfl le_rfl aux4,
    integralmulsum c hf_diff hf_int _ _ _ aux5 le_rfl aux2 aux6 le_rfl]
-- Lean 4 proof step from Mathlib.NumberTheory.AbelSummation (goal)
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
c : ℕ → 𝕜
f : ℝ → 𝕜
a b : ℝ
ha : 0 ≤ a
hab : a ≤ b
hf_diff : ∀ t ∈ Set.Icc a b, DifferentiableAt ℝ f t
hf_int : IntegrableOn (mα := MeasureSpace.toMeasurableSpace) (deriv f) (Set.Icc a b) volume
aux1 : (↑⌊a⌋₊ : ℝ) ≤ a
aux2 : b ≤ HAdd.hAdd (α := ℝ) (↑⌊b⌋₊ : ℝ) 1
hb : ⌊a⌋₊ < ⌊b⌋₊
aux3 : a ≤ HAdd.hAdd (α := ℝ) (↑⌊a⌋₊ : ℝ) 1
aux4 : HAdd.hAdd (α := ℝ) (↑⌊a⌋₊ : ℝ) 1 ≤ b
aux5 : (↑⌊b⌋₊ : ℝ) ≤ b
aux6 : a ≤ (↑⌊b⌋₊ : ℝ)
this :
  Eq.{u_1 + 1} (α := 𝕜) (∑ k ∈ Ioc ⌊a⌋₊ (⌊b⌋₊ - 1), (f (↑(k + 1) : ℝ) - f (↑k : ℝ)) * ∑ n ∈ Icc 0 k, c n)
    (∑ k ∈ Ico (⌊a⌋₊ + 1) ⌊b⌋₊, ∫ (t : ℝ) in (↑k : ℝ)..(↑(k + 1) : ℝ), deriv f t * ∑ n ∈ Icc 0 ⌊t⌋₊, c n)
inr :
  f (↑⌊b⌋₊ : ℝ) * ∑ x ∈ Icc 0 ⌊b⌋₊, c x - f (HAdd.hAdd (α := ℝ) (↑⌊a⌋₊ : ℝ) 1) * ∑ x ∈ Icc 0 ⌊a⌋₊, c x -
      ((∫ (x : ℝ) in a..(↑⌊b⌋₊ : ℝ), deriv f x * ∑ n ∈ Icc 0 ⌊x⌋₊, c n) -
        (f (HAdd.hAdd (α := ℝ) (↑⌊a⌋₊ : ℝ) 1) - f a) * ∑ k ∈ Icc 0 ⌊a⌋₊, c k) =
    f b * ∑ x ∈ Icc 0 ⌊b⌋₊, c x - f a * ∑ x ∈ Icc 0 ⌊a⌋₊, c x -
      ((∫ (x : ℝ) in a..(↑⌊b⌋₊ : ℝ), deriv f x * ∑ x ∈ Icc 0 ⌊x⌋₊, c x) + (f b - f (↑⌊b⌋₊ : ℝ)) * ∑ k ∈ Icc 0 ⌊b⌋₊, c k)
⊢ f (↑⌊b⌋₊ : ℝ) * ∑ x ∈ Icc 0 ⌊b⌋₊, c x - f (↑(⌊a⌋₊ + 1) : ℝ) * ∑ x ∈ Icc 0 ⌊a⌋₊, c x -
      ∑ x ∈ Ioc ⌊a⌋₊ (⌊b⌋₊ - 1), (f (↑(x + 1) : ℝ) - f (↑x : ℝ)) * ∑ x ∈ Icc 0 x, c x =
    f b * ∑ x ∈ Icc 0 ⌊b⌋₊, c x - f a * ∑ x ∈ Icc 0 ⌊a⌋₊, c x - ∫ (x : ℝ) in a..b, deriv f x * ∑ x ∈ Icc 0 ⌊x⌋₊, c x
have inr₁ : IntervalIntegrable.{u_1} (ε := 𝕜) (fun (x : ℝ) ↦ deriv f x * ∑ x ∈ Icc 0 ⌊x⌋₊, c x) volume a (↑⌊b⌋₊ : ℝ)
Tactic: rw [this, sum_integral_adjacent_intervals_Ico hb, Nat.cast_add, Nat.cast_one,
    ← integral_interval_sub_left (a := a) (c := ⌊a⌋₊ + 1),
    ← integral_add_adjacent_intervals (b := ⌊b⌋₊) (c := b),
    integralmulsum c hf_diff hf_int _ _ _ aux3 aux1 le_rfl le_rfl aux4,
    integralmulsum c hf_diff hf_int _ _ _ aux5 le_rfl aux2 aux6 le_rfl]
-- Lean 4 proof step from Mathlib.NumberTheory.AbelSummation (goal)
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
c : ℕ → 𝕜
f : ℝ → 𝕜
a b : ℝ
ha : 0 ≤ a
hab : a ≤ b
hf_diff : ∀ t ∈ Set.Icc a b, DifferentiableAt ℝ f t
hf_int : IntegrableOn (mα := MeasureSpace.toMeasurableSpace) (deriv f) (Set.Icc a b) volume
aux1 : (↑⌊a⌋₊ : ℝ) ≤ a
aux2 : b ≤ HAdd.hAdd (α := ℝ) (↑⌊b⌋₊ : ℝ) 1
hb : ⌊a⌋₊ < ⌊b⌋₊
aux3 : a ≤ HAdd.hAdd (α := ℝ) (↑⌊a⌋₊ : ℝ) 1
aux4 : HAdd.hAdd (α := ℝ) (↑⌊a⌋₊ : ℝ) 1 ≤ b
aux5 : (↑⌊b⌋₊ : ℝ) ≤ b
aux6 : a ≤ (↑⌊b⌋₊ : ℝ)
this :
  Eq.{u_1 + 1} (α := 𝕜) (∑ k ∈ Ioc ⌊a⌋₊ (⌊b⌋₊ - 1), (f (↑(k + 1) : ℝ) - f (↑k : ℝ)) * ∑ n ∈ Icc 0 k, c n)
    (∑ k ∈ Ico (⌊a⌋₊ + 1) ⌊b⌋₊, ∫ (t : ℝ) in (↑k : ℝ)..(↑(k + 1) : ℝ), deriv f t * ∑ n ∈ Icc 0 ⌊t⌋₊, c n)
inr :
  f (↑⌊b⌋₊ : ℝ) * ∑ x ∈ Icc 0 ⌊b⌋₊, c x - f (HAdd.hAdd (α := ℝ) (↑⌊a⌋₊ : ℝ) 1) * ∑ x ∈ Icc 0 ⌊a⌋₊, c x -
      ((∫ (x : ℝ) in a..(↑⌊b⌋₊ : ℝ), deriv f x * ∑ n ∈ Icc 0 ⌊x⌋₊, c n) -
        (f (HAdd.hAdd (α := ℝ) (↑⌊a⌋₊ : ℝ) 1) - f a) * ∑ k ∈ Icc 0 ⌊a⌋₊, c k) =
    f b * ∑ x ∈ Icc 0 ⌊b⌋₊, c x - f a * ∑ x ∈ Icc 0 ⌊a⌋₊, c x -
      ((∫ (x : ℝ) in a..(↑⌊b⌋₊ : ℝ), deriv f x * ∑ x ∈ Icc 0 ⌊x⌋₊, c x) + (f b - f (↑⌊b⌋₊ : ℝ)) * ∑ k ∈ Icc 0 ⌊b⌋₊, c k)
inr₁ : IntervalIntegrable.{u_1} (ε := 𝕜) (fun (x : ℝ) ↦ deriv f x * ∑ x ∈ Icc 0 ⌊x⌋₊, c x) volume a (↑⌊b⌋₊ : ℝ)
⊢ f (↑⌊b⌋₊ : ℝ) * ∑ x ∈ Icc 0 ⌊b⌋₊, c x - f (↑(⌊a⌋₊ + 1) : ℝ) * ∑ x ∈ Icc 0 ⌊a⌋₊, c x -
      ∑ x ∈ Ioc ⌊a⌋₊ (⌊b⌋₊ - 1), (f (↑(x + 1) : ℝ) - f (↑x : ℝ)) * ∑ x ∈ Icc 0 x, c x =
    f b * ∑ x ∈ Icc 0 ⌊b⌋₊, c x - f a * ∑ x ∈ Icc 0 ⌊a⌋₊, c x - ∫ (x : ℝ) in a..b, deriv f x * ∑ x ∈ Icc 0 ⌊x⌋₊, c x
have inr₂ : IntervalIntegrable.{u_1} (ε := 𝕜) (fun (x : ℝ) ↦ deriv f x * ∑ x ∈ Icc 0 ⌊x⌋₊, c x) volume (↑⌊b⌋₊ : ℝ) b
Tactic: rw [this, sum_integral_adjacent_intervals_Ico hb, Nat.cast_add, Nat.cast_one,
    ← integral_interval_sub_left (a := a) (c := ⌊a⌋₊ + 1),
    ← integral_add_adjacent_intervals (b := ⌊b⌋₊) (c := b),
    integralmulsum c hf_diff hf_int _ _ _ aux3 aux1 le_rfl le_rfl aux4,
    integralmulsum c hf_diff hf_int _ _ _ aux5 le_rfl aux2 aux6 le_rfl]
-- Lean 4 proof step from Mathlib.NumberTheory.AbelSummation (goal)
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
c : ℕ → 𝕜
f : ℝ → 𝕜
a b : ℝ
ha : 0 ≤ a
hab : a ≤ b
hf_diff : ∀ t ∈ Set.Icc a b, DifferentiableAt ℝ f t
hf_int : IntegrableOn (mα := MeasureSpace.toMeasurableSpace) (deriv f) (Set.Icc a b) volume
aux1 : (↑⌊a⌋₊ : ℝ) ≤ a
aux2 : b ≤ HAdd.hAdd (α := ℝ) (↑⌊b⌋₊ : ℝ) 1
hb : ⌊a⌋₊ < ⌊b⌋₊
aux3 : a ≤ HAdd.hAdd (α := ℝ) (↑⌊a⌋₊ : ℝ) 1
aux4 : HAdd.hAdd (α := ℝ) (↑⌊a⌋₊ : ℝ) 1 ≤ b
aux5 : (↑⌊b⌋₊ : ℝ) ≤ b
aux6 : a ≤ (↑⌊b⌋₊ : ℝ)
this :
  Eq.{u_1 + 1} (α := 𝕜) (∑ k ∈ Ioc ⌊a⌋₊ (⌊b⌋₊ - 1), (f (↑(k + 1) : ℝ) - f (↑k : ℝ)) * ∑ n ∈ Icc 0 k, c n)
    (∑ k ∈ Ico (⌊a⌋₊ + 1) ⌊b⌋₊, ∫ (t : ℝ) in (↑k : ℝ)..(↑(k + 1) : ℝ), deriv f t * ∑ n ∈ Icc 0 ⌊t⌋₊, c n)
inr :
  f (↑⌊b⌋₊ : ℝ) * ∑ x ∈ Icc 0 ⌊b⌋₊, c x - f (HAdd.hAdd (α := ℝ) (↑⌊a⌋₊ : ℝ) 1) * ∑ x ∈ Icc 0 ⌊a⌋₊, c x -
      ((∫ (x : ℝ) in a..(↑⌊b⌋₊ : ℝ), deriv f x * ∑ n ∈ Icc 0 ⌊x⌋₊, c n) -
        (f (HAdd.hAdd (α := ℝ) (↑⌊a⌋₊ : ℝ) 1) - f a) * ∑ k ∈ Icc 0 ⌊a⌋₊, c k) =
    f b * ∑ x ∈ Icc 0 ⌊b⌋₊, c x - f a * ∑ x ∈ Icc 0 ⌊a⌋₊, c x -
      ((∫ (x : ℝ) in a..(↑⌊b⌋₊ : ℝ), deriv f x * ∑ x ∈ Icc 0 ⌊x⌋₊, c x) + (f b - f (↑⌊b⌋₊ : ℝ)) * ∑ k ∈ Icc 0 ⌊b⌋₊, c k)
inr₁ : IntervalIntegrable.{u_1} (ε := 𝕜) (fun (x : ℝ) ↦ deriv f x * ∑ x ∈ Icc 0 ⌊x⌋₊, c x) volume a (↑⌊b⌋₊ : ℝ)
inr₂ : IntervalIntegrable.{u_1} (ε := 𝕜) (fun (x : ℝ) ↦ deriv f x * ∑ x ∈ Icc 0 ⌊x⌋₊, c x) volume (↑⌊b⌋₊ : ℝ) b
inr₃ : IntervalIntegrable.{u_1} (ε := 𝕜) (fun (x : ℝ) ↦ deriv f x * ∑ n ∈ Icc 0 ⌊x⌋₊, c n) volume a (↑⌊b⌋₊ : ℝ)
⊢ f (↑⌊b⌋₊ : ℝ) * ∑ x ∈ Icc 0 ⌊b⌋₊, c x - f (↑(⌊a⌋₊ + 1) : ℝ) * ∑ x ∈ Icc 0 ⌊a⌋₊, c x -
      ∑ x ∈ Ioc ⌊a⌋₊ (⌊b⌋₊ - 1), (f (↑(x + 1) : ℝ) - f (↑x : ℝ)) * ∑ x ∈ Icc 0 x, c x =
    f b * ∑ x ∈ Icc 0 ⌊b⌋₊, c x - f a * ∑ x ∈ Icc 0 ⌊a⌋₊, c x - ∫ (x : ℝ) in a..b, deriv f x * ∑ x ∈ Icc 0 ⌊x⌋₊, c x
have inr₄ : IntervalIntegrable.{u_1} (ε := 𝕜) (fun (x : ℝ) ↦ deriv f x * ∑ n ∈ Icc 0 ⌊x⌋₊, c n) volume a
  (HAdd.hAdd (α := ℝ) (↑⌊a⌋₊ : ℝ) 1)
Tactic: rw [this, sum_integral_adjacent_intervals_Ico hb, Nat.cast_add, Nat.cast_one,
    ← integral_interval_sub_left (a := a) (c := ⌊a⌋₊ + 1),
    ← integral_add_adjacent_intervals (b := ⌊b⌋₊) (c := b),
    integralmulsum c hf_diff hf_int _ _ _ aux3 aux1 le_rfl le_rfl aux4,
    integralmulsum c hf_diff hf_int _ _ _ aux5 le_rfl aux2 aux6 le_rfl]
-- Lean 4 proof step from Mathlib.NumberTheory.AbelSummation (goal)
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
c : ℕ → 𝕜
f : ℝ → 𝕜
a b : ℝ
ha : 0 ≤ a
hab : a ≤ b
hf_diff : ∀ t ∈ Set.Icc a b, DifferentiableAt ℝ f t
hf_int : IntegrableOn (mα := MeasureSpace.toMeasurableSpace) (deriv f) (Set.Icc a b) volume
aux1 : (↑⌊a⌋₊ : ℝ) ≤ a
aux2 : b ≤ HAdd.hAdd (α := ℝ) (↑⌊b⌋₊ : ℝ) 1
hb : ⌊a⌋₊ < ⌊b⌋₊
aux3 : a ≤ HAdd.hAdd (α := ℝ) (↑⌊a⌋₊ : ℝ) 1
aux4 : HAdd.hAdd (α := ℝ) (↑⌊a⌋₊ : ℝ) 1 ≤ b
aux5 : (↑⌊b⌋₊ : ℝ) ≤ b
aux6 : a ≤ (↑⌊b⌋₊ : ℝ)
this :
  Eq.{u_1 + 1} (α := 𝕜) (∑ k ∈ Ioc ⌊a⌋₊ (⌊b⌋₊ - 1), (f (↑(k + 1) : ℝ) - f (↑k : ℝ)) * ∑ n ∈ Icc 0 k, c n)
    (∑ k ∈ Ico (⌊a⌋₊ + 1) ⌊b⌋₊, ∫ (t : ℝ) in (↑k : ℝ)..(↑(k + 1) : ℝ), deriv f t * ∑ n ∈ Icc 0 ⌊t⌋₊, c n)
inr :
  f (↑⌊b⌋₊ : ℝ) * ∑ x ∈ Icc 0 ⌊b⌋₊, c x - f (HAdd.hAdd (α := ℝ) (↑⌊a⌋₊ : ℝ) 1) * ∑ x ∈ Icc 0 ⌊a⌋₊, c x -
      ((∫ (x : ℝ) in a..(↑⌊b⌋₊ : ℝ), deriv f x * ∑ n ∈ Icc 0 ⌊x⌋₊, c n) -
        (f (HAdd.hAdd (α := ℝ) (↑⌊a⌋₊ : ℝ) 1) - f a) * ∑ k ∈ Icc 0 ⌊a⌋₊, c k) =
    f b * ∑ x ∈ Icc 0 ⌊b⌋₊, c x - f a * ∑ x ∈ Icc 0 ⌊a⌋₊, c x -
      ((∫ (x : ℝ) in a..(↑⌊b⌋₊ : ℝ), deriv f x * ∑ x ∈ Icc 0 ⌊x⌋₊, c x) + (f b - f (↑⌊b⌋₊ : ℝ)) * ∑ k ∈ Icc 0 ⌊b⌋₊, c k)
inr₁ : IntervalIntegrable.{u_1} (ε := 𝕜) (fun (x : ℝ) ↦ deriv f x * ∑ x ∈ Icc 0 ⌊x⌋₊, c x) volume a (↑⌊b⌋₊ : ℝ)
inr₂ : IntervalIntegrable.{u_1} (ε := 𝕜) (fun (x : ℝ) ↦ deriv f x * ∑ x ∈ Icc 0 ⌊x⌋₊, c x) volume (↑⌊b⌋₊ : ℝ) b
inr₃ : IntervalIntegrable.{u_1} (ε := 𝕜) (fun (x : ℝ) ↦ deriv f x * ∑ n ∈ Icc 0 ⌊x⌋₊, c n) volume a (↑⌊b⌋₊ : ℝ)
inr₄ :
  IntervalIntegrable.{u_1} (ε := 𝕜) (fun (x : ℝ) ↦ deriv f x * ∑ n ∈ Icc 0 ⌊x⌋₊, c n) volume a
    (HAdd.hAdd (α := ℝ) (↑⌊a⌋₊ : ℝ) 1)
⊢ f (↑⌊b⌋₊ : ℝ) * ∑ x ∈ Icc 0 ⌊b⌋₊, c x - f (↑(⌊a⌋₊ + 1) : ℝ) * ∑ x ∈ Icc 0 ⌊a⌋₊, c x -
      ∑ x ∈ Ioc ⌊a⌋₊ (⌊b⌋₊ - 1), (f (↑(x + 1) : ℝ) - f (↑x : ℝ)) * ∑ x ∈ Icc 0 x, c x =
    f b * ∑ x ∈ Icc 0 ⌊b⌋₊, c x - f a * ∑ x ∈ Icc 0 ⌊a⌋₊, c x - ∫ (x : ℝ) in a..b, deriv f x * ∑ x ∈ Icc 0 ⌊x⌋₊, c x
have inr₅ : ∀ k ∈ Set.Ico ⌊a⌋₊.succ ⌊b⌋₊,
  IntervalIntegrable.{u_1} (ε := 𝕜) (fun (t : ℝ) ↦ deriv f t * ∑ n ∈ Icc 0 ⌊t⌋₊, c n) volume (↑k : ℝ) (↑(k + 1) : ℝ)
Tactic: rw [this, sum_integral_adjacent_intervals_Ico hb, Nat.cast_add, Nat.cast_one,
    ← integral_interval_sub_left (a := a) (c := ⌊a⌋₊ + 1),
    ← integral_add_adjacent_intervals (b := ⌊b⌋₊) (c := b),
    integralmulsum c hf_diff hf_int _ _ _ aux3 aux1 le_rfl le_rfl aux4,
    integralmulsum c hf_diff hf_int _ _ _ aux5 le_rfl aux2 aux6 le_rfl]
-- Lean 4 proof step from Mathlib.NumberTheory.AbelSummation (goal)
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
c : ℕ → 𝕜
f : ℝ → 𝕜
a b : ℝ
ha : 0 ≤ a
hab : a ≤ b
hf_diff : ∀ t ∈ Set.Icc a b, DifferentiableAt ℝ f t
hf_int : IntegrableOn (mα := MeasureSpace.toMeasurableSpace) (deriv f) (Set.Icc a b) volume
aux1 : (↑⌊a⌋₊ : ℝ) ≤ a
aux2 : b ≤ HAdd.hAdd (α := ℝ) (↑⌊b⌋₊ : ℝ) 1
hb : ⌊a⌋₊ < ⌊b⌋₊
aux3 : a ≤ HAdd.hAdd (α := ℝ) (↑⌊a⌋₊ : ℝ) 1
aux4 : HAdd.hAdd (α := ℝ) (↑⌊a⌋₊ : ℝ) 1 ≤ b
aux5 : (↑⌊b⌋₊ : ℝ) ≤ b
aux6 : a ≤ (↑⌊b⌋₊ : ℝ)
this :
  Eq.{u_1 + 1} (α := 𝕜) (∑ k ∈ Ioc ⌊a⌋₊ (⌊b⌋₊ - 1), (f (↑(k + 1) : ℝ) - f (↑k : ℝ)) * ∑ n ∈ Icc 0 k, c n)
    (∑ k ∈ Ico (⌊a⌋₊ + 1) ⌊b⌋₊, ∫ (t : ℝ) in (↑k : ℝ)..(↑(k + 1) : ℝ), deriv f t * ∑ n ∈ Icc 0 ⌊t⌋₊, c n)
⊢ IntervalIntegrable.{u_1} (ε := 𝕜) (fun (x : ℝ) ↦ deriv f x * ∑ x ∈ Icc 0 ⌊x⌋₊, c x) volume a (↑⌊b⌋₊ : ℝ)
have inr : IntegrableOn.{0, u_1} (ε := 𝕜) (mα := Real.measurableSpace) (fun (x : ℝ) ↦ deriv f x * ∑ x ∈ Icc 0 ⌊x⌋₊, c x)
  (Set.Icc a (↑⌊b⌋₊ : ℝ)) volume
Tactic: rw [intervalIntegrable_iff_integrableOn_Icc_of_le aux6]
-- Lean 4 proof step from Mathlib.NumberTheory.AbelSummation (goal)
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
c : ℕ → 𝕜
f : ℝ → 𝕜
a b : ℝ
ha : 0 ≤ a
hab : a ≤ b
hf_diff : ∀ t ∈ Set.Icc a b, DifferentiableAt ℝ f t
hf_int : IntegrableOn (mα := MeasureSpace.toMeasurableSpace) (deriv f) (Set.Icc a b) volume
aux1 : (↑⌊a⌋₊ : ℝ) ≤ a
aux2 : b ≤ HAdd.hAdd (α := ℝ) (↑⌊b⌋₊ : ℝ) 1
hb : ⌊a⌋₊ < ⌊b⌋₊
aux3 : a ≤ HAdd.hAdd (α := ℝ) (↑⌊a⌋₊ : ℝ) 1
aux4 : HAdd.hAdd (α := ℝ) (↑⌊a⌋₊ : ℝ) 1 ≤ b
aux5 : (↑⌊b⌋₊ : ℝ) ≤ b
aux6 : a ≤ (↑⌊b⌋₊ : ℝ)
this :
  Eq.{u_1 + 1} (α := 𝕜) (∑ k ∈ Ioc ⌊a⌋₊ (⌊b⌋₊ - 1), (f (↑(k + 1) : ℝ) - f (↑k : ℝ)) * ∑ n ∈ Icc 0 k, c n)
    (∑ k ∈ Ico (⌊a⌋₊ + 1) ⌊b⌋₊, ∫ (t : ℝ) in (↑k : ℝ)..(↑(k + 1) : ℝ), deriv f t * ∑ n ∈ Icc 0 ⌊t⌋₊, c n)
⊢ IntervalIntegrable.{u_1} (ε := 𝕜) (fun (x : ℝ) ↦ deriv f x * ∑ x ∈ Icc 0 ⌊x⌋₊, c x) volume (↑⌊b⌋₊ : ℝ) b
have inr : IntegrableOn.{0, u_1} (ε := 𝕜) (mα := Real.measurableSpace) (fun (x : ℝ) ↦ deriv f x * ∑ x ∈ Icc 0 ⌊x⌋₊, c x)
  (Set.Icc (↑⌊b⌋₊ : ℝ) b) volume
Tactic: rw [intervalIntegrable_iff_integrableOn_Icc_of_le aux5]
-- Lean 4 proof step from Mathlib.NumberTheory.AbelSummation (goal)
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
c : ℕ → 𝕜
f : ℝ → 𝕜
a b : ℝ
ha : 0 ≤ a
hab : a ≤ b
hf_diff : ∀ t ∈ Set.Icc a b, DifferentiableAt ℝ f t
hf_int : IntegrableOn (mα := MeasureSpace.toMeasurableSpace) (deriv f) (Set.Icc a b) volume
aux1 : (↑⌊a⌋₊ : ℝ) ≤ a
aux2 : b ≤ HAdd.hAdd (α := ℝ) (↑⌊b⌋₊ : ℝ) 1
hb : ⌊a⌋₊ < ⌊b⌋₊
aux3 : a ≤ HAdd.hAdd (α := ℝ) (↑⌊a⌋₊ : ℝ) 1
aux4 : HAdd.hAdd (α := ℝ) (↑⌊a⌋₊ : ℝ) 1 ≤ b
aux5 : (↑⌊b⌋₊ : ℝ) ≤ b
aux6 : a ≤ (↑⌊b⌋₊ : ℝ)
this :
  Eq.{u_1 + 1} (α := 𝕜) (∑ k ∈ Ioc ⌊a⌋₊ (⌊b⌋₊ - 1), (f (↑(k + 1) : ℝ) - f (↑k : ℝ)) * ∑ n ∈ Icc 0 k, c n)
    (∑ k ∈ Ico (⌊a⌋₊ + 1) ⌊b⌋₊, ∫ (t : ℝ) in (↑k : ℝ)..(↑(k + 1) : ℝ), deriv f t * ∑ n ∈ Icc 0 ⌊t⌋₊, c n)
⊢ IntervalIntegrable.{u_1} (ε := 𝕜) (fun (x : ℝ) ↦ deriv f x * ∑ n ∈ Icc 0 ⌊x⌋₊, c n) volume a (↑⌊b⌋₊ : ℝ)
have inr : IntegrableOn.{0, u_1} (ε := 𝕜) (mα := Real.measurableSpace) (fun (x : ℝ) ↦ deriv f x * ∑ n ∈ Icc 0 ⌊x⌋₊, c n)
  (Set.Icc a (↑⌊b⌋₊ : ℝ)) volume
Tactic: rw [intervalIntegrable_iff_integrableOn_Icc_of_le aux6]