-- Mathlib/Analysis/Fourier/PoissonSummation.lean
theorem isBigO_norm_Icc_restrict_atBot {f : C(ℝ, E)} {b : ℝ} (hb : 0 < b)
    (hf : f =O[atBot] fun x : ℝ => |x| ^ (-b)) (R S : ℝ) :
    (fun x : ℝ => ‖f.restrict (Icc (x + R) (x + S))‖) =O[atBot] fun x : ℝ => |x| ^ (-b)

Proof state:
E : Type u_1
inst✝ : NormedAddCommGroup E
f : C(ℝ, E)
b : ℝ
hb : 0 < b
hf : ⇑f =O[atBot] fun x => |x| ^ (-b)
R S : ℝ
h1 : ⇑(f.comp { toFun := fun a => -a, continuous_toFun := ⋯ }) =O[atTop] fun x => |x| ^ (-b)
h2 :
  ((fun x =>
        ‖ContinuousMap.restrict (Icc (x + -S) (x + -R)) (f.comp { toFun := fun a => -a, continuous_toFun := ⋯ })‖) ∘
      Neg.neg) =O[atBot]
    ((fun x => |x| ^ (-b)) ∘ Neg.neg)
⊢ (fun x => |x| ^ (-b)) ∘ Neg.neg = fun x => |x| ^ (-b)

Tactic:
ext1 x

Result:
case h
E : Type u_1
inst✝ : NormedAddCommGroup E
f : C(ℝ, E)
b : ℝ
hb : 0 < b
hf : ⇑f =O[atBot] fun x => |x| ^ (-b)
R S : ℝ
h1 : ⇑(f.comp { toFun := fun a => -a, continuous_toFun := ⋯ }) =O[atTop] fun x => |x| ^ (-b)
h2 :
  ((fun x =>
        ‖ContinuousMap.restrict (Icc (x + -S) (x + -R)) (f.comp { toFun := fun a => -a, continuous_toFun := ⋯ })‖) ∘
      Neg.neg) =O[atBot]
    ((fun x => |x| ^ (-b)) ∘ Neg.neg)
x : ℝ
⊢ ((fun x => |x| ^ (-b)) ∘ Neg.neg) x = |x| ^ (-b)

Proof state:
case mk
E : Type u_1
inst✝ : NormedAddCommGroup E
f : C(ℝ, E)
b : ℝ
hb : 0 < b
hf : ⇑f =O[atBot] fun x => |x| ^ (-b)
R S : ℝ
h1 : ⇑(f.comp { toFun := fun a => -a, continuous_toFun := ⋯ }) =O[atTop] fun x => |x| ^ (-b)
h2 :
  ((fun x =>
        ‖ContinuousMap.restrict (Icc (x + -S) (x + -R)) (f.comp { toFun := fun a => -a, continuous_toFun := ⋯ })‖) ∘
      Neg.neg) =O[atBot]
    fun x => |x| ^ (-b)
this : (fun x => |x| ^ (-b)) ∘ Neg.neg = fun x => |x| ^ (-b)
x✝ x : ℝ
hx : x ∈ Icc (x✝ + R) (x✝ + S)
⊢ ‖f x‖ ≤ ‖ContinuousMap.restrict (Icc (-x✝ + -S) (-x✝ + -R)) (f.comp { toFun := fun a => -a, continuous_toFun := ⋯ })‖

Tactic:
refine (le_of_eq ?_).trans (ContinuousMap.norm_coe_le_norm _ ⟨-x, ?_⟩)

Result:
case mk.refine_1
E : Type u_1
inst✝ : NormedAddCommGroup E
f : C(ℝ, E)
b : ℝ
hb : 0 < b
hf : ⇑f =O[atBot] fun x => |x| ^ (-b)
R S : ℝ
h1 : ⇑(f.comp { toFun := fun a => -a, continuous_toFun := ⋯ }) =O[atTop] fun x => |x| ^ (-b)
h2 :
  ((fun x =>
        ‖ContinuousMap.restrict (Icc (x + -S) (x + -R)) (f.comp { toFun := fun a => -a, continuous_toFun := ⋯ })‖) ∘
      Neg.neg) =O[atBot]
    fun x => |x| ^ (-b)
this : (fun x => |x| ^ (-b)) ∘ Neg.neg = fun x => |x| ^ (-b)
x✝ x : ℝ
hx : x ∈ Icc (x✝ + R) (x✝ + S)
⊢ ‖f x‖ =
    ‖(ContinuousMap.restrict (Icc (-x✝ + -S) (-x✝ + -R)) (f.comp { toFun := fun a => -a, continuous_toFun := ⋯ }))
        ⟨-x, ?mk.refine_2⟩‖

case mk.refine_2
E : Type u_1
inst✝ : NormedAddCommGroup E
f : C(ℝ, E)
b : ℝ
hb : 0 < b
hf : ⇑f =O[atBot] fun x => |x| ^ (-b)
R S : ℝ
h1 : ⇑(f.comp { toFun := fun a => -a, continuous_toFun := ⋯ }) =O[atTop] fun x => |x| ^ (-b)
h2 :
  ((fun x =>
        ‖ContinuousMap.restrict (Icc (x + -S) (x + -R)) (f.comp { toFun := fun a => -a, continuous_toFun := ⋯ })‖) ∘
      Neg.neg) =O[atBot]
    fun x => |x| ^ (-b)
this : (fun x => |x| ^ (-b)) ∘ Neg.neg = fun x => |x| ^ (-b)
x✝ x : ℝ
hx : x ∈ Icc (x✝ + R) (x✝ + S)
⊢ -x ∈ Icc (-x✝ + -S) (-x✝ + -R)

Proof state:
E : Type u_1
inst✝ : NormedAddCommGroup E
f : C(ℝ, E)
b : ℝ
hb : 0 < b
hf : ⇑f =O[atBot] fun x => |x| ^ (-b)
R S : ℝ
h1 : ⇑(f.comp { toFun := fun a => -a, continuous_toFun := ⋯ }) =O[atTop] fun x => |x| ^ (-b)
h2 :
  ((fun x =>
        ‖ContinuousMap.restrict (Icc (x + -S) (x + -R)) (f.comp { toFun := fun a => -a, continuous_toFun := ⋯ })‖) ∘
      Neg.neg) =O[atBot]
    fun x => |x| ^ (-b)
this : (fun x => |x| ^ (-b)) ∘ Neg.neg = fun x => |x| ^ (-b)
x✝ x : ℝ
hx : x ∈ Icc (x✝ + R) (x✝ + S)
⊢ -x ≤ -x✝ + -R

Tactic:
linarith [hx.1]

Result:
no goals

Proof state:
case mk
E : Type u_1
inst✝ : NormedAddCommGroup E
f : C(ℝ, E)
b : ℝ
hb : 0 < b
hf : ⇑f =O[atBot] fun x => |x| ^ (-b)
R S : ℝ
h1 : ⇑(f.comp { toFun := fun a => -a, continuous_toFun := ⋯ }) =O[atTop] fun x => |x| ^ (-b)
h2 :
  ((fun x =>
        ‖ContinuousMap.restrict (Icc (x + -S) (x + -R)) (f.comp { toFun := fun a => -a, continuous_toFun := ⋯ })‖) ∘
      Neg.neg) =O[atBot]
    fun x => |x| ^ (-b)
this : (fun x => |x| ^ (-b)) ∘ Neg.neg = fun x => |x| ^ (-b)
x✝ x : ℝ
hx : x ∈ Icc (x✝ + R) (x✝ + S)
⊢ ‖(ContinuousMap.restrict (Icc (x✝ + R) (x✝ + S)) f) ⟨x, hx⟩‖ ≤
    ‖ContinuousMap.restrict (Icc (-x✝ + -S) (-x✝ + -R)) (f.comp { toFun := fun a => -a, continuous_toFun := ⋯ })‖

Tactic:
rw [ContinuousMap.restrict_apply_mk]

Result:
case mk
E : Type u_1
inst✝ : NormedAddCommGroup E
f : C(ℝ, E)
b : ℝ
hb : 0 < b
hf : ⇑f =O[atBot] fun x => |x| ^ (-b)
R S : ℝ
h1 : ⇑(f.comp { toFun := fun a => -a, continuous_toFun := ⋯ }) =O[atTop] fun x => |x| ^ (-b)
h2 :
  ((fun x =>
        ‖ContinuousMap.restrict (Icc (x + -S) (x + -R)) (f.comp { toFun := fun a => -a, continuous_toFun := ⋯ })‖) ∘
      Neg.neg) =O[atBot]
    fun x => |x| ^ (-b)
this : (fun x => |x| ^ (-b)) ∘ Neg.neg = fun x => |x| ^ (-b)
x✝ x : ℝ
hx : x ∈ Icc (x✝ + R) (x✝ + S)
⊢ ‖f x‖ ≤ ‖ContinuousMap.restrict (Icc (-x✝ + -S) (-x✝ + -R)) (f.comp { toFun := fun a => -a, continuous_toFun := ⋯ })‖

Proof state:
case mk.refine_1
E : Type u_1
inst✝ : NormedAddCommGroup E
f : C(ℝ, E)
b : ℝ
hb : 0 < b
hf : ⇑f =O[atBot] fun x => |x| ^ (-b)
R S : ℝ
h1 : ⇑(f.comp { toFun := fun a => -a, continuous_toFun := ⋯ }) =O[atTop] fun x => |x| ^ (-b)
h2 :
  ((fun x =>
        ‖ContinuousMap.restrict (Icc (x + -S) (x + -R)) (f.comp { toFun := fun a => -a, continuous_toFun := ⋯ })‖) ∘
      Neg.neg) =O[atBot]
    fun x => |x| ^ (-b)
this : (fun x => |x| ^ (-b)) ∘ Neg.neg = fun x => |x| ^ (-b)
x✝ x : ℝ
hx : x ∈ Icc (x✝ + R) (x✝ + S)
⊢ ‖f x‖ =
    ‖(ContinuousMap.restrict (Icc (-x✝ + -S) (-x✝ + -R)) (f.comp { toFun := fun a => -a, continuous_toFun := ⋯ }))
        ⟨-x, ?mk.refine_2⟩‖

Tactic:
rw [ContinuousMap.restrict_apply_mk, ContinuousMap.comp_apply, ContinuousMap.coe_mk,
  ContinuousMap.coe_mk, neg_neg]

Result:
no goals

Proof state:
E : Type u_1
inst✝ : NormedAddCommGroup E
f : C(ℝ, E)
b : ℝ
hb : 0 < b
hf : ⇑f =O[atBot] fun x => |x| ^ (-b)
R S : ℝ
h1 : ⇑(f.comp { toFun := fun a => -a, continuous_toFun := ⋯ }) =O[atTop] fun x => |x| ^ (-b)
h2 :
  ((fun x =>
        ‖ContinuousMap.restrict (Icc (x + -S) (x + -R)) (f.comp { toFun := fun a => -a, continuous_toFun := ⋯ })‖) ∘
      Neg.neg) =O[atBot]
    fun x => |x| ^ (-b)
this : (fun x => |x| ^ (-b)) ∘ Neg.neg = fun x => |x| ^ (-b)
x : ℝ
⊢ ∀ (x_1 : ↑(Icc (x + R) (x + S))),
    ‖(ContinuousMap.restrict (Icc (x + R) (x + S)) f) x_1‖ ≤
      ‖ContinuousMap.restrict (Icc (-x + -S) (-x + -R)) (f.comp { toFun := fun a => -a, continuous_toFun := ⋯ })‖

Tactic:
rintro ⟨x, hx⟩

Result:
case mk
E : Type u_1
inst✝ : NormedAddCommGroup E
f : C(ℝ, E)
b : ℝ
hb : 0 < b
hf : ⇑f =O[atBot] fun x => |x| ^ (-b)
R S : ℝ
h1 : ⇑(f.comp { toFun := fun a => -a, continuous_toFun := ⋯ }) =O[atTop] fun x => |x| ^ (-b)
h2 :
  ((fun x =>
        ‖ContinuousMap.restrict (Icc (x + -S) (x + -R)) (f.comp { toFun := fun a => -a, continuous_toFun := ⋯ })‖) ∘
      Neg.neg) =O[atBot]
    fun x => |x| ^ (-b)
this : (fun x => |x| ^ (-b)) ∘ Neg.neg = fun x => |x| ^ (-b)
x✝ x : ℝ
hx : x ∈ Icc (x✝ + R) (x✝ + S)
⊢ ‖(ContinuousMap.restrict (Icc (x✝ + R) (x✝ + S)) f) ⟨x, hx⟩‖ ≤
    ‖ContinuousMap.restrict (Icc (-x✝ + -S) (-x✝ + -R)) (f.comp { toFun := fun a => -a, continuous_toFun := ⋯ })‖