awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.AbelSummation
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
c : ℕ → 𝕜
a b : ℝ
m : ℕ
ha : 0 ≤ a
g : ℝ → 𝕜
hg_int : IntegrableOn (mα := MeasureSpace.toMeasurableSpace) g (Set.Icc a b) volume
hab : a ≤ b
hb : ⌊a⌋₊ < ⌊b⌋₊
h_locint :
  ∀ {t₁ t₂ : ℝ} {n : ℕ} (h : t₁ ≤ t₂) (h₁ : (↑n : ℝ) ≤ t₁) (h₂ : t₂ ≤ HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) (h₃ : a ≤ t₁)
    (h₄ : t₂ ≤ b), IntervalIntegrable.{u_1} (ε := 𝕜) (fun (t : ℝ) ↦ g t * ∑ k ∈ Icc m ⌊t⌋₊, c k) volume t₁ t₂
aux1 : 0 ≤ b
aux2 : HAdd.hAdd (α := ℝ) (↑⌊a⌋₊ : ℝ) 1 ≤ b
aux3 : a ≤ HAdd.hAdd (α := ℝ) (↑⌊a⌋₊ : ℝ) 1
aux4 : a ≤ (↑⌊b⌋₊ : ℝ)
I1 : IntervalIntegrable.{u_1} (ε := 𝕜) (fun (t : ℝ) ↦ g t * ∑ k ∈ Icc m ⌊t⌋₊, c k) volume a (↑(⌊a⌋₊ + 1) : ℝ)
I2 : IntervalIntegrable.{u_1} (ε := 𝕜) (fun (t : ℝ) ↦ g t * ∑ k ∈ Icc m ⌊t⌋₊, c k) volume (↑(⌊a⌋₊ + 1) : ℝ) (↑⌊b⌋₊ : ℝ)
I3 : IntervalIntegrable.{u_1} (ε := 𝕜) (fun (t : ℝ) ↦ g t * ∑ k ∈ Icc m ⌊t⌋₊, c k) volume (↑⌊b⌋₊ : ℝ) b
⊢ IntervalIntegrable.{u_1} (ε := 𝕜) (fun (t : ℝ) ↦ g t * ∑ k ∈ Icc m ⌊t⌋₊, c k) volume a b

Tactic:
exact (I1.trans I2).trans I3

Premises used: IntervalIntegrable.trans
-- Module: Mathlib.NumberTheory.AbelSummation
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
c : ℕ → 𝕜
a b : ℝ
m : ℕ
ha : 0 ≤ a
g : ℝ → 𝕜
hg_int : IntegrableOn (mα := MeasureSpace.toMeasurableSpace) g (Set.Icc a b) volume
hab : b < a
inr :
  IntegrableOn.{0, u_1} (ε := 𝕜) (mα := MeasureSpace.toMeasurableSpace) (fun (t : ℝ) ↦ g t * ∑ k ∈ Icc m ⌊t⌋₊, c k) ∅
    volume
⊢ IntegrableOn.{0, u_1} (ε := 𝕜) (mα := MeasureSpace.toMeasurableSpace) (fun (t : ℝ) ↦ g t * ∑ k ∈ Icc m ⌊t⌋₊, c k)
    (Set.Icc a b) volume

Tactic:
rw [Set.Icc_eq_empty_of_lt hab]

Premises used: Set.Icc_eq_empty_of_lt
-- Module: Mathlib.NumberTheory.AbelSummation
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
c : ℕ → 𝕜
a b : ℝ
m : ℕ
ha : 0 ≤ a
g : ℝ → 𝕜
hg_int : IntegrableOn (mα := MeasureSpace.toMeasurableSpace) g (Set.Icc a b) volume
hab : b < a
⊢ IntegrableOn.{0, u_1} (ε := 𝕜) (mα := MeasureSpace.toMeasurableSpace) (fun (t : ℝ) ↦ g t * ∑ k ∈ Icc m ⌊t⌋₊, c k) ∅
    volume

Tactic:
integrableOn_empty

Premises used: MeasureTheory.integrableOn_empty
-- Module: Mathlib.NumberTheory.AbelSummation
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
c : ℕ → 𝕜
a b : ℝ
m : ℕ
ha : 0 ≤ a
g : ℝ → 𝕜
hg_int : IntegrableOn (mα := MeasureSpace.toMeasurableSpace) g (Set.Icc a b) volume
hab : b < a
⊢ IntegrableOn.{0, u_1} (ε := 𝕜) (mα := MeasureSpace.toMeasurableSpace) (fun (t : ℝ) ↦ g t * ∑ k ∈ Icc m ⌊t⌋₊, c k) ∅
    volume

Tactic:
exact integrableOn_empty

Premises used: MeasureTheory.integrableOn_empty
-- Module: Mathlib.NumberTheory.AbelSummation
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
rw :
  ∑ 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
⊢ ∑ k ∈ Ioc ⌊a⌋₊ ⌊b⌋₊, f (↑k : ℝ) * c k =
    f b * ∑ k ∈ Icc 0 ⌊b⌋₊, c k - f a * ∑ k ∈ Icc 0 ⌊a⌋₊, c k -
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Set.Ioc a b)) fun (t : ℝ) ↦
        deriv f t * ∑ k ∈ Icc 0 ⌊t⌋₊, c k

Tactic:
rw [← integral_of_le hab]

Premises used: intervalIntegral.integral_of_le
-- Module: Mathlib.NumberTheory.AbelSummation
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
⊢ (↑⌊a⌋₊ : ℝ) ≤ a

Tactic:
have aux1 : ⌊a⌋₊ ≤ a := Nat.floor_le ha
-- Module: Mathlib.NumberTheory.AbelSummation
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
⊢ b ≤ HAdd.hAdd (α := ℝ) (↑⌊b⌋₊ : ℝ) 1

Tactic:
have aux2 : b ≤ ⌊b⌋₊ + 1 := (Nat.lt_floor_add_one _).le
-- Module: Mathlib.NumberTheory.AbelSummation
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
inl :
  ∀ (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
inr :
  ∀ (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
⊢ ∑ 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

Tactic:
obtain hb | hb := eq_or_lt_of_le (Nat.floor_le_floor hab)

Premises used: Nat.floor_le_floor, eq_or_lt_of_le
-- Module: Mathlib.NumberTheory.AbelSummation
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
inl₅ inl₆ : Eq.{u_1 + 1} (α := 𝕜) 0 0
⊢ ∑ 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

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]

Premises used: le_rfl, sub_self, Eq.rec, sub_mul, _private.0.abelSummationProof.integralmulsum, Nat.floor, Finset.sum_empty, Finset.Ioc_eq_empty_of_le
-- Module: Mathlib.NumberTheory.AbelSummation
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⌋₊
⊢ a ≤ HAdd.hAdd (α := ℝ) (↑⌊a⌋₊ : ℝ) 1

Tactic:
have aux3 : a ≤ ⌊a⌋₊ + 1 := (Nat.lt_floor_add_one _).le
-- Module: Mathlib.NumberTheory.AbelSummation
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
rwa₁ rwa₂ rwa₃ rwa₄ : ⌊a⌋₊ + 1 ≤ ⌊b⌋₊
⊢ HAdd.hAdd (α := ℝ) (↑⌊a⌋₊ : ℝ) 1 ≤ b

Tactic:
rwa [← Nat.cast_add_one, ← Nat.le_floor_iff (ha.trans hab)]

Premises used: Nat.le_floor_iff, LE.le.trans, Nat.cast_add_one
-- Module: Mathlib.NumberTheory.AbelSummation
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

Tactic:
have aux4 : ⌊a⌋₊ + 1 ≤ b := by rwa [← Nat.cast_add_one, ← Nat.le_floor_iff (ha.trans hab)]
-- Module: Mathlib.NumberTheory.AbelSummation
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
⊢ (↑⌊b⌋₊ : ℝ) ≤ b

Tactic:
have aux5 : ⌊b⌋₊ ≤ b := Nat.floor_le (ha.trans hab)
-- Module: Mathlib.NumberTheory.AbelSummation
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
⊢ a ≤ (↑⌊b⌋₊ : ℝ)

Tactic:
have aux6 : a ≤ ⌊b⌋₊ := Nat.floor_lt ha |>.mp hb |>.le
-- Module: Mathlib.NumberTheory.AbelSummation
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⌋₊ : ℝ)
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
⊢ ∑ 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

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]

Premises used: Nat.cast, Finset.Ico_add_one_right_eq_Icc, Finset.range_eq_Ico, Finset.sum_Ioc_by_parts, smul_eq_mul
-- Module: Mathlib.NumberTheory.AbelSummation
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⌋₊ : ℝ)
⊢ 1 ≤ ⌊b⌋₊

Tactic:
lia
-- Module: Mathlib.NumberTheory.AbelSummation
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⌋₊ : ℝ)
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)
⊢ 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:
rw [← Ico_add_one_add_one_eq_Ioc, Nat.sub_add_cancel (by lia), Eq.comm]

Premises used: Nat.sub_add_cancel, Eq.comm, Finset.Ico_add_one_add_one_eq_Ioc
-- Module: Mathlib.NumberTheory.AbelSummation
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 ∈ 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:
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)

Premises used: le_rfl, congrArg, Nat.cast_add._simp_1, cast, Nat.le_succ, Nat.cast_le._simp_1, LE.le, Nat.cast, And.right, And.left, HAdd.hAdd, _private.0.abelSummationProof.integralmulsum, congrFun', OfNat.ofNat, Eq.symm, Nat.cast_one, Finset.sum_congr, _private.0.abelSummationProof.ineqofmemIco', rfl, Eq.trans
-- Module: Mathlib.NumberTheory.AbelSummation
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 ∈ 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:
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)

Premises used: le_rfl, Nat.cast, And.left, _private.0.abelSummationProof.integralmulsum, Finset.sum_congr, _private.0.abelSummationProof.ineqofmemIco', rfl
-- Module: Mathlib.NumberTheory.AbelSummation
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)

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)
-- Module: Mathlib.NumberTheory.AbelSummation
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)
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) : ℝ)
⊢ 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:
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]

Premises used: le_rfl, intervalIntegral.integral_add_adjacent_intervals, intervalIntegral.sum_integral_adjacent_intervals_Ico, Nat.cast_add, _private.0.abelSummationProof.integralmulsum, Nat.cast_one, intervalIntegral.integral_interval_sub_left
-- Module: Mathlib.NumberTheory.AbelSummation
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 (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:
ring
-- Module: Mathlib.NumberTheory.AbelSummation
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 :
  IntegrableOn.{0, u_1} (ε := 𝕜) (mα := Real.measurableSpace) (fun (x : ℝ) ↦ deriv f x * ∑ x ∈ Icc 0 ⌊x⌋₊, c x)
    (Set.Icc a (↑⌊b⌋₊ : ℝ)) volume
⊢ IntervalIntegrable.{u_1} (ε := 𝕜) (fun (x : ℝ) ↦ deriv f x * ∑ x ∈ Icc 0 ⌊x⌋₊, c x) volume a (↑⌊b⌋₊ : ℝ)

Tactic:
rw [intervalIntegrable_iff_integrableOn_Icc_of_le aux6]

Premises used: intervalIntegrable_iff_integrableOn_Icc_of_le
-- Module: Mathlib.NumberTheory.AbelSummation
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)
⊢ IntegrableOn.{0, u_1} (ε := 𝕜) (mα := Real.measurableSpace) (fun (x : ℝ) ↦ deriv f x * ∑ x ∈ Icc 0 ⌊x⌋₊, c x)
    (Set.Icc a (↑⌊b⌋₊ : ℝ)) volume

Tactic:
(integrableOn_mul_sum_Icc c ha hf_int).mono_set (Set.Icc_subset_Icc_right aux5)

Premises used: Set.Icc_subset_Icc_right, MeasureTheory.IntegrableOn.mono_set, integrableOn_mul_sum_Icc
-- Module: Mathlib.NumberTheory.AbelSummation
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)
⊢ IntegrableOn.{0, u_1} (ε := 𝕜) (mα := Real.measurableSpace) (fun (x : ℝ) ↦ deriv f x * ∑ x ∈ Icc 0 ⌊x⌋₊, c x)
    (Set.Icc a (↑⌊b⌋₊ : ℝ)) volume

Tactic:
exact (integrableOn_mul_sum_Icc c ha hf_int).mono_set (Set.Icc_subset_Icc_right aux5)

Premises used: Set.Icc_subset_Icc_right, MeasureTheory.IntegrableOn.mono_set, integrableOn_mul_sum_Icc
-- Module: Mathlib.NumberTheory.AbelSummation
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 :
  IntegrableOn.{0, u_1} (ε := 𝕜) (mα := Real.measurableSpace) (fun (x : ℝ) ↦ deriv f x * ∑ x ∈ Icc 0 ⌊x⌋₊, c x)
    (Set.Icc (↑⌊b⌋₊ : ℝ) b) volume
⊢ IntervalIntegrable.{u_1} (ε := 𝕜) (fun (x : ℝ) ↦ deriv f x * ∑ x ∈ Icc 0 ⌊x⌋₊, c x) volume (↑⌊b⌋₊ : ℝ) b

Tactic:
rw [intervalIntegrable_iff_integrableOn_Icc_of_le aux5]

Premises used: intervalIntegrable_iff_integrableOn_Icc_of_le