awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.AbelSummation
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
c : ℕ → 𝕜
f : ℝ → 𝕜
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
t₁ t₂ : ℝ
n : ℕ
h : t₁ ≤ t₂
h₁ : (↑n : ℝ) ≤ t₁
h₂ : t₂ ≤ HAdd.hAdd (α := ℝ) (↑n : ℝ) 1
h₃ : a ≤ t₁
h₄ : t₂ ≤ b
h_inc₁ : Ι t₁ t₂ ⊆ Set.Icc (↑n : ℝ) (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)
h_inc₂ : [[t₁, t₂]] ⊆ Set.Icc a b
⊢ IntervalIntegrable (deriv f) volume t₁ t₂

Tactic:
(intervalIntegrable_iff_integrableOn_Icc_of_le h).mpr (hf_int.mono_set ?_)

Premises used: Iff.mpr, intervalIntegrable_iff_integrableOn_Icc_of_le, MeasureTheory.IntegrableOn.mono_set
-- Module: Mathlib.NumberTheory.AbelSummation
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
c : ℕ → 𝕜
f : ℝ → 𝕜
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
t₁ t₂ : ℝ
n : ℕ
h : t₁ ≤ t₂
h₁ : (↑n : ℝ) ≤ t₁
h₂ : t₂ ≤ HAdd.hAdd (α := ℝ) (↑n : ℝ) 1
h₃ : a ≤ t₁
h₄ : t₂ ≤ b
h_inc₁ : Ι t₁ t₂ ⊆ Set.Icc (↑n : ℝ) (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)
h_inc₂ : [[t₁, t₂]] ⊆ Set.Icc a b
refine : Set.Icc t₁ t₂ ⊆ Set.Icc a b
⊢ IntervalIntegrable (deriv f) volume t₁ t₂

Tactic:
refine (intervalIntegrable_iff_integrableOn_Icc_of_le h).mpr (hf_int.mono_set ?_)

Premises used: Iff.mpr, intervalIntegrable_iff_integrableOn_Icc_of_le, MeasureTheory.IntegrableOn.mono_set
-- Module: Mathlib.NumberTheory.AbelSummation
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
c : ℕ → 𝕜
f : ℝ → 𝕜
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
t₁ t₂ : ℝ
n : ℕ
h : t₁ ≤ t₂
h₁ : (↑n : ℝ) ≤ t₁
h₂ : t₂ ≤ HAdd.hAdd (α := ℝ) (↑n : ℝ) 1
h₃ : a ≤ t₁
h₄ : t₂ ≤ b
h_inc₁ : Ι t₁ t₂ ⊆ Set.Icc (↑n : ℝ) (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)
h_inc₂ rwa rwa₁ rwa₂ rwa₃ : [[t₁, t₂]] ⊆ Set.Icc a b
⊢ Set.Icc t₁ t₂ ⊆ Set.Icc a b

Tactic:
rwa [← Set.uIcc_of_le h]

Premises used: Set.uIcc_of_le
-- Module: Mathlib.NumberTheory.AbelSummation
Goal:
a b : ℝ
k : ℕ
hk : k ∈ Set.Ico (⌊a⌋₊ + 1) ⌊b⌋₊
left : a ≤ (↑k : ℝ)
right : HAdd.hAdd (α := ℝ) (↑k : ℝ) 1 ≤ b
⊢ a ≤ (↑k : ℝ) ∧ HAdd.hAdd (α := ℝ) (↑k : ℝ) 1 ≤ b

Tactic:
constructor
-- Module: Mathlib.NumberTheory.AbelSummation
Goal:
a b : ℝ
k : ℕ
hk : k ∈ Set.Ico (⌊a⌋₊ + 1) ⌊b⌋₊
⊢ ⌊a⌋₊ + 1 ≤ k

Tactic:
have := (Set.mem_Ico.mp hk).1
-- Module: Mathlib.NumberTheory.AbelSummation
Goal:
a b : ℝ
k : ℕ
hk : k ∈ Set.Ico (⌊a⌋₊ + 1) ⌊b⌋₊
this : ⌊a⌋₊ + 1 ≤ k
⊢ k ≠ 0

Tactic:
lia
-- Module: Mathlib.NumberTheory.AbelSummation
Goal:
a b : ℝ
k : ℕ
hk : k ∈ Set.Ico (⌊a⌋₊ + 1) ⌊b⌋₊
this : ⌊a⌋₊ + 1 ≤ k
⊢ a ≤ (↑k : ℝ)

Tactic:
exact le_of_lt <| (Nat.floor_lt' (by lia)).mp this

Premises used: le_of_lt, Nat.floor_lt', Iff.mp
-- Module: Mathlib.NumberTheory.AbelSummation
Goal:
a b : ℝ
k : ℕ
hk : k ∈ Set.Ico (⌊a⌋₊ + 1) ⌊b⌋₊
right : k.succ ≤ ⌊b⌋₊
⊢ HAdd.hAdd (α := ℝ) (↑k : ℝ) 1 ≤ b

Tactic:
rw [← Nat.cast_add_one, ← Nat.le_floor_iff' (Nat.succ_ne_zero k)]

Premises used: Nat.le_floor_iff', Nat.succ_ne_zero, Nat.cast_add_one
-- Module: Mathlib.NumberTheory.AbelSummation
Goal:
a b : ℝ
k : ℕ
hk : k ∈ Set.Ico (⌊a⌋₊ + 1) ⌊b⌋₊
⊢ k.succ ≤ ⌊b⌋₊

Tactic:
(Set.mem_Ico.mp hk).2

Premises used: Set.mem_Ico, And.right, Iff.mp, Nat.lt
-- Module: Mathlib.NumberTheory.AbelSummation
Goal:
a b : ℝ
k : ℕ
hk : k ∈ Set.Ico (⌊a⌋₊ + 1) ⌊b⌋₊
⊢ k.succ ≤ ⌊b⌋₊

Tactic:
exact (Set.mem_Ico.mp hk).2

Premises used: Set.mem_Ico, And.right, Iff.mp
-- Module: Mathlib.NumberTheory.AbelSummation
Goal:
a b : ℝ
k : ℕ
hk : k ∈ Ico (⌊a⌋₊ + 1) ⌊b⌋₊
rwa rwa₁ rwa₂ rwa₃ : k ∈ (↑(Ico (⌊a⌋₊ + 1) ⌊b⌋₊) : Set ℕ)
⊢ k ∈ Set.Ico (⌊a⌋₊ + 1) ⌊b⌋₊

Tactic:
rwa [← Finset.coe_Ico]

Premises used: Finset.coe_Ico
-- Module: Mathlib.NumberTheory.AbelSummation
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
inl :
  ∀ (hab : a ≤ b),
    IntegrableOn.{0, u_1} (ε := 𝕜) (mα := MeasureSpace.toMeasurableSpace) (fun (t : ℝ) ↦ g t * ∑ k ∈ Icc m ⌊t⌋₊, c k)
      (Set.Icc a b) volume
inr :
  ∀ (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
⊢ IntegrableOn.{0, u_1} (ε := 𝕜) (mα := MeasureSpace.toMeasurableSpace) (fun (t : ℝ) ↦ g t * ∑ k ∈ Icc m ⌊t⌋₊, c k)
    (Set.Icc a b) volume

Tactic:
obtain hab | hab := le_or_gt a b

Premises used: le_or_gt
-- Module: Mathlib.NumberTheory.AbelSummation
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
inl :
  ∀ (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
inl₁ :
  ∀ (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
⊢ IntegrableOn.{0, u_1} (ε := 𝕜) (mα := MeasureSpace.toMeasurableSpace) (fun (t : ℝ) ↦ g t * ∑ k ∈ Icc m ⌊t⌋₊, c k)
    (Set.Icc a b) volume

Tactic:
obtain hb | hb := eq_or_lt_of_le (Nat.floor_le_floor hab)

Premises used: Nat.floor_le_floor, eq_or_lt_of_le
-- Module: Mathlib.NumberTheory.AbelSummation
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 :
  ∀ (t : ℝ)
    (ht₁ :
      t ∈ Set.Icc (↑⌊a⌋₊ : ℝ) (HAdd.hAdd (α := ℝ) (↑⌊a⌋₊ : ℝ) 1) →
        Eq.{u_1 + 1} (α := 𝕜) (∑ k ∈ Icc m ⌊t⌋₊, c k) (∑ k ∈ Icc m ⌊a⌋₊, c k))
    (ht₂ : t ∈ Set.Icc a b), Eq.{u_1 + 1} (α := 𝕜) (∑ k ∈ Icc m ⌊a⌋₊, c k) (∑ k ∈ Icc m ⌊t⌋₊, c k)
⊢ ∀ᵐ (t : ℝ), t ∈ Set.Icc a b → Eq.{u_1 + 1} (α := 𝕜) (∑ k ∈ Icc m ⌊a⌋₊, c k) (∑ k ∈ Icc m ⌊t⌋₊, c k)

Tactic:
filter_upwards [sumlocc c ⌊a⌋₊] with t ht₁ ht₂

Premises used: Nat.floor, _private.0.abelSummationProof.sumlocc
-- Module: Mathlib.NumberTheory.AbelSummation
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 : ℝ
ht₁ :
  t ∈ Set.Icc (↑⌊a⌋₊ : ℝ) (HAdd.hAdd (α := ℝ) (↑⌊a⌋₊ : ℝ) 1) →
    Eq.{u_1 + 1} (α := 𝕜) (∑ k ∈ Icc m ⌊t⌋₊, c k) (∑ k ∈ Icc m ⌊a⌋₊, c k)
ht₂ : t ∈ Set.Icc a b
h h₁ : Eq.{u_1 + 1} (α := 𝕜) (∑ k ∈ Icc m ⌊a⌋₊, c k) (∑ k ∈ Icc m ⌊a⌋₊, c k)
⊢ Eq.{u_1 + 1} (α := 𝕜) (∑ k ∈ Icc m ⌊a⌋₊, c k) (∑ k ∈ Icc m ⌊t⌋₊, c k)

Tactic:
rw [ht₁ ⟨(Nat.floor_le ha).trans ht₂.1, hb ▸ ht₂.2.trans (Nat.lt_floor_add_one b).le⟩]

Premises used: Eq.rec, LT.lt.le, And.right, And.left, And.intro, Nat.floor_le, LE.le.trans, Eq.symm, Nat.lt_floor_add_one
-- Module: Mathlib.NumberTheory.AbelSummation
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 ∈ Set.Icc a b → Eq.{u_1 + 1} (α := 𝕜) (∑ k ∈ Icc m ⌊a⌋₊, c k) (∑ k ∈ Icc m ⌊t⌋₊, c k)

Tactic:
have : ∀ᵐ t, t ∈ Set.Icc a b → ∑ k ∈ Icc m ⌊a⌋₊, c k = ∑ k ∈ Icc m ⌊t⌋₊, c k := by
        filter_upwards [sumlocc c ⌊a⌋₊] with t ht₁ ht₂
        rw [ht₁ ⟨(Nat.floor_le ha).trans ht₂.1, hb ▸ ht₂.2.trans (Nat.lt_floor_add_one b).le⟩]
-- Module: Mathlib.NumberTheory.AbelSummation
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)
⊢ ∀ᵐ (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

Premises used: measurableSet_Icc, MeasureTheory.ae_restrict_iff'
-- Module: Mathlib.NumberTheory.AbelSummation
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 :
  ∀ᵐ (x : ℝ) ∂Measure.restrict volume (Set.Icc a b),
    Eq.{u_1 + 1} (α := 𝕜) (∑ k ∈ Icc m ⌊a⌋₊, c k) (∑ k ∈ Icc m ⌊x⌋₊, c k)
⊢ IntegrableOn.{0, u_1} (ε := 𝕜) (mα := MeasureSpace.toMeasurableSpace) (fun (t : ℝ) ↦ g t * ∑ k ∈ Icc m ⌊t⌋₊, c k)
    (Set.Icc a b) volume

Tactic:
IntegrableOn.congr_fun_ae
        (hg_int.mul_const _) ((Filter.EventuallyEq.refl _ g).mul this)

Premises used: Filter.EventuallyEq.mul, MeasureTheory.IntegrableOn.congr_fun_ae, Filter.EventuallyEq.refl, MeasureTheory.Integrable.mul_const
-- Module: Mathlib.NumberTheory.AbelSummation
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 :
  ∀ᵐ (x : ℝ) ∂Measure.restrict volume (Set.Icc a b),
    Eq.{u_1 + 1} (α := 𝕜) (∑ k ∈ Icc m ⌊a⌋₊, c k) (∑ k ∈ Icc m ⌊x⌋₊, c k)
⊢ IntegrableOn.{0, u_1} (ε := 𝕜) (mα := MeasureSpace.toMeasurableSpace) (fun (t : ℝ) ↦ g t * ∑ k ∈ Icc m ⌊t⌋₊, c k)
    (Set.Icc a b) volume

Tactic:
exact IntegrableOn.congr_fun_ae
        (hg_int.mul_const _) ((Filter.EventuallyEq.refl _ g).mul this)

Premises used: Filter.EventuallyEq.mul, MeasureTheory.IntegrableOn.congr_fun_ae, Filter.EventuallyEq.refl, MeasureTheory.Integrable.mul_const
-- Module: Mathlib.NumberTheory.AbelSummation
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
rw :
  IntegrableOn.{0, u_1} (ε := 𝕜) (mα := Real.measurableSpace) (fun (t : ℝ) ↦ g t * ∑ k ∈ Icc m ⌊t⌋₊, c k)
    (Set.Icc t₁ t₂) volume
⊢ IntervalIntegrable.{u_1} (ε := 𝕜) (fun (t : ℝ) ↦ g t * ∑ k ∈ Icc m ⌊t⌋₊, c k) volume t₁ t₂

Tactic:
rw [intervalIntegrable_iff_integrableOn_Icc_of_le h]

Premises used: intervalIntegrable_iff_integrableOn_Icc_of_le
-- Module: Mathlib.NumberTheory.AbelSummation
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)
rw rw₁ : g t * ∑ k ∈ Icc m n, c k = g t * ∑ k ∈ Icc m n, c k
⊢ g t * ∑ k ∈ Icc m n, c k = g t * ∑ k ∈ Icc m ⌊t⌋₊, c k

Tactic:
rw [h ht]
-- Module: Mathlib.NumberTheory.AbelSummation
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
h₆ h₇ :
  ∀ (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
⊢ ∀ᵐ (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)

Tactic:
filter_upwards [sumlocc c n] with t h ht using by rw [h ht]

Premises used: _private.0.abelSummationProof.sumlocc
-- Module: Mathlib.NumberTheory.AbelSummation
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
⊢ IntegrableOn.{0, u_1} (ε := 𝕜) (mα := Real.measurableSpace) (fun (t : ℝ) ↦ g t * ∑ k ∈ Icc m ⌊t⌋₊, c k)
    (Set.Icc t₁ t₂) volume

Tactic:
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])

Premises used: Iff.mpr, MeasureTheory.ae_restrict_of_ae_restrict_of_subset, MeasureTheory.IntegrableOn.mono_set, MeasureTheory.Integrable.congr, Set.Icc_subset_Icc, measurableSet_Icc, MeasureTheory.Integrable.mul_const, MeasureTheory.ae_restrict_iff'
-- Module: Mathlib.NumberTheory.AbelSummation
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₂

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])
-- Module: Mathlib.NumberTheory.AbelSummation
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₂
⊢ 0 ≤ b

Tactic:
have aux1 : 0 ≤ b := (Nat.pos_of_floor_pos <| (Nat.zero_le _).trans_lt hb).le
-- Module: Mathlib.NumberTheory.AbelSummation
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
rwa₁ rwa₂ rwa₃ rwa₄ : ⌊a⌋₊ + 1 ≤ ⌊b⌋₊
⊢ HAdd.hAdd (α := ℝ) (↑⌊a⌋₊ : ℝ) 1 ≤ b

Tactic:
rwa [← Nat.cast_add_one, ← Nat.le_floor_iff aux1]

Premises used: Nat.le_floor_iff, Nat.cast_add_one
-- Module: Mathlib.NumberTheory.AbelSummation
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

Tactic:
have aux2 : ⌊a⌋₊ + 1 ≤ b := by rwa [← Nat.cast_add_one, ← Nat.le_floor_iff aux1]
-- Module: Mathlib.NumberTheory.AbelSummation
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
⊢ a ≤ HAdd.hAdd (α := ℝ) (↑⌊a⌋₊ : ℝ) 1

Tactic:
have aux3 : a ≤ ⌊a⌋₊ + 1 := (Nat.lt_floor_add_one _).le
-- Module: Mathlib.NumberTheory.AbelSummation
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
rwa rwa₁ rwa₂ rwa₃ : ⌊a⌋₊ < ⌊b⌋₊
⊢ a < (↑⌊b⌋₊ : ℝ)

Tactic:
rwa [← Nat.floor_lt ha]

Premises used: Nat.floor_lt
-- Module: Mathlib.NumberTheory.AbelSummation
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
⊢ a ≤ (↑⌊b⌋₊ : ℝ)

Tactic:
have aux4 : a ≤ ⌊b⌋₊ := le_of_lt (by rwa [← Nat.floor_lt ha])
-- Module: Mathlib.NumberTheory.AbelSummation
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⌋₊ : ℝ)
inl : IntervalIntegrable.{u_1} (ε := 𝕜) (fun (t : ℝ) ↦ g t * ∑ k ∈ Icc m ⌊t⌋₊, c k) volume a b
⊢ IntegrableOn.{0, u_1} (ε := 𝕜) (mα := MeasureSpace.toMeasurableSpace) (fun (t : ℝ) ↦ g t * ∑ k ∈ Icc m ⌊t⌋₊, c k)
    (Set.Icc a b) volume

Tactic:
rw [← intervalIntegrable_iff_integrableOn_Icc_of_le (aux3.trans aux2)]

Premises used: intervalIntegrable_iff_integrableOn_Icc_of_le, LE.le.trans
-- Module: Mathlib.NumberTheory.AbelSummation
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 (↑(⌊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)
-- Module: Mathlib.NumberTheory.AbelSummation
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⌋₊ + 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)
-- Module: Mathlib.NumberTheory.AbelSummation
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 (↑⌊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
-- Module: Mathlib.NumberTheory.AbelSummation
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⌋₊ : ℝ)
I3 : IntervalIntegrable.{u_1} (ε := 𝕜) (fun (t : ℝ) ↦ g t * ∑ k ∈ Icc m ⌊t⌋₊, c k) volume (↑⌊b⌋₊ : ℝ) b
⊢ IntervalIntegrable.{u_1} (ε := 𝕜) (fun (t : ℝ) ↦ g t * ∑ k ∈ Icc m ⌊t⌋₊, c k) volume a b

Tactic:
(I1.trans I2).trans I3

Premises used: IntervalIntegrable.trans