-- Mathlib/Analysis/MellinTransform.lean
theorem mellin_convergent_top_of_isBigO {f : ℝ → ℝ}
    (hfc : AEStronglyMeasurable f <| volume.restrict (Ioi 0)) {a s : ℝ}
    (hf : f =O[atTop] (· ^ (-a))) (hs : s < a) :
    ∃ c : ℝ, 0 < c ∧ IntegrableOn (fun t : ℝ => t ^ (s - 1) * f t) (Ioi c)

Proof state:
f : ℝ → ℝ
hfc : AEStronglyMeasurable f (volume.restrict (Ioi 0))
a s : ℝ
hf : f =O[atTop] fun x => x ^ (-a)
hs : s < a
d e : ℝ
he : ∀ b ≥ e, ‖f b‖ ≤ d * ‖b ^ (-a)‖
he' : 0 < e ⊔ 1
t : ℝ
ht : t ∈ Ioi (e ⊔ 1)
⊢ ‖t ^ (s - 1) * f t‖ ≤ t ^ (s - 1 + -a) * d

Tactic:
have ht' : 0 < t := he'.trans ht

Result:
f : ℝ → ℝ
hfc : AEStronglyMeasurable f (volume.restrict (Ioi 0))
a s : ℝ
hf : f =O[atTop] fun x => x ^ (-a)
hs : s < a
d e : ℝ
he : ∀ b ≥ e, ‖f b‖ ≤ d * ‖b ^ (-a)‖
he' : 0 < e ⊔ 1
t : ℝ
ht : t ∈ Ioi (e ⊔ 1)
ht' : 0 < t
⊢ ‖t ^ (s - 1) * f t‖ ≤ t ^ (s - 1 + -a) * d

Proof state:
f : ℝ → ℝ
hfc : AEStronglyMeasurable f (volume.restrict (Ioi 0))
a s : ℝ
hf : f =O[atTop] fun x => x ^ (-a)
hs : s < a
d e : ℝ
he : ∀ b ≥ e, ‖f b‖ ≤ d * ‖b ^ (-a)‖
he' : 0 < e ⊔ 1
t : ℝ
ht : t ∈ Ioi (e ⊔ 1)
ht' : 0 < t
⊢ ‖t ^ (s - 1) * f t‖ ≤ t ^ (s - 1 + -a) * d

Tactic:
rw [norm_mul, rpow_add ht', ← norm_of_nonneg (rpow_nonneg ht'.le (-a)), mul_assoc,
  mul_comm _ d, norm_of_nonneg (rpow_nonneg ht'.le _)]

Result:
f : ℝ → ℝ
hfc : AEStronglyMeasurable f (volume.restrict (Ioi 0))
a s : ℝ
hf : f =O[atTop] fun x => x ^ (-a)
hs : s < a
d e : ℝ
he : ∀ b ≥ e, ‖f b‖ ≤ d * ‖b ^ (-a)‖
he' : 0 < e ⊔ 1
t : ℝ
ht : t ∈ Ioi (e ⊔ 1)
ht' : 0 < t
⊢ t ^ (s - 1) * ‖f t‖ ≤ t ^ (s - 1) * (d * ‖t ^ (-a)‖)

Proof state:
case intro.intro.refine_1
f : ℝ → ℝ
hfc : AEStronglyMeasurable f (volume.restrict (Ioi 0))
a s : ℝ
hf : f =O[atTop] fun x => x ^ (-a)
hs : s < a
d e : ℝ
he : ∀ b ≥ e, ‖f b‖ ≤ d * ‖b ^ (-a)‖
he' : 0 < e ⊔ 1
⊢ AEStronglyMeasurable (fun t => t ^ (s - 1) * f t) (volume.restrict (Ioi (e ⊔ 1)))

Tactic:
refine AEStronglyMeasurable.mul ?_ (hfc.mono_set (Ioi_subset_Ioi he'.le))

Result:
case intro.intro.refine_1
f : ℝ → ℝ
hfc : AEStronglyMeasurable f (volume.restrict (Ioi 0))
a s : ℝ
hf : f =O[atTop] fun x => x ^ (-a)
hs : s < a
d e : ℝ
he : ∀ b ≥ e, ‖f b‖ ≤ d * ‖b ^ (-a)‖
he' : 0 < e ⊔ 1
⊢ AEStronglyMeasurable (fun t => t ^ (s - 1)) (volume.restrict (Ioi (e ⊔ 1)))

Proof state:
case h
f : ℝ → ℝ
hfc : AEStronglyMeasurable f (volume.restrict (Ioi 0))
a s : ℝ
hf : f =O[atTop] fun x => x ^ (-a)
hs : s < a
d e : ℝ
he : ∀ b ≥ e, ‖f b‖ ≤ d * ‖b ^ (-a)‖
he' : 0 < e ⊔ 1
t : ℝ
ht : t ∈ Ioi (e ⊔ 1)
ht' : 0 < t
⊢ ‖f t‖ ≤ d * ‖t ^ (-a)‖

Tactic:
exact he t ((le_max_left e 1).trans_lt ht).le

Result:
no goals

Proof state:
case intro.intro.refine_2
f : ℝ → ℝ
hfc : AEStronglyMeasurable f (volume.restrict (Ioi 0))
a s : ℝ
hf : f =O[atTop] fun x => x ^ (-a)
hs : s < a
d e : ℝ
he : ∀ b ≥ e, ‖f b‖ ≤ d * ‖b ^ (-a)‖
he' : 0 < e ⊔ 1
this : ∀ᵐ (t : ℝ) ∂volume.restrict (Ioi (e ⊔ 1)), ‖t ^ (s - 1) * f t‖ ≤ t ^ (s - 1 + -a) * d
⊢ HasFiniteIntegral (fun t => t ^ (s - 1) * f t) (volume.restrict (Ioi (e ⊔ 1)))

Tactic:
refine (HasFiniteIntegral.mul_const ?_ _).mono' this

Result:
case intro.intro.refine_2
f : ℝ → ℝ
hfc : AEStronglyMeasurable f (volume.restrict (Ioi 0))
a s : ℝ
hf : f =O[atTop] fun x => x ^ (-a)
hs : s < a
d e : ℝ
he : ∀ b ≥ e, ‖f b‖ ≤ d * ‖b ^ (-a)‖
he' : 0 < e ⊔ 1
this : ∀ᵐ (t : ℝ) ∂volume.restrict (Ioi (e ⊔ 1)), ‖t ^ (s - 1) * f t‖ ≤ t ^ (s - 1 + -a) * d
⊢ HasFiniteIntegral (fun a_1 => a_1 ^ (s - 1 + -a)) (volume.restrict (Ioi (e ⊔ 1)))