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⌋₊
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
    (HAdd.hAdd (α := ℝ) (↑⌊a⌋₊ : ℝ) 1)
have 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
Tactic: rw [intervalIntegrable_iff_integrableOn_Icc_of_le aux3]
-- Lean 4 proof step from Mathlib.NumberTheory.AbelSummation (goal)
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 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
have h₁ : n = Nat.floor (α := ℝ) (↑n : ℝ)
Tactic: convert! sum_mul_eq_sub_sub_integral_mul c n.cast_nonneg (Nat.cast_le.mpr h) hf_diff hf_int
-- Lean 4 proof step from Mathlib.NumberTheory.AbelSummation (goal)
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 : ℝ)
⊢ ∑ 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
have h₂ : m = Nat.floor (α := ℝ) (↑m : ℝ)
Tactic: convert! sum_mul_eq_sub_sub_integral_mul c n.cast_nonneg (Nat.cast_le.mpr h) hf_diff hf_int
-- Lean 4 proof step from Mathlib.NumberTheory.AbelSummation (goal)
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
⊢ n = Nat.floor (α := ℝ) (↑n : ℝ)
have h₁ : n = n
Tactic: rw [Nat.floor_natCast]
-- Lean 4 proof step from Mathlib.NumberTheory.AbelSummation (goal)
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
⊢ m = Nat.floor (α := ℝ) (↑m : ℝ)
have h₁ : m = m
Tactic: rw [Nat.floor_natCast]
-- Lean 4 proof step from Mathlib.NumberTheory.AbelSummation (goal)
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
⊢ ∑ 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
have 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
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]
-- Lean 4 proof step from Mathlib.NumberTheory.AbelSummation (goal)
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 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
have h : m = Nat.floor (α := ℝ) (↑m : ℝ)
Tactic: convert! sum_mul_eq_sub_integral_mul c m.cast_nonneg hf_diff hf_int
-- Lean 4 proof step from Mathlib.NumberTheory.AbelSummation (goal)
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
⊢ m = Nat.floor (α := ℝ) (↑m : ℝ)
have h : m = m
Tactic: rw [Nat.floor_natCast]
-- Lean 4 proof step from Mathlib.NumberTheory.AbelSummation (goal)
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
⊢ ∑ 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
have 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
Tactic: obtain hb | hb := le_or_gt 1 b
-- Lean 4 proof step from Mathlib.NumberTheory.AbelSummation (goal)
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
⊢ ∑ 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
have 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
Tactic: obtain hb | hb := le_or_gt 1 b
-- Lean 4 proof step from Mathlib.NumberTheory.AbelSummation (hypothesis)
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
⊢ ∑ 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
have this : 1 ≤ ⌊b⌋₊
Tactic: have : 1 ≤ ⌊b⌋₊ := (Nat.one_le_floor_iff _).mpr hb
-- Lean 4 proof step from Mathlib.NumberTheory.AbelSummation (goal)
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⌋₊
⊢ ∑ 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
have 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
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]
-- Lean 4 proof step from Mathlib.NumberTheory.AbelSummation (goal)
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 (↑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
have 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
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]
-- Lean 4 proof step from Mathlib.NumberTheory.AbelSummation (goal)
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 : 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
have inr : ∑ x ∈ Icc 0 0, f (↑x : ℝ) * c x =
  f b * ∑ x ∈ Icc 0 0, c x -
    @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Set.Ioc 1 b)) fun (t : ℝ) ↦
      deriv f t * ∑ x ∈ Icc 0 ⌊t⌋₊, c x
Tactic: simp_rw [Nat.floor_eq_zero.mpr hb, Icc_self, sum_singleton, Nat.cast_zero, hc, mul_zero,
      Set.Ioc_eq_empty_of_le hb.le, Measure.restrict_empty, integral_zero_measure, sub_self]
-- Lean 4 proof step from Mathlib.NumberTheory.AbelSummation (goal)
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 : b < 1
inr :
  ∑ x ∈ Icc 0 0, f (↑x : ℝ) * c x =
    f b * ∑ x ∈ Icc 0 0, c x -
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Set.Ioc 1 b)) fun (t : ℝ) ↦
        deriv f t * ∑ x ∈ Icc 0 ⌊t⌋₊, c x
⊢ ∑ 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
have inr₁ : ∑ x ∈ {0}, f (↑x : ℝ) * c x =
  f b * ∑ x ∈ {0}, c x -
    @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Set.Ioc 1 b)) fun (t : ℝ) ↦
      deriv f t * ∑ x ∈ Icc 0 ⌊t⌋₊, c x
Tactic: simp_rw [Nat.floor_eq_zero.mpr hb, Icc_self, sum_singleton, Nat.cast_zero, hc, mul_zero,
      Set.Ioc_eq_empty_of_le hb.le, Measure.restrict_empty, integral_zero_measure, sub_self]
-- Lean 4 proof step from Mathlib.NumberTheory.AbelSummation (goal)
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 : b < 1
inr :
  ∑ x ∈ Icc 0 0, f (↑x : ℝ) * c x =
    f b * ∑ x ∈ Icc 0 0, c x -
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Set.Ioc 1 b)) fun (t : ℝ) ↦
        deriv f t * ∑ x ∈ Icc 0 ⌊t⌋₊, c x
inr₁ :
  ∑ x ∈ {0}, f (↑x : ℝ) * c x =
    f b * ∑ x ∈ {0}, c x -
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Set.Ioc 1 b)) fun (t : ℝ) ↦
        deriv f t * ∑ x ∈ Icc 0 ⌊t⌋₊, c x
⊢ ∑ 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
have inr₂ : f (↑0 : ℝ) * c 0 =
  f b * c 0 -
    @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Set.Ioc 1 b)) fun (t : ℝ) ↦
      deriv f t * ∑ x ∈ Icc 0 ⌊t⌋₊, c x
Tactic: simp_rw [Nat.floor_eq_zero.mpr hb, Icc_self, sum_singleton, Nat.cast_zero, hc, mul_zero,
      Set.Ioc_eq_empty_of_le hb.le, Measure.restrict_empty, integral_zero_measure, sub_self]
-- Lean 4 proof step from Mathlib.NumberTheory.AbelSummation (goal)
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 : b < 1
inr :
  ∑ x ∈ Icc 0 0, f (↑x : ℝ) * c x =
    f b * ∑ x ∈ Icc 0 0, c x -
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Set.Ioc 1 b)) fun (t : ℝ) ↦
        deriv f t * ∑ x ∈ Icc 0 ⌊t⌋₊, c x
inr₁ :
  ∑ x ∈ {0}, f (↑x : ℝ) * c x =
    f b * ∑ x ∈ {0}, c x -
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Set.Ioc 1 b)) fun (t : ℝ) ↦
        deriv f t * ∑ x ∈ Icc 0 ⌊t⌋₊, c x
inr₂ :
  f (↑0 : ℝ) * c 0 =
    f b * c 0 -
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Set.Ioc 1 b)) fun (t : ℝ) ↦
        deriv f t * ∑ x ∈ Icc 0 ⌊t⌋₊, c x
⊢ ∑ 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
have inr₃ : f 0 * c 0 =
  f b * c 0 -
    @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Set.Ioc 1 b)) fun (t : ℝ) ↦
      deriv f t * ∑ x ∈ Icc 0 ⌊t⌋₊, c x
Tactic: simp_rw [Nat.floor_eq_zero.mpr hb, Icc_self, sum_singleton, Nat.cast_zero, hc, mul_zero,
      Set.Ioc_eq_empty_of_le hb.le, Measure.restrict_empty, integral_zero_measure, sub_self]
-- Lean 4 proof step from Mathlib.NumberTheory.AbelSummation (goal)
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 : b < 1
inr :
  ∑ x ∈ Icc 0 0, f (↑x : ℝ) * c x =
    f b * ∑ x ∈ Icc 0 0, c x -
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Set.Ioc 1 b)) fun (t : ℝ) ↦
        deriv f t * ∑ x ∈ Icc 0 ⌊t⌋₊, c x
inr₁ :
  ∑ x ∈ {0}, f (↑x : ℝ) * c x =
    f b * ∑ x ∈ {0}, c x -
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Set.Ioc 1 b)) fun (t : ℝ) ↦
        deriv f t * ∑ x ∈ Icc 0 ⌊t⌋₊, c x
inr₂ :
  f (↑0 : ℝ) * c 0 =
    f b * c 0 -
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Set.Ioc 1 b)) fun (t : ℝ) ↦
        deriv f t * ∑ x ∈ Icc 0 ⌊t⌋₊, c x
inr₃ :
  f 0 * c 0 =
    f b * c 0 -
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Set.Ioc 1 b)) fun (t : ℝ) ↦
        deriv f t * ∑ x ∈ Icc 0 ⌊t⌋₊, c x
⊢ ∑ 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
have inr₄ : f 0 * 0 =
  f b * 0 -
    @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Set.Ioc 1 b)) fun (t : ℝ) ↦
      deriv f t * ∑ x ∈ Icc 0 ⌊t⌋₊, c x
Tactic: simp_rw [Nat.floor_eq_zero.mpr hb, Icc_self, sum_singleton, Nat.cast_zero, hc, mul_zero,
      Set.Ioc_eq_empty_of_le hb.le, Measure.restrict_empty, integral_zero_measure, sub_self]
-- Lean 4 proof step from Mathlib.NumberTheory.AbelSummation (goal)
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 : b < 1
inr :
  ∑ x ∈ Icc 0 0, f (↑x : ℝ) * c x =
    f b * ∑ x ∈ Icc 0 0, c x -
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Set.Ioc 1 b)) fun (t : ℝ) ↦
        deriv f t * ∑ x ∈ Icc 0 ⌊t⌋₊, c x
inr₁ :
  ∑ x ∈ {0}, f (↑x : ℝ) * c x =
    f b * ∑ x ∈ {0}, c x -
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Set.Ioc 1 b)) fun (t : ℝ) ↦
        deriv f t * ∑ x ∈ Icc 0 ⌊t⌋₊, c x
inr₂ :
  f (↑0 : ℝ) * c 0 =
    f b * c 0 -
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Set.Ioc 1 b)) fun (t : ℝ) ↦
        deriv f t * ∑ x ∈ Icc 0 ⌊t⌋₊, c x
inr₃ :
  f 0 * c 0 =
    f b * c 0 -
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Set.Ioc 1 b)) fun (t : ℝ) ↦
        deriv f t * ∑ x ∈ Icc 0 ⌊t⌋₊, c x
inr₄ :
  f 0 * 0 =
    f b * 0 -
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Set.Ioc 1 b)) fun (t : ℝ) ↦
        deriv f t * ∑ x ∈ Icc 0 ⌊t⌋₊, c x
⊢ ∑ 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
have inr₅ : 0 =
  HSub.hSub (α := 𝕜) 0
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Set.Ioc 1 b)) fun (t : ℝ) ↦
      deriv f t * ∑ x ∈ Icc 0 ⌊t⌋₊, c x)
Tactic: simp_rw [Nat.floor_eq_zero.mpr hb, Icc_self, sum_singleton, Nat.cast_zero, hc, mul_zero,
      Set.Ioc_eq_empty_of_le hb.le, Measure.restrict_empty, integral_zero_measure, sub_self]
-- Lean 4 proof step from Mathlib.NumberTheory.AbelSummation (goal)
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 : b < 1
inr :
  ∑ x ∈ Icc 0 0, f (↑x : ℝ) * c x =
    f b * ∑ x ∈ Icc 0 0, c x -
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Set.Ioc 1 b)) fun (t : ℝ) ↦
        deriv f t * ∑ x ∈ Icc 0 ⌊t⌋₊, c x
inr₁ :
  ∑ x ∈ {0}, f (↑x : ℝ) * c x =
    f b * ∑ x ∈ {0}, c x -
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Set.Ioc 1 b)) fun (t : ℝ) ↦
        deriv f t * ∑ x ∈ Icc 0 ⌊t⌋₊, c x
inr₂ :
  f (↑0 : ℝ) * c 0 =
    f b * c 0 -
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Set.Ioc 1 b)) fun (t : ℝ) ↦
        deriv f t * ∑ x ∈ Icc 0 ⌊t⌋₊, c x
inr₃ :
  f 0 * c 0 =
    f b * c 0 -
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Set.Ioc 1 b)) fun (t : ℝ) ↦
        deriv f t * ∑ x ∈ Icc 0 ⌊t⌋₊, c x
inr₄ :
  f 0 * 0 =
    f b * 0 -
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Set.Ioc 1 b)) fun (t : ℝ) ↦
        deriv f t * ∑ x ∈ Icc 0 ⌊t⌋₊, c x
inr₅ :
  0 =
    HSub.hSub (α := 𝕜) 0
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Set.Ioc 1 b)) fun (t : ℝ) ↦
        deriv f t * ∑ x ∈ Icc 0 ⌊t⌋₊, c x)
⊢ ∑ 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
have inr₆ : 0 =
  HSub.hSub (α := 𝕜) 0
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume ∅) fun (t : ℝ) ↦
      deriv f t * ∑ x ∈ Icc 0 ⌊t⌋₊, c x)
Tactic: simp_rw [Nat.floor_eq_zero.mpr hb, Icc_self, sum_singleton, Nat.cast_zero, hc, mul_zero,
      Set.Ioc_eq_empty_of_le hb.le, Measure.restrict_empty, integral_zero_measure, sub_self]
-- Lean 4 proof step from Mathlib.NumberTheory.AbelSummation (goal)
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 : b < 1
inr :
  ∑ x ∈ Icc 0 0, f (↑x : ℝ) * c x =
    f b * ∑ x ∈ Icc 0 0, c x -
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Set.Ioc 1 b)) fun (t : ℝ) ↦
        deriv f t * ∑ x ∈ Icc 0 ⌊t⌋₊, c x
inr₁ :
  ∑ x ∈ {0}, f (↑x : ℝ) * c x =
    f b * ∑ x ∈ {0}, c x -
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Set.Ioc 1 b)) fun (t : ℝ) ↦
        deriv f t * ∑ x ∈ Icc 0 ⌊t⌋₊, c x
inr₂ :
  f (↑0 : ℝ) * c 0 =
    f b * c 0 -
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Set.Ioc 1 b)) fun (t : ℝ) ↦
        deriv f t * ∑ x ∈ Icc 0 ⌊t⌋₊, c x
inr₃ :
  f 0 * c 0 =
    f b * c 0 -
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Set.Ioc 1 b)) fun (t : ℝ) ↦
        deriv f t * ∑ x ∈ Icc 0 ⌊t⌋₊, c x
inr₄ :
  f 0 * 0 =
    f b * 0 -
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Set.Ioc 1 b)) fun (t : ℝ) ↦
        deriv f t * ∑ x ∈ Icc 0 ⌊t⌋₊, c x
inr₅ :
  0 =
    HSub.hSub (α := 𝕜) 0
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Set.Ioc 1 b)) fun (t : ℝ) ↦
        deriv f t * ∑ x ∈ Icc 0 ⌊t⌋₊, c x)
inr₆ :
  0 =
    HSub.hSub (α := 𝕜) 0
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume ∅) fun (t : ℝ) ↦
        deriv f t * ∑ x ∈ Icc 0 ⌊t⌋₊, c x)
⊢ ∑ 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
have inr₇ : 0 =
  HSub.hSub (α := 𝕜) 0
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace 0 fun (t : ℝ) ↦ deriv f t * ∑ x ∈ Icc 0 ⌊t⌋₊, c x)
Tactic: simp_rw [Nat.floor_eq_zero.mpr hb, Icc_self, sum_singleton, Nat.cast_zero, hc, mul_zero,
      Set.Ioc_eq_empty_of_le hb.le, Measure.restrict_empty, integral_zero_measure, sub_self]