awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.NumberTheory.AbelSummation (hypothesis)
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
c : ℕ → 𝕜
a b : ℝ
m : ℕ
ha : 0 ≤ a
g : ℝ → 𝕜
hg_int : IntegrableOn (mα := MeasureSpace.toMeasurableSpace) g (Set.Icc a b) volume
hab : a ≤ b
hb : ⌊a⌋₊ = ⌊b⌋₊
this : ∀ᵐ (t : ℝ), t ∈ Set.Icc a b → Eq.{u_1 + 1} (α := 𝕜) (∑ k ∈ Icc m ⌊a⌋₊, c k) (∑ k ∈ Icc m ⌊t⌋₊, c k)
⊢ IntegrableOn.{0, u_1} (ε := 𝕜) (mα := MeasureSpace.toMeasurableSpace) (fun (t : ℝ) ↦ g t * ∑ k ∈ Icc m ⌊t⌋₊, c k)
    (Set.Icc a b) volume
have this₁ : ∀ᵐ (x : ℝ) ∂Measure.restrict volume (Set.Icc a b), Eq.{u_1 + 1} (α := 𝕜) (∑ k ∈ Icc m ⌊a⌋₊, c k) (∑ k ∈ Icc m ⌊x⌋₊, c k)
Tactic: rw [← ae_restrict_iff' measurableSet_Icc] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.NumberTheory.AbelSummation (goal)
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
c : ℕ → 𝕜
a b : ℝ
m : ℕ
ha : 0 ≤ a
g : ℝ → 𝕜
hg_int : IntegrableOn (mα := MeasureSpace.toMeasurableSpace) g (Set.Icc a b) volume
hab : a ≤ b
hb : ⌊a⌋₊ < ⌊b⌋₊
t₁ t₂ : ℝ
n : ℕ
h : t₁ ≤ t₂
h₁ : (↑n : ℝ) ≤ t₁
h₂ : t₂ ≤ HAdd.hAdd (α := ℝ) (↑n : ℝ) 1
h₃ : a ≤ t₁
h₄ : t₂ ≤ b
⊢ IntervalIntegrable.{u_1} (ε := 𝕜) (fun (t : ℝ) ↦ g t * ∑ k ∈ Icc m ⌊t⌋₊, c k) volume t₁ t₂
have rw : IntegrableOn.{0, u_1} (ε := 𝕜) (mα := Real.measurableSpace) (fun (t : ℝ) ↦ g t * ∑ k ∈ Icc m ⌊t⌋₊, c k) (Set.Icc t₁ t₂)
  volume
Tactic: rw [intervalIntegrable_iff_integrableOn_Icc_of_le h]
-- Lean 4 proof step from Mathlib.NumberTheory.AbelSummation (goal)
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
c : ℕ → 𝕜
a b : ℝ
m : ℕ
ha : 0 ≤ a
g : ℝ → 𝕜
hg_int : IntegrableOn (mα := MeasureSpace.toMeasurableSpace) g (Set.Icc a b) volume
hab : a ≤ b
hb : ⌊a⌋₊ < ⌊b⌋₊
t₁ t₂ : ℝ
n : ℕ
h_1 : t₁ ≤ t₂
h₁ : (↑n : ℝ) ≤ t₁
h₂ : t₂ ≤ HAdd.hAdd (α := ℝ) (↑n : ℝ) 1
h₃ : a ≤ t₁
h₄ : t₂ ≤ b
t : ℝ
h :
  t ∈ Set.Icc (↑n : ℝ) (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) →
    Eq.{u_1 + 1} (α := 𝕜) (∑ k ∈ Icc m ⌊t⌋₊, c k) (∑ k ∈ Icc m n, c k)
ht : t ∈ Set.Icc (↑n : ℝ) (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)
⊢ g t * ∑ k ∈ Icc m n, c k = g t * ∑ k ∈ Icc m ⌊t⌋₊, c k
have rw : g t * ∑ k ∈ Icc m n, c k = g t * ∑ k ∈ Icc m n, c k
Tactic: rw [h ht]
-- Lean 4 proof step from Mathlib.NumberTheory.AbelSummation (goal)
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
c : ℕ → 𝕜
a b : ℝ
m : ℕ
ha : 0 ≤ a
g : ℝ → 𝕜
hg_int : IntegrableOn (mα := MeasureSpace.toMeasurableSpace) g (Set.Icc a b) volume
hab : a ≤ b
hb : ⌊a⌋₊ < ⌊b⌋₊
t₁ t₂ : ℝ
n : ℕ
h : t₁ ≤ t₂
h₁ : (↑n : ℝ) ≤ t₁
h₂ : t₂ ≤ HAdd.hAdd (α := ℝ) (↑n : ℝ) 1
h₃ : a ≤ t₁
h₄ : t₂ ≤ b
⊢ ∀ᵐ (x : ℝ),
    x ∈ Set.Icc (↑n : ℝ) (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) →
      Eq.{u_1 + 1} (α := 𝕜) ((fun (x : ℝ) ↦ g x * ∑ k ∈ Icc m n, c k) x) ((fun (t : ℝ) ↦ g t * ∑ k ∈ Icc m ⌊t⌋₊, c k) x)
have h₅ : ∀ (a : ℝ),
  Membership.mem (γ := Set ℝ)
    {x : ℝ |
      Membership.mem (γ := Set ℝ)
          {x : ℝ |
            (fun (t : ℝ) ↦
                t ∈ Set.Icc (↑n : ℝ) (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) →
                  Eq.{u_1 + 1} (α := 𝕜) (∑ k ∈ Icc m ⌊t⌋₊, c k) (∑ k ∈ Icc m n, c k))
              x}
          x →
        Membership.mem (γ := Set ℝ)
          {x : ℝ |
            (fun (x : ℝ) ↦
                x ∈ Set.Icc (↑n : ℝ) (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) →
                  Eq.{u_1 + 1} (α := 𝕜) ((fun (x : ℝ) ↦ g x * ∑ k ∈ Icc m n, c k) x)
                    ((fun (t : ℝ) ↦ g t * ∑ k ∈ Icc m ⌊t⌋₊, c k) x))
              x}
          x}
    a
Tactic: filter_upwards [sumlocc c n] with t h ht using by rw [h ht]
-- Lean 4 proof step from Mathlib.NumberTheory.AbelSummation (goal)
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
c : ℕ → 𝕜
a b : ℝ
m : ℕ
ha : 0 ≤ a
g : ℝ → 𝕜
hg_int : IntegrableOn (mα := MeasureSpace.toMeasurableSpace) g (Set.Icc a b) volume
hab : a ≤ b
hb : ⌊a⌋₊ < ⌊b⌋₊
t₁ t₂ : ℝ
n : ℕ
h : t₁ ≤ t₂
h₁ : (↑n : ℝ) ≤ t₁
h₂ : t₂ ≤ HAdd.hAdd (α := ℝ) (↑n : ℝ) 1
h₃ : a ≤ t₁
h₄ : t₂ ≤ b
h₅ :
  ∀ (a : ℝ),
    Membership.mem (γ := Set ℝ)
      {x : ℝ |
        Membership.mem (γ := Set ℝ)
            {x : ℝ |
              (fun (t : ℝ) ↦
                  t ∈ Set.Icc (↑n : ℝ) (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) →
                    Eq.{u_1 + 1} (α := 𝕜) (∑ k ∈ Icc m ⌊t⌋₊, c k) (∑ k ∈ Icc m n, c k))
                x}
            x →
          Membership.mem (γ := Set ℝ)
            {x : ℝ |
              (fun (x : ℝ) ↦
                  x ∈ Set.Icc (↑n : ℝ) (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) →
                    Eq.{u_1 + 1} (α := 𝕜) ((fun (x : ℝ) ↦ g x * ∑ k ∈ Icc m n, c k) x)
                      ((fun (t : ℝ) ↦ g t * ∑ k ∈ Icc m ⌊t⌋₊, c k) x))
                x}
            x}
      a
⊢ ∀ᵐ (x : ℝ),
    x ∈ Set.Icc (↑n : ℝ) (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) →
      Eq.{u_1 + 1} (α := 𝕜) ((fun (x : ℝ) ↦ g x * ∑ k ∈ Icc m n, c k) x) ((fun (t : ℝ) ↦ g t * ∑ k ∈ Icc m ⌊t⌋₊, c k) x)
have h₆ : ∀ (a : ℝ),
  (a ∈ Set.Icc (↑n : ℝ) (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) →
      Eq.{u_1 + 1} (α := 𝕜) (∑ k ∈ Icc m ⌊a⌋₊, c k) (∑ k ∈ Icc m n, c k)) →
    a ∈ Set.Icc (↑n : ℝ) (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) → g a * ∑ k ∈ Icc m n, c k = g a * ∑ k ∈ Icc m ⌊a⌋₊, c k
Tactic: filter_upwards [sumlocc c n] with t h ht using by rw [h ht]
-- Lean 4 proof step from Mathlib.NumberTheory.AbelSummation (hypothesis)
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
c : ℕ → 𝕜
a b : ℝ
m : ℕ
ha : 0 ≤ a
g : ℝ → 𝕜
hg_int : IntegrableOn (mα := MeasureSpace.toMeasurableSpace) g (Set.Icc a b) volume
hab : a ≤ b
hb : ⌊a⌋₊ < ⌊b⌋₊
⊢ IntegrableOn.{0, u_1} (ε := 𝕜) (mα := MeasureSpace.toMeasurableSpace) (fun (t : ℝ) ↦ g t * ∑ k ∈ Icc m ⌊t⌋₊, c k)
    (Set.Icc a b) volume
have h_locint : ∀ {t₁ t₂ : ℝ} {n : ℕ} (h : t₁ ≤ t₂) (h₁ : (↑n : ℝ) ≤ t₁) (h₂ : t₂ ≤ HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) (h₃ : a ≤ t₁)
  (h₄ : t₂ ≤ b), IntervalIntegrable.{u_1} (ε := 𝕜) (fun (t : ℝ) ↦ g t * ∑ k ∈ Icc m ⌊t⌋₊, c k) volume t₁ t₂
Tactic: have h_locint {t₁ t₂ : ℝ} {n : ℕ} (h : t₁ ≤ t₂) (h₁ : n ≤ t₁) (h₂ : t₂ ≤ n + 1)
          (h₃ : a ≤ t₁) (h₄ : t₂ ≤ b) :
          IntervalIntegrable (fun t ↦ g t * ∑ k ∈ Icc m ⌊t⌋₊, c k) volume t₁ t₂ := by
        rw [intervalIntegrable_iff_integrableOn_Icc_of_le h]
        exact (IntegrableOn.mono_set (hg_int.mul_const _) (Set.Icc_subset_Icc h₃ h₄)).congr
          <| ae_restrict_of_ae_restrict_of_subset (Set.Icc_subset_Icc h₁ h₂)
            <| (ae_restrict_iff' measurableSet_Icc).mpr
              (by filter_upwards [sumlocc c n] with t h ht using by rw [h ht])
-- Lean 4 proof step from Mathlib.NumberTheory.AbelSummation (hypothesis)
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
c : ℕ → 𝕜
a b : ℝ
m : ℕ
ha : 0 ≤ a
g : ℝ → 𝕜
hg_int : IntegrableOn (mα := MeasureSpace.toMeasurableSpace) g (Set.Icc a b) volume
hab : a ≤ b
hb : ⌊a⌋₊ < ⌊b⌋₊
h_locint :
  ∀ {t₁ t₂ : ℝ} {n : ℕ} (h : t₁ ≤ t₂) (h₁ : (↑n : ℝ) ≤ t₁) (h₂ : t₂ ≤ HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) (h₃ : a ≤ t₁)
    (h₄ : t₂ ≤ b), IntervalIntegrable.{u_1} (ε := 𝕜) (fun (t : ℝ) ↦ g t * ∑ k ∈ Icc m ⌊t⌋₊, c k) volume t₁ t₂
⊢ IntegrableOn.{0, u_1} (ε := 𝕜) (mα := MeasureSpace.toMeasurableSpace) (fun (t : ℝ) ↦ g t * ∑ k ∈ Icc m ⌊t⌋₊, c k)
    (Set.Icc a b) volume
have aux1 : 0 ≤ b
Tactic: have aux1 : 0 ≤ b := (Nat.pos_of_floor_pos <| (Nat.zero_le _).trans_lt hb).le
-- Lean 4 proof step from Mathlib.NumberTheory.AbelSummation (goal)
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
c : ℕ → 𝕜
a b : ℝ
m : ℕ
ha : 0 ≤ a
g : ℝ → 𝕜
hg_int : IntegrableOn (mα := MeasureSpace.toMeasurableSpace) g (Set.Icc a b) volume
hab : a ≤ b
hb : ⌊a⌋₊ < ⌊b⌋₊
h_locint :
  ∀ {t₁ t₂ : ℝ} {n : ℕ} (h : t₁ ≤ t₂) (h₁ : (↑n : ℝ) ≤ t₁) (h₂ : t₂ ≤ HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) (h₃ : a ≤ t₁)
    (h₄ : t₂ ≤ b), IntervalIntegrable.{u_1} (ε := 𝕜) (fun (t : ℝ) ↦ g t * ∑ k ∈ Icc m ⌊t⌋₊, c k) volume t₁ t₂
aux1 : 0 ≤ b
⊢ HAdd.hAdd (α := ℝ) (↑⌊a⌋₊ : ℝ) 1 ≤ b
have rwa : (↑(⌊a⌋₊ + 1) : ℝ) ≤ b
Tactic: rwa [← Nat.cast_add_one, ← Nat.le_floor_iff aux1]
-- Lean 4 proof step from Mathlib.NumberTheory.AbelSummation (goal)
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
c : ℕ → 𝕜
a b : ℝ
m : ℕ
ha : 0 ≤ a
g : ℝ → 𝕜
hg_int : IntegrableOn (mα := MeasureSpace.toMeasurableSpace) g (Set.Icc a b) volume
hab : a ≤ b
hb : ⌊a⌋₊ < ⌊b⌋₊
h_locint :
  ∀ {t₁ t₂ : ℝ} {n : ℕ} (h : t₁ ≤ t₂) (h₁ : (↑n : ℝ) ≤ t₁) (h₂ : t₂ ≤ HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) (h₃ : a ≤ t₁)
    (h₄ : t₂ ≤ b), IntervalIntegrable.{u_1} (ε := 𝕜) (fun (t : ℝ) ↦ g t * ∑ k ∈ Icc m ⌊t⌋₊, c k) volume t₁ t₂
aux1 : 0 ≤ b
rwa : (↑(⌊a⌋₊ + 1) : ℝ) ≤ b
⊢ HAdd.hAdd (α := ℝ) (↑⌊a⌋₊ : ℝ) 1 ≤ b
have rwa₁ : ⌊a⌋₊ + 1 ≤ ⌊b⌋₊
Tactic: rwa [← Nat.cast_add_one, ← Nat.le_floor_iff aux1]
-- Lean 4 proof step from Mathlib.NumberTheory.AbelSummation (hypothesis)
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
c : ℕ → 𝕜
a b : ℝ
m : ℕ
ha : 0 ≤ a
g : ℝ → 𝕜
hg_int : IntegrableOn (mα := MeasureSpace.toMeasurableSpace) g (Set.Icc a b) volume
hab : a ≤ b
hb : ⌊a⌋₊ < ⌊b⌋₊
h_locint :
  ∀ {t₁ t₂ : ℝ} {n : ℕ} (h : t₁ ≤ t₂) (h₁ : (↑n : ℝ) ≤ t₁) (h₂ : t₂ ≤ HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) (h₃ : a ≤ t₁)
    (h₄ : t₂ ≤ b), IntervalIntegrable.{u_1} (ε := 𝕜) (fun (t : ℝ) ↦ g t * ∑ k ∈ Icc m ⌊t⌋₊, c k) volume t₁ t₂
aux1 : 0 ≤ b
⊢ IntegrableOn.{0, u_1} (ε := 𝕜) (mα := MeasureSpace.toMeasurableSpace) (fun (t : ℝ) ↦ g t * ∑ k ∈ Icc m ⌊t⌋₊, c k)
    (Set.Icc a b) volume
have aux2 : HAdd.hAdd (α := ℝ) (↑⌊a⌋₊ : ℝ) 1 ≤ b
Tactic: have aux2 : ⌊a⌋₊ + 1 ≤ b := by rwa [← Nat.cast_add_one, ← Nat.le_floor_iff aux1]
-- Lean 4 proof step from Mathlib.NumberTheory.AbelSummation (hypothesis)
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
c : ℕ → 𝕜
a b : ℝ
m : ℕ
ha : 0 ≤ a
g : ℝ → 𝕜
hg_int : IntegrableOn (mα := MeasureSpace.toMeasurableSpace) g (Set.Icc a b) volume
hab : a ≤ b
hb : ⌊a⌋₊ < ⌊b⌋₊
h_locint :
  ∀ {t₁ t₂ : ℝ} {n : ℕ} (h : t₁ ≤ t₂) (h₁ : (↑n : ℝ) ≤ t₁) (h₂ : t₂ ≤ HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) (h₃ : a ≤ t₁)
    (h₄ : t₂ ≤ b), IntervalIntegrable.{u_1} (ε := 𝕜) (fun (t : ℝ) ↦ g t * ∑ k ∈ Icc m ⌊t⌋₊, c k) volume t₁ t₂
aux1 : 0 ≤ b
aux2 : HAdd.hAdd (α := ℝ) (↑⌊a⌋₊ : ℝ) 1 ≤ b
⊢ IntegrableOn.{0, u_1} (ε := 𝕜) (mα := MeasureSpace.toMeasurableSpace) (fun (t : ℝ) ↦ g t * ∑ k ∈ Icc m ⌊t⌋₊, c k)
    (Set.Icc a b) volume
have aux3 : a ≤ HAdd.hAdd (α := ℝ) (↑⌊a⌋₊ : ℝ) 1
Tactic: have aux3 : a ≤ ⌊a⌋₊ + 1 := (Nat.lt_floor_add_one _).le
-- Lean 4 proof step from Mathlib.NumberTheory.AbelSummation (hypothesis)
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
c : ℕ → 𝕜
a b : ℝ
m : ℕ
ha : 0 ≤ a
g : ℝ → 𝕜
hg_int : IntegrableOn (mα := MeasureSpace.toMeasurableSpace) g (Set.Icc a b) volume
hab : a ≤ b
hb : ⌊a⌋₊ < ⌊b⌋₊
h_locint :
  ∀ {t₁ t₂ : ℝ} {n : ℕ} (h : t₁ ≤ t₂) (h₁ : (↑n : ℝ) ≤ t₁) (h₂ : t₂ ≤ HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) (h₃ : a ≤ t₁)
    (h₄ : t₂ ≤ b), IntervalIntegrable.{u_1} (ε := 𝕜) (fun (t : ℝ) ↦ g t * ∑ k ∈ Icc m ⌊t⌋₊, c k) volume t₁ t₂
aux1 : 0 ≤ b
aux2 : HAdd.hAdd (α := ℝ) (↑⌊a⌋₊ : ℝ) 1 ≤ b
aux3 : a ≤ HAdd.hAdd (α := ℝ) (↑⌊a⌋₊ : ℝ) 1
⊢ IntegrableOn.{0, u_1} (ε := 𝕜) (mα := MeasureSpace.toMeasurableSpace) (fun (t : ℝ) ↦ g t * ∑ k ∈ Icc m ⌊t⌋₊, c k)
    (Set.Icc a b) volume
have aux4 : a ≤ (↑⌊b⌋₊ : ℝ)
Tactic: have aux4 : a ≤ ⌊b⌋₊ := le_of_lt (by rwa [← Nat.floor_lt ha])
-- Lean 4 proof step from Mathlib.NumberTheory.AbelSummation (goal)
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
c : ℕ → 𝕜
a b : ℝ
m : ℕ
ha : 0 ≤ a
g : ℝ → 𝕜
hg_int : IntegrableOn (mα := MeasureSpace.toMeasurableSpace) g (Set.Icc a b) volume
hab : a ≤ b
hb : ⌊a⌋₊ < ⌊b⌋₊
h_locint :
  ∀ {t₁ t₂ : ℝ} {n : ℕ} (h : t₁ ≤ t₂) (h₁ : (↑n : ℝ) ≤ t₁) (h₂ : t₂ ≤ HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) (h₃ : a ≤ t₁)
    (h₄ : t₂ ≤ b), IntervalIntegrable.{u_1} (ε := 𝕜) (fun (t : ℝ) ↦ g t * ∑ k ∈ Icc m ⌊t⌋₊, c k) volume t₁ t₂
aux1 : 0 ≤ b
aux2 : HAdd.hAdd (α := ℝ) (↑⌊a⌋₊ : ℝ) 1 ≤ b
aux3 : a ≤ HAdd.hAdd (α := ℝ) (↑⌊a⌋₊ : ℝ) 1
aux4 : a ≤ (↑⌊b⌋₊ : ℝ)
⊢ IntegrableOn.{0, u_1} (ε := 𝕜) (mα := MeasureSpace.toMeasurableSpace) (fun (t : ℝ) ↦ g t * ∑ k ∈ Icc m ⌊t⌋₊, c k)
    (Set.Icc a b) volume
have inl : IntervalIntegrable.{u_1} (ε := 𝕜) (fun (t : ℝ) ↦ g t * ∑ k ∈ Icc m ⌊t⌋₊, c k) volume a b
Tactic: rw [← intervalIntegrable_iff_integrableOn_Icc_of_le (aux3.trans aux2)]
-- Lean 4 proof step from Mathlib.NumberTheory.AbelSummation (hypothesis)
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
c : ℕ → 𝕜
a b : ℝ
m : ℕ
ha : 0 ≤ a
g : ℝ → 𝕜
hg_int : IntegrableOn (mα := MeasureSpace.toMeasurableSpace) g (Set.Icc a b) volume
hab : a ≤ b
hb : ⌊a⌋₊ < ⌊b⌋₊
h_locint :
  ∀ {t₁ t₂ : ℝ} {n : ℕ} (h : t₁ ≤ t₂) (h₁ : (↑n : ℝ) ≤ t₁) (h₂ : t₂ ≤ HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) (h₃ : a ≤ t₁)
    (h₄ : t₂ ≤ b), IntervalIntegrable.{u_1} (ε := 𝕜) (fun (t : ℝ) ↦ g t * ∑ k ∈ Icc m ⌊t⌋₊, c k) volume t₁ t₂
aux1 : 0 ≤ b
aux2 : HAdd.hAdd (α := ℝ) (↑⌊a⌋₊ : ℝ) 1 ≤ b
aux3 : a ≤ HAdd.hAdd (α := ℝ) (↑⌊a⌋₊ : ℝ) 1
aux4 : a ≤ (↑⌊b⌋₊ : ℝ)
⊢ IntervalIntegrable.{u_1} (ε := 𝕜) (fun (t : ℝ) ↦ g t * ∑ k ∈ Icc m ⌊t⌋₊, c k) volume a b
have I1 : IntervalIntegrable.{u_1} (ε := 𝕜) (fun (t : ℝ) ↦ g t * ∑ k ∈ Icc m ⌊t⌋₊, c k) volume a (↑(⌊a⌋₊ + 1) : ℝ)
Tactic: have I1 : IntervalIntegrable _ volume a ↑(⌊a⌋₊ + 1) :=
        h_locint (mod_cast aux3) (Nat.floor_le ha) (mod_cast le_rfl) le_rfl (mod_cast aux2)
-- Lean 4 proof step from Mathlib.NumberTheory.AbelSummation (hypothesis)
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
c : ℕ → 𝕜
a b : ℝ
m : ℕ
ha : 0 ≤ a
g : ℝ → 𝕜
hg_int : IntegrableOn (mα := MeasureSpace.toMeasurableSpace) g (Set.Icc a b) volume
hab : a ≤ b
hb : ⌊a⌋₊ < ⌊b⌋₊
h_locint :
  ∀ {t₁ t₂ : ℝ} {n : ℕ} (h : t₁ ≤ t₂) (h₁ : (↑n : ℝ) ≤ t₁) (h₂ : t₂ ≤ HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) (h₃ : a ≤ t₁)
    (h₄ : t₂ ≤ b), IntervalIntegrable.{u_1} (ε := 𝕜) (fun (t : ℝ) ↦ g t * ∑ k ∈ Icc m ⌊t⌋₊, c k) volume t₁ t₂
aux1 : 0 ≤ b
aux2 : HAdd.hAdd (α := ℝ) (↑⌊a⌋₊ : ℝ) 1 ≤ b
aux3 : a ≤ HAdd.hAdd (α := ℝ) (↑⌊a⌋₊ : ℝ) 1
aux4 : a ≤ (↑⌊b⌋₊ : ℝ)
I1 : IntervalIntegrable.{u_1} (ε := 𝕜) (fun (t : ℝ) ↦ g t * ∑ k ∈ Icc m ⌊t⌋₊, c k) volume a (↑(⌊a⌋₊ + 1) : ℝ)
⊢ IntervalIntegrable.{u_1} (ε := 𝕜) (fun (t : ℝ) ↦ g t * ∑ k ∈ Icc m ⌊t⌋₊, c k) volume a b
have I2 : IntervalIntegrable.{u_1} (ε := 𝕜) (fun (t : ℝ) ↦ g t * ∑ k ∈ Icc m ⌊t⌋₊, c k) volume (↑(⌊a⌋₊ + 1) : ℝ) (↑⌊b⌋₊ : ℝ)
Tactic: have I2 : IntervalIntegrable _ volume ↑(⌊a⌋₊ + 1) ⌊b⌋₊ :=
        trans_iterate_Ico hb fun k hk ↦ h_locint (mod_cast k.le_succ)
          le_rfl (mod_cast le_rfl) (ineqofmemIco hk).1 (mod_cast (ineqofmemIco hk).2)
-- Lean 4 proof step from Mathlib.NumberTheory.AbelSummation (hypothesis)
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
c : ℕ → 𝕜
a b : ℝ
m : ℕ
ha : 0 ≤ a
g : ℝ → 𝕜
hg_int : IntegrableOn (mα := MeasureSpace.toMeasurableSpace) g (Set.Icc a b) volume
hab : a ≤ b
hb : ⌊a⌋₊ < ⌊b⌋₊
h_locint :
  ∀ {t₁ t₂ : ℝ} {n : ℕ} (h : t₁ ≤ t₂) (h₁ : (↑n : ℝ) ≤ t₁) (h₂ : t₂ ≤ HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) (h₃ : a ≤ t₁)
    (h₄ : t₂ ≤ b), IntervalIntegrable.{u_1} (ε := 𝕜) (fun (t : ℝ) ↦ g t * ∑ k ∈ Icc m ⌊t⌋₊, c k) volume t₁ t₂
aux1 : 0 ≤ b
aux2 : HAdd.hAdd (α := ℝ) (↑⌊a⌋₊ : ℝ) 1 ≤ b
aux3 : a ≤ HAdd.hAdd (α := ℝ) (↑⌊a⌋₊ : ℝ) 1
aux4 : a ≤ (↑⌊b⌋₊ : ℝ)
I1 : IntervalIntegrable.{u_1} (ε := 𝕜) (fun (t : ℝ) ↦ g t * ∑ k ∈ Icc m ⌊t⌋₊, c k) volume a (↑(⌊a⌋₊ + 1) : ℝ)
I2 : IntervalIntegrable.{u_1} (ε := 𝕜) (fun (t : ℝ) ↦ g t * ∑ k ∈ Icc m ⌊t⌋₊, c k) volume (↑(⌊a⌋₊ + 1) : ℝ) (↑⌊b⌋₊ : ℝ)
⊢ IntervalIntegrable.{u_1} (ε := 𝕜) (fun (t : ℝ) ↦ g t * ∑ k ∈ Icc m ⌊t⌋₊, c k) volume a b
have I3 : IntervalIntegrable.{u_1} (ε := 𝕜) (fun (t : ℝ) ↦ g t * ∑ k ∈ Icc m ⌊t⌋₊, c k) volume (↑⌊b⌋₊ : ℝ) b
Tactic: have I3 : IntervalIntegrable _ volume ⌊b⌋₊ b :=
        h_locint (Nat.floor_le aux1) le_rfl (Nat.lt_floor_add_one _).le aux4 le_rfl
-- Lean 4 proof step from Mathlib.NumberTheory.AbelSummation (goal)
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
c : ℕ → 𝕜
a b : ℝ
m : ℕ
ha : 0 ≤ a
g : ℝ → 𝕜
hg_int : IntegrableOn (mα := MeasureSpace.toMeasurableSpace) g (Set.Icc a b) volume
hab : b < a
⊢ IntegrableOn.{0, u_1} (ε := 𝕜) (mα := MeasureSpace.toMeasurableSpace) (fun (t : ℝ) ↦ g t * ∑ k ∈ Icc m ⌊t⌋₊, c k)
    (Set.Icc a b) volume
have inr : IntegrableOn.{0, u_1} (ε := 𝕜) (mα := MeasureSpace.toMeasurableSpace) (fun (t : ℝ) ↦ g t * ∑ k ∈ Icc m ⌊t⌋₊, c k) ∅
  volume
Tactic: rw [Set.Icc_eq_empty_of_lt hab]
-- 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
⊢ ∑ k ∈ Ioc ⌊a⌋₊ ⌊b⌋₊, f (↑k : ℝ) * c k =
    f b * ∑ k ∈ Icc 0 ⌊b⌋₊, c k - f a * ∑ k ∈ Icc 0 ⌊a⌋₊, c k -
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Set.Ioc a b)) fun (t : ℝ) ↦
        deriv f t * ∑ k ∈ Icc 0 ⌊t⌋₊, c k
have rw : ∑ k ∈ Ioc ⌊a⌋₊ ⌊b⌋₊, f (↑k : ℝ) * c k =
  f b * ∑ k ∈ Icc 0 ⌊b⌋₊, c k - f a * ∑ k ∈ Icc 0 ⌊a⌋₊, c k - ∫ (x : ℝ) in a..b, deriv f x * ∑ k ∈ Icc 0 ⌊x⌋₊, c k
Tactic: rw [← integral_of_le hab]
-- Lean 4 proof step from Mathlib.NumberTheory.AbelSummation (hypothesis)
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
⊢ ∑ k ∈ Ioc ⌊a⌋₊ ⌊b⌋₊, f (↑k : ℝ) * c k =
    f b * ∑ k ∈ Icc 0 ⌊b⌋₊, c k - f a * ∑ k ∈ Icc 0 ⌊a⌋₊, c k - ∫ (x : ℝ) in a..b, deriv f x * ∑ k ∈ Icc 0 ⌊x⌋₊, c k
have aux1 : (↑⌊a⌋₊ : ℝ) ≤ a
Tactic: have aux1 : ⌊a⌋₊ ≤ a := Nat.floor_le ha
-- Lean 4 proof step from Mathlib.NumberTheory.AbelSummation (hypothesis)
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
⊢ ∑ k ∈ Ioc ⌊a⌋₊ ⌊b⌋₊, f (↑k : ℝ) * c k =
    f b * ∑ k ∈ Icc 0 ⌊b⌋₊, c k - f a * ∑ k ∈ Icc 0 ⌊a⌋₊, c k - ∫ (x : ℝ) in a..b, deriv f x * ∑ k ∈ Icc 0 ⌊x⌋₊, c k
have aux2 : b ≤ HAdd.hAdd (α := ℝ) (↑⌊b⌋₊ : ℝ) 1
Tactic: have aux2 : b ≤ ⌊b⌋₊ + 1 := (Nat.lt_floor_add_one _).le
-- 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
⊢ ∑ k ∈ Ioc ⌊a⌋₊ ⌊b⌋₊, f (↑k : ℝ) * c k =
    f b * ∑ k ∈ Icc 0 ⌊b⌋₊, c k - f a * ∑ k ∈ Icc 0 ⌊a⌋₊, c k - ∫ (x : ℝ) in a..b, deriv f x * ∑ k ∈ Icc 0 ⌊x⌋₊, c k
have inl : ∀ (hb : ⌊a⌋₊ = ⌊b⌋₊),
  ∑ k ∈ Ioc ⌊a⌋₊ ⌊b⌋₊, f (↑k : ℝ) * c k =
    f b * ∑ k ∈ Icc 0 ⌊b⌋₊, c k - f a * ∑ k ∈ Icc 0 ⌊a⌋₊, c k - ∫ (x : ℝ) in a..b, deriv f x * ∑ k ∈ Icc 0 ⌊x⌋₊, c k
Tactic: obtain hb | hb := eq_or_lt_of_le (Nat.floor_le_floor hab)
-- 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
inl :
  ∀ (hb : ⌊a⌋₊ = ⌊b⌋₊),
    ∑ k ∈ Ioc ⌊a⌋₊ ⌊b⌋₊, f (↑k : ℝ) * c k =
      f b * ∑ k ∈ Icc 0 ⌊b⌋₊, c k - f a * ∑ k ∈ Icc 0 ⌊a⌋₊, c k - ∫ (x : ℝ) in a..b, deriv f x * ∑ k ∈ Icc 0 ⌊x⌋₊, c k
⊢ ∑ k ∈ Ioc ⌊a⌋₊ ⌊b⌋₊, f (↑k : ℝ) * c k =
    f b * ∑ k ∈ Icc 0 ⌊b⌋₊, c k - f a * ∑ k ∈ Icc 0 ⌊a⌋₊, c k - ∫ (x : ℝ) in a..b, deriv f x * ∑ k ∈ Icc 0 ⌊x⌋₊, c k
have inr : ∀ (hb : ⌊a⌋₊ < ⌊b⌋₊),
  ∑ k ∈ Ioc ⌊a⌋₊ ⌊b⌋₊, f (↑k : ℝ) * c k =
    f b * ∑ k ∈ Icc 0 ⌊b⌋₊, c k - f a * ∑ k ∈ Icc 0 ⌊a⌋₊, c k - ∫ (x : ℝ) in a..b, deriv f x * ∑ k ∈ Icc 0 ⌊x⌋₊, c k
Tactic: obtain hb | hb := eq_or_lt_of_le (Nat.floor_le_floor hab)
-- 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⌋₊
⊢ ∑ k ∈ Ioc ⌊a⌋₊ ⌊b⌋₊, f (↑k : ℝ) * c k =
    f b * ∑ k ∈ Icc 0 ⌊b⌋₊, c k - f a * ∑ k ∈ Icc 0 ⌊a⌋₊, c k - ∫ (x : ℝ) in a..b, deriv f x * ∑ k ∈ Icc 0 ⌊x⌋₊, c k
have inl : ∑ k ∈ Ioc ⌊b⌋₊ ⌊b⌋₊, f (↑k : ℝ) * c k =
  f b * ∑ k ∈ Icc 0 ⌊b⌋₊, c k - f a * ∑ k ∈ Icc 0 ⌊b⌋₊, c k - ∫ (x : ℝ) in a..b, deriv f x * ∑ k ∈ Icc 0 ⌊x⌋₊, c k
Tactic: rw [hb, Ioc_eq_empty_of_le le_rfl, sum_empty, ← sub_mul,
      integralmulsum c hf_diff hf_int _ _ ⌊b⌋₊ hab (hb ▸ aux1) aux2 le_rfl le_rfl, sub_self]
-- 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⌋₊
inl :
  ∑ k ∈ Ioc ⌊b⌋₊ ⌊b⌋₊, f (↑k : ℝ) * c k =
    f b * ∑ k ∈ Icc 0 ⌊b⌋₊, c k - f a * ∑ k ∈ Icc 0 ⌊b⌋₊, c k - ∫ (x : ℝ) in a..b, deriv f x * ∑ k ∈ Icc 0 ⌊x⌋₊, c k
⊢ ∑ k ∈ Ioc ⌊a⌋₊ ⌊b⌋₊, f (↑k : ℝ) * c k =
    f b * ∑ k ∈ Icc 0 ⌊b⌋₊, c k - f a * ∑ k ∈ Icc 0 ⌊a⌋₊, c k - ∫ (x : ℝ) in a..b, deriv f x * ∑ k ∈ Icc 0 ⌊x⌋₊, c k
have inl₁ : ∑ k ∈ ∅, f (↑k : ℝ) * c k =
  f b * ∑ k ∈ Icc 0 ⌊b⌋₊, c k - f a * ∑ k ∈ Icc 0 ⌊b⌋₊, c k - ∫ (x : ℝ) in a..b, deriv f x * ∑ k ∈ Icc 0 ⌊x⌋₊, c k
Tactic: rw [hb, Ioc_eq_empty_of_le le_rfl, sum_empty, ← sub_mul,
      integralmulsum c hf_diff hf_int _ _ ⌊b⌋₊ hab (hb ▸ aux1) aux2 le_rfl le_rfl, sub_self]
-- 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⌋₊
inl :
  ∑ k ∈ Ioc ⌊b⌋₊ ⌊b⌋₊, f (↑k : ℝ) * c k =
    f b * ∑ k ∈ Icc 0 ⌊b⌋₊, c k - f a * ∑ k ∈ Icc 0 ⌊b⌋₊, c k - ∫ (x : ℝ) in a..b, deriv f x * ∑ k ∈ Icc 0 ⌊x⌋₊, c k
inl₁ :
  ∑ k ∈ ∅, f (↑k : ℝ) * c k =
    f b * ∑ k ∈ Icc 0 ⌊b⌋₊, c k - f a * ∑ k ∈ Icc 0 ⌊b⌋₊, c k - ∫ (x : ℝ) in a..b, deriv f x * ∑ k ∈ Icc 0 ⌊x⌋₊, c k
⊢ ∑ k ∈ Ioc ⌊a⌋₊ ⌊b⌋₊, f (↑k : ℝ) * c k =
    f b * ∑ k ∈ Icc 0 ⌊b⌋₊, c k - f a * ∑ k ∈ Icc 0 ⌊a⌋₊, c k - ∫ (x : ℝ) in a..b, deriv f x * ∑ k ∈ Icc 0 ⌊x⌋₊, c k
have inl₂ : 0 = f b * ∑ k ∈ Icc 0 ⌊b⌋₊, c k - f a * ∑ k ∈ Icc 0 ⌊b⌋₊, c k - ∫ (x : ℝ) in a..b, deriv f x * ∑ k ∈ Icc 0 ⌊x⌋₊, c k
Tactic: rw [hb, Ioc_eq_empty_of_le le_rfl, sum_empty, ← sub_mul,
      integralmulsum c hf_diff hf_int _ _ ⌊b⌋₊ hab (hb ▸ aux1) aux2 le_rfl le_rfl, sub_self]
-- 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⌋₊
inl :
  ∑ k ∈ Ioc ⌊b⌋₊ ⌊b⌋₊, f (↑k : ℝ) * c k =
    f b * ∑ k ∈ Icc 0 ⌊b⌋₊, c k - f a * ∑ k ∈ Icc 0 ⌊b⌋₊, c k - ∫ (x : ℝ) in a..b, deriv f x * ∑ k ∈ Icc 0 ⌊x⌋₊, c k
inl₁ :
  ∑ k ∈ ∅, f (↑k : ℝ) * c k =
    f b * ∑ k ∈ Icc 0 ⌊b⌋₊, c k - f a * ∑ k ∈ Icc 0 ⌊b⌋₊, c k - ∫ (x : ℝ) in a..b, deriv f x * ∑ k ∈ Icc 0 ⌊x⌋₊, c k
inl₂ :
  0 = f b * ∑ k ∈ Icc 0 ⌊b⌋₊, c k - f a * ∑ k ∈ Icc 0 ⌊b⌋₊, c k - ∫ (x : ℝ) in a..b, deriv f x * ∑ k ∈ Icc 0 ⌊x⌋₊, c k
⊢ ∑ k ∈ Ioc ⌊a⌋₊ ⌊b⌋₊, f (↑k : ℝ) * c k =
    f b * ∑ k ∈ Icc 0 ⌊b⌋₊, c k - f a * ∑ k ∈ Icc 0 ⌊a⌋₊, c k - ∫ (x : ℝ) in a..b, deriv f x * ∑ k ∈ Icc 0 ⌊x⌋₊, c k
have inl₃ : 0 = (f b - f a) * ∑ k ∈ Icc 0 ⌊b⌋₊, c k - ∫ (x : ℝ) in a..b, deriv f x * ∑ k ∈ Icc 0 ⌊x⌋₊, c k
Tactic: rw [hb, Ioc_eq_empty_of_le le_rfl, sum_empty, ← sub_mul,
      integralmulsum c hf_diff hf_int _ _ ⌊b⌋₊ hab (hb ▸ aux1) aux2 le_rfl le_rfl, sub_self]