awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.MellinTransform (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℝ → E
s : ℂ
pos :
  ∀ (hE : CompleteSpace E),
    mellin (fun (t : ℝ) ↦ f (HPow.hPow (β := ℝ) t 0)) s = HSMul.hSMul (α := ℝ) |0|⁻¹ (mellin f (s / (↑0 : ℂ)))
⊢ mellin (fun (t : ℝ) ↦ f (HPow.hPow (β := ℝ) t 0)) s = HSMul.hSMul (α := ℝ) |0|⁻¹ (mellin f (s / (↑0 : ℂ)))
have neg : ∀ (hE : ¬CompleteSpace E),
  mellin (fun (t : ℝ) ↦ f (HPow.hPow (β := ℝ) t 0)) s = HSMul.hSMul (α := ℝ) |0|⁻¹ (mellin f (s / (↑0 : ℂ)))
Tactic: by_cases hE : CompleteSpace E
-- Lean 4 proof step from Mathlib.Analysis.MellinTransform (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℝ → E
s : ℂ
a : ℝ
ha : a ≠ 0
⊢ mellin (fun (t : ℝ) ↦ f (t ^ a)) s = |a|⁻¹ • mellin f (s / (↑a : ℂ))
have inr : (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (t : ℝ) ↦
    (↑t : ℂ) ^ (s - 1) • f (t ^ a)) =
  HSMul.hSMul (β := E) |a|⁻¹
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (t : ℝ) ↦
      (↑t : ℂ) ^ (s / (↑a : ℂ) - 1) • f t)
Tactic: simp_rw [mellin]
-- Lean 4 proof step from Mathlib.Analysis.MellinTransform (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℝ → E
s : ℂ
a : ℝ
ha : a ≠ 0
| HSMul.hSMul (β := E) |a|⁻¹
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (t : ℝ) ↦
      (↑t : ℂ) ^ (s / (↑a : ℂ) - 1) • f t)
have rw : @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (a_1 : ℝ) ↦
  |a|⁻¹ • (|a| * a_1 ^ (a - 1)) • (↑(a_1 ^ a) : ℂ) ^ (s / (↑a : ℂ) - 1) • f (a_1 ^ a)
Tactic: rw [← integral_comp_rpow_Ioi _ ha, ← integral_smul]
-- Lean 4 proof step from Mathlib.Analysis.MellinTransform (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℝ → E
s : ℂ
a : ℝ
ha : a ≠ 0
⊢ (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (t : ℝ) ↦
      (↑t : ℂ) ^ (s - 1) • f (t ^ a)) =
    HSMul.hSMul (β := E) |a|⁻¹
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (t : ℝ) ↦
        (↑t : ℂ) ^ (s / (↑a : ℂ) - 1) • f t)
have inr : Eq.{u_1 + 1} (α := E)
  (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (t : ℝ) ↦
    (↑t : ℂ) ^ (s - 1) • f (t ^ a))
  (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (a_1 : ℝ) ↦
    |a|⁻¹ • (|a| * a_1 ^ (a - 1)) • (↑(a_1 ^ a) : ℂ) ^ (s / (↑a : ℂ) - 1) • f (a_1 ^ a))
Tactic: conv_rhs => rw [← integral_comp_rpow_Ioi _ ha, ← integral_smul]
-- Lean 4 proof step from Mathlib.Analysis.MellinTransform (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℝ → E
s : ℂ
a : ℝ
ha : a ≠ 0
⊢ Eq.{u_1 + 1} (α := E)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (t : ℝ) ↦
      (↑t : ℂ) ^ (s - 1) • f (t ^ a))
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (a_1 : ℝ) ↦
      |a|⁻¹ • (|a| * a_1 ^ (a - 1)) • (↑(a_1 ^ a) : ℂ) ^ (s / (↑a : ℂ) - 1) • f (a_1 ^ a))
have inr : ∀ (t : ℝ) (ht : Membership.mem (γ := Set ℝ) (Ioi 0) t),
  (↑t : ℂ) ^ (s - 1) • f (t ^ a) = |a|⁻¹ • (|a| * t ^ (a - 1)) • (↑(t ^ a) : ℂ) ^ (s / (↑a : ℂ) - 1) • f (t ^ a)
Tactic: refine setIntegral_congr_fun measurableSet_Ioi fun t ht => ?_
-- Lean 4 proof step from Mathlib.Analysis.MellinTransform (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℝ → E
s : ℂ
a : ℝ
ha : a ≠ 0
t : ℝ
ht : Membership.mem (γ := Set ℝ) (Ioi 0) t
⊢ (↑t : ℂ) ^ (s - 1) • f (t ^ a) = |a|⁻¹ • (|a| * t ^ (a - 1)) • (↑(t ^ a) : ℂ) ^ (s / (↑a : ℂ) - 1) • f (t ^ a)
have inr : (↑t : ℂ) ^ (s - 1) • f (t ^ a) = ((↑(t ^ (a - 1)) : ℂ) * (↑(t ^ a) : ℂ) ^ (s / (↑a : ℂ) - 1)) • f (t ^ a)
Tactic: rw [← mul_smul, ← mul_assoc, inv_mul_cancel₀ (mt abs_eq_zero.1 ha), one_mul, ← smul_assoc,
    real_smul]
-- Lean 4 proof step from Mathlib.Analysis.MellinTransform (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℝ → E
s : ℂ
a : ℝ
ha : a ≠ 0
t : ℝ
ht : Membership.mem (γ := Set ℝ) (Ioi 0) t
⊢ (↑t : ℂ) ^ (s - 1) • f (t ^ a) = ((↑(t ^ (a - 1)) : ℂ) * (↑(t ^ a) : ℂ) ^ (s / (↑a : ℂ) - 1)) • f (t ^ a)
have inr : (↑t : ℂ) ^ (s - 1) • f (t ^ a) = ((↑t : ℂ) ^ (↑(a - 1) : ℂ) * (↑(t ^ a) : ℂ) ^ (s / (↑a : ℂ) - 1)) • f (t ^ a)
Tactic: rw [ofReal_cpow (le_of_lt ht), ← cpow_mul_ofReal_nonneg (le_of_lt ht), ←
    cpow_add _ _ (ofReal_ne_zero.mpr <| ne_of_gt ht), ofReal_sub, ofReal_one, mul_sub,
    mul_div_cancel₀ _ (ofReal_ne_zero.mpr ha), add_comm, ← add_sub_assoc, mul_one, sub_add_cancel]
-- Lean 4 proof step from Mathlib.Analysis.MellinTransform (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℝ → E
s : ℂ
a : ℝ
ha : a ≠ 0
t : ℝ
ht : Membership.mem (γ := Set ℝ) (Ioi 0) t
inr : (↑t : ℂ) ^ (s - 1) • f (t ^ a) = ((↑t : ℂ) ^ (↑(a - 1) : ℂ) * (↑(t ^ a) : ℂ) ^ (s / (↑a : ℂ) - 1)) • f (t ^ a)
⊢ (↑t : ℂ) ^ (s - 1) • f (t ^ a) = ((↑(t ^ (a - 1)) : ℂ) * (↑(t ^ a) : ℂ) ^ (s / (↑a : ℂ) - 1)) • f (t ^ a)
have inr₁ : (↑t : ℂ) ^ (s - 1) • f (t ^ a) = ((↑t : ℂ) ^ (↑(a - 1) : ℂ) * (↑t : ℂ) ^ ((↑a : ℂ) * (s / (↑a : ℂ) - 1))) • f (t ^ a)
Tactic: rw [ofReal_cpow (le_of_lt ht), ← cpow_mul_ofReal_nonneg (le_of_lt ht), ←
    cpow_add _ _ (ofReal_ne_zero.mpr <| ne_of_gt ht), ofReal_sub, ofReal_one, mul_sub,
    mul_div_cancel₀ _ (ofReal_ne_zero.mpr ha), add_comm, ← add_sub_assoc, mul_one, sub_add_cancel]
-- Lean 4 proof step from Mathlib.Analysis.MellinTransform (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℝ → E
s : ℂ
a : ℝ
ha : a ≠ 0
t : ℝ
ht : Membership.mem (γ := Set ℝ) (Ioi 0) t
inr : (↑t : ℂ) ^ (s - 1) • f (t ^ a) = ((↑t : ℂ) ^ (↑(a - 1) : ℂ) * (↑(t ^ a) : ℂ) ^ (s / (↑a : ℂ) - 1)) • f (t ^ a)
inr₁ :
  (↑t : ℂ) ^ (s - 1) • f (t ^ a) = ((↑t : ℂ) ^ (↑(a - 1) : ℂ) * (↑t : ℂ) ^ ((↑a : ℂ) * (s / (↑a : ℂ) - 1))) • f (t ^ a)
⊢ (↑t : ℂ) ^ (s - 1) • f (t ^ a) = ((↑(t ^ (a - 1)) : ℂ) * (↑(t ^ a) : ℂ) ^ (s / (↑a : ℂ) - 1)) • f (t ^ a)
have inr₂ : (↑t : ℂ) ^ (s - 1) • f (t ^ a) = (↑t : ℂ) ^ ((↑(a - 1) : ℂ) + (↑a : ℂ) * (s / (↑a : ℂ) - 1)) • f (t ^ a)
Tactic: rw [ofReal_cpow (le_of_lt ht), ← cpow_mul_ofReal_nonneg (le_of_lt ht), ←
    cpow_add _ _ (ofReal_ne_zero.mpr <| ne_of_gt ht), ofReal_sub, ofReal_one, mul_sub,
    mul_div_cancel₀ _ (ofReal_ne_zero.mpr ha), add_comm, ← add_sub_assoc, mul_one, sub_add_cancel]
-- Lean 4 proof step from Mathlib.Analysis.MellinTransform (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℝ → E
s : ℂ
a : ℝ
ha : a ≠ 0
t : ℝ
ht : Membership.mem (γ := Set ℝ) (Ioi 0) t
inr : (↑t : ℂ) ^ (s - 1) • f (t ^ a) = ((↑t : ℂ) ^ (↑(a - 1) : ℂ) * (↑(t ^ a) : ℂ) ^ (s / (↑a : ℂ) - 1)) • f (t ^ a)
inr₁ :
  (↑t : ℂ) ^ (s - 1) • f (t ^ a) = ((↑t : ℂ) ^ (↑(a - 1) : ℂ) * (↑t : ℂ) ^ ((↑a : ℂ) * (s / (↑a : ℂ) - 1))) • f (t ^ a)
inr₂ : (↑t : ℂ) ^ (s - 1) • f (t ^ a) = (↑t : ℂ) ^ ((↑(a - 1) : ℂ) + (↑a : ℂ) * (s / (↑a : ℂ) - 1)) • f (t ^ a)
⊢ (↑t : ℂ) ^ (s - 1) • f (t ^ a) = ((↑(t ^ (a - 1)) : ℂ) * (↑(t ^ a) : ℂ) ^ (s / (↑a : ℂ) - 1)) • f (t ^ a)
have inr₃ : (↑t : ℂ) ^ (s - 1) • f (t ^ a) = (↑t : ℂ) ^ ((↑a : ℂ) - (↑1 : ℂ) + (↑a : ℂ) * (s / (↑a : ℂ) - 1)) • f (t ^ a)
Tactic: rw [ofReal_cpow (le_of_lt ht), ← cpow_mul_ofReal_nonneg (le_of_lt ht), ←
    cpow_add _ _ (ofReal_ne_zero.mpr <| ne_of_gt ht), ofReal_sub, ofReal_one, mul_sub,
    mul_div_cancel₀ _ (ofReal_ne_zero.mpr ha), add_comm, ← add_sub_assoc, mul_one, sub_add_cancel]
-- Lean 4 proof step from Mathlib.Analysis.MellinTransform (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℝ → E
s : ℂ
a : ℝ
ha : a ≠ 0
t : ℝ
ht : Membership.mem (γ := Set ℝ) (Ioi 0) t
inr : (↑t : ℂ) ^ (s - 1) • f (t ^ a) = ((↑t : ℂ) ^ (↑(a - 1) : ℂ) * (↑(t ^ a) : ℂ) ^ (s / (↑a : ℂ) - 1)) • f (t ^ a)
inr₁ :
  (↑t : ℂ) ^ (s - 1) • f (t ^ a) = ((↑t : ℂ) ^ (↑(a - 1) : ℂ) * (↑t : ℂ) ^ ((↑a : ℂ) * (s / (↑a : ℂ) - 1))) • f (t ^ a)
inr₂ : (↑t : ℂ) ^ (s - 1) • f (t ^ a) = (↑t : ℂ) ^ ((↑(a - 1) : ℂ) + (↑a : ℂ) * (s / (↑a : ℂ) - 1)) • f (t ^ a)
inr₃ : (↑t : ℂ) ^ (s - 1) • f (t ^ a) = (↑t : ℂ) ^ ((↑a : ℂ) - (↑1 : ℂ) + (↑a : ℂ) * (s / (↑a : ℂ) - 1)) • f (t ^ a)
⊢ (↑t : ℂ) ^ (s - 1) • f (t ^ a) = ((↑(t ^ (a - 1)) : ℂ) * (↑(t ^ a) : ℂ) ^ (s / (↑a : ℂ) - 1)) • f (t ^ a)
have inr₄ : (↑t : ℂ) ^ (s - 1) • f (t ^ a) = (↑t : ℂ) ^ ((↑a : ℂ) - 1 + (↑a : ℂ) * (s / (↑a : ℂ) - 1)) • f (t ^ a)
Tactic: rw [ofReal_cpow (le_of_lt ht), ← cpow_mul_ofReal_nonneg (le_of_lt ht), ←
    cpow_add _ _ (ofReal_ne_zero.mpr <| ne_of_gt ht), ofReal_sub, ofReal_one, mul_sub,
    mul_div_cancel₀ _ (ofReal_ne_zero.mpr ha), add_comm, ← add_sub_assoc, mul_one, sub_add_cancel]
-- Lean 4 proof step from Mathlib.Analysis.MellinTransform (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℝ → E
s : ℂ
a : ℝ
ha : a ≠ 0
t : ℝ
ht : Membership.mem (γ := Set ℝ) (Ioi 0) t
inr : (↑t : ℂ) ^ (s - 1) • f (t ^ a) = ((↑t : ℂ) ^ (↑(a - 1) : ℂ) * (↑(t ^ a) : ℂ) ^ (s / (↑a : ℂ) - 1)) • f (t ^ a)
inr₁ :
  (↑t : ℂ) ^ (s - 1) • f (t ^ a) = ((↑t : ℂ) ^ (↑(a - 1) : ℂ) * (↑t : ℂ) ^ ((↑a : ℂ) * (s / (↑a : ℂ) - 1))) • f (t ^ a)
inr₂ : (↑t : ℂ) ^ (s - 1) • f (t ^ a) = (↑t : ℂ) ^ ((↑(a - 1) : ℂ) + (↑a : ℂ) * (s / (↑a : ℂ) - 1)) • f (t ^ a)
inr₃ : (↑t : ℂ) ^ (s - 1) • f (t ^ a) = (↑t : ℂ) ^ ((↑a : ℂ) - (↑1 : ℂ) + (↑a : ℂ) * (s / (↑a : ℂ) - 1)) • f (t ^ a)
inr₄ : (↑t : ℂ) ^ (s - 1) • f (t ^ a) = (↑t : ℂ) ^ ((↑a : ℂ) - 1 + (↑a : ℂ) * (s / (↑a : ℂ) - 1)) • f (t ^ a)
⊢ (↑t : ℂ) ^ (s - 1) • f (t ^ a) = ((↑(t ^ (a - 1)) : ℂ) * (↑(t ^ a) : ℂ) ^ (s / (↑a : ℂ) - 1)) • f (t ^ a)
have inr₅ : (↑t : ℂ) ^ (s - 1) • f (t ^ a) = (↑t : ℂ) ^ ((↑a : ℂ) - 1 + ((↑a : ℂ) * (s / (↑a : ℂ)) - (↑a : ℂ) * 1)) • f (t ^ a)
Tactic: rw [ofReal_cpow (le_of_lt ht), ← cpow_mul_ofReal_nonneg (le_of_lt ht), ←
    cpow_add _ _ (ofReal_ne_zero.mpr <| ne_of_gt ht), ofReal_sub, ofReal_one, mul_sub,
    mul_div_cancel₀ _ (ofReal_ne_zero.mpr ha), add_comm, ← add_sub_assoc, mul_one, sub_add_cancel]
-- Lean 4 proof step from Mathlib.Analysis.MellinTransform (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℝ → E
s : ℂ
a : ℝ
ha : a ≠ 0
t : ℝ
ht : Membership.mem (γ := Set ℝ) (Ioi 0) t
inr : (↑t : ℂ) ^ (s - 1) • f (t ^ a) = ((↑t : ℂ) ^ (↑(a - 1) : ℂ) * (↑(t ^ a) : ℂ) ^ (s / (↑a : ℂ) - 1)) • f (t ^ a)
inr₁ :
  (↑t : ℂ) ^ (s - 1) • f (t ^ a) = ((↑t : ℂ) ^ (↑(a - 1) : ℂ) * (↑t : ℂ) ^ ((↑a : ℂ) * (s / (↑a : ℂ) - 1))) • f (t ^ a)
inr₂ : (↑t : ℂ) ^ (s - 1) • f (t ^ a) = (↑t : ℂ) ^ ((↑(a - 1) : ℂ) + (↑a : ℂ) * (s / (↑a : ℂ) - 1)) • f (t ^ a)
inr₃ : (↑t : ℂ) ^ (s - 1) • f (t ^ a) = (↑t : ℂ) ^ ((↑a : ℂ) - (↑1 : ℂ) + (↑a : ℂ) * (s / (↑a : ℂ) - 1)) • f (t ^ a)
inr₄ : (↑t : ℂ) ^ (s - 1) • f (t ^ a) = (↑t : ℂ) ^ ((↑a : ℂ) - 1 + (↑a : ℂ) * (s / (↑a : ℂ) - 1)) • f (t ^ a)
inr₅ :
  (↑t : ℂ) ^ (s - 1) • f (t ^ a) = (↑t : ℂ) ^ ((↑a : ℂ) - 1 + ((↑a : ℂ) * (s / (↑a : ℂ)) - (↑a : ℂ) * 1)) • f (t ^ a)
⊢ (↑t : ℂ) ^ (s - 1) • f (t ^ a) = ((↑(t ^ (a - 1)) : ℂ) * (↑(t ^ a) : ℂ) ^ (s / (↑a : ℂ) - 1)) • f (t ^ a)
have inr₆ : (↑t : ℂ) ^ (s - 1) • f (t ^ a) = (↑t : ℂ) ^ ((↑a : ℂ) - 1 + (s - (↑a : ℂ) * 1)) • f (t ^ a)
Tactic: rw [ofReal_cpow (le_of_lt ht), ← cpow_mul_ofReal_nonneg (le_of_lt ht), ←
    cpow_add _ _ (ofReal_ne_zero.mpr <| ne_of_gt ht), ofReal_sub, ofReal_one, mul_sub,
    mul_div_cancel₀ _ (ofReal_ne_zero.mpr ha), add_comm, ← add_sub_assoc, mul_one, sub_add_cancel]
-- Lean 4 proof step from Mathlib.Analysis.MellinTransform (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℝ → E
s : ℂ
a : ℝ
ha : a ≠ 0
t : ℝ
ht : Membership.mem (γ := Set ℝ) (Ioi 0) t
inr : (↑t : ℂ) ^ (s - 1) • f (t ^ a) = ((↑t : ℂ) ^ (↑(a - 1) : ℂ) * (↑(t ^ a) : ℂ) ^ (s / (↑a : ℂ) - 1)) • f (t ^ a)
inr₁ :
  (↑t : ℂ) ^ (s - 1) • f (t ^ a) = ((↑t : ℂ) ^ (↑(a - 1) : ℂ) * (↑t : ℂ) ^ ((↑a : ℂ) * (s / (↑a : ℂ) - 1))) • f (t ^ a)
inr₂ : (↑t : ℂ) ^ (s - 1) • f (t ^ a) = (↑t : ℂ) ^ ((↑(a - 1) : ℂ) + (↑a : ℂ) * (s / (↑a : ℂ) - 1)) • f (t ^ a)
inr₃ : (↑t : ℂ) ^ (s - 1) • f (t ^ a) = (↑t : ℂ) ^ ((↑a : ℂ) - (↑1 : ℂ) + (↑a : ℂ) * (s / (↑a : ℂ) - 1)) • f (t ^ a)
inr₄ : (↑t : ℂ) ^ (s - 1) • f (t ^ a) = (↑t : ℂ) ^ ((↑a : ℂ) - 1 + (↑a : ℂ) * (s / (↑a : ℂ) - 1)) • f (t ^ a)
inr₅ :
  (↑t : ℂ) ^ (s - 1) • f (t ^ a) = (↑t : ℂ) ^ ((↑a : ℂ) - 1 + ((↑a : ℂ) * (s / (↑a : ℂ)) - (↑a : ℂ) * 1)) • f (t ^ a)
inr₆ : (↑t : ℂ) ^ (s - 1) • f (t ^ a) = (↑t : ℂ) ^ ((↑a : ℂ) - 1 + (s - (↑a : ℂ) * 1)) • f (t ^ a)
⊢ (↑t : ℂ) ^ (s - 1) • f (t ^ a) = ((↑(t ^ (a - 1)) : ℂ) * (↑(t ^ a) : ℂ) ^ (s / (↑a : ℂ) - 1)) • f (t ^ a)
have inr₇ : (↑t : ℂ) ^ (s - 1) • f (t ^ a) = (↑t : ℂ) ^ (s - (↑a : ℂ) * 1 + ((↑a : ℂ) - 1)) • f (t ^ a)
Tactic: rw [ofReal_cpow (le_of_lt ht), ← cpow_mul_ofReal_nonneg (le_of_lt ht), ←
    cpow_add _ _ (ofReal_ne_zero.mpr <| ne_of_gt ht), ofReal_sub, ofReal_one, mul_sub,
    mul_div_cancel₀ _ (ofReal_ne_zero.mpr ha), add_comm, ← add_sub_assoc, mul_one, sub_add_cancel]
-- Lean 4 proof step from Mathlib.Analysis.MellinTransform (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℝ → E
s : ℂ
a : ℝ
ha : a ≠ 0
t : ℝ
ht : Membership.mem (γ := Set ℝ) (Ioi 0) t
inr : (↑t : ℂ) ^ (s - 1) • f (t ^ a) = ((↑t : ℂ) ^ (↑(a - 1) : ℂ) * (↑(t ^ a) : ℂ) ^ (s / (↑a : ℂ) - 1)) • f (t ^ a)
inr₁ :
  (↑t : ℂ) ^ (s - 1) • f (t ^ a) = ((↑t : ℂ) ^ (↑(a - 1) : ℂ) * (↑t : ℂ) ^ ((↑a : ℂ) * (s / (↑a : ℂ) - 1))) • f (t ^ a)
inr₂ : (↑t : ℂ) ^ (s - 1) • f (t ^ a) = (↑t : ℂ) ^ ((↑(a - 1) : ℂ) + (↑a : ℂ) * (s / (↑a : ℂ) - 1)) • f (t ^ a)
inr₃ : (↑t : ℂ) ^ (s - 1) • f (t ^ a) = (↑t : ℂ) ^ ((↑a : ℂ) - (↑1 : ℂ) + (↑a : ℂ) * (s / (↑a : ℂ) - 1)) • f (t ^ a)
inr₄ : (↑t : ℂ) ^ (s - 1) • f (t ^ a) = (↑t : ℂ) ^ ((↑a : ℂ) - 1 + (↑a : ℂ) * (s / (↑a : ℂ) - 1)) • f (t ^ a)
inr₅ :
  (↑t : ℂ) ^ (s - 1) • f (t ^ a) = (↑t : ℂ) ^ ((↑a : ℂ) - 1 + ((↑a : ℂ) * (s / (↑a : ℂ)) - (↑a : ℂ) * 1)) • f (t ^ a)
inr₆ : (↑t : ℂ) ^ (s - 1) • f (t ^ a) = (↑t : ℂ) ^ ((↑a : ℂ) - 1 + (s - (↑a : ℂ) * 1)) • f (t ^ a)
inr₇ : (↑t : ℂ) ^ (s - 1) • f (t ^ a) = (↑t : ℂ) ^ (s - (↑a : ℂ) * 1 + ((↑a : ℂ) - 1)) • f (t ^ a)
⊢ (↑t : ℂ) ^ (s - 1) • f (t ^ a) = ((↑(t ^ (a - 1)) : ℂ) * (↑(t ^ a) : ℂ) ^ (s / (↑a : ℂ) - 1)) • f (t ^ a)
have inr₈ : (↑t : ℂ) ^ (s - 1) • f (t ^ a) = (↑t : ℂ) ^ (s - (↑a : ℂ) * 1 + (↑a : ℂ) - 1) • f (t ^ a)
Tactic: rw [ofReal_cpow (le_of_lt ht), ← cpow_mul_ofReal_nonneg (le_of_lt ht), ←
    cpow_add _ _ (ofReal_ne_zero.mpr <| ne_of_gt ht), ofReal_sub, ofReal_one, mul_sub,
    mul_div_cancel₀ _ (ofReal_ne_zero.mpr ha), add_comm, ← add_sub_assoc, mul_one, sub_add_cancel]
-- Lean 4 proof step from Mathlib.Analysis.MellinTransform (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℝ → E
s : ℂ
a : ℝ
ha : a ≠ 0
t : ℝ
ht : Membership.mem (γ := Set ℝ) (Ioi 0) t
inr : (↑t : ℂ) ^ (s - 1) • f (t ^ a) = ((↑t : ℂ) ^ (↑(a - 1) : ℂ) * (↑(t ^ a) : ℂ) ^ (s / (↑a : ℂ) - 1)) • f (t ^ a)
inr₁ :
  (↑t : ℂ) ^ (s - 1) • f (t ^ a) = ((↑t : ℂ) ^ (↑(a - 1) : ℂ) * (↑t : ℂ) ^ ((↑a : ℂ) * (s / (↑a : ℂ) - 1))) • f (t ^ a)
inr₂ : (↑t : ℂ) ^ (s - 1) • f (t ^ a) = (↑t : ℂ) ^ ((↑(a - 1) : ℂ) + (↑a : ℂ) * (s / (↑a : ℂ) - 1)) • f (t ^ a)
inr₃ : (↑t : ℂ) ^ (s - 1) • f (t ^ a) = (↑t : ℂ) ^ ((↑a : ℂ) - (↑1 : ℂ) + (↑a : ℂ) * (s / (↑a : ℂ) - 1)) • f (t ^ a)
inr₄ : (↑t : ℂ) ^ (s - 1) • f (t ^ a) = (↑t : ℂ) ^ ((↑a : ℂ) - 1 + (↑a : ℂ) * (s / (↑a : ℂ) - 1)) • f (t ^ a)
inr₅ :
  (↑t : ℂ) ^ (s - 1) • f (t ^ a) = (↑t : ℂ) ^ ((↑a : ℂ) - 1 + ((↑a : ℂ) * (s / (↑a : ℂ)) - (↑a : ℂ) * 1)) • f (t ^ a)
inr₆ : (↑t : ℂ) ^ (s - 1) • f (t ^ a) = (↑t : ℂ) ^ ((↑a : ℂ) - 1 + (s - (↑a : ℂ) * 1)) • f (t ^ a)
inr₇ : (↑t : ℂ) ^ (s - 1) • f (t ^ a) = (↑t : ℂ) ^ (s - (↑a : ℂ) * 1 + ((↑a : ℂ) - 1)) • f (t ^ a)
inr₈ : (↑t : ℂ) ^ (s - 1) • f (t ^ a) = (↑t : ℂ) ^ (s - (↑a : ℂ) * 1 + (↑a : ℂ) - 1) • f (t ^ a)
⊢ (↑t : ℂ) ^ (s - 1) • f (t ^ a) = ((↑(t ^ (a - 1)) : ℂ) * (↑(t ^ a) : ℂ) ^ (s / (↑a : ℂ) - 1)) • f (t ^ a)
have inr₉ : (↑t : ℂ) ^ (s - 1) • f (t ^ a) = (↑t : ℂ) ^ (s - (↑a : ℂ) + (↑a : ℂ) - 1) • f (t ^ a)
Tactic: rw [ofReal_cpow (le_of_lt ht), ← cpow_mul_ofReal_nonneg (le_of_lt ht), ←
    cpow_add _ _ (ofReal_ne_zero.mpr <| ne_of_gt ht), ofReal_sub, ofReal_one, mul_sub,
    mul_div_cancel₀ _ (ofReal_ne_zero.mpr ha), add_comm, ← add_sub_assoc, mul_one, sub_add_cancel]
-- Lean 4 proof step from Mathlib.Analysis.MellinTransform (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℝ → E
s : ℂ
a : ℝ
ha : a ≠ 0
t : ℝ
ht : Membership.mem (γ := Set ℝ) (Ioi 0) t
inr : (↑t : ℂ) ^ (s - 1) • f (t ^ a) = ((↑t : ℂ) ^ (↑(a - 1) : ℂ) * (↑(t ^ a) : ℂ) ^ (s / (↑a : ℂ) - 1)) • f (t ^ a)
inr₁ :
  (↑t : ℂ) ^ (s - 1) • f (t ^ a) = ((↑t : ℂ) ^ (↑(a - 1) : ℂ) * (↑t : ℂ) ^ ((↑a : ℂ) * (s / (↑a : ℂ) - 1))) • f (t ^ a)
inr₂ : (↑t : ℂ) ^ (s - 1) • f (t ^ a) = (↑t : ℂ) ^ ((↑(a - 1) : ℂ) + (↑a : ℂ) * (s / (↑a : ℂ) - 1)) • f (t ^ a)
inr₃ : (↑t : ℂ) ^ (s - 1) • f (t ^ a) = (↑t : ℂ) ^ ((↑a : ℂ) - (↑1 : ℂ) + (↑a : ℂ) * (s / (↑a : ℂ) - 1)) • f (t ^ a)
inr₄ : (↑t : ℂ) ^ (s - 1) • f (t ^ a) = (↑t : ℂ) ^ ((↑a : ℂ) - 1 + (↑a : ℂ) * (s / (↑a : ℂ) - 1)) • f (t ^ a)
inr₅ :
  (↑t : ℂ) ^ (s - 1) • f (t ^ a) = (↑t : ℂ) ^ ((↑a : ℂ) - 1 + ((↑a : ℂ) * (s / (↑a : ℂ)) - (↑a : ℂ) * 1)) • f (t ^ a)
inr₆ : (↑t : ℂ) ^ (s - 1) • f (t ^ a) = (↑t : ℂ) ^ ((↑a : ℂ) - 1 + (s - (↑a : ℂ) * 1)) • f (t ^ a)
inr₇ : (↑t : ℂ) ^ (s - 1) • f (t ^ a) = (↑t : ℂ) ^ (s - (↑a : ℂ) * 1 + ((↑a : ℂ) - 1)) • f (t ^ a)
inr₈ : (↑t : ℂ) ^ (s - 1) • f (t ^ a) = (↑t : ℂ) ^ (s - (↑a : ℂ) * 1 + (↑a : ℂ) - 1) • f (t ^ a)
inr₉ : (↑t : ℂ) ^ (s - 1) • f (t ^ a) = (↑t : ℂ) ^ (s - (↑a : ℂ) + (↑a : ℂ) - 1) • f (t ^ a)
⊢ (↑t : ℂ) ^ (s - 1) • f (t ^ a) = ((↑(t ^ (a - 1)) : ℂ) * (↑(t ^ a) : ℂ) ^ (s / (↑a : ℂ) - 1)) • f (t ^ a)
have inr₁₀ : (↑t : ℂ) ^ (s - 1) • f (t ^ a) = (↑t : ℂ) ^ (s - 1) • f (t ^ a)
Tactic: rw [ofReal_cpow (le_of_lt ht), ← cpow_mul_ofReal_nonneg (le_of_lt ht), ←
    cpow_add _ _ (ofReal_ne_zero.mpr <| ne_of_gt ht), ofReal_sub, ofReal_one, mul_sub,
    mul_div_cancel₀ _ (ofReal_ne_zero.mpr ha), add_comm, ← add_sub_assoc, mul_one, sub_add_cancel]
-- Lean 4 proof step from Mathlib.Analysis.MellinTransform (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℝ → E
s : ℂ
a : ℝ
ha : 0 < a
⊢ mellin (fun (t : ℝ) ↦ f (a * t)) s = (↑a : ℂ) ^ (-s) • mellin f s
have simp_rw : (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (t : ℝ) ↦
    (↑t : ℂ) ^ (s - 1) • f (a * t)) =
  HSMul.hSMul (β := E) ((↑a : ℂ) ^ (-s))
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (t : ℝ) ↦
      (↑t : ℂ) ^ (s - 1) • f t)
Tactic: simp_rw [mellin]
-- Lean 4 proof step from Mathlib.Analysis.MellinTransform (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℝ → E
s : ℂ
a : ℝ
ha : 0 < a
t : ℝ
ht : Membership.mem (γ := Set ℝ) (Ioi 0) t
⊢ (↑t : ℂ) ^ (s - 1) • f (a * t) = (↑a : ℂ) ^ (1 - s) • (↑(a * t) : ℂ) ^ (s - 1) • f (a * t)
have h : (↑a : ℂ) ^ (s - 1) ≠ 0
Tactic: rw [ofReal_mul, mul_cpow_ofReal_nonneg ha.le (le_of_lt ht), ← mul_smul,
      (by ring : 1 - s = -(s - 1)), cpow_neg, inv_mul_cancel_left₀]
-- Lean 4 proof step from Mathlib.Analysis.MellinTransform (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℝ → E
s : ℂ
a : ℝ
ha : 0 < a
t : ℝ
ht : Membership.mem (γ := Set ℝ) (Ioi 0) t
⊢ (↑a : ℂ) ^ (s - 1) ≠ 0
have h : ¬a = 0 ∨ ¬s - 1 ≠ 0
Tactic: rw [Ne, cpow_eq_zero_iff, ofReal_eq_zero, not_and_or]
-- Lean 4 proof step from Mathlib.Analysis.MellinTransform (hypothesis)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℝ → E
s : ℂ
a : ℝ
ha : 0 < a
⊢ (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (t : ℝ) ↦
      (↑t : ℂ) ^ (s - 1) • f (a * t)) =
    HSMul.hSMul (β := E) ((↑a : ℂ) ^ (-s))
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (t : ℝ) ↦
        (↑t : ℂ) ^ (s - 1) • f t)
have this : EqOn.{0, u_1} (β := E) (fun (t : ℝ) ↦ (↑t : ℂ) ^ (s - 1) • f (a * t))
  (fun (t : ℝ) ↦ HSMul.hSMul (β := E) ((↑a : ℂ) ^ (1 - s)) ((fun (u : ℝ) ↦ (↑u : ℂ) ^ (s - 1) • f u) (a * t))) (Ioi 0)
Tactic: have : EqOn (fun t : ℝ => (t : ℂ) ^ (s - 1) • f (a * t))
      (fun t : ℝ => (a : ℂ) ^ (1 - s) • (fun u : ℝ => (u : ℂ) ^ (s - 1) • f u) (a * t))
        (Ioi 0) := fun t ht ↦ by
    dsimp only
    rw [ofReal_mul, mul_cpow_ofReal_nonneg ha.le (le_of_lt ht), ← mul_smul,
      (by ring : 1 - s = -(s - 1)), cpow_neg, inv_mul_cancel_left₀]
    rw [Ne, cpow_eq_zero_iff, ofReal_eq_zero, not_and_or]
    exact Or.inl ha.ne'
-- Lean 4 proof step from Mathlib.Analysis.MellinTransform (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℝ → E
s : ℂ
a : ℝ
ha : 0 < a
this :
  EqOn.{0, u_1} (β := E) (fun (t : ℝ) ↦ (↑t : ℂ) ^ (s - 1) • f (a * t))
    (fun (t : ℝ) ↦ HSMul.hSMul (β := E) ((↑a : ℂ) ^ (1 - s)) ((fun (u : ℝ) ↦ (↑u : ℂ) ^ (s - 1) • f u) (a * t))) (Ioi 0)
⊢ (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (t : ℝ) ↦
      (↑t : ℂ) ^ (s - 1) • f (a * t)) =
    HSMul.hSMul (β := E) ((↑a : ℂ) ^ (-s))
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (t : ℝ) ↦
        (↑t : ℂ) ^ (s - 1) • f t)
have rw : (@integral _ _ _ _ Real.measurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦
    HSMul.hSMul (β := E) ((↑a : ℂ) ^ (1 - s)) ((fun (u : ℝ) ↦ (↑u : ℂ) ^ (s - 1) • f u) (a * x))) =
  HSMul.hSMul (β := E) ((↑a : ℂ) ^ (-s))
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (t : ℝ) ↦
      (↑t : ℂ) ^ (s - 1) • f t)
Tactic: rw [setIntegral_congr_fun measurableSet_Ioi this, integral_smul,
    integral_comp_mul_left_Ioi (fun u ↦ (u : ℂ) ^ (s - 1) • f u) _ ha,
    mul_zero, ← Complex.coe_smul, ← mul_smul, sub_eq_add_neg,
    cpow_add _ _ (ofReal_ne_zero.mpr ha.ne'), cpow_one, ofReal_inv,
    mul_assoc, mul_comm, inv_mul_cancel_right₀ (ofReal_ne_zero.mpr ha.ne')]
-- Lean 4 proof step from Mathlib.Analysis.MellinTransform (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℝ → E
s : ℂ
a : ℝ
ha : 0 < a
this :
  EqOn.{0, u_1} (β := E) (fun (t : ℝ) ↦ (↑t : ℂ) ^ (s - 1) • f (a * t))
    (fun (t : ℝ) ↦ HSMul.hSMul (β := E) ((↑a : ℂ) ^ (1 - s)) ((fun (u : ℝ) ↦ (↑u : ℂ) ^ (s - 1) • f u) (a * t))) (Ioi 0)
rw :
  (@integral _ _ _ _ Real.measurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦
      HSMul.hSMul (β := E) ((↑a : ℂ) ^ (1 - s)) ((fun (u : ℝ) ↦ (↑u : ℂ) ^ (s - 1) • f u) (a * x))) =
    HSMul.hSMul (β := E) ((↑a : ℂ) ^ (-s))
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (t : ℝ) ↦
        (↑t : ℂ) ^ (s - 1) • f t)
⊢ (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (t : ℝ) ↦
      (↑t : ℂ) ^ (s - 1) • f (a * t)) =
    HSMul.hSMul (β := E) ((↑a : ℂ) ^ (-s))
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (t : ℝ) ↦
        (↑t : ℂ) ^ (s - 1) • f t)
have rw₁ : HSMul.hSMul (β := E) ((↑a : ℂ) ^ (1 - s))
    (@integral _ _ _ _ Real.measurableSpace (Measure.restrict volume (Ioi 0)) fun (a_1 : ℝ) ↦
      (fun (u : ℝ) ↦ (↑u : ℂ) ^ (s - 1) • f u) (a * a_1)) =
  HSMul.hSMul (β := E) ((↑a : ℂ) ^ (-s))
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (t : ℝ) ↦
      (↑t : ℂ) ^ (s - 1) • f t)
Tactic: rw [setIntegral_congr_fun measurableSet_Ioi this, integral_smul,
    integral_comp_mul_left_Ioi (fun u ↦ (u : ℂ) ^ (s - 1) • f u) _ ha,
    mul_zero, ← Complex.coe_smul, ← mul_smul, sub_eq_add_neg,
    cpow_add _ _ (ofReal_ne_zero.mpr ha.ne'), cpow_one, ofReal_inv,
    mul_assoc, mul_comm, inv_mul_cancel_right₀ (ofReal_ne_zero.mpr ha.ne')]