awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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)
inr₇ :
  0 =
    HSub.hSub (α := 𝕜) 0
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace 0 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 0
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
hc1 : c 1 = 0
b : ℝ
hf_diff : ∀ t ∈ Set.Icc 2 b, DifferentiableAt ℝ f t
hf_int : IntegrableOn (mα := MeasureSpace.toMeasurableSpace) (deriv f) (Set.Icc 2 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 2 b)) fun (t : ℝ) ↦
        deriv f t * ∑ k ∈ Icc 0 ⌊t⌋₊, c k
have pos : ∀ (hb : b < 2),
  ∑ k ∈ Icc 0 ⌊b⌋₊, f (↑k : ℝ) * c k =
    f b * ∑ k ∈ Icc 0 ⌊b⌋₊, c k -
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Set.Ioc 2 b)) fun (t : ℝ) ↦
        deriv f t * ∑ k ∈ Icc 0 ⌊t⌋₊, c k
Tactic: by_cases! hb : b < 2
-- Lean 4 proof step from Mathlib.NumberTheory.AbelSummation (goal)
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
c : ℕ → 𝕜
f : ℝ → 𝕜
hc : c 0 = 0
hc1 : c 1 = 0
b : ℝ
hf_diff : ∀ t ∈ Set.Icc 2 b, DifferentiableAt ℝ f t
hf_int : IntegrableOn (mα := MeasureSpace.toMeasurableSpace) (deriv f) (Set.Icc 2 b) volume
pos :
  ∀ (hb : b < 2),
    ∑ k ∈ Icc 0 ⌊b⌋₊, f (↑k : ℝ) * c k =
      f b * ∑ k ∈ Icc 0 ⌊b⌋₊, c k -
        @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Set.Ioc 2 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 2 b)) fun (t : ℝ) ↦
        deriv f t * ∑ k ∈ Icc 0 ⌊t⌋₊, c k
have neg : ∀ (hb : 2 ≤ 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 2 b)) fun (t : ℝ) ↦
        deriv f t * ∑ k ∈ Icc 0 ⌊t⌋₊, c k
Tactic: by_cases! hb : b < 2
-- Lean 4 proof step from Mathlib.NumberTheory.AbelSummation (hypothesis)
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
c : ℕ → 𝕜
f : ℝ → 𝕜
hc : c 0 = 0
hc1 : c 1 = 0
b : ℝ
hf_diff : ∀ t ∈ Set.Icc 2 b, DifferentiableAt ℝ f t
hf_int : IntegrableOn (mα := MeasureSpace.toMeasurableSpace) (deriv f) (Set.Icc 2 b) volume
hb : b < 2
⊢ ∑ k ∈ Icc 0 ⌊b⌋₊, f (↑k : ℝ) * c k =
    f b * ∑ k ∈ Icc 0 ⌊b⌋₊, c k -
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Set.Ioc 2 b)) fun (t : ℝ) ↦
        deriv f t * ∑ k ∈ Icc 0 ⌊t⌋₊, c k
have H₁ : ∀ n ∈ Icc 0 ⌊b⌋₊, c n = 0
Tactic: have H₁ : ∀ n ∈ Icc 0 ⌊b⌋₊, c n = 0 := by grind [(Nat.floor_lt' two_ne_zero).mpr hb]
-- Lean 4 proof step from Mathlib.NumberTheory.AbelSummation (hypothesis)
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
c : ℕ → 𝕜
f : ℝ → 𝕜
hc : c 0 = 0
hc1 : c 1 = 0
b : ℝ
hf_diff : ∀ t ∈ Set.Icc 2 b, DifferentiableAt ℝ f t
hf_int : IntegrableOn (mα := MeasureSpace.toMeasurableSpace) (deriv f) (Set.Icc 2 b) volume
hb : b < 2
H₁ : ∀ n ∈ Icc 0 ⌊b⌋₊, c n = 0
⊢ ∑ k ∈ Icc 0 ⌊b⌋₊, f (↑k : ℝ) * c k =
    f b * ∑ k ∈ Icc 0 ⌊b⌋₊, c k -
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Set.Ioc 2 b)) fun (t : ℝ) ↦
        deriv f t * ∑ k ∈ Icc 0 ⌊t⌋₊, c k
have H₂ : ∀ n ∈ Icc 0 ⌊b⌋₊, f (↑n : ℝ) * c n = 0
Tactic: have H₂ : ∀ n ∈ Icc 0 ⌊b⌋₊, f n * c n = 0 := by grind
-- Lean 4 proof step from Mathlib.NumberTheory.AbelSummation (hypothesis)
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
c : ℕ → 𝕜
f : ℝ → 𝕜
hc : c 0 = 0
hc1 : c 1 = 0
b : ℝ
hf_diff : ∀ t ∈ Set.Icc 2 b, DifferentiableAt ℝ f t
hf_int : IntegrableOn (mα := MeasureSpace.toMeasurableSpace) (deriv f) (Set.Icc 2 b) volume
hb : 2 ≤ 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 2 b)) fun (t : ℝ) ↦
        deriv f t * ∑ k ∈ Icc 0 ⌊t⌋₊, c k
have this : 2 ≤ ⌊b⌋₊
Tactic: have : 2 ≤ ⌊b⌋₊ := Nat.le_floor hb
-- Lean 4 proof step from Mathlib.NumberTheory.AbelSummation (goal)
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
c : ℕ → 𝕜
f : ℝ → 𝕜
hc : c 0 = 0
hc1 : c 1 = 0
b : ℝ
hf_diff : ∀ t ∈ Set.Icc 2 b, DifferentiableAt ℝ f t
hf_int : IntegrableOn (mα := MeasureSpace.toMeasurableSpace) (deriv f) (Set.Icc 2 b) volume
hb : 2 ≤ b
this : 2 ≤ ⌊b⌋₊
⊢ ∑ k ∈ Icc 0 ⌊b⌋₊, f (↑k : ℝ) * c k = f (↑2 : ℝ) * c 2 + ∑ k ∈ Ioc 2 ⌊b⌋₊, f (↑k : ℝ) * c k
have rw : Eq.{u_1 + 1} (α := 𝕜) (∑ k ∈ {0, 1} ∪ Icc 2 ⌊b⌋₊, f (↑k : ℝ) * c k) (∑ x ∈ Icc 2 ⌊b⌋₊, f (↑x : ℝ) * c x)
Tactic: rw [add_sum_Ioc_eq_sum_Icc (f := fun (k : ℕ) ↦ f k * c k) this,
      show Icc 0 ⌊b⌋₊ = {0, 1} ∪ Icc 2 ⌊b⌋₊ by grind]
-- Lean 4 proof step from Mathlib.NumberTheory.AbelSummation (hypothesis)
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
c : ℕ → 𝕜
f : ℝ → 𝕜
hc : c 0 = 0
hc1 : c 1 = 0
b : ℝ
hf_diff : ∀ t ∈ Set.Icc 2 b, DifferentiableAt ℝ f t
hf_int : IntegrableOn (mα := MeasureSpace.toMeasurableSpace) (deriv f) (Set.Icc 2 b) volume
hb : 2 ≤ b
this : 2 ≤ ⌊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 2 b)) fun (t : ℝ) ↦
        deriv f t * ∑ k ∈ Icc 0 ⌊t⌋₊, c k
have H : ∑ k ∈ Icc 0 ⌊b⌋₊, f (↑k : ℝ) * c k = f (↑2 : ℝ) * c 2 + ∑ k ∈ Ioc 2 ⌊b⌋₊, f (↑k : ℝ) * c k
Tactic: have H : ∑ k ∈ Icc 0 ⌊b⌋₊, f ↑k * c k = f (2 :) * c 2 + ∑ k ∈ Ioc 2 ⌊b⌋₊, f ↑k * c k := by
    rw [add_sum_Ioc_eq_sum_Icc (f := fun (k : ℕ) ↦ f k * c k) this,
      show Icc 0 ⌊b⌋₊ = {0, 1} ∪ Icc 2 ⌊b⌋₊ by grind]
    exact sum_union_eq_right fun k hk hk' ↦ by grind
-- Lean 4 proof step from Mathlib.NumberTheory.AbelSummation (goal)
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
c : ℕ → 𝕜
f : ℝ → 𝕜
hc : c 0 = 0
hc1 : c 1 = 0
b : ℝ
hf_diff : ∀ t ∈ Set.Icc 2 b, DifferentiableAt ℝ f t
hf_int : IntegrableOn (mα := MeasureSpace.toMeasurableSpace) (deriv f) (Set.Icc 2 b) volume
hb : 2 ≤ b
this : 2 ≤ ⌊b⌋₊
H : ∑ k ∈ Icc 0 ⌊b⌋₊, f (↑k : ℝ) * c k = f (↑2 : ℝ) * c 2 + ∑ k ∈ Ioc 2 ⌊b⌋₊, f (↑k : ℝ) * 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 2 b)) fun (t : ℝ) ↦
        deriv f t * ∑ k ∈ Icc 0 ⌊t⌋₊, c k
have neg : f (↑2 : ℝ) * c 2 + ∑ k ∈ Ioc 2 ⌊b⌋₊, f (↑k : ℝ) * c k =
  f b * ∑ k ∈ Icc 0 ⌊b⌋₊, c k -
    @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Set.Ioc 2 b)) fun (t : ℝ) ↦
      deriv f t * ∑ k ∈ Icc 0 ⌊t⌋₊, c k
Tactic: rw [H]
-- Lean 4 proof step from Mathlib.NumberTheory.AbelSummation (goal)
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
c : ℕ → 𝕜
f : ℝ → 𝕜
hc : c 0 = 0
hc1 : c 1 = 0
b : ℝ
hf_diff : ∀ t ∈ Set.Icc 2 b, DifferentiableAt ℝ f t
hf_int : IntegrableOn (mα := MeasureSpace.toMeasurableSpace) (deriv f) (Set.Icc 2 b) volume
hb : 2 ≤ b
this : 2 ≤ ⌊b⌋₊
H : ∑ k ∈ Icc 0 ⌊b⌋₊, f (↑k : ℝ) * c k = f (↑2 : ℝ) * c 2 + ∑ k ∈ Ioc 2 ⌊b⌋₊, f (↑k : ℝ) * c k
⊢ f (↑2 : ℝ) * c 2 + ∑ k ∈ Ioc 2 ⌊b⌋₊, f (↑k : ℝ) * c k =
    f b * ∑ k ∈ Icc 0 ⌊b⌋₊, c k -
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Set.Ioc 2 b)) fun (t : ℝ) ↦
        deriv f t * ∑ k ∈ Icc 0 ⌊t⌋₊, c k
have neg : f (↑2 : ℝ) * c 2 + ∑ k ∈ Ioc (Nat.floor (α := ℝ) 2) ⌊b⌋₊, f (↑k : ℝ) * c k =
  f b * ∑ k ∈ Icc 0 ⌊b⌋₊, c k -
    @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Set.Ioc 2 b)) fun (t : ℝ) ↦
      deriv f t * ∑ k ∈ Icc 0 ⌊t⌋₊, c k
Tactic: nth_rewrite 3 [show 2 = ⌊(2 : ℝ)⌋₊ by simp]
-- Lean 4 proof step from Mathlib.NumberTheory.AbelSummation (goal)
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
c : ℕ → 𝕜
f : ℝ → 𝕜
hc : c 0 = 0
hc1 : c 1 = 0
b : ℝ
hf_diff : ∀ t ∈ Set.Icc 2 b, DifferentiableAt ℝ f t
hf_int : IntegrableOn (mα := MeasureSpace.toMeasurableSpace) (deriv f) (Set.Icc 2 b) volume
hb : 2 ≤ b
this : 2 ≤ ⌊b⌋₊
H : ∑ k ∈ Icc 0 ⌊b⌋₊, f (↑k : ℝ) * c k = f (↑2 : ℝ) * c 2 + ∑ k ∈ Ioc 2 ⌊b⌋₊, f (↑k : ℝ) * c k
⊢ f (↑2 : ℝ) * c 2 + ∑ k ∈ Ioc (Nat.floor (α := ℝ) 2) ⌊b⌋₊, f (↑k : ℝ) * c k =
    f b * ∑ k ∈ Icc 0 ⌊b⌋₊, c k -
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Set.Ioc 2 b)) fun (t : ℝ) ↦
        deriv f t * ∑ k ∈ Icc 0 ⌊t⌋₊, c k
have neg : f (↑2 : ℝ) * c 2 +
    (f b * ∑ k ∈ Icc 0 ⌊b⌋₊, c k - f 2 * ∑ k ∈ Icc 0 (Nat.floor (α := ℝ) 2), c k -
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Set.Ioc 2 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 2 b)) fun (t : ℝ) ↦
      deriv f t * ∑ k ∈ Icc 0 ⌊t⌋₊, c k
Tactic: rw [sum_mul_eq_sub_sub_integral_mul c zero_le_two hb hf_diff hf_int]
-- Lean 4 proof step from Mathlib.NumberTheory.AbelSummation (goal)
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
c : ℕ → 𝕜
f : ℝ → 𝕜
hc : c 0 = 0
hc1 : c 1 = 0
b : ℝ
hf_diff : ∀ t ∈ Set.Icc 2 b, DifferentiableAt ℝ f t
hf_int : IntegrableOn (mα := MeasureSpace.toMeasurableSpace) (deriv f) (Set.Icc 2 b) volume
hb : 2 ≤ b
this : 2 ≤ ⌊b⌋₊
H : ∑ k ∈ Icc 0 ⌊b⌋₊, f (↑k : ℝ) * c k = f (↑2 : ℝ) * c 2 + ∑ k ∈ Ioc 2 ⌊b⌋₊, f (↑k : ℝ) * c k
⊢ f (↑2 : ℝ) * c 2 +
      (f b * ∑ k ∈ Icc 0 ⌊b⌋₊, c k - f 2 * ∑ k ∈ Icc 0 (Nat.floor (α := ℝ) 2), c k -
        @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Set.Ioc 2 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 2 b)) fun (t : ℝ) ↦
        deriv f t * ∑ k ∈ Icc 0 ⌊t⌋₊, c k
have neg : f 2 * c 2 +
    (f b * ∑ k ∈ Icc 0 ⌊b⌋₊, c k - f 2 * c 2 -
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Set.Ioc 2 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 2 b)) fun (t : ℝ) ↦
      deriv f t * ∑ k ∈ Icc 0 ⌊t⌋₊, c k
Tactic: simp [show Icc 0 2 = {0, 1, 2} by rfl, hc, hc1]
-- Lean 4 proof step from Mathlib.NumberTheory.AbelSummation (goal)
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
c : ℕ → 𝕜
a : ℝ
m : ℕ
ha : 0 ≤ a
g : ℝ → 𝕜
hg : LocallyIntegrableOn g (Set.Ici a) volume
⊢ LocallyIntegrableOn.{0, u_1} (ε := 𝕜) (fun (t : ℝ) ↦ g t * ∑ k ∈ Icc m ⌊t⌋₊, c k) (Set.Ici a) volume
have refine : ∀ (K : Set ℝ) (hK₁ : K ⊆ Set.Ici a) (hK₂ : IsCompact K),
  IntegrableOn.{0, u_1} (ε := 𝕜) (mα := Real.measurableSpace) (fun (t : ℝ) ↦ g t * ∑ k ∈ Icc m ⌊t⌋₊, c k) K volume
Tactic: refine (locallyIntegrableOn_iff isLocallyClosed_Ici).mpr fun K hK₁ hK₂ ↦ ?_
-- Lean 4 proof step from Mathlib.NumberTheory.AbelSummation (goal)
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
c : ℕ → 𝕜
a : ℝ
m : ℕ
ha : 0 ≤ a
g : ℝ → 𝕜
hg : LocallyIntegrableOn g (Set.Ici a) volume
K : Set ℝ
hK₁ : K ⊆ Set.Ici a
hK₂ : IsCompact K
⊢ IntegrableOn.{0, u_1} (ε := 𝕜) (mα := Real.measurableSpace) (fun (t : ℝ) ↦ g t * ∑ k ∈ Icc m ⌊t⌋₊, c k) K volume
have pos : ∀ (hK₃ : K.Nonempty),
  IntegrableOn.{0, u_1} (ε := 𝕜) (mα := Real.measurableSpace) (fun (t : ℝ) ↦ g t * ∑ k ∈ Icc m ⌊t⌋₊, c k) K volume
Tactic: by_cases hK₃ : K.Nonempty
-- Lean 4 proof step from Mathlib.NumberTheory.AbelSummation (goal)
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
c : ℕ → 𝕜
a : ℝ
m : ℕ
ha : 0 ≤ a
g : ℝ → 𝕜
hg : LocallyIntegrableOn g (Set.Ici a) volume
K : Set ℝ
hK₁ : K ⊆ Set.Ici a
hK₂ : IsCompact K
pos :
  ∀ (hK₃ : K.Nonempty),
    IntegrableOn.{0, u_1} (ε := 𝕜) (mα := Real.measurableSpace) (fun (t : ℝ) ↦ g t * ∑ k ∈ Icc m ⌊t⌋₊, c k) K volume
⊢ IntegrableOn.{0, u_1} (ε := 𝕜) (mα := Real.measurableSpace) (fun (t : ℝ) ↦ g t * ∑ k ∈ Icc m ⌊t⌋₊, c k) K volume
have neg : ∀ (hK₃ : ¬K.Nonempty),
  IntegrableOn.{0, u_1} (ε := 𝕜) (mα := Real.measurableSpace) (fun (t : ℝ) ↦ g t * ∑ k ∈ Icc m ⌊t⌋₊, c k) K volume
Tactic: by_cases hK₃ : K.Nonempty
-- Lean 4 proof step from Mathlib.NumberTheory.AbelSummation (hypothesis)
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
c : ℕ → 𝕜
a : ℝ
m : ℕ
ha : 0 ≤ a
g : ℝ → 𝕜
hg : LocallyIntegrableOn g (Set.Ici a) volume
K : Set ℝ
hK₁ : K ⊆ Set.Ici a
hK₂ : IsCompact K
hK₃ : K.Nonempty
⊢ IntegrableOn.{0, u_1} (ε := 𝕜) (mα := Real.measurableSpace) (fun (t : ℝ) ↦ g t * ∑ k ∈ Icc m ⌊t⌋₊, c k) K volume
have h_inf : a ≤ sInf K
Tactic: have h_inf : a ≤ sInf K := (hK₁ (hK₂.sInf_mem hK₃))
-- Lean 4 proof step from Mathlib.NumberTheory.AbelSummation (goal)
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
c : ℕ → 𝕜
a : ℝ
m : ℕ
ha : 0 ≤ a
g : ℝ → 𝕜
hg : LocallyIntegrableOn g (Set.Ici a) volume
K : Set ℝ
hK₁ : K ⊆ Set.Ici a
hK₂ : IsCompact K
hK₃ : K.Nonempty
h_inf : a ≤ sInf K
⊢ IntegrableOn.{0, u_1} (ε := 𝕜) (mα := Real.measurableSpace) (fun (t : ℝ) ↦ g t * ∑ k ∈ Icc m ⌊t⌋₊, c k) K volume
have pos : IntegrableOn.{0, u_1} (ε := 𝕜) (mα := Real.measurableSpace) (fun (t : ℝ) ↦ g t * ∑ k ∈ Icc m ⌊t⌋₊, c k)
  (Set.Icc (sInf K) (sSup K)) volume
Tactic: refine IntegrableOn.mono_set ?_ (Bornology.IsBounded.subset_Icc_sInf_sSup hK₂.isBounded)
-- Lean 4 proof step from Mathlib.NumberTheory.AbelSummation (goal)
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
c : ℕ → 𝕜
a : ℝ
m : ℕ
ha : 0 ≤ a
g : ℝ → 𝕜
hg : LocallyIntegrableOn g (Set.Ici a) volume
K : Set ℝ
hK₁ : K ⊆ Set.Ici a
hK₂ : IsCompact K
hK₃ : K.Nonempty
h_inf : a ≤ sInf K
⊢ IntegrableOn.{0, u_1} (ε := 𝕜) (mα := Real.measurableSpace) (fun (t : ℝ) ↦ g t * ∑ k ∈ Icc m ⌊t⌋₊, c k)
    (Set.Icc (sInf K) (sSup K)) volume
have pos : IntegrableOn (mα := MeasureSpace.toMeasurableSpace) g (Set.Icc (sInf K) (sSup K)) volume
Tactic: refine integrableOn_mul_sum_Icc _ (ha.trans h_inf) ?_
-- Lean 4 proof step from Mathlib.NumberTheory.AbelSummation (goal)
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
c : ℕ → 𝕜
a : ℝ
m : ℕ
ha : 0 ≤ a
g : ℝ → 𝕜
hg : LocallyIntegrableOn g (Set.Ici a) volume
K : Set ℝ
hK₁ : K ⊆ Set.Ici a
hK₂ : IsCompact K
hK₃ : K.Nonempty
h_inf : a ≤ sInf K
⊢ IntegrableOn (mα := MeasureSpace.toMeasurableSpace) g (Set.Icc (sInf K) (sSup K)) volume
have pos : Set.Icc (sInf K) (sSup K) ⊆ Set.Ici a
Tactic: refine hg.integrableOn_compact_subset ?_ isCompact_Icc
-- Lean 4 proof step from Mathlib.NumberTheory.AbelSummation (goal)
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
c : ℕ → 𝕜
a : ℝ
m : ℕ
ha : 0 ≤ a
g : ℝ → 𝕜
hg : LocallyIntegrableOn g (Set.Ici a) volume
K : Set ℝ
hK₁ : K ⊆ Set.Ici a
hK₂ : IsCompact K
hK₃ : ¬K.Nonempty
⊢ IntegrableOn.{0, u_1} (ε := 𝕜) (mα := Real.measurableSpace) (fun (t : ℝ) ↦ g t * ∑ k ∈ Icc m ⌊t⌋₊, c k) K volume
have neg : IntegrableOn.{0, u_1} (ε := 𝕜) (mα := Real.measurableSpace) (fun (t : ℝ) ↦ g t * ∑ k ∈ Icc m ⌊t⌋₊, c k) ∅ volume
Tactic: rw [Set.not_nonempty_iff_eq_empty.mp hK₃]
-- Lean 4 proof step from Mathlib.NumberTheory.AbelSummation (goal)
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
c : ℕ → 𝕜
f : ℝ → 𝕜
hf_diff : ∀ (t : ℝ), Membership.mem (γ := Set ℝ) (Set.Ici 0) t → DifferentiableAt ℝ f t
hf_int : LocallyIntegrableOn (deriv f) (Set.Ici 0) volume
l : 𝕜
h_lim : Tendsto (fun (n : ℕ) ↦ f (↑n : ℝ) * ∑ k ∈ Icc 0 n, c k) atTop (𝓝 l)
g : ℝ → 𝕜
hg_dom : Asymptotics.IsBigO (E := 𝕜) atTop (fun (t : ℝ) ↦ deriv f t * ∑ k ∈ Icc 0 ⌊t⌋₊, c k) g
hg_int : IntegrableAtFilter (mα := MeasureSpace.toMeasurableSpace) g atTop volume
x : ℕ
⊢ Eq.{u_1 + 1} (α := 𝕜) (∫ (x : ℝ) in 0..(↑x : ℝ), deriv f x * ∑ k ∈ Icc 0 ⌊x⌋₊, c k)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Set.Ioc 0 (↑x : ℝ))) fun (t : ℝ) ↦
      deriv f t * ∑ k ∈ Icc 0 ⌊t⌋₊, c k)
have rw : Eq.{u_1 + 1} (α := 𝕜) (∫ (x : ℝ) in 0..(↑x : ℝ), deriv f x * ∑ k ∈ Icc 0 ⌊x⌋₊, c k)
  (∫ (x : ℝ) in 0..(↑x : ℝ), deriv f x * ∑ k ∈ Icc 0 ⌊x⌋₊, c k)
Tactic: rw [← integral_of_le (Nat.cast_nonneg _)]
-- Lean 4 proof step from Mathlib.NumberTheory.AbelSummation (goal)
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
c : ℕ → 𝕜
f : ℝ → 𝕜
hf_diff : ∀ (t : ℝ), Membership.mem (γ := Set ℝ) (Set.Ici 0) t → DifferentiableAt ℝ f t
hf_int : LocallyIntegrableOn (deriv f) (Set.Ici 0) volume
l : 𝕜
h_lim : Tendsto (fun (n : ℕ) ↦ f (↑n : ℝ) * ∑ k ∈ Icc 0 n, c k) atTop (𝓝 l)
g : ℝ → 𝕜
hg_dom : Asymptotics.IsBigO (E := 𝕜) atTop (fun (t : ℝ) ↦ deriv f t * ∑ k ∈ Icc 0 ⌊t⌋₊, c k) g
hg_int : IntegrableAtFilter (mα := MeasureSpace.toMeasurableSpace) g atTop volume
⊢ Tendsto.{0, u_1} (β := 𝕜)
    (fun (n : ℕ) ↦
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Set.Ioc 0 (↑n : ℝ))) fun (t : ℝ) ↦
        deriv f t * ∑ k ∈ Icc 0 ⌊t⌋₊, c k)
    atTop
    (𝓝
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Set.Ioi 0)) fun (t : ℝ) ↦
        deriv f t * ∑ k ∈ Icc 0 ⌊t⌋₊, c k))
have refine : Tendsto.{0, u_1} (β := 𝕜) (fun (x : ℕ) ↦ ∫ (x : ℝ) in 0..(↑x : ℝ), deriv f x * ∑ k ∈ Icc 0 ⌊x⌋₊, c k) atTop
  (𝓝
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Set.Ioi 0)) fun (t : ℝ) ↦
      deriv f t * ∑ k ∈ Icc 0 ⌊t⌋₊, c k))
Tactic: refine Tendsto.congr (fun _ ↦ by rw [← integral_of_le (Nat.cast_nonneg _)]) ?_
-- Lean 4 proof step from Mathlib.NumberTheory.AbelSummation (goal)
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
c : ℕ → 𝕜
f : ℝ → 𝕜
hf_diff : ∀ (t : ℝ), Membership.mem (γ := Set ℝ) (Set.Ici 0) t → DifferentiableAt ℝ f t
hf_int : LocallyIntegrableOn (deriv f) (Set.Ici 0) volume
l : 𝕜
h_lim : Tendsto (fun (n : ℕ) ↦ f (↑n : ℝ) * ∑ k ∈ Icc 0 n, c k) atTop (𝓝 l)
g : ℝ → 𝕜
hg_dom : Asymptotics.IsBigO (E := 𝕜) atTop (fun (t : ℝ) ↦ deriv f t * ∑ k ∈ Icc 0 ⌊t⌋₊, c k) g
hg_int : IntegrableAtFilter (mα := MeasureSpace.toMeasurableSpace) g atTop volume
⊢ Tendsto.{0, u_1} (β := 𝕜) (fun (x : ℕ) ↦ ∫ (x : ℝ) in 0..(↑x : ℝ), deriv f x * ∑ k ∈ Icc 0 ⌊x⌋₊, c k) atTop
    (𝓝
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Set.Ioi 0)) fun (t : ℝ) ↦
        deriv f t * ∑ k ∈ Icc 0 ⌊t⌋₊, c k))
have refine : IntegrableOn.{0, u_1} (ε := 𝕜) (mα := Real.measurableSpace) (fun (x : ℝ) ↦ deriv f x * ∑ k ∈ Icc 0 ⌊x⌋₊, c k)
  (Set.Ioi 0) volume
Tactic: refine intervalIntegral_tendsto_integral_Ioi _ ?_ tendsto_natCast_atTop_atTop
-- Lean 4 proof step from Mathlib.NumberTheory.AbelSummation (hypothesis)
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
c : ℕ → 𝕜
f : ℝ → 𝕜
hf_diff : ∀ (t : ℝ), Membership.mem (γ := Set ℝ) (Set.Ici 0) t → DifferentiableAt ℝ f t
hf_int : LocallyIntegrableOn (deriv f) (Set.Ici 0) volume
l : 𝕜
h_lim : Tendsto (fun (n : ℕ) ↦ f (↑n : ℝ) * ∑ k ∈ Icc 0 n, c k) atTop (𝓝 l)
g : ℝ → 𝕜
hg_dom : Asymptotics.IsBigO (E := 𝕜) atTop (fun (t : ℝ) ↦ deriv f t * ∑ k ∈ Icc 0 ⌊t⌋₊, c k) g
hg_int : IntegrableAtFilter (mα := MeasureSpace.toMeasurableSpace) g atTop volume
⊢ Tendsto (fun (n : ℕ) ↦ ∑ k ∈ Icc 0 n, f (↑k : ℝ) * c k) atTop
    (𝓝
      (l -
        @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Set.Ioi 0)) fun (t : ℝ) ↦
          deriv f t * ∑ k ∈ Icc 0 ⌊t⌋₊, c k))
have h_lim' : Tendsto.{0, u_1} (β := 𝕜)
  (fun (n : ℕ) ↦
    @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Set.Ioc 0 (↑n : ℝ))) fun (t : ℝ) ↦
      deriv f t * ∑ k ∈ Icc 0 ⌊t⌋₊, c k)
  atTop
  (𝓝
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Set.Ioi 0)) fun (t : ℝ) ↦
      deriv f t * ∑ k ∈ Icc 0 ⌊t⌋₊, c k))
Tactic: have h_lim' : Tendsto (fun n : ℕ ↦ ∫ t in Set.Ioc (0 : ℝ) n, deriv f t * ∑ k ∈ Icc 0 ⌊t⌋₊, c k)
      atTop (𝓝 (∫ t in Set.Ioi 0, deriv f t * ∑ k ∈ Icc 0 ⌊t⌋₊, c k)) := by
    refine Tendsto.congr (fun _ ↦ by rw [← integral_of_le (Nat.cast_nonneg _)]) ?_
    refine intervalIntegral_tendsto_integral_Ioi _ ?_ tendsto_natCast_atTop_atTop
    exact Iff.mp integrableOn_Ici_iff_integrableOn_Ioi
      <| (locallyIntegrableOn_mul_sum_Icc c le_rfl hf_int).integrableOn_of_isBigO_atTop
        hg_dom hg_int
-- Lean 4 proof step from Mathlib.NumberTheory.AbelSummation (goal)
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
c : ℕ → 𝕜
f : ℝ → 𝕜
hf_diff : ∀ (t : ℝ), Membership.mem (γ := Set ℝ) (Set.Ici 0) t → DifferentiableAt ℝ f t
hf_int : LocallyIntegrableOn (deriv f) (Set.Ici 0) volume
l : 𝕜
h_lim : Tendsto (fun (n : ℕ) ↦ f (↑n : ℝ) * ∑ k ∈ Icc 0 n, c k) atTop (𝓝 l)
g : ℝ → 𝕜
hg_dom : Asymptotics.IsBigO (E := 𝕜) atTop (fun (t : ℝ) ↦ deriv f t * ∑ k ∈ Icc 0 ⌊t⌋₊, c k) g
hg_int : IntegrableAtFilter (mα := MeasureSpace.toMeasurableSpace) g atTop volume
h_lim' :
  Tendsto.{0, u_1} (β := 𝕜)
    (fun (n : ℕ) ↦
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Set.Ioc 0 (↑n : ℝ))) fun (t : ℝ) ↦
        deriv f t * ∑ k ∈ Icc 0 ⌊t⌋₊, c k)
    atTop
    (𝓝
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Set.Ioi 0)) fun (t : ℝ) ↦
        deriv f t * ∑ k ∈ Icc 0 ⌊t⌋₊, c k))
⊢ Tendsto (fun (n : ℕ) ↦ ∑ k ∈ Icc 0 n, f (↑k : ℝ) * c k) atTop
    (𝓝
      (l -
        @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Set.Ioi 0)) fun (t : ℝ) ↦
          deriv f t * ∑ k ∈ Icc 0 ⌊t⌋₊, c k))
have refine : ∀ (x : ℕ),
  (f (↑x : ℝ) * ∑ k ∈ Icc 0 x, c k -
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Set.Ioc 0 (↑x : ℝ))) fun (t : ℝ) ↦
        deriv f t * ∑ k ∈ Icc 0 ⌊t⌋₊, c k) =
    ∑ k ∈ Icc 0 x, f (↑k : ℝ) * c k
Tactic: refine (h_lim.sub h_lim').congr (fun _ ↦ ?_)
-- Lean 4 proof step from Mathlib.NumberTheory.AbelSummation (goal)
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
c : ℕ → 𝕜
f : ℝ → 𝕜
hf_diff : ∀ (t : ℝ), Membership.mem (γ := Set ℝ) (Set.Ici 0) t → DifferentiableAt ℝ f t
hf_int : LocallyIntegrableOn (deriv f) (Set.Ici 0) volume
l : 𝕜
h_lim : Tendsto (fun (n : ℕ) ↦ f (↑n : ℝ) * ∑ k ∈ Icc 0 n, c k) atTop (𝓝 l)
g : ℝ → 𝕜
hg_dom : Asymptotics.IsBigO (E := 𝕜) atTop (fun (t : ℝ) ↦ deriv f t * ∑ k ∈ Icc 0 ⌊t⌋₊, c k) g
hg_int : IntegrableAtFilter (mα := MeasureSpace.toMeasurableSpace) g atTop volume
h_lim' :
  Tendsto.{0, u_1} (β := 𝕜)
    (fun (n : ℕ) ↦
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Set.Ioc 0 (↑n : ℝ))) fun (t : ℝ) ↦
        deriv f t * ∑ k ∈ Icc 0 ⌊t⌋₊, c k)
    atTop
    (𝓝
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Set.Ioi 0)) fun (t : ℝ) ↦
        deriv f t * ∑ k ∈ Icc 0 ⌊t⌋₊, c k))
x : ℕ
⊢ (f (↑x : ℝ) * ∑ k ∈ Icc 0 x, c k -
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Set.Ioc 0 (↑x : ℝ))) fun (t : ℝ) ↦
        deriv f t * ∑ k ∈ Icc 0 ⌊t⌋₊, c k) =
    ∑ k ∈ Icc 0 x, f (↑k : ℝ) * c k
have rw : IntegrableOn (mα := MeasureSpace.toMeasurableSpace) (deriv f) (Set.Icc 0 (↑x : ℝ)) volume
Tactic: rw [sum_mul_eq_sub_integral_mul' _ _ (fun t ht ↦ hf_diff _ ht.1)]