-- Module: Mathlib.Analysis.SpecialFunctions.Gamma.Basic
Goal:
s : ℂ
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Ioi 0) x
rw :
  (↑(rexp (-x)) : ℂ) * (↑x : ℂ) ^ HSub.hSub (α := ℂ) (β := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) s : ℂ) (1 : ℂ) =
    HMul.hMul (α := ℂ) (β := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) (↑(rexp (-x)) : ℂ) : ℂ)
      ((starRingEnd ℂ : (a : ℂ) → ℂ) ((↑x : ℂ) ^ (s - 1)) : ℂ)
rw₁ :
  (↑(rexp (-x)) : ℂ) * (↑x : ℂ) ^ HSub.hSub (α := ℂ) (β := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) s : ℂ) (1 : ℂ) =
    HMul.hMul (β := ℂ) (↑(rexp (-x)) : ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) ((↑x : ℂ) ^ (s - 1)) : ℂ)
rw₂ :
  (↑(rexp (-x)) : ℂ) * cexp (log (↑x : ℂ) * HSub.hSub (α := ℂ) (β := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) s : ℂ) (1 : ℂ)) =
    HMul.hMul (β := ℂ) (↑(rexp (-x)) : ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) ((↑x : ℂ) ^ (s - 1)) : ℂ)
rw₃ :
  (↑(rexp (-x)) : ℂ) * cexp (log (↑x : ℂ) * HSub.hSub (α := ℂ) (β := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) s : ℂ) (1 : ℂ)) =
    HMul.hMul (β := ℂ) (↑(rexp (-x)) : ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) (cexp (log (↑x : ℂ) * (s - 1))) : ℂ)
rw₄ :
  (↑(rexp (-x)) : ℂ) * cexp (log (↑x : ℂ) * HSub.hSub (α := ℂ) (β := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) s : ℂ) (1 : ℂ)) =
    (↑(rexp (-x)) : ℂ) * cexp ((starRingEnd ℂ : (a : ℂ) → ℂ) (log (↑x : ℂ) * (s - 1)))
rw₅ :
  (↑(rexp (-x)) : ℂ) * cexp (log (↑x : ℂ) * HSub.hSub (α := ℂ) (β := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) s : ℂ) (1 : ℂ)) =
    (↑(rexp (-x)) : ℂ) *
      cexp
        (HMul.hMul (α := ℂ) (β := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) (log (↑x : ℂ)) : ℂ)
          ((starRingEnd ℂ : (a : ℂ) → ℂ) (s - 1) : ℂ))
rw₆ :
  (↑(rexp (-x)) : ℂ) *
      cexp ((↑(Real.log x) : ℂ) * HSub.hSub (α := ℂ) (β := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) s : ℂ) (1 : ℂ)) =
    (↑(rexp (-x)) : ℂ) *
      cexp
        (HMul.hMul (α := ℂ) (β := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) (↑(Real.log x) : ℂ) : ℂ)
          ((starRingEnd ℂ : (a : ℂ) → ℂ) (s - 1) : ℂ))
rw₇ :
  (↑(rexp (-x)) : ℂ) *
      cexp ((↑(Real.log x) : ℂ) * HSub.hSub (α := ℂ) (β := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) s : ℂ) (1 : ℂ)) =
    (↑(rexp (-x)) : ℂ) * cexp (HMul.hMul (β := ℂ) (↑(Real.log x) : ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) (s - 1) : ℂ))
rw₈ :
  (↑(rexp (-x)) : ℂ) *
      cexp ((↑(Real.log x) : ℂ) * HSub.hSub (α := ℂ) (β := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) s : ℂ) (1 : ℂ)) =
    (↑(rexp (-x)) : ℂ) *
      cexp
        ((↑(Real.log x) : ℂ) *
          HSub.hSub (α := ℂ) (β := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) s : ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) 1 : ℂ))
rw₉ rw₁₀ :
  (↑(rexp (-x)) : ℂ) *
      cexp ((↑(Real.log x) : ℂ) * HSub.hSub (α := ℂ) (β := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) s : ℂ) (1 : ℂ)) =
    (↑(rexp (-x)) : ℂ) *
      cexp ((↑(Real.log x) : ℂ) * HSub.hSub (α := ℂ) (β := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) s : ℂ) (1 : ℂ))
⊢ (↑(rexp (-x)) : ℂ) * (↑x : ℂ) ^ HSub.hSub (α := ℂ) (β := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) s : ℂ) (1 : ℂ) =
    (starRingEnd ℂ : (a : ℂ) → ℂ) ((↑(rexp (-x)) : ℂ) * (↑x : ℂ) ^ (s - 1))

Tactic:
rw [map_mul, conj_ofReal, cpow_def_of_ne_zero (ofReal_ne_zero.mpr (ne_of_gt hx)),
    cpow_def_of_ne_zero (ofReal_ne_zero.mpr (ne_of_gt hx)), ← exp_conj, map_mul,
    ← ofReal_log (le_of_lt hx), conj_ofReal, map_sub, map_one]

Premises used: Iff.mpr, map_sub, Complex.ofReal_log, le_of_lt, Complex.ofReal_ne_zero, ne_of_gt, map_mul, map_one, Complex.exp_conj, Complex.conj_ofReal, Complex.cpow_def_of_ne_zero