-- Mathlib/NumberTheory/AbelSummation.lean
theorem _root_.integrableOn_mul_sum_Icc {m : ℕ} (ha : 0 ≤ a) {g : ℝ → 𝕜}
    (hg_int : IntegrableOn g (Set.Icc a b)) :
    IntegrableOn (fun t ↦ g t * ∑ k ∈ Icc m ⌊t⌋₊, c k) (Set.Icc a b)

Proof state:
case inl
𝕜 : Type u_1
inst✝ : RCLike 𝕜
c : ℕ → 𝕜
a b : ℝ
m : ℕ
ha : 0 ≤ a
g : ℝ → 𝕜
hg_int : IntegrableOn g (Set.Icc a b) volume
hab : a ≤ b
⊢ IntegrableOn (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)

Result:
case inl.inl
𝕜 : Type u_1
inst✝ : RCLike 𝕜
c : ℕ → 𝕜
a b : ℝ
m : ℕ
ha : 0 ≤ a
g : ℝ → 𝕜
hg_int : IntegrableOn g (Set.Icc a b) volume
hab : a ≤ b
hb : ⌊a⌋₊ = ⌊b⌋₊
⊢ IntegrableOn (fun t => g t * ∑ k ∈ Icc m ⌊t⌋₊, c k) (Set.Icc a b) volume

case inl.inr
𝕜 : Type u_1
inst✝ : RCLike 𝕜
c : ℕ → 𝕜
a b : ℝ
m : ℕ
ha : 0 ≤ a
g : ℝ → 𝕜
hg_int : IntegrableOn g (Set.Icc a b) volume
hab : a ≤ b
hb : ⌊a⌋₊ < ⌊b⌋₊
⊢ IntegrableOn (fun t => g t * ∑ k ∈ Icc m ⌊t⌋₊, c k) (Set.Icc a b) volume

Proof state:
case inr
𝕜 : Type u_1
inst✝ : RCLike 𝕜
c : ℕ → 𝕜
a b : ℝ
m : ℕ
ha : 0 ≤ a
g : ℝ → 𝕜
hg_int : IntegrableOn g (Set.Icc a b) volume
hab : a > b
⊢ IntegrableOn (fun t => g t * ∑ k ∈ Icc m ⌊t⌋₊, c k) (Set.Icc a b) volume

Tactic:
rw [Set.Icc_eq_empty_of_lt hab]

Result:
case inr
𝕜 : Type u_1
inst✝ : RCLike 𝕜
c : ℕ → 𝕜
a b : ℝ
m : ℕ
ha : 0 ≤ a
g : ℝ → 𝕜
hg_int : IntegrableOn g (Set.Icc a b) volume
hab : a > b
⊢ IntegrableOn (fun t => g t * ∑ k ∈ Icc m ⌊t⌋₊, c k) ∅ volume

Proof state:
case h
𝕜 : Type u_1
inst✝ : RCLike 𝕜
c : ℕ → 𝕜
a b : ℝ
m : ℕ
ha : 0 ≤ a
g : ℝ → 𝕜
hg_int : IntegrableOn g (Set.Icc a b) volume
hab : a ≤ b
hb : ⌊a⌋₊ = ⌊b⌋₊
t : ℝ
ht₁ : t ∈ Set.Icc (↑⌊a⌋₊) (↑⌊a⌋₊ + 1) → ∑ k ∈ Icc ?m.13040 ⌊t⌋₊, c k = ∑ k ∈ Icc ?m.13040 ⌊a⌋₊, c k
ht₂ : t ∈ Set.Icc a b
⊢ ∑ 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⟩]

Result:
no goals

Proof state:
𝕜 : Type u_1
inst✝ : RCLike 𝕜
c : ℕ → 𝕜
a b : ℝ
m : ℕ
ha : 0 ≤ a
g : ℝ → 𝕜
hg_int : IntegrableOn g (Set.Icc a b) volume
⊢ IntegrableOn (fun t => g t * ∑ k ∈ Icc m ⌊t⌋₊, c k) (Set.Icc a b) volume

Tactic:
obtain hab | hab := le_or_gt a b

Result:
case inl
𝕜 : Type u_1
inst✝ : RCLike 𝕜
c : ℕ → 𝕜
a b : ℝ
m : ℕ
ha : 0 ≤ a
g : ℝ → 𝕜
hg_int : IntegrableOn g (Set.Icc a b) volume
hab : a ≤ b
⊢ IntegrableOn (fun t => g t * ∑ k ∈ Icc m ⌊t⌋₊, c k) (Set.Icc a b) volume

case inr
𝕜 : Type u_1
inst✝ : RCLike 𝕜
c : ℕ → 𝕜
a b : ℝ
m : ℕ
ha : 0 ≤ a
g : ℝ → 𝕜
hg_int : IntegrableOn g (Set.Icc a b) volume
hab : a > b
⊢ IntegrableOn (fun t => g t * ∑ k ∈ Icc m ⌊t⌋₊, c k) (Set.Icc a b) volume

Proof state:
case inl.inl
𝕜 : Type u_1
inst✝ : RCLike 𝕜
c : ℕ → 𝕜
a b : ℝ
m : ℕ
ha : 0 ≤ a
g : ℝ → 𝕜
hg_int : IntegrableOn g (Set.Icc a b) volume
hab : a ≤ b
hb : ⌊a⌋₊ = ⌊b⌋₊
this : ∀ᵐ (x : ℝ) ∂volume.restrict (Set.Icc a b), ∑ k ∈ Icc m ⌊a⌋₊, c k = ∑ k ∈ Icc m ⌊x⌋₊, c k
⊢ IntegrableOn (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)

Result:
no goals

Proof state:
case inl.inr
𝕜 : Type u_1
inst✝ : RCLike 𝕜
c : ℕ → 𝕜
a b : ℝ
m : ℕ
ha : 0 ≤ a
g : ℝ → 𝕜
hg_int : IntegrableOn g (Set.Icc a b) volume
hab : a ≤ b
hb : ⌊a⌋₊ < ⌊b⌋₊
h_locint :
  ∀ {t₁ t₂ : ℝ} {n : ℕ},
    t₁ ≤ t₂ →
      ↑n ≤ t₁ → t₂ ≤ ↑n + 1 → a ≤ t₁ → t₂ ≤ b → IntervalIntegrable (fun t => g t * ∑ k ∈ Icc m ⌊t⌋₊, c k) volume t₁ t₂
aux1 : 0 ≤ b
aux2 : ↑⌊a⌋₊ + 1 ≤ b
aux3 : a ≤ ↑⌊a⌋₊ + 1
aux4 : a ≤ ↑⌊b⌋₊
⊢ IntegrableOn (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)]

Result:
case inl.inr
𝕜 : Type u_1
inst✝ : RCLike 𝕜
c : ℕ → 𝕜
a b : ℝ
m : ℕ
ha : 0 ≤ a
g : ℝ → 𝕜
hg_int : IntegrableOn g (Set.Icc a b) volume
hab : a ≤ b
hb : ⌊a⌋₊ < ⌊b⌋₊
h_locint :
  ∀ {t₁ t₂ : ℝ} {n : ℕ},
    t₁ ≤ t₂ →
      ↑n ≤ t₁ → t₂ ≤ ↑n + 1 → a ≤ t₁ → t₂ ≤ b → IntervalIntegrable (fun t => g t * ∑ k ∈ Icc m ⌊t⌋₊, c k) volume t₁ t₂
aux1 : 0 ≤ b
aux2 : ↑⌊a⌋₊ + 1 ≤ b
aux3 : a ≤ ↑⌊a⌋₊ + 1
aux4 : a ≤ ↑⌊b⌋₊
⊢ IntervalIntegrable (fun t => g t * ∑ k ∈ Icc m ⌊t⌋₊, c k) volume a b

Proof state:
case inl.inr
𝕜 : Type u_1
inst✝ : RCLike 𝕜
c : ℕ → 𝕜
a b : ℝ
m : ℕ
ha : 0 ≤ a
g : ℝ → 𝕜
hg_int : IntegrableOn g (Set.Icc a b) volume
hab : a ≤ b
hb : ⌊a⌋₊ < ⌊b⌋₊
h_locint :
  ∀ {t₁ t₂ : ℝ} {n : ℕ},
    t₁ ≤ t₂ →
      ↑n ≤ t₁ → t₂ ≤ ↑n + 1 → a ≤ t₁ → t₂ ≤ b → IntervalIntegrable (fun t => g t * ∑ k ∈ Icc m ⌊t⌋₊, c k) volume t₁ t₂
aux1 : 0 ≤ b
aux2 : ↑⌊a⌋₊ + 1 ≤ b
aux3 : a ≤ ↑⌊a⌋₊ + 1
aux4 : a ≤ ↑⌊b⌋₊
I1 : IntervalIntegrable (fun t => g t * ∑ k ∈ Icc m ⌊t⌋₊, c k) volume a ↑(⌊a⌋₊ + 1)
I2 : IntervalIntegrable (fun t => g t * ∑ k ∈ Icc m ⌊t⌋₊, c k) volume ↑(⌊a⌋₊ + 1) ↑⌊b⌋₊
⊢ IntervalIntegrable (fun t => g t * ∑ k ∈ Icc m ⌊t⌋₊, c k) volume a 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

Result:
case inl.inr
𝕜 : Type u_1
inst✝ : RCLike 𝕜
c : ℕ → 𝕜
a b : ℝ
m : ℕ
ha : 0 ≤ a
g : ℝ → 𝕜
hg_int : IntegrableOn g (Set.Icc a b) volume
hab : a ≤ b
hb : ⌊a⌋₊ < ⌊b⌋₊
h_locint :
  ∀ {t₁ t₂ : ℝ} {n : ℕ},
    t₁ ≤ t₂ →
      ↑n ≤ t₁ → t₂ ≤ ↑n + 1 → a ≤ t₁ → t₂ ≤ b → IntervalIntegrable (fun t => g t * ∑ k ∈ Icc m ⌊t⌋₊, c k) volume t₁ t₂
aux1 : 0 ≤ b
aux2 : ↑⌊a⌋₊ + 1 ≤ b
aux3 : a ≤ ↑⌊a⌋₊ + 1
aux4 : a ≤ ↑⌊b⌋₊
I1 : IntervalIntegrable (fun t => g t * ∑ k ∈ Icc m ⌊t⌋₊, c k) volume a ↑(⌊a⌋₊ + 1)
I2 : IntervalIntegrable (fun t => g t * ∑ k ∈ Icc m ⌊t⌋₊, c k) volume ↑(⌊a⌋₊ + 1) ↑⌊b⌋₊
I3 : IntervalIntegrable (fun t => g t * ∑ k ∈ Icc m ⌊t⌋₊, c k) volume (↑⌊b⌋₊) b
⊢ IntervalIntegrable (fun t => g t * ∑ k ∈ Icc m ⌊t⌋₊, c k) volume a b