ι : Type ?u.2084269
𝕜 : Type ?u.2084272
E : Type u_1
F : Type ?u.2084278
A : Type ?u.2084281
inst✝ : NormedAddCommGroup E
f : ℝ → E
a✝ b c d : ℝ
μ ν : MeasureTheory.Measure ℝ
a : ℕ → ℝ
m n : ℕ
hmn : m ≤ n
⊢ (∀ (k : ℕ), k ∈ Ico m n → IntervalIntegrable f μ (a k) (a (k + 1))) → IntervalIntegrable f μ (a m) (a n)
ι : Type ?u.2084269
𝕜 : Type ?u.2084272
E : Type u_1
F : Type ?u.2084278
A : Type ?u.2084281
inst✝ : NormedAddCommGroup E
f : ℝ → E
a✝ b c d : ℝ
μ ν : MeasureTheory.Measure ℝ
a : ℕ → ℝ
m n : ℕ
hmn : m ≤ n
hint : ∀ (k : ℕ), k ∈ Ico m n → IntervalIntegrable f μ (a k) (a (k + 1))
⊢ IntervalIntegrable f μ (a m) (a n)
revert hint
case refine'_1
ι : Type ?u.2084269
𝕜 : Type ?u.2084272
E : Type u_1
F : Type ?u.2084278
A : Type ?u.2084281
inst✝ : NormedAddCommGroup E
f : ℝ → E
a✝ b c d : ℝ
μ ν : MeasureTheory.Measure ℝ
a : ℕ → ℝ
m n : ℕ
hmn : m ≤ n
⊢ (∀ (k : ℕ), k ∈ Ico m m → IntervalIntegrable f μ (a k) (a (k + 1))) → IntervalIntegrable f μ (a m) (a m)

case refine'_2
ι : Type ?u.2084269
𝕜 : Type ?u.2084272
E : Type u_1
F : Type ?u.2084278
A : Type ?u.2084281
inst✝ : NormedAddCommGroup E
f : ℝ → E
a✝ b c d : ℝ
μ ν : MeasureTheory.Measure ℝ
a : ℕ → ℝ
m n : ℕ
hmn : m ≤ n
⊢ ∀ (n : ℕ),
    m ≤ n →
      ((∀ (k : ℕ), k ∈ Ico m n → IntervalIntegrable f μ (a k) (a (k + 1))) → IntervalIntegrable f μ (a m) (a n)) →
        (∀ (k : ℕ), k ∈ Ico m (n + 1) → IntervalIntegrable f μ (a k) (a (k + 1))) →
          IntervalIntegrable f μ (a m) (a (n + 1))
ι : Type ?u.2084269
𝕜 : Type ?u.2084272
E : Type u_1
F : Type ?u.2084278
A : Type ?u.2084281
inst✝ : NormedAddCommGroup E
f : ℝ → E
a✝ b c d : ℝ
μ ν : MeasureTheory.Measure ℝ
a : ℕ → ℝ
m n : ℕ
hmn : m ≤ n
⊢ (∀ (k : ℕ), k ∈ Ico m n → IntervalIntegrable f μ (a k) (a (k + 1))) → IntervalIntegrable f μ (a m) (a n)
refine' Nat.le_induction _ _ n hmn
no goals
case refine'_1
ι : Type ?u.2084269
𝕜 : Type ?u.2084272
E : Type u_1
F : Type ?u.2084278
A : Type ?u.2084281
inst✝ : NormedAddCommGroup E
f : ℝ → E
a✝ b c d : ℝ
μ ν : MeasureTheory.Measure ℝ
a : ℕ → ℝ
m n : ℕ
hmn : m ≤ n
⊢ (∀ (k : ℕ), k ∈ Ico m m → IntervalIntegrable f μ (a k) (a (k + 1))) → IntervalIntegrable f μ (a m) (a m)
simp
case refine'_2
ι : Type ?u.2084269
𝕜 : Type ?u.2084272
E : Type u_1
F : Type ?u.2084278
A : Type ?u.2084281
inst✝ : NormedAddCommGroup E
f : ℝ → E
a✝ b c d : ℝ
μ ν : MeasureTheory.Measure ℝ
a : ℕ → ℝ
m n : ℕ
hmn : m ≤ n
p : ℕ
hp : m ≤ p
IH : (∀ (k : ℕ), k ∈ Ico m p → IntervalIntegrable f μ (a k) (a (k + 1))) → IntervalIntegrable f μ (a m) (a p)
h : ∀ (k : ℕ), k ∈ Ico m (p + 1) → IntervalIntegrable f μ (a k) (a (k + 1))
⊢ IntervalIntegrable f μ (a m) (a (p + 1))
case refine'_2
ι : Type ?u.2084269
𝕜 : Type ?u.2084272
E : Type u_1
F : Type ?u.2084278
A : Type ?u.2084281
inst✝ : NormedAddCommGroup E
f : ℝ → E
a✝ b c d : ℝ
μ ν : MeasureTheory.Measure ℝ
a : ℕ → ℝ
m n : ℕ
hmn : m ≤ n
⊢ ∀ (n : ℕ),
    m ≤ n →
      ((∀ (k : ℕ), k ∈ Ico m n → IntervalIntegrable f μ (a k) (a (k + 1))) → IntervalIntegrable f μ (a m) (a n)) →
        (∀ (k : ℕ), k ∈ Ico m (n + 1) → IntervalIntegrable f μ (a k) (a (k + 1))) →
          IntervalIntegrable f μ (a m) (a (n + 1))
intro p hp IH h
no goals
case refine'_2
ι : Type ?u.2084269
𝕜 : Type ?u.2084272
E : Type u_1
F : Type ?u.2084278
A : Type ?u.2084281
inst✝ : NormedAddCommGroup E
f : ℝ → E
a✝ b c d : ℝ
μ ν : MeasureTheory.Measure ℝ
a : ℕ → ℝ
m n : ℕ
hmn : m ≤ n
p : ℕ
hp : m ≤ p
IH : (∀ (k : ℕ), k ∈ Ico m p → IntervalIntegrable f μ (a k) (a (k + 1))) → IntervalIntegrable f μ (a m) (a p)
h : ∀ (k : ℕ), k ∈ Ico m (p + 1) → IntervalIntegrable f μ (a k) (a (k + 1))
⊢ IntervalIntegrable f μ (a m) (a (p + 1))
exact (IH fun k hk => h k (Ico_subset_Ico_right p.le_succ hk)).trans (h p (by simp [hp]))
no goals
ι : Type ?u.2084269
𝕜 : Type ?u.2084272
E : Type u_1
F : Type ?u.2084278
A : Type ?u.2084281
inst✝ : NormedAddCommGroup E
f : ℝ → E
a✝ b c d : ℝ
μ ν : MeasureTheory.Measure ℝ
a : ℕ → ℝ
m n : ℕ
hmn : m ≤ n
p : ℕ
hp : m ≤ p
IH : (∀ (k : ℕ), k ∈ Ico m p → IntervalIntegrable f μ (a k) (a (k + 1))) → IntervalIntegrable f μ (a m) (a p)
h : ∀ (k : ℕ), k ∈ Ico m (p + 1) → IntervalIntegrable f μ (a k) (a (k + 1))
⊢ p ∈ Ico m (p + 1)
simp [hp]