case refine'_1
E : Type u_1
inst✝ : NormedAddCommGroup E
f : C(ℝ, E)
hf : Summable fun n => ‖ContinuousMap.restrict (Icc 0 1) (comp f (ContinuousMap.addRight ↑n))‖
⊢ ℤ → Compacts ℝ

case refine'_2
E : Type u_1
inst✝ : NormedAddCommGroup E
f : C(ℝ, E)
hf : Summable fun n => ‖ContinuousMap.restrict (Icc 0 1) (comp f (ContinuousMap.addRight ↑n))‖
n : ℤ
⊢ ‖ContinuousMap.restrict (↑(?refine'_1 n)) f‖ * ENNReal.toReal (↑↑volume ↑(?refine'_1 n)) ≤
    ‖ContinuousMap.restrict (Icc 0 1) (comp f (ContinuousMap.addRight ↑n))‖

case refine'_3
E : Type u_1
inst✝ : NormedAddCommGroup E
f : C(ℝ, E)
hf : Summable fun n => ‖ContinuousMap.restrict (Icc 0 1) (comp f (ContinuousMap.addRight ↑n))‖
⊢ (⋃ (i : ℤ), ↑(?refine'_1 i)) = univ
E : Type u_1
inst✝ : NormedAddCommGroup E
f : C(ℝ, E)
hf : Summable fun n => ‖ContinuousMap.restrict (Icc 0 1) (comp f (ContinuousMap.addRight ↑n))‖
⊢ Integrable ↑f
refine'
  @integrable_of_summable_norm_restrict ℝ ℤ E _ volume  _ _ _ _ _ _ _ _
    (summable_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) _
case refine'_1
E : Type u_1
inst✝ : NormedAddCommGroup E
f : C(ℝ, E)
hf : Summable fun n => ‖ContinuousMap.restrict (Icc 0 1) (comp f (ContinuousMap.addRight ↑n))‖
n : ℤ
⊢ Compacts ℝ
case refine'_1
E : Type u_1
inst✝ : NormedAddCommGroup E
f : C(ℝ, E)
hf : Summable fun n => ‖ContinuousMap.restrict (Icc 0 1) (comp f (ContinuousMap.addRight ↑n))‖
⊢ ℤ → Compacts ℝ
intro n
no goals
case refine'_1
E : Type u_1
inst✝ : NormedAddCommGroup E
f : C(ℝ, E)
hf : Summable fun n => ‖ContinuousMap.restrict (Icc 0 1) (comp f (ContinuousMap.addRight ↑n))‖
n : ℤ
⊢ Compacts ℝ
exact ⟨Icc (n : ℝ) ((n : ℝ) + 1), isCompact_Icc⟩
case refine'_2
E : Type u_1
inst✝ : NormedAddCommGroup E
f : C(ℝ, E)
hf : Summable fun n => ‖ContinuousMap.restrict (Icc 0 1) (comp f (ContinuousMap.addRight ↑n))‖
n : ℤ
⊢ ∀ (x : ↑(Icc (↑n) (↑n + 1))),
    ‖↑(ContinuousMap.restrict (Icc (↑n) (↑n + 1)) f) x‖ ≤
      ‖ContinuousMap.restrict (Icc 0 1) (comp f (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) (comp f (ContinuousMap.addRight ↑n))‖
n : ℤ
⊢ ‖ContinuousMap.restrict (↑{ carrier := Icc (↑n) (↑n + 1), isCompact' := (_ : IsCompact (Icc (↑n) (↑n + 1))) }) f‖ *
      ENNReal.toReal (↑↑volume ↑{ carrier := Icc (↑n) (↑n + 1), isCompact' := (_ : IsCompact (Icc (↑n) (↑n + 1))) }) ≤
    ‖ContinuousMap.restrict (Icc 0 1) (comp f (ContinuousMap.addRight ↑n))‖
simp only [Compacts.coe_mk, Real.volume_Icc, add_sub_cancel', ENNReal.toReal_ofReal zero_le_one,
  mul_one, norm_le _ (norm_nonneg _)]
case refine'_2
E : Type u_1
inst✝ : NormedAddCommGroup E
f : C(ℝ, E)
hf : Summable fun n => ‖ContinuousMap.restrict (Icc 0 1) (comp f (ContinuousMap.addRight ↑n))‖
n : ℤ
x : ↑(Icc (↑n) (↑n + 1))
⊢ ‖↑(ContinuousMap.restrict (Icc (↑n) (↑n + 1)) f) x‖ ≤
    ‖ContinuousMap.restrict (Icc 0 1) (comp f (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) (comp f (ContinuousMap.addRight ↑n))‖
n : ℤ
⊢ ∀ (x : ↑(Icc (↑n) (↑n + 1))),
    ‖↑(ContinuousMap.restrict (Icc (↑n) (↑n + 1)) f) x‖ ≤
      ‖ContinuousMap.restrict (Icc 0 1) (comp f (ContinuousMap.addRight ↑n))‖
intro x
case refine'_2
E : Type u_1
inst✝ : NormedAddCommGroup E
f : C(ℝ, E)
hf : Summable fun n => ‖ContinuousMap.restrict (Icc 0 1) (comp f (ContinuousMap.addRight ↑n))‖
n : ℤ
x : ↑(Icc (↑n) (↑n + 1))
this :
  ‖↑(ContinuousMap.restrict (Icc 0 1) (comp f (ContinuousMap.addRight ↑n)))
        { val := ↑x - ↑n, property := (_ : 0 ≤ ↑x - ↑n ∧ ↑x - ↑n ≤ 1) }‖ ≤
    ‖ContinuousMap.restrict (Icc 0 1) (comp f (ContinuousMap.addRight ↑n))‖
⊢ ‖↑(ContinuousMap.restrict (Icc (↑n) (↑n + 1)) f) x‖ ≤
    ‖ContinuousMap.restrict (Icc 0 1) (comp f (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) (comp f (ContinuousMap.addRight ↑n))‖
n : ℤ
x : ↑(Icc (↑n) (↑n + 1))
⊢ ‖↑(ContinuousMap.restrict (Icc (↑n) (↑n + 1)) f) x‖ ≤
    ‖ContinuousMap.restrict (Icc 0 1) (comp f (ContinuousMap.addRight ↑n))‖
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⟩⟩
no goals
case refine'_2
E : Type u_1
inst✝ : NormedAddCommGroup E
f : C(ℝ, E)
hf : Summable fun n => ‖ContinuousMap.restrict (Icc 0 1) (comp f (ContinuousMap.addRight ↑n))‖
n : ℤ
x : ↑(Icc (↑n) (↑n + 1))
this :
  ‖↑(ContinuousMap.restrict (Icc 0 1) (comp f (ContinuousMap.addRight ↑n)))
        { val := ↑x - ↑n, property := (_ : 0 ≤ ↑x - ↑n ∧ ↑x - ↑n ≤ 1) }‖ ≤
    ‖ContinuousMap.restrict (Icc 0 1) (comp f (ContinuousMap.addRight ↑n))‖
⊢ ‖↑(ContinuousMap.restrict (Icc (↑n) (↑n + 1)) f) x‖ ≤
    ‖ContinuousMap.restrict (Icc 0 1) (comp f (ContinuousMap.addRight ↑n))‖
simpa only [ContinuousMap.restrict_apply, comp_apply, coe_addRight, Subtype.coe_mk,
  sub_add_cancel] using this
no goals
case refine'_3
E : Type u_1
inst✝ : NormedAddCommGroup E
f : C(ℝ, E)
hf : Summable fun n => ‖ContinuousMap.restrict (Icc 0 1) (comp f (ContinuousMap.addRight ↑n))‖
⊢ (⋃ (i : ℤ), ↑{ carrier := Icc (↑i) (↑i + 1), isCompact' := (_ : IsCompact (Icc (↑i) (↑i + 1))) }) = univ
exact iUnion_Icc_int_cast ℝ