awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 : 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)
inr₈ : 0 = HSub.hSub (α := 𝕜) 0 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 1 b)) fun (t : ℝ) ↦
        deriv f t * ∑ k ∈ Icc 0 ⌊t⌋₊, c k

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]

Premises used: Iff.mpr, MeasureTheory.Measure.restrict_empty, sub_self, LT.lt.le, MulZeroClass.mul_zero, Finset.sum_singleton, Finset.Icc_self, Set.Ioc_eq_empty_of_le, Nat.floor_eq_zero, MeasureTheory.integral_zero_measure, Nat.cast_zero
-- Module: Mathlib.NumberTheory.AbelSummation
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
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
⊢ ∑ 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
-- Module: Mathlib.NumberTheory.AbelSummation
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
⊢ ∀ n ∈ Icc 0 ⌊b⌋₊, c n = 0

Tactic:
grind [(Nat.floor_lt' two_ne_zero).mpr hb]

Premises used: Iff.mpr, Nat.floor_lt', two_ne_zero
-- Module: Mathlib.NumberTheory.AbelSummation
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
⊢ ∀ 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]
-- Module: Mathlib.NumberTheory.AbelSummation
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
⊢ ∀ n ∈ Icc 0 ⌊b⌋₊, f (↑n : ℝ) * c n = 0

Tactic:
grind
-- Module: Mathlib.NumberTheory.AbelSummation
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
⊢ ∀ n ∈ Icc 0 ⌊b⌋₊, f (↑n : ℝ) * c n = 0

Tactic:
have H₂ : ∀ n ∈ Icc 0 ⌊b⌋₊, f n * c n = 0 := by grind
-- Module: Mathlib.NumberTheory.AbelSummation
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
H₂ : ∀ n ∈ Icc 0 ⌊b⌋₊, f (↑n : ℝ) * 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

Tactic:
simp [sum_eq_zero H₁, sum_eq_zero H₂, Set.Ioc_eq_empty_of_le hb.le]

Premises used: Finset.sum_eq_zero, LT.lt.le, Set.Ioc_eq_empty_of_le
-- Module: Mathlib.NumberTheory.AbelSummation
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
⊢ 2 ≤ ⌊b⌋₊

Tactic:
have : 2 ≤ ⌊b⌋₊ := Nat.le_floor hb
-- Module: Mathlib.NumberTheory.AbelSummation
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⌋₊
⊢ Icc 0 ⌊b⌋₊ = {0, 1} ∪ Icc 2 ⌊b⌋₊

Tactic:
grind
-- Module: Mathlib.NumberTheory.AbelSummation
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⌋₊
rw : Eq.{u_1 + 1} (α := 𝕜) (∑ k ∈ {0, 1} ∪ Icc 2 ⌊b⌋₊, f (↑k : ℝ) * c k) (∑ x ∈ Icc 2 ⌊b⌋₊, f (↑x : ℝ) * c x)
⊢ ∑ k ∈ Icc 0 ⌊b⌋₊, f (↑k : ℝ) * c k = f (↑2 : ℝ) * c 2 + ∑ k ∈ Ioc 2 ⌊b⌋₊, f (↑k : ℝ) * c k

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]

Premises used: Finset.add_sum_Ioc_eq_sum_Icc
-- Module: Mathlib.NumberTheory.AbelSummation
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 : ℕ
hk : Membership.mem (γ := Finset ℕ) {0, 1} k
hk' : k ∉ Icc 2 ⌊b⌋₊
⊢ f (↑k : ℝ) * c k = 0

Tactic:
grind
-- Module: Mathlib.NumberTheory.AbelSummation
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⌋₊
⊢ Eq.{u_1 + 1} (α := 𝕜) (∑ k ∈ {0, 1} ∪ Icc 2 ⌊b⌋₊, f (↑k : ℝ) * c k) (∑ x ∈ Icc 2 ⌊b⌋₊, f (↑x : ℝ) * c x)

Tactic:
exact sum_union_eq_right fun k hk hk' ↦ by grind

Premises used: Finset.sum_union_eq_right
-- Module: Mathlib.NumberTheory.AbelSummation
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

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
-- Module: Mathlib.NumberTheory.AbelSummation
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
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
⊢ ∑ 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:
rw [H]
-- Module: Mathlib.NumberTheory.AbelSummation
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
⊢ 2 = Nat.floor (α := ℝ) 2

Tactic:
simp
-- Module: Mathlib.NumberTheory.AbelSummation
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
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
⊢ 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:
nth_rewrite 3 [show 2 = ⌊(2 : ℝ)⌋₊ by simp]
-- Module: Mathlib.NumberTheory.AbelSummation
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
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
⊢ 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:
rw [sum_mul_eq_sub_sub_integral_mul c zero_le_two hb hf_diff hf_int]

Premises used: zero_le_two, sum_mul_eq_sub_sub_integral_mul
-- Module: Mathlib.NumberTheory.AbelSummation
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
⊢ Eq (α := Finset ℕ) (Icc 0 2) {0, 1, 2}

Tactic:
rfl
-- Module: Mathlib.NumberTheory.AbelSummation
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
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
⊢ 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:
simp [show Icc 0 2 = {0, 1, 2} by rfl, hc, hc1]
-- Module: Mathlib.NumberTheory.AbelSummation
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 * 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:
grind
-- Module: Mathlib.NumberTheory.AbelSummation
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

Tactic:
(locallyIntegrableOn_iff isLocallyClosed_Ici).mpr fun K hK₁ hK₂ ↦ ?_

Premises used: MeasureTheory.locallyIntegrableOn_iff, Iff.mpr, isLocallyClosed_Ici
-- Module: Mathlib.NumberTheory.AbelSummation
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
c : ℕ → 𝕜
a : ℝ
m : ℕ
ha : 0 ≤ a
g : ℝ → 𝕜
hg : LocallyIntegrableOn g (Set.Ici a) volume
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
⊢ LocallyIntegrableOn.{0, u_1} (ε := 𝕜) (fun (t : ℝ) ↦ g t * ∑ k ∈ Icc m ⌊t⌋₊, c k) (Set.Ici a) volume

Tactic:
refine (locallyIntegrableOn_iff isLocallyClosed_Ici).mpr fun K hK₁ hK₂ ↦ ?_

Premises used: MeasureTheory.locallyIntegrableOn_iff, Iff.mpr, isLocallyClosed_Ici
-- Module: Mathlib.NumberTheory.AbelSummation
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
neg :
  ∀ (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

Tactic:
by_cases hK₃ : K.Nonempty

Premises used: Set.Nonempty
-- Module: Mathlib.NumberTheory.AbelSummation
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
⊢ a ≤ sInf K

Tactic:
have h_inf : a ≤ sInf K := (hK₁ (hK₂.sInf_mem hK₃))
-- Module: Mathlib.NumberTheory.AbelSummation
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

Tactic:
IntegrableOn.mono_set ?_ (Bornology.IsBounded.subset_Icc_sInf_sSup hK₂.isBounded)

Premises used: Bornology.IsBounded.subset_Icc_sInf_sSup, IsCompact.isBounded, MeasureTheory.IntegrableOn.mono_set
-- Module: Mathlib.NumberTheory.AbelSummation
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
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
⊢ IntegrableOn.{0, u_1} (ε := 𝕜) (mα := Real.measurableSpace) (fun (t : ℝ) ↦ g t * ∑ k ∈ Icc m ⌊t⌋₊, c k) K volume

Tactic:
refine IntegrableOn.mono_set ?_ (Bornology.IsBounded.subset_Icc_sInf_sSup hK₂.isBounded)

Premises used: Bornology.IsBounded.subset_Icc_sInf_sSup, IsCompact.isBounded, MeasureTheory.IntegrableOn.mono_set
-- Module: Mathlib.NumberTheory.AbelSummation
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

Tactic:
integrableOn_mul_sum_Icc _ (ha.trans h_inf) ?_

Premises used: integrableOn_mul_sum_Icc, LE.le.trans
-- Module: Mathlib.NumberTheory.AbelSummation
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
pos : IntegrableOn (mα := MeasureSpace.toMeasurableSpace) g (Set.Icc (sInf K) (sSup K)) volume
⊢ 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_mul_sum_Icc _ (ha.trans h_inf) ?_

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

Tactic:
hg.integrableOn_compact_subset ?_ isCompact_Icc

Premises used: CompactIccSpace.isCompact_Icc, MeasureTheory.LocallyIntegrableOn.integrableOn_compact_subset
-- Module: Mathlib.NumberTheory.AbelSummation
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
pos : Set.Icc (sInf K) (sSup K) ⊆ Set.Ici a
⊢ IntegrableOn (mα := MeasureSpace.toMeasurableSpace) g (Set.Icc (sInf K) (sSup K)) volume

Tactic:
refine hg.integrableOn_compact_subset ?_ isCompact_Icc

Premises used: CompactIccSpace.isCompact_Icc, MeasureTheory.LocallyIntegrableOn.integrableOn_compact_subset
-- Module: Mathlib.NumberTheory.AbelSummation
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
⊢ Set.Icc (sInf K) (sSup K) ⊆ Set.Ici a

Tactic:
(Set.Icc_subset_Ici_iff (Real.sInf_le_sSup _ hK₂.bddBelow hK₂.bddAbove)).mpr h_inf

Premises used: IsCompact.bddBelow, Iff.mpr, Real.sInf_le_sSup, IsCompact.bddAbove, Set.Icc_subset_Ici_iff
-- Module: Mathlib.NumberTheory.AbelSummation
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
⊢ Set.Icc (sInf K) (sSup K) ⊆ Set.Ici a

Tactic:
exact (Set.Icc_subset_Ici_iff (Real.sInf_le_sSup _ hK₂.bddBelow hK₂.bddAbove)).mpr h_inf

Premises used: IsCompact.bddBelow, Iff.mpr, Real.sInf_le_sSup, IsCompact.bddAbove, Set.Icc_subset_Ici_iff
-- Module: Mathlib.NumberTheory.AbelSummation
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
neg : IntegrableOn.{0, u_1} (ε := 𝕜) (mα := Real.measurableSpace) (fun (t : ℝ) ↦ g t * ∑ k ∈ Icc m ⌊t⌋₊, c k) ∅ volume
⊢ IntegrableOn.{0, u_1} (ε := 𝕜) (mα := Real.measurableSpace) (fun (t : ℝ) ↦ g t * ∑ k ∈ Icc m ⌊t⌋₊, c k) K volume

Tactic:
rw [Set.not_nonempty_iff_eq_empty.mp hK₃]

Premises used: Set.not_nonempty_iff_eq_empty, Iff.mp
-- Module: Mathlib.NumberTheory.AbelSummation
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) ∅ volume

Tactic:
integrableOn_empty

Premises used: MeasureTheory.integrableOn_empty
-- Module: Mathlib.NumberTheory.AbelSummation
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) ∅ volume

Tactic:
exact integrableOn_empty

Premises used: MeasureTheory.integrableOn_empty
-- Module: Mathlib.NumberTheory.AbelSummation
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 : ℕ
rw 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)
⊢ 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)

Tactic:
rw [← integral_of_le (Nat.cast_nonneg _)]

Premises used: Nat.cast_nonneg, intervalIntegral.integral_of_le