-- Mathlib/Analysis/MellinTransform.lean
theorem MellinConvergent.comp_mul_left {f : ℝ → E} {s : ℂ} {a : ℝ} (ha : 0 < a) :
    MellinConvergent (fun t => f (a * t)) s ↔ MellinConvergent f s

Proof state:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℝ → E
s : ℂ
a : ℝ
ha : 0 < a
⊢ MellinConvergent (fun t => f (a * t)) s ↔ MellinConvergent f s

Tactic:
have := integrableOn_Ioi_comp_mul_left_iff (fun t : ℝ => (t : ℂ) ^ (s - 1) • f t) 0 ha

Result:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℝ → E
s : ℂ
a : ℝ
ha : 0 < a
this :
  IntegrableOn (fun x => (fun t => ↑t ^ (s - 1) • f t) (a * x)) (Ioi 0) volume ↔
    IntegrableOn (fun t => ↑t ^ (s - 1) • f t) (Ioi (a * 0)) volume
⊢ MellinConvergent (fun t => f (a * t)) s ↔ MellinConvergent f s

Proof state:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℝ → E
s : ℂ
a : ℝ
ha : 0 < a
this :
  IntegrableOn (fun x => (fun t => ↑t ^ (s - 1) • f t) (a * x)) (Ioi 0) volume ↔
    IntegrableOn (fun t => ↑t ^ (s - 1) • f t) (Ioi 0) volume
h1 : EqOn (fun t => ↑(a * t) ^ (s - 1) • f (a * t)) (↑a ^ (s - 1) • fun t => ↑t ^ (s - 1) • f (a * t)) (Ioi 0)
⊢ MellinConvergent (fun t => f (a * t)) s ↔ MellinConvergent f s

Tactic:
have h2 : (a : ℂ) ^ (s - 1) ≠ 0 := by
  rw [Ne, cpow_eq_zero_iff, not_and_or, ofReal_eq_zero]
  exact Or.inl ha.ne'

Result:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℝ → E
s : ℂ
a : ℝ
ha : 0 < a
this :
  IntegrableOn (fun x => (fun t => ↑t ^ (s - 1) • f t) (a * x)) (Ioi 0) volume ↔
    IntegrableOn (fun t => ↑t ^ (s - 1) • f t) (Ioi 0) volume
h1 : EqOn (fun t => ↑(a * t) ^ (s - 1) • f (a * t)) (↑a ^ (s - 1) • fun t => ↑t ^ (s - 1) • f (a * t)) (Ioi 0)
h2 : ↑a ^ (s - 1) ≠ 0
⊢ MellinConvergent (fun t => f (a * t)) s ↔ MellinConvergent f s

Proof state:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℝ → E
s : ℂ
a : ℝ
ha : 0 < a
this :
  IntegrableOn (fun x => (fun t => ↑t ^ (s - 1) • f t) (a * x)) (Ioi 0) volume ↔
    IntegrableOn (fun t => ↑t ^ (s - 1) • f t) (Ioi 0) volume
h1 : EqOn (fun t => ↑(a * t) ^ (s - 1) • f (a * t)) (↑a ^ (s - 1) • fun t => ↑t ^ (s - 1) • f (a * t)) (Ioi 0)
h2 : ↑a ^ (s - 1) ≠ 0
⊢ MellinConvergent (fun t => f (a * t)) s ↔ MellinConvergent f s

Tactic:
rw [MellinConvergent, MellinConvergent, ← this, integrableOn_congr_fun h1 measurableSet_Ioi,
  IntegrableOn, IntegrableOn, integrable_smul_iff h2]

Result:
no goals

Proof state:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℝ → E
s : ℂ
a : ℝ
ha : 0 < a
this :
  IntegrableOn (fun x => (fun t => ↑t ^ (s - 1) • f t) (a * x)) (Ioi 0) volume ↔
    IntegrableOn (fun t => ↑t ^ (s - 1) • f t) (Ioi 0) volume
⊢ MellinConvergent (fun t => f (a * t)) s ↔ MellinConvergent f s

Tactic:
have h1 : EqOn (fun t : ℝ => (↑(a * t) : ℂ) ^ (s - 1) • f (a * t))
    ((a : ℂ) ^ (s - 1) • fun t : ℝ => (t : ℂ) ^ (s - 1) • f (a * t)) (Ioi 0) := fun t ht ↦ by
  simp only [ofReal_mul, mul_cpow_ofReal_nonneg ha.le (le_of_lt ht), mul_smul, Pi.smul_apply]

Result:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℝ → E
s : ℂ
a : ℝ
ha : 0 < a
this :
  IntegrableOn (fun x => (fun t => ↑t ^ (s - 1) • f t) (a * x)) (Ioi 0) volume ↔
    IntegrableOn (fun t => ↑t ^ (s - 1) • f t) (Ioi 0) volume
h1 : EqOn (fun t => ↑(a * t) ^ (s - 1) • f (a * t)) (↑a ^ (s - 1) • fun t => ↑t ^ (s - 1) • f (a * t)) (Ioi 0)
⊢ MellinConvergent (fun t => f (a * t)) s ↔ MellinConvergent f s

Proof state:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℝ → E
s : ℂ
a : ℝ
ha : 0 < a
this :
  IntegrableOn (fun x => (fun t => ↑t ^ (s - 1) • f t) (a * x)) (Ioi 0) volume ↔
    IntegrableOn (fun t => ↑t ^ (s - 1) • f t) (Ioi 0) volume
t : ℝ
ht : t ∈ Ioi 0
⊢ (fun t => ↑(a * t) ^ (s - 1) • f (a * t)) t = (↑a ^ (s - 1) • fun t => ↑t ^ (s - 1) • f (a * t)) t

Tactic:
simp only [ofReal_mul, mul_cpow_ofReal_nonneg ha.le (le_of_lt ht), mul_smul, Pi.smul_apply]

Result:
no goals

Proof state:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℝ → E
s : ℂ
a : ℝ
ha : 0 < a
this :
  IntegrableOn (fun x => (fun t => ↑t ^ (s - 1) • f t) (a * x)) (Ioi 0) volume ↔
    IntegrableOn (fun t => ↑t ^ (s - 1) • f t) (Ioi 0) volume
h1 : EqOn (fun t => ↑(a * t) ^ (s - 1) • f (a * t)) (↑a ^ (s - 1) • fun t => ↑t ^ (s - 1) • f (a * t)) (Ioi 0)
⊢ ↑a ^ (s - 1) ≠ 0

Tactic:
rw [Ne, cpow_eq_zero_iff, not_and_or, ofReal_eq_zero]

Result:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℝ → E
s : ℂ
a : ℝ
ha : 0 < a
this :
  IntegrableOn (fun x => (fun t => ↑t ^ (s - 1) • f t) (a * x)) (Ioi 0) volume ↔
    IntegrableOn (fun t => ↑t ^ (s - 1) • f t) (Ioi 0) volume
h1 : EqOn (fun t => ↑(a * t) ^ (s - 1) • f (a * t)) (↑a ^ (s - 1) • fun t => ↑t ^ (s - 1) • f (a * t)) (Ioi 0)
⊢ ¬a = 0 ∨ ¬s - 1 ≠ 0

Proof state:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℝ → E
s : ℂ
a : ℝ
ha : 0 < a
this :
  IntegrableOn (fun x => (fun t => ↑t ^ (s - 1) • f t) (a * x)) (Ioi 0) volume ↔
    IntegrableOn (fun t => ↑t ^ (s - 1) • f t) (Ioi 0) volume
h1 : EqOn (fun t => ↑(a * t) ^ (s - 1) • f (a * t)) (↑a ^ (s - 1) • fun t => ↑t ^ (s - 1) • f (a * t)) (Ioi 0)
⊢ ¬a = 0 ∨ ¬s - 1 ≠ 0

Tactic:
exact Or.inl ha.ne'

Result:
no goals

Proof state:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℝ → E
s : ℂ
a : ℝ
ha : 0 < a
this :
  IntegrableOn (fun x => (fun t => ↑t ^ (s - 1) • f t) (a * x)) (Ioi 0) volume ↔
    IntegrableOn (fun t => ↑t ^ (s - 1) • f t) (Ioi (a * 0)) volume
⊢ MellinConvergent (fun t => f (a * t)) s ↔ MellinConvergent f s

Tactic:
rw [mul_zero] at this

Result:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℝ → E
s : ℂ
a : ℝ
ha : 0 < a
this :
  IntegrableOn (fun x => (fun t => ↑t ^ (s - 1) • f t) (a * x)) (Ioi 0) volume ↔
    IntegrableOn (fun t => ↑t ^ (s - 1) • f t) (Ioi 0) volume
⊢ MellinConvergent (fun t => f (a * t)) s ↔ MellinConvergent f s