-- Mathlib/MeasureTheory/Integral/IntervalIntegral.lean
theorem sum_integral_adjacent_intervals_Ico {a : ℕ → ℝ} {m n : ℕ} (hmn : m ≤ n)
    (hint : ∀ k ∈ Ico m n, IntervalIntegrable f μ (a k) (a <| k + 1)) :
    ∑ k ∈ Finset.Ico m n, ∫ x in a k..a <| k + 1, f x ∂μ = ∫ x in a m..a n, f x ∂μ

Proof state:
case refine_2
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
μ : Measure ℝ
a : ℕ → ℝ
m n : ℕ
hmn : m ≤ n
p : ℕ
hmp : m ≤ p
IH :
  (∀ k ∈ Ico m p, IntervalIntegrable f μ (a k) (a (k + 1))) →
    ∑ k ∈ Finset.Ico m p, ∫ (x : ℝ) in a k..a (k + 1), f x ∂μ = ∫ (x : ℝ) in a m..a p, f x ∂μ
h : ∀ k ∈ Ico m (p + 1), IntervalIntegrable f μ (a k) (a (k + 1))
⊢ ∀ k ∈ Ico m p, IntervalIntegrable f μ (a k) (a (k + 1))

Tactic:
intro k hk

Result:
case refine_2
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
μ : Measure ℝ
a : ℕ → ℝ
m n : ℕ
hmn : m ≤ n
p : ℕ
hmp : m ≤ p
IH :
  (∀ k ∈ Ico m p, IntervalIntegrable f μ (a k) (a (k + 1))) →
    ∑ k ∈ Finset.Ico m p, ∫ (x : ℝ) in a k..a (k + 1), f x ∂μ = ∫ (x : ℝ) in a m..a p, f x ∂μ
h : ∀ k ∈ Ico m (p + 1), IntervalIntegrable f μ (a k) (a (k + 1))
k : ℕ
hk : k ∈ Ico m p
⊢ IntervalIntegrable f μ (a k) (a (k + 1))

Proof state:
case refine_1
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
μ : Measure ℝ
a : ℕ → ℝ
m n : ℕ
hmn : m ≤ n
⊢ (∀ k ∈ Ico m m, IntervalIntegrable f μ (a k) (a (k + 1))) →
    ∑ k ∈ Finset.Ico m m, ∫ (x : ℝ) in a k..a (k + 1), f x ∂μ = ∫ (x : ℝ) in a m..a m, f x ∂μ

Tactic:
simp

Result:
no goals

Proof state:
case refine_2
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
μ : Measure ℝ
a : ℕ → ℝ
m n : ℕ
hmn : m ≤ n
p : ℕ
hmp : m ≤ p
IH :
  (∀ k ∈ Ico m p, IntervalIntegrable f μ (a k) (a (k + 1))) →
    ∑ k ∈ Finset.Ico m p, ∫ (x : ℝ) in a k..a (k + 1), f x ∂μ = ∫ (x : ℝ) in a m..a p, f x ∂μ
h : ∀ k ∈ Ico m (p + 1), IntervalIntegrable f μ (a k) (a (k + 1))
k : ℕ
hk : k ∈ Ico m p
⊢ IntervalIntegrable f μ (a k) (a (k + 1))

Tactic:
exact h _ (Ico_subset_Ico_right p.le_succ hk)

Result:
no goals

Proof state:
case refine_2.hbc
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
μ : Measure ℝ
a : ℕ → ℝ
m n : ℕ
hmn : m ≤ n
p : ℕ
hmp : m ≤ p
IH :
  (∀ k ∈ Ico m p, IntervalIntegrable f μ (a k) (a (k + 1))) →
    ∑ k ∈ Finset.Ico m p, ∫ (x : ℝ) in a k..a (k + 1), f x ∂μ = ∫ (x : ℝ) in a m..a p, f x ∂μ
h : ∀ k ∈ Ico m (p + 1), IntervalIntegrable f μ (a k) (a (k + 1))
⊢ IntervalIntegrable f μ (a p) (a (p + 1))

Tactic:
apply h

Result:
case refine_2.hbc.a
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
μ : Measure ℝ
a : ℕ → ℝ
m n : ℕ
hmn : m ≤ n
p : ℕ
hmp : m ≤ p
IH :
  (∀ k ∈ Ico m p, IntervalIntegrable f μ (a k) (a (k + 1))) →
    ∑ k ∈ Finset.Ico m p, ∫ (x : ℝ) in a k..a (k + 1), f x ∂μ = ∫ (x : ℝ) in a m..a p, f x ∂μ
h : ∀ k ∈ Ico m (p + 1), IntervalIntegrable f μ (a k) (a (k + 1))
⊢ p ∈ Ico m (p + 1)

Proof state:
case refine_2.hbc.a
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
μ : Measure ℝ
a : ℕ → ℝ
m n : ℕ
hmn : m ≤ n
p : ℕ
hmp : m ≤ p
IH :
  (∀ k ∈ Ico m p, IntervalIntegrable f μ (a k) (a (k + 1))) →
    ∑ k ∈ Finset.Ico m p, ∫ (x : ℝ) in a k..a (k + 1), f x ∂μ = ∫ (x : ℝ) in a m..a p, f x ∂μ
h : ∀ k ∈ Ico m (p + 1), IntervalIntegrable f μ (a k) (a (k + 1))
⊢ p ∈ Ico m (p + 1)

Tactic:
simp [hmp]

Result:
no goals

Proof state:
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
μ : Measure ℝ
a : ℕ → ℝ
m n : ℕ
hmn : m ≤ n
⊢ (∀ k ∈ Ico m n, IntervalIntegrable f μ (a k) (a (k + 1))) →
    ∑ k ∈ Finset.Ico m n, ∫ (x : ℝ) in a k..a (k + 1), f x ∂μ = ∫ (x : ℝ) in a m..a n, f x ∂μ

Tactic:
refine Nat.le_induction ?_ ?_ n hmn

Result:
case refine_1
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
μ : Measure ℝ
a : ℕ → ℝ
m n : ℕ
hmn : m ≤ n
⊢ (∀ k ∈ Ico m m, IntervalIntegrable f μ (a k) (a (k + 1))) →
    ∑ k ∈ Finset.Ico m m, ∫ (x : ℝ) in a k..a (k + 1), f x ∂μ = ∫ (x : ℝ) in a m..a m, f x ∂μ

case refine_2
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
μ : Measure ℝ
a : ℕ → ℝ
m n : ℕ
hmn : m ≤ n
⊢ ∀ (n : ℕ),
    m ≤ n →
      ((∀ k ∈ Ico m n, IntervalIntegrable f μ (a k) (a (k + 1))) →
          ∑ k ∈ Finset.Ico m n, ∫ (x : ℝ) in a k..a (k + 1), f x ∂μ = ∫ (x : ℝ) in a m..a n, f x ∂μ) →
        (∀ k ∈ Ico m (n + 1), IntervalIntegrable f μ (a k) (a (k + 1))) →
          ∑ k ∈ Finset.Ico m (n + 1), ∫ (x : ℝ) in a k..a (k + 1), f x ∂μ = ∫ (x : ℝ) in a m..a (n + 1), f x ∂μ

Proof state:
case refine_2.hab
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
μ : Measure ℝ
a : ℕ → ℝ
m n : ℕ
hmn : m ≤ n
p : ℕ
hmp : m ≤ p
IH :
  (∀ k ∈ Ico m p, IntervalIntegrable f μ (a k) (a (k + 1))) →
    ∑ k ∈ Finset.Ico m p, ∫ (x : ℝ) in a k..a (k + 1), f x ∂μ = ∫ (x : ℝ) in a m..a p, f x ∂μ
h : ∀ k ∈ Ico m (p + 1), IntervalIntegrable f μ (a k) (a (k + 1))
k : ℕ
hk : k ∈ Ico m p
⊢ k ∈ Ico m (p + 1)

Tactic:
exact (Ico_subset_Ico le_rfl (Nat.le_succ _)) hk

Result:
no goals

Proof state:
case refine_2
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
μ : Measure ℝ
a : ℕ → ℝ
m n : ℕ
hmn : m ≤ n
p : ℕ
hmp : m ≤ p
IH :
  (∀ k ∈ Ico m p, IntervalIntegrable f μ (a k) (a (k + 1))) →
    ∑ k ∈ Finset.Ico m p, ∫ (x : ℝ) in a k..a (k + 1), f x ∂μ = ∫ (x : ℝ) in a m..a p, f x ∂μ
h : ∀ k ∈ Ico m (p + 1), IntervalIntegrable f μ (a k) (a (k + 1))
⊢ ∑ k ∈ Finset.Ico m (p + 1), ∫ (x : ℝ) in a k..a (k + 1), f x ∂μ = ∫ (x : ℝ) in a m..a (p + 1), f x ∂μ

Tactic:
rw [Finset.sum_Ico_succ_top hmp, IH, integral_add_adjacent_intervals]

Result:
case refine_2.hab
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
μ : Measure ℝ
a : ℕ → ℝ
m n : ℕ
hmn : m ≤ n
p : ℕ
hmp : m ≤ p
IH :
  (∀ k ∈ Ico m p, IntervalIntegrable f μ (a k) (a (k + 1))) →
    ∑ k ∈ Finset.Ico m p, ∫ (x : ℝ) in a k..a (k + 1), f x ∂μ = ∫ (x : ℝ) in a m..a p, f x ∂μ
h : ∀ k ∈ Ico m (p + 1), IntervalIntegrable f μ (a k) (a (k + 1))
⊢ IntervalIntegrable f μ (a m) (a p)

case refine_2.hbc
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
μ : Measure ℝ
a : ℕ → ℝ
m n : ℕ
hmn : m ≤ n
p : ℕ
hmp : m ≤ p
IH :
  (∀ k ∈ Ico m p, IntervalIntegrable f μ (a k) (a (k + 1))) →
    ∑ k ∈ Finset.Ico m p, ∫ (x : ℝ) in a k..a (k + 1), f x ∂μ = ∫ (x : ℝ) in a m..a p, f x ∂μ
h : ∀ k ∈ Ico m (p + 1), IntervalIntegrable f μ (a k) (a (k + 1))
⊢ IntervalIntegrable f μ (a p) (a (p + 1))

case refine_2
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
μ : Measure ℝ
a : ℕ → ℝ
m n : ℕ
hmn : m ≤ n
p : ℕ
hmp : m ≤ p
IH :
  (∀ k ∈ Ico m p, IntervalIntegrable f μ (a k) (a (k + 1))) →
    ∑ k ∈ Finset.Ico m p, ∫ (x : ℝ) in a k..a (k + 1), f x ∂μ = ∫ (x : ℝ) in a m..a p, f x ∂μ
h : ∀ k ∈ Ico m (p + 1), IntervalIntegrable f μ (a k) (a (k + 1))
⊢ ∀ k ∈ Ico m p, IntervalIntegrable f μ (a k) (a (k + 1))

Proof state:
case refine_2.hab
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
μ : Measure ℝ
a : ℕ → ℝ
m n : ℕ
hmn : m ≤ n
p : ℕ
hmp : m ≤ p
IH :
  (∀ k ∈ Ico m p, IntervalIntegrable f μ (a k) (a (k + 1))) →
    ∑ k ∈ Finset.Ico m p, ∫ (x : ℝ) in a k..a (k + 1), f x ∂μ = ∫ (x : ℝ) in a m..a p, f x ∂μ
h : ∀ k ∈ Ico m (p + 1), IntervalIntegrable f μ (a k) (a (k + 1))
⊢ IntervalIntegrable f μ (a m) (a p)

Tactic:
refine IntervalIntegrable.trans_iterate_Ico hmp fun k hk => h k ?_

Result:
case refine_2.hab
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
μ : Measure ℝ
a : ℕ → ℝ
m n : ℕ
hmn : m ≤ n
p : ℕ
hmp : m ≤ p
IH :
  (∀ k ∈ Ico m p, IntervalIntegrable f μ (a k) (a (k + 1))) →
    ∑ k ∈ Finset.Ico m p, ∫ (x : ℝ) in a k..a (k + 1), f x ∂μ = ∫ (x : ℝ) in a m..a p, f x ∂μ
h : ∀ k ∈ Ico m (p + 1), IntervalIntegrable f μ (a k) (a (k + 1))
k : ℕ
hk : k ∈ Ico m p
⊢ k ∈ Ico m (p + 1)