awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 (↑⌊b⌋₊ : ℝ) b) volume

Tactic:
(integrableOn_mul_sum_Icc c ha hf_int).mono_set (Set.Icc_subset_Icc_left aux6)

Premises used: Set.Icc_subset_Icc_left, 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 (↑⌊b⌋₊ : ℝ) b) volume

Tactic:
exact (integrableOn_mul_sum_Icc c ha hf_int).mono_set (Set.Icc_subset_Icc_left aux6)

Premises used: Set.Icc_subset_Icc_left, 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 * ∑ n ∈ Icc 0 ⌊x⌋₊, c n)
    (Set.Icc a (↑⌊b⌋₊ : ℝ)) volume
⊢ IntervalIntegrable.{u_1} (ε := 𝕜) (fun (x : ℝ) ↦ deriv f x * ∑ n ∈ Icc 0 ⌊x⌋₊, c n) 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 * ∑ n ∈ Icc 0 ⌊x⌋₊, c n)
    (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 * ∑ n ∈ Icc 0 ⌊x⌋₊, c n)
    (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 * ∑ n ∈ Icc 0 ⌊x⌋₊, c n)
    (Set.Icc a (HAdd.hAdd (α := ℝ) (↑⌊a⌋₊ : ℝ) 1)) volume
⊢ IntervalIntegrable.{u_1} (ε := 𝕜) (fun (x : ℝ) ↦ deriv f x * ∑ n ∈ Icc 0 ⌊x⌋₊, c n) volume a
    (HAdd.hAdd (α := ℝ) (↑⌊a⌋₊ : ℝ) 1)

Tactic:
rw [intervalIntegrable_iff_integrableOn_Icc_of_le aux3]

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 * ∑ n ∈ Icc 0 ⌊x⌋₊, c n)
    (Set.Icc a (HAdd.hAdd (α := ℝ) (↑⌊a⌋₊ : ℝ) 1)) volume

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

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 * ∑ n ∈ Icc 0 ⌊x⌋₊, c n)
    (Set.Icc a (HAdd.hAdd (α := ℝ) (↑⌊a⌋₊ : ℝ) 1)) volume

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

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)
⊢ ∀ 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:
fun k hk ↦ (intervalIntegrable_iff_integrableOn_Icc_of_le (mod_cast k.le_succ)).mpr
      <| (integrableOn_mul_sum_Icc c ha hf_int).mono_set
        <| (Set.Icc_subset_Icc_iff (mod_cast k.le_succ)).mpr <| mod_cast (ineqofmemIco hk)

Premises used: Iff.mpr, intervalIntegrable_iff_integrableOn_Icc_of_le, congrArg, Set.Icc_subset_Icc_iff, Nat.cast_add._simp_1, cast, Nat.le_succ, Nat.cast_le._simp_1, LE.le, Nat.cast, _private.0.abelSummationProof.ineqofmemIco, And, MeasureTheory.IntegrableOn.mono_set, HAdd.hAdd, integrableOn_mul_sum_Icc, congrFun', OfNat.ofNat, Eq.symm, Nat.cast_one, 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⌋₊ : ℝ)
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)
⊢ ∀ 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:
exact fun k hk ↦ (intervalIntegrable_iff_integrableOn_Icc_of_le (mod_cast k.le_succ)).mpr
      <| (integrableOn_mul_sum_Icc c ha hf_int).mono_set
        <| (Set.Icc_subset_Icc_iff (mod_cast k.le_succ)).mpr <| mod_cast (ineqofmemIco hk)

Premises used: Iff.mpr, intervalIntegrable_iff_integrableOn_Icc_of_le, Set.Icc_subset_Icc_iff, MeasureTheory.IntegrableOn.mono_set, integrableOn_mul_sum_Icc
-- Module: Mathlib.NumberTheory.AbelSummation
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
c : ℕ → 𝕜
f : ℝ → 𝕜
n m : ℕ
h : n ≤ m
hf_diff : ∀ (t : ℝ), Membership.mem (γ := Set ℝ) (Set.Icc (↑n : ℝ) (↑m : ℝ)) t → DifferentiableAt ℝ f t
hf_int : IntegrableOn (mα := MeasureSpace.toMeasurableSpace) (deriv f) (Set.Icc (↑n : ℝ) (↑m : ℝ)) volume
⊢ ∑ k ∈ Ioc (Nat.floor (α := ℝ) (↑n : ℝ)) (Nat.floor (α := ℝ) (↑m : ℝ)), f (↑k : ℝ) * c k =
    f (↑m : ℝ) * ∑ k ∈ Icc 0 (Nat.floor (α := ℝ) (↑m : ℝ)), c k -
        f (↑n : ℝ) * ∑ k ∈ Icc 0 (Nat.floor (α := ℝ) (↑n : ℝ)), c k -
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Set.Ioc (↑n : ℝ) (↑m : ℝ)))
        fun (t : ℝ) ↦ deriv f t * ∑ k ∈ Icc 0 ⌊t⌋₊, c k

Tactic:
sum_mul_eq_sub_sub_integral_mul c n.cast_nonneg (Nat.cast_le.mpr h) hf_diff hf_int

Premises used: Iff.mpr, Nat.cast_nonneg, Nat.cast_le, sum_mul_eq_sub_sub_integral_mul
-- Module: Mathlib.NumberTheory.AbelSummation
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
c : ℕ → 𝕜
f : ℝ → 𝕜
n m : ℕ
h : n ≤ m
hf_diff : ∀ (t : ℝ), Membership.mem (γ := Set ℝ) (Set.Icc (↑n : ℝ) (↑m : ℝ)) t → DifferentiableAt ℝ f t
hf_int : IntegrableOn (mα := MeasureSpace.toMeasurableSpace) (deriv f) (Set.Icc (↑n : ℝ) (↑m : ℝ)) volume
h₁ : n = Nat.floor (α := ℝ) (↑n : ℝ)
h₂ h₃ : m = Nat.floor (α := ℝ) (↑m : ℝ)
h₄ : n = Nat.floor (α := ℝ) (↑n : ℝ)
⊢ ∑ k ∈ Ioc n m, f (↑k : ℝ) * c k =
    f (↑m : ℝ) * ∑ k ∈ Icc 0 m, c k - f (↑n : ℝ) * ∑ k ∈ Icc 0 n, c k -
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Set.Ioc (↑n : ℝ) (↑m : ℝ)))
        fun (t : ℝ) ↦ deriv f t * ∑ k ∈ Icc 0 ⌊t⌋₊, c k

Tactic:
convert! sum_mul_eq_sub_sub_integral_mul c n.cast_nonneg (Nat.cast_le.mpr h) hf_diff hf_int

Premises used: Iff.mpr, Nat.cast_nonneg, Nat.cast_le, sum_mul_eq_sub_sub_integral_mul
-- Module: Mathlib.NumberTheory.AbelSummation
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
c : ℕ → 𝕜
f : ℝ → 𝕜
n m : ℕ
h : n ≤ m
hf_diff : ∀ (t : ℝ), Membership.mem (γ := Set ℝ) (Set.Icc (↑n : ℝ) (↑m : ℝ)) t → DifferentiableAt ℝ f t
hf_int : IntegrableOn (mα := MeasureSpace.toMeasurableSpace) (deriv f) (Set.Icc (↑n : ℝ) (↑m : ℝ)) volume
h₁ h₂ : n = n
⊢ n = Nat.floor (α := ℝ) (↑n : ℝ)

Tactic:
rw [Nat.floor_natCast]

Premises used: Nat.floor_natCast
-- Module: Mathlib.NumberTheory.AbelSummation
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
c : ℕ → 𝕜
f : ℝ → 𝕜
n m : ℕ
h : n ≤ m
hf_diff : ∀ (t : ℝ), Membership.mem (γ := Set ℝ) (Set.Icc (↑n : ℝ) (↑m : ℝ)) t → DifferentiableAt ℝ f t
hf_int : IntegrableOn (mα := MeasureSpace.toMeasurableSpace) (deriv f) (Set.Icc (↑n : ℝ) (↑m : ℝ)) volume
h₁ h₂ : m = m
⊢ m = Nat.floor (α := ℝ) (↑m : ℝ)

Tactic:
rw [Nat.floor_natCast]

Premises used: Nat.floor_natCast
-- Module: Mathlib.NumberTheory.AbelSummation
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
c : ℕ → 𝕜
f : ℝ → 𝕜
b : ℝ
hb : 0 ≤ b
hf_diff : ∀ t ∈ Set.Icc 0 b, DifferentiableAt ℝ f t
hf_int : IntegrableOn (mα := MeasureSpace.toMeasurableSpace) (deriv f) (Set.Icc 0 b) volume
rw :
  f 0 * c 0 +
      (f b * ∑ k ∈ Icc 0 ⌊b⌋₊, c k - f 0 * c 0 -
        @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Set.Ioc 0 b)) fun (t : ℝ) ↦
          deriv f t * ∑ k ∈ Icc 0 ⌊t⌋₊, c k) =
    f b * ∑ k ∈ Icc 0 ⌊b⌋₊, c k -
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Set.Ioc 0 b)) fun (t : ℝ) ↦
        deriv f t * ∑ k ∈ Icc 0 ⌊t⌋₊, c k
⊢ ∑ k ∈ cons 0 (Ioc 0 ⌊b⌋₊) ⋯, f (↑k : ℝ) * c k =
    f b * ∑ k ∈ Icc 0 ⌊b⌋₊, c k -
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Set.Ioc 0 b)) fun (t : ℝ) ↦
        deriv f t * ∑ k ∈ Icc 0 ⌊t⌋₊, c k

Tactic:
rw [sum_cons, ← Nat.floor_zero (R := ℝ), sum_mul_eq_sub_sub_integral_mul c le_rfl hb hf_diff
    hf_int, Nat.floor_zero, Nat.cast_zero, Icc_self, sum_singleton]

Premises used: le_rfl, Finset.sum_cons, Finset.sum_singleton, Finset.Icc_self, Nat.cast_zero, Nat.floor_zero, sum_mul_eq_sub_sub_integral_mul
-- Module: Mathlib.NumberTheory.AbelSummation
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
c : ℕ → 𝕜
f : ℝ → 𝕜
b : ℝ
hb : 0 ≤ b
hf_diff : ∀ t ∈ Set.Icc 0 b, DifferentiableAt ℝ f t
hf_int : IntegrableOn (mα := MeasureSpace.toMeasurableSpace) (deriv f) (Set.Icc 0 b) volume
⊢ f 0 * c 0 +
      (f b * ∑ k ∈ Icc 0 ⌊b⌋₊, c k - f 0 * c 0 -
        @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Set.Ioc 0 b)) fun (t : ℝ) ↦
          deriv f t * ∑ k ∈ Icc 0 ⌊t⌋₊, c k) =
    f b * ∑ k ∈ Icc 0 ⌊b⌋₊, c k -
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Set.Ioc 0 b)) fun (t : ℝ) ↦
        deriv f t * ∑ k ∈ Icc 0 ⌊t⌋₊, c k

Tactic:
ring
-- Module: Mathlib.NumberTheory.AbelSummation
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
c : ℕ → 𝕜
f : ℝ → 𝕜
m : ℕ
hf_diff : ∀ (t : ℝ), Membership.mem (γ := Set ℝ) (Set.Icc 0 (↑m : ℝ)) t → DifferentiableAt ℝ f t
hf_int : IntegrableOn (mα := MeasureSpace.toMeasurableSpace) (deriv f) (Set.Icc 0 (↑m : ℝ)) volume
⊢ ∑ k ∈ Icc 0 (Nat.floor (α := ℝ) (↑m : ℝ)), f (↑k : ℝ) * c k =
    f (↑m : ℝ) * ∑ k ∈ Icc 0 (Nat.floor (α := ℝ) (↑m : ℝ)), c k -
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Set.Ioc 0 (↑m : ℝ))) fun (t : ℝ) ↦
        deriv f t * ∑ k ∈ Icc 0 ⌊t⌋₊, c k

Tactic:
sum_mul_eq_sub_integral_mul c m.cast_nonneg hf_diff hf_int

Premises used: Nat.cast_nonneg, sum_mul_eq_sub_integral_mul
-- Module: Mathlib.NumberTheory.AbelSummation
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
c : ℕ → 𝕜
f : ℝ → 𝕜
m : ℕ
hf_diff : ∀ (t : ℝ), Membership.mem (γ := Set ℝ) (Set.Icc 0 (↑m : ℝ)) t → DifferentiableAt ℝ f t
hf_int : IntegrableOn (mα := MeasureSpace.toMeasurableSpace) (deriv f) (Set.Icc 0 (↑m : ℝ)) volume
h h₁ : m = Nat.floor (α := ℝ) (↑m : ℝ)
⊢ ∑ k ∈ Icc 0 m, f (↑k : ℝ) * c k =
    f (↑m : ℝ) * ∑ k ∈ Icc 0 m, c k -
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Set.Ioc 0 (↑m : ℝ))) fun (t : ℝ) ↦
        deriv f t * ∑ k ∈ Icc 0 ⌊t⌋₊, c k

Tactic:
convert! sum_mul_eq_sub_integral_mul c m.cast_nonneg hf_diff hf_int

Premises used: Nat.cast_nonneg, sum_mul_eq_sub_integral_mul
-- Module: Mathlib.NumberTheory.AbelSummation
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
c : ℕ → 𝕜
f : ℝ → 𝕜
m : ℕ
hf_diff : ∀ (t : ℝ), Membership.mem (γ := Set ℝ) (Set.Icc 0 (↑m : ℝ)) t → DifferentiableAt ℝ f t
hf_int : IntegrableOn (mα := MeasureSpace.toMeasurableSpace) (deriv f) (Set.Icc 0 (↑m : ℝ)) volume
h h₁ : m = m
⊢ m = Nat.floor (α := ℝ) (↑m : ℝ)

Tactic:
rw [Nat.floor_natCast]

Premises used: Nat.floor_natCast
-- Module: Mathlib.NumberTheory.AbelSummation
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
c : ℕ → 𝕜
f : ℝ → 𝕜
hc : c 0 = 0
b : ℝ
hf_diff : ∀ t ∈ Set.Icc 1 b, DifferentiableAt ℝ f t
hf_int : IntegrableOn (mα := MeasureSpace.toMeasurableSpace) (deriv f) (Set.Icc 1 b) volume
inl :
  ∀ (hb : 1 ≤ b),
    ∑ k ∈ Icc 0 ⌊b⌋₊, f (↑k : ℝ) * c k =
      f b * ∑ k ∈ Icc 0 ⌊b⌋₊, c k -
        @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Set.Ioc 1 b)) fun (t : ℝ) ↦
          deriv f t * ∑ k ∈ Icc 0 ⌊t⌋₊, c k
inr :
  ∀ (hb : b < 1),
    ∑ k ∈ Icc 0 ⌊b⌋₊, f (↑k : ℝ) * c k =
      f b * ∑ k ∈ Icc 0 ⌊b⌋₊, c k -
        @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Set.Ioc 1 b)) fun (t : ℝ) ↦
          deriv f t * ∑ k ∈ Icc 0 ⌊t⌋₊, c k
⊢ ∑ k ∈ Icc 0 ⌊b⌋₊, f (↑k : ℝ) * c k =
    f b * ∑ k ∈ Icc 0 ⌊b⌋₊, c k -
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Set.Ioc 1 b)) fun (t : ℝ) ↦
        deriv f t * ∑ k ∈ Icc 0 ⌊t⌋₊, c k

Tactic:
obtain hb | hb := le_or_gt 1 b

Premises used: le_or_gt, OfNat.ofNat
-- Module: Mathlib.NumberTheory.AbelSummation
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
c : ℕ → 𝕜
f : ℝ → 𝕜
hc : c 0 = 0
b : ℝ
hf_diff : ∀ t ∈ Set.Icc 1 b, DifferentiableAt ℝ f t
hf_int : IntegrableOn (mα := MeasureSpace.toMeasurableSpace) (deriv f) (Set.Icc 1 b) volume
hb : 1 ≤ b
⊢ 1 ≤ ⌊b⌋₊

Tactic:
have : 1 ≤ ⌊b⌋₊ := (Nat.one_le_floor_iff _).mpr hb
-- Module: Mathlib.NumberTheory.AbelSummation
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
c : ℕ → 𝕜
f : ℝ → 𝕜
hc : c 0 = 0
b : ℝ
hf_diff : ∀ t ∈ Set.Icc 1 b, DifferentiableAt ℝ f t
hf_int : IntegrableOn (mα := MeasureSpace.toMeasurableSpace) (deriv f) (Set.Icc 1 b) volume
hb : 1 ≤ b
this : 1 ≤ ⌊b⌋₊
⊢ HAdd.hAdd (α := ℕ) 0 1 ≤ ⌊b⌋₊

Tactic:
lia
-- Module: Mathlib.NumberTheory.AbelSummation
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
c : ℕ → 𝕜
f : ℝ → 𝕜
hc : c 0 = 0
b : ℝ
hf_diff : ∀ t ∈ Set.Icc 1 b, DifferentiableAt ℝ f t
hf_int : IntegrableOn (mα := MeasureSpace.toMeasurableSpace) (deriv f) (Set.Icc 1 b) volume
hb : 1 ≤ b
this : 1 ≤ ⌊b⌋₊
inl :
  f (↑0 : ℝ) * c 0 +
      (f (↑(HAdd.hAdd (α := ℕ) 0 1) : ℝ) * c (HAdd.hAdd (α := ℕ) 0 1) +
        ∑ x ∈ Ioc (HAdd.hAdd (α := ℕ) 0 1) ⌊b⌋₊, f (↑x : ℝ) * c x) =
    f b * ∑ k ∈ Icc 0 ⌊b⌋₊, c k -
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Set.Ioc 1 b)) fun (t : ℝ) ↦
        deriv f t * ∑ k ∈ Icc 0 ⌊t⌋₊, c k
⊢ ∑ k ∈ Icc 0 ⌊b⌋₊, f (↑k : ℝ) * c k =
    f b * ∑ k ∈ Icc 0 ⌊b⌋₊, c k -
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Set.Ioc 1 b)) fun (t : ℝ) ↦
        deriv f t * ∑ k ∈ Icc 0 ⌊t⌋₊, c k

Tactic:
nth_rewrite 1 [Icc_eq_cons_Ioc (Nat.zero_le _), sum_cons, ← Icc_add_one_left_eq_Ioc,
      Icc_eq_cons_Ioc (by lia), sum_cons]

Premises used: Finset.Icc_add_one_left_eq_Ioc, Nat.zero_le, Finset.sum_cons, Finset.Icc_eq_cons_Ioc
-- Module: Mathlib.NumberTheory.AbelSummation
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
c : ℕ → 𝕜
f : ℝ → 𝕜
hc : c 0 = 0
b : ℝ
hf_diff : ∀ t ∈ Set.Icc 1 b, DifferentiableAt ℝ f t
hf_int : IntegrableOn (mα := MeasureSpace.toMeasurableSpace) (deriv f) (Set.Icc 1 b) volume
hb : 1 ≤ b
this : 1 ≤ ⌊b⌋₊
⊢ 1 = HAdd.hAdd (α := ℕ) 0 1

Tactic:
rfl
-- Module: Mathlib.NumberTheory.AbelSummation
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
c : ℕ → 𝕜
f : ℝ → 𝕜
hc : c 0 = 0
b : ℝ
hf_diff : ∀ t ∈ Set.Icc 1 b, DifferentiableAt ℝ f t
hf_int : IntegrableOn (mα := MeasureSpace.toMeasurableSpace) (deriv f) (Set.Icc 1 b) volume
hb : 1 ≤ b
this : 1 ≤ ⌊b⌋₊
inl :
  f 1 * c 1 +
      (f b * ∑ k ∈ Icc 0 ⌊b⌋₊, c k - f 1 * (0 + c 1) -
        @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Set.Ioc 1 b)) fun (t : ℝ) ↦
          deriv f t * ∑ k ∈ Icc 0 ⌊t⌋₊, c k) =
    f b * ∑ k ∈ Icc 0 ⌊b⌋₊, c k -
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Set.Ioc 1 b)) fun (t : ℝ) ↦
        deriv f t * ∑ k ∈ Icc 0 ⌊t⌋₊, c k
⊢ f (↑0 : ℝ) * c 0 +
      (f (↑(HAdd.hAdd (α := ℕ) 0 1) : ℝ) * c (HAdd.hAdd (α := ℕ) 0 1) +
        ∑ x ∈ Ioc (HAdd.hAdd (α := ℕ) 0 1) ⌊b⌋₊, f (↑x : ℝ) * c x) =
    f b * ∑ k ∈ Icc 0 ⌊b⌋₊, c k -
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Set.Ioc 1 b)) fun (t : ℝ) ↦
        deriv f t * ∑ k ∈ Icc 0 ⌊t⌋₊, c k

Tactic:
rw [zero_add, ← Nat.floor_one (R := ℝ),
      sum_mul_eq_sub_sub_integral_mul c zero_le_one hb hf_diff hf_int, Nat.floor_one, Nat.cast_one,
      Icc_eq_cons_Ioc zero_le_one, sum_cons, show 1 = 0 + 1 by rfl, Nat.Ioc_succ_singleton,
      zero_add, sum_singleton, hc, mul_zero, zero_add]

Premises used: Nat.Ioc_succ_singleton, Finset.sum_cons, Finset.Icc_eq_cons_Ioc, zero_add, MulZeroClass.mul_zero, zero_le_one, Finset.sum_singleton, Nat.floor_one, Nat.cast_one, sum_mul_eq_sub_sub_integral_mul
-- Module: Mathlib.NumberTheory.AbelSummation
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
c : ℕ → 𝕜
f : ℝ → 𝕜
hc : c 0 = 0
b : ℝ
hf_diff : ∀ t ∈ Set.Icc 1 b, DifferentiableAt ℝ f t
hf_int : IntegrableOn (mα := MeasureSpace.toMeasurableSpace) (deriv f) (Set.Icc 1 b) volume
hb : 1 ≤ b
this : 1 ≤ ⌊b⌋₊
⊢ f 1 * c 1 +
      (f b * ∑ k ∈ Icc 0 ⌊b⌋₊, c k - f 1 * (0 + c 1) -
        @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Set.Ioc 1 b)) fun (t : ℝ) ↦
          deriv f t * ∑ k ∈ Icc 0 ⌊t⌋₊, c k) =
    f b * ∑ k ∈ Icc 0 ⌊b⌋₊, c k -
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Set.Ioc 1 b)) fun (t : ℝ) ↦
        deriv f t * ∑ k ∈ Icc 0 ⌊t⌋₊, c k

Tactic:
ring