-- Mathlib/Analysis/MellinTransform.lean
theorem hasMellin_one_Ioc {s : ℂ} (hs : 0 < re s) :
    HasMellin (indicator (Ioc 0 1) (fun _ => 1 : ℝ → ℂ)) s (1 / s)

Proof state:
s : ℂ
hs : 0 < s.re
⊢ HasMellin ((Ioc 0 1).indicator fun x => 1) s (1 / s)

Tactic:
have aux1 : -1 < (s - 1).re := by
  simpa only [sub_re, one_re, sub_eq_add_neg] using lt_add_of_pos_left _ hs

Result:
s : ℂ
hs : 0 < s.re
aux1 : -1 < (s - 1).re
⊢ HasMellin ((Ioc 0 1).indicator fun x => 1) s (1 / s)

Proof state:
s : ℂ
hs : 0 < s.re
aux1 : -1 < (s - 1).re
aux2 : s ≠ 0
aux3 : MeasurableSet (Ioc 0 1)
⊢ IntervalIntegrable (fun a => ↑a ^ (s - 1)) volume 0 1 ∧ ∫ (a : ℝ) in Ioc 0 1, ↑a ^ (s - 1) ∂volume = 1 / s

Tactic:
refine ⟨intervalIntegral.intervalIntegrable_cpow' aux1, ?_⟩

Result:
s : ℂ
hs : 0 < s.re
aux1 : -1 < (s - 1).re
aux2 : s ≠ 0
aux3 : MeasurableSet (Ioc 0 1)
⊢ ∫ (a : ℝ) in Ioc 0 1, ↑a ^ (s - 1) ∂volume = 1 / s

Proof state:
s : ℂ
hs : 0 < s.re
aux1 : -1 < (s - 1).re
aux2 : s ≠ 0
aux3 : MeasurableSet (Ioc 0 1)
⊢ ∫ (a : ℝ) in Ioc 0 1, ↑a ^ (s - 1) ∂volume = 1 / s

Tactic:
rw [← intervalIntegral.integral_of_le zero_le_one, integral_cpow (Or.inl aux1), sub_add_cancel,
  ofReal_zero, ofReal_one, one_cpow, zero_cpow aux2, sub_zero]

Result:
no goals

Proof state:
s : ℂ
hs : 0 < s.re
⊢ -1 < (s - 1).re

Tactic:
simpa only [sub_re, one_re, sub_eq_add_neg] using lt_add_of_pos_left _ hs

Result:
no goals

Proof state:
s : ℂ
aux1 : -1 < (s - 1).re
hs : s = 0
⊢ s.re ≤ 0

Tactic:
rw [hs, zero_re]

Result:
no goals

Proof state:
s : ℂ
hs : 0 < s.re
aux1 : -1 < (s - 1).re
aux2 : s ≠ 0
aux3 : MeasurableSet (Ioc 0 1)
⊢ Integrable (fun a => ↑a ^ (s - 1)) (volume.restrict (Ioc 0 1)) ∧ ∫ (a : ℝ) in Ioc 0 1, ↑a ^ (s - 1) ∂volume = 1 / s

Tactic:
rw [← IntegrableOn, ← intervalIntegrable_iff_integrableOn_Ioc_of_le zero_le_one]

Result:
s : ℂ
hs : 0 < s.re
aux1 : -1 < (s - 1).re
aux2 : s ≠ 0
aux3 : MeasurableSet (Ioc 0 1)
⊢ IntervalIntegrable (fun a => ↑a ^ (s - 1)) volume 0 1 ∧ ∫ (a : ℝ) in Ioc 0 1, ↑a ^ (s - 1) ∂volume = 1 / s

Proof state:
s : ℂ
hs : 0 < s.re
aux1 : -1 < (s - 1).re
aux2 : s ≠ 0
⊢ HasMellin ((Ioc 0 1).indicator fun x => 1) s (1 / s)

Tactic:
have aux3 : MeasurableSet (Ioc (0 : ℝ) 1) := measurableSet_Ioc

Result:
s : ℂ
hs : 0 < s.re
aux1 : -1 < (s - 1).re
aux2 : s ≠ 0
aux3 : MeasurableSet (Ioc 0 1)
⊢ HasMellin ((Ioc 0 1).indicator fun x => 1) s (1 / s)

Proof state:
s : ℂ
hs : 0 < s.re
aux1 : -1 < (s - 1).re
aux2 : s ≠ 0
aux3 : MeasurableSet (Ioc 0 1)
⊢ HasMellin ((Ioc 0 1).indicator fun x => 1) s (1 / s)

Tactic:
simp_rw [HasMellin, mellin, MellinConvergent, ← indicator_smul, IntegrableOn,
  integrable_indicator_iff aux3, smul_eq_mul, integral_indicator aux3, mul_one, IntegrableOn,
  Measure.restrict_restrict_of_subset Ioc_subset_Ioi_self]

Result:
s : ℂ
hs : 0 < s.re
aux1 : -1 < (s - 1).re
aux2 : s ≠ 0
aux3 : MeasurableSet (Ioc 0 1)
⊢ Integrable (fun a => ↑a ^ (s - 1)) (volume.restrict (Ioc 0 1)) ∧ ∫ (a : ℝ) in Ioc 0 1, ↑a ^ (s - 1) ∂volume = 1 / s

Proof state:
s : ℂ
hs : 0 < s.re
aux1 : -1 < (s - 1).re
⊢ HasMellin ((Ioc 0 1).indicator fun x => 1) s (1 / s)

Tactic:
have aux2 : s ≠ 0 := by contrapose! hs; rw [hs, zero_re]

Result:
s : ℂ
hs : 0 < s.re
aux1 : -1 < (s - 1).re
aux2 : s ≠ 0
⊢ HasMellin ((Ioc 0 1).indicator fun x => 1) s (1 / s)

Proof state:
s : ℂ
hs : 0 < s.re
aux1 : -1 < (s - 1).re
⊢ s ≠ 0

Tactic:
contrapose! hs

Result:
s : ℂ
aux1 : -1 < (s - 1).re
hs : s = 0
⊢ s.re ≤ 0