-- Mathlib/MeasureTheory/Measure/Lebesgue/Integral.lean
theorem Real.integrable_of_summable_norm_Icc {E : Type*} [NormedAddCommGroup E] {f : C(ℝ, E)}
    (hf : Summable fun n : ℤ => ‖(f.comp <| ContinuousMap.addRight n).restrict (Icc 0 1)‖) :
    Integrable f

Proof state:
E : Type u_1
inst✝ : NormedAddCommGroup E
f : C(ℝ, E)
hf : Summable fun n => ‖ContinuousMap.restrict (Icc 0 1) (f.comp (ContinuousMap.addRight ↑n))‖
⊢ Integrable (⇑f) volume

Tactic:
refine integrable_of_summable_norm_restrict (.of_nonneg_of_le
  (fun n : ℤ => mul_nonneg (norm_nonneg
    (f.restrict (⟨Icc (n : ℝ) ((n : ℝ) + 1), isCompact_Icc⟩ : Compacts ℝ)))
      ENNReal.toReal_nonneg) (fun n => ?_) hf) ?_

Result:
case refine_1
E : Type u_1
inst✝ : NormedAddCommGroup E
f : C(ℝ, E)
hf : Summable fun n => ‖ContinuousMap.restrict (Icc 0 1) (f.comp (ContinuousMap.addRight ↑n))‖
n : ℤ
⊢ ‖ContinuousMap.restrict (↑{ carrier := Icc (↑n) (↑n + 1), isCompact' := ⋯ }) f‖ *
      (volume ↑{ carrier := Icc (↑n) (↑n + 1), isCompact' := ⋯ }).toReal ≤
    ‖ContinuousMap.restrict (Icc 0 1) (f.comp (ContinuousMap.addRight ↑n))‖

case refine_2
E : Type u_1
inst✝ : NormedAddCommGroup E
f : C(ℝ, E)
hf : Summable fun n => ‖ContinuousMap.restrict (Icc 0 1) (f.comp (ContinuousMap.addRight ↑n))‖
⊢ ⋃ i, ↑{ carrier := Icc (↑i) (↑i + 1), isCompact' := ⋯ } = univ

Proof state:
case refine_2
E : Type u_1
inst✝ : NormedAddCommGroup E
f : C(ℝ, E)
hf : Summable fun n => ‖ContinuousMap.restrict (Icc 0 1) (f.comp (ContinuousMap.addRight ↑n))‖
⊢ ⋃ i, ↑{ carrier := Icc (↑i) (↑i + 1), isCompact' := ⋯ } = univ

Tactic:
exact iUnion_Icc_intCast ℝ

Result:
no goals

Proof state:
case refine_1
E : Type u_1
inst✝ : NormedAddCommGroup E
f : C(ℝ, E)
hf : Summable fun n => ‖ContinuousMap.restrict (Icc 0 1) (f.comp (ContinuousMap.addRight ↑n))‖
n : ℤ
⊢ ∀ (x : ↑(Icc (↑n) (↑n + 1))),
    ‖(ContinuousMap.restrict (Icc (↑n) (↑n + 1)) f) x‖ ≤
      ‖ContinuousMap.restrict (Icc 0 1) (f.comp (ContinuousMap.addRight ↑n))‖

Tactic:
intro x

Result:
case refine_1
E : Type u_1
inst✝ : NormedAddCommGroup E
f : C(ℝ, E)
hf : Summable fun n => ‖ContinuousMap.restrict (Icc 0 1) (f.comp (ContinuousMap.addRight ↑n))‖
n : ℤ
x : ↑(Icc (↑n) (↑n + 1))
⊢ ‖(ContinuousMap.restrict (Icc (↑n) (↑n + 1)) f) x‖ ≤
    ‖ContinuousMap.restrict (Icc 0 1) (f.comp (ContinuousMap.addRight ↑n))‖

Proof state:
case refine_1
E : Type u_1
inst✝ : NormedAddCommGroup E
f : C(ℝ, E)
hf : Summable fun n => ‖ContinuousMap.restrict (Icc 0 1) (f.comp (ContinuousMap.addRight ↑n))‖
n : ℤ
x : ↑(Icc (↑n) (↑n + 1))
this :
  ‖(ContinuousMap.restrict (Icc 0 1) (f.comp (ContinuousMap.addRight ↑n))) ⟨↑x - ↑n, ⋯⟩‖ ≤
    ‖ContinuousMap.restrict (Icc 0 1) (f.comp (ContinuousMap.addRight ↑n))‖
⊢ ‖(ContinuousMap.restrict (Icc (↑n) (↑n + 1)) f) x‖ ≤
    ‖ContinuousMap.restrict (Icc 0 1) (f.comp (ContinuousMap.addRight ↑n))‖

Tactic:
simpa only [ContinuousMap.restrict_apply, comp_apply, coe_addRight, Subtype.coe_mk,
  sub_add_cancel] using this

Result:
no goals

Proof state:
case refine_1
E : Type u_1
inst✝ : NormedAddCommGroup E
f : C(ℝ, E)
hf : Summable fun n => ‖ContinuousMap.restrict (Icc 0 1) (f.comp (ContinuousMap.addRight ↑n))‖
n : ℤ
x : ↑(Icc (↑n) (↑n + 1))
⊢ ‖(ContinuousMap.restrict (Icc (↑n) (↑n + 1)) f) x‖ ≤
    ‖ContinuousMap.restrict (Icc 0 1) (f.comp (ContinuousMap.addRight ↑n))‖

Tactic:
have := ((f.comp <| ContinuousMap.addRight n).restrict (Icc 0 1)).norm_coe_le_norm
    ⟨x - n, ⟨sub_nonneg.mpr x.2.1, sub_le_iff_le_add'.mpr x.2.2⟩⟩

Result:
case refine_1
E : Type u_1
inst✝ : NormedAddCommGroup E
f : C(ℝ, E)
hf : Summable fun n => ‖ContinuousMap.restrict (Icc 0 1) (f.comp (ContinuousMap.addRight ↑n))‖
n : ℤ
x : ↑(Icc (↑n) (↑n + 1))
this :
  ‖(ContinuousMap.restrict (Icc 0 1) (f.comp (ContinuousMap.addRight ↑n))) ⟨↑x - ↑n, ⋯⟩‖ ≤
    ‖ContinuousMap.restrict (Icc 0 1) (f.comp (ContinuousMap.addRight ↑n))‖
⊢ ‖(ContinuousMap.restrict (Icc (↑n) (↑n + 1)) f) x‖ ≤
    ‖ContinuousMap.restrict (Icc 0 1) (f.comp (ContinuousMap.addRight ↑n))‖

Proof state:
case refine_1
E : Type u_1
inst✝ : NormedAddCommGroup E
f : C(ℝ, E)
hf : Summable fun n => ‖ContinuousMap.restrict (Icc 0 1) (f.comp (ContinuousMap.addRight ↑n))‖
n : ℤ
⊢ ‖ContinuousMap.restrict (↑{ carrier := Icc (↑n) (↑n + 1), isCompact' := ⋯ }) f‖ *
      (volume ↑{ carrier := Icc (↑n) (↑n + 1), isCompact' := ⋯ }).toReal ≤
    ‖ContinuousMap.restrict (Icc 0 1) (f.comp (ContinuousMap.addRight ↑n))‖

Tactic:
simp only [Compacts.coe_mk, Real.volume_Icc, add_sub_cancel_left,
  ENNReal.toReal_ofReal zero_le_one, mul_one, norm_le _ (norm_nonneg _)]

Result:
case refine_1
E : Type u_1
inst✝ : NormedAddCommGroup E
f : C(ℝ, E)
hf : Summable fun n => ‖ContinuousMap.restrict (Icc 0 1) (f.comp (ContinuousMap.addRight ↑n))‖
n : ℤ
⊢ ∀ (x : ↑(Icc (↑n) (↑n + 1))),
    ‖(ContinuousMap.restrict (Icc (↑n) (↑n + 1)) f) x‖ ≤
      ‖ContinuousMap.restrict (Icc 0 1) (f.comp (ContinuousMap.addRight ↑n))‖