awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Basic (goal)
Goal:
s : ℝ
h : 0 < s
⊢ IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ rexp (-x) * x ^ (s - 1)) (Ioi 1) volume
have right : ContinuousOn (Y := ℝ) (fun (x : ℝ) ↦ rexp (-x) * x ^ (s - 1)) (Ici 1)
Tactic: refine integrable_of_isBigO_exp_neg one_half_pos ?_ (Gamma_integrand_isLittleO _).isBigO
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Basic (goal)
Goal:
s : ℂ
hs : 0 < s.re
⊢ IntegrableOn (ε := ℂ) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ (↑(rexp (-x)) : ℂ) * (↑x : ℂ) ^ (s - 1))
    (Ioi 0) volume
have left : AEStronglyMeasurable (β := ℂ) (m₀ := MeasureSpace.toMeasurableSpace)
  (fun (x : ℝ) ↦ (↑(rexp (-x)) : ℂ) * (↑x : ℂ) ^ (s - 1)) (Measure.restrict volume (Ioi 0))
Tactic: constructor
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Basic (goal)
Goal:
s : ℂ
hs : 0 < s.re
left :
  AEStronglyMeasurable (β := ℂ) (m₀ := MeasureSpace.toMeasurableSpace)
    (fun (x : ℝ) ↦ (↑(rexp (-x)) : ℂ) * (↑x : ℂ) ^ (s - 1)) (Measure.restrict volume (Ioi 0))
⊢ IntegrableOn (ε := ℂ) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ (↑(rexp (-x)) : ℂ) * (↑x : ℂ) ^ (s - 1))
    (Ioi 0) volume
have right : @HasFiniteIntegral _ ℂ _ MeasureSpace.toMeasurableSpace (fun (x : ℝ) ↦ (↑(rexp (-x)) : ℂ) * (↑x : ℂ) ^ (s - 1))
  (Measure.restrict volume (Ioi 0))
Tactic: constructor
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Basic (goal)
Goal:
s : ℂ
hs : 0 < s.re
⊢ AEStronglyMeasurable (β := ℂ) (m₀ := MeasureSpace.toMeasurableSpace)
    (fun (x : ℝ) ↦ (↑(rexp (-x)) : ℂ) * (↑x : ℂ) ^ (s - 1)) (Measure.restrict volume (Ioi 0))
have left : ContinuousOn (Y := ℂ) (fun (x : ℝ) ↦ (↑(rexp (-x)) : ℂ) * (↑x : ℂ) ^ (s - 1)) (Ioi 0)
Tactic: refine ContinuousOn.aestronglyMeasurable ?_ measurableSet_Ioi
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Basic (goal)
Goal:
s : ℂ
hs : 0 < s.re
⊢ ContinuousOn (Y := ℂ) (fun (x : ℝ) ↦ (↑(rexp (-x)) : ℂ) * (↑x : ℂ) ^ (s - 1)) (Ioi 0)
have left : ContinuousOn (Y := ℂ) (fun (x : ℝ) ↦ (↑x : ℂ) ^ (s - 1)) (Ioi 0)
Tactic: apply (continuous_ofReal.comp continuous_neg.rexp).continuousOn.mul
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Basic (goal)
Goal:
s : ℂ
hs : 0 < s.re
⊢ ContinuousOn (Y := ℂ) (fun (x : ℝ) ↦ (↑x : ℂ) ^ (s - 1)) (Ioi 0)
have left : ∀ (x : ℝ), Membership.mem (γ := Set ℝ) (Ioi 0) x → ContinuousAt (Y := ℂ) (fun (x : ℝ) ↦ (↑x : ℂ) ^ (s - 1)) x
Tactic: apply continuousOn_of_forall_continuousAt
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Basic (hypothesis)
Goal:
s : ℂ
hs : 0 < s.re
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Ioi 0) x
⊢ ContinuousAt (Y := ℂ) (fun (x : ℝ) ↦ (↑x : ℂ) ^ (s - 1)) x
have this : ContinuousAt (Y := ℂ) (fun (x : ℂ) ↦ x ^ (s - 1)) (↑x : ℂ)
Tactic: have : ContinuousAt (fun x : ℂ => x ^ (s - 1)) ↑x :=
      continuousAt_cpow_const <| ofReal_mem_slitPlane.2 hx
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Basic (goal)
Goal:
s : ℂ
hs : 0 < s.re
⊢ @HasFiniteIntegral _ ℂ _ MeasureSpace.toMeasurableSpace (fun (x : ℝ) ↦ (↑(rexp (-x)) : ℂ) * (↑x : ℂ) ^ (s - 1))
    (Measure.restrict volume (Ioi 0))
have right : @HasFiniteIntegral _ ℝ _ MeasureSpace.toMeasurableSpace (fun (a : ℝ) ↦ ‖(↑(rexp (-a)) : ℂ) * (↑a : ℂ) ^ (s - 1)‖)
  (Measure.restrict volume (Ioi 0))
Tactic: rw [← hasFiniteIntegral_norm_iff]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Basic (goal)
Goal:
s : ℂ
hs : 0 < s.re
⊢ @HasFiniteIntegral _ ℝ _ MeasureSpace.toMeasurableSpace (fun (a : ℝ) ↦ ‖(↑(rexp (-a)) : ℂ) * (↑a : ℂ) ^ (s - 1)‖)
    (Measure.restrict volume (Ioi 0))
have right : (ae (F := Measure ℝ) (Measure.restrict volume (Ioi 0))).EventuallyEq (β := ℝ) (fun (x : ℝ) ↦ rexp (-x) * x ^ (s.re - 1))
  fun (a : ℝ) ↦ ‖(↑(rexp (-a)) : ℂ) * (↑a : ℂ) ^ (s - 1)‖
Tactic: refine HasFiniteIntegral.congr (Real.GammaIntegral_convergent hs).2 ?_
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Basic (goal)
Goal:
s : ℂ
hs : 0 < s.re
⊢ (ae (F := Measure ℝ) (Measure.restrict volume (Ioi 0))).EventuallyEq (β := ℝ)
    (fun (x : ℝ) ↦ rexp (-x) * x ^ (s.re - 1)) fun (a : ℝ) ↦ ‖(↑(rexp (-a)) : ℂ) * (↑a : ℂ) ^ (s - 1)‖
have right : ∀ᵐ (x : ℝ),
  Membership.mem (γ := Set ℝ) (Ioi 0) x →
    Eq (α := ℝ) ((fun (x : ℝ) ↦ rexp (-x) * x ^ (s.re - 1)) x)
      ((fun (a : ℝ) ↦ ‖(↑(rexp (-a)) : ℂ) * (↑a : ℂ) ^ (s - 1)‖) x)
Tactic: apply (ae_restrict_iff' measurableSet_Ioi).mpr
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Basic (goal)
Goal:
s : ℂ
hs : 0 < s.re
⊢ ∀ᵐ (x : ℝ),
    Membership.mem (γ := Set ℝ) (Ioi 0) x →
      Eq (α := ℝ) ((fun (x : ℝ) ↦ rexp (-x) * x ^ (s.re - 1)) x)
        ((fun (a : ℝ) ↦ ‖(↑(rexp (-a)) : ℂ) * (↑a : ℂ) ^ (s - 1)‖) x)
have right : ∀ (x : ℝ) (hx : Membership.mem (γ := Set ℝ) (Ioi 0) x),
  rexp (-x) * x ^ (s.re - 1) = ‖(↑(rexp (-x)) : ℂ) * (↑x : ℂ) ^ (s - 1)‖
Tactic: filter_upwards with x hx
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Basic (goal)
Goal:
s : ℂ
hs : 0 < s.re
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Ioi 0) x
⊢ rexp (-x) * x ^ (s.re - 1) = ‖(↑(rexp (-x)) : ℂ) * (↑x : ℂ) ^ (s - 1)‖
have right : rexp (-x) * x ^ (s.re - 1) = rexp (-x) * x ^ (s - 1).re
Tactic: rw [norm_mul, Complex.norm_of_nonneg <| le_of_lt <| exp_pos <| -x,
      norm_cpow_eq_rpow_re_of_pos hx _]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Basic (goal)
Goal:
s : ℂ
⊢ GammaIntegral ((starRingEnd ℂ : (a : ℂ) → ℂ) s) = (starRingEnd ℂ : (a : ℂ) → ℂ) s.GammaIntegral
have rw : Eq (α := ℂ)
  (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦
    (↑(rexp (-x)) : ℂ) * (↑x : ℂ) ^ HSub.hSub (α := ℂ) (β := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) s : ℂ) (1 : ℂ))
  (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦
    (starRingEnd ℂ : (a : ℂ) → ℂ) ((↑(rexp (-x)) : ℂ) * (↑x : ℂ) ^ (s - 1)))
Tactic: rw [GammaIntegral, GammaIntegral, ← integral_conj]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Basic (goal)
Goal:
s : ℂ
⊢ Eq (α := ℂ)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦
      (↑(rexp (-x)) : ℂ) * (↑x : ℂ) ^ HSub.hSub (α := ℂ) (β := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) s : ℂ) (1 : ℂ))
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (x : ℝ) ↦
      (starRingEnd ℂ : (a : ℂ) → ℂ) ((↑(rexp (-x)) : ℂ) * (↑x : ℂ) ^ (s - 1)))
have refine : ∀ (x : ℝ) (hx : Membership.mem (γ := Set ℝ) (Ioi 0) x),
  (↑(rexp (-x)) : ℂ) * (↑x : ℂ) ^ HSub.hSub (α := ℂ) (β := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) s : ℂ) (1 : ℂ) =
    (starRingEnd ℂ : (a : ℂ) → ℂ) ((↑(rexp (-x)) : ℂ) * (↑x : ℂ) ^ (s - 1))
Tactic: refine setIntegral_congr_fun measurableSet_Ioi fun x hx => ?_
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Basic (goal)
Goal:
s : ℂ
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Ioi 0) x
⊢ (↑(rexp (-x)) : ℂ) * (↑x : ℂ) ^ HSub.hSub (α := ℂ) (β := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) s : ℂ) (1 : ℂ) =
    (starRingEnd ℂ : (a : ℂ) → ℂ) ((↑(rexp (-x)) : ℂ) * (↑x : ℂ) ^ (s - 1))
have rw : (↑(rexp (-x)) : ℂ) * (↑x : ℂ) ^ HSub.hSub (α := ℂ) (β := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) s : ℂ) (1 : ℂ) =
  HMul.hMul (α := ℂ) (β := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) (↑(rexp (-x)) : ℂ) : ℂ)
    ((starRingEnd ℂ : (a : ℂ) → ℂ) ((↑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]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Basic (goal)
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)) : ℂ)
⊢ (↑(rexp (-x)) : ℂ) * (↑x : ℂ) ^ HSub.hSub (α := ℂ) (β := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) s : ℂ) (1 : ℂ) =
    (starRingEnd ℂ : (a : ℂ) → ℂ) ((↑(rexp (-x)) : ℂ) * (↑x : ℂ) ^ (s - 1))
have rw₁ : (↑(rexp (-x)) : ℂ) * (↑x : ℂ) ^ HSub.hSub (α := ℂ) (β := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) s : ℂ) (1 : ℂ) =
  HMul.hMul (β := ℂ) (↑(rexp (-x)) : ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) ((↑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]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Basic (goal)
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)) : ℂ)
⊢ (↑(rexp (-x)) : ℂ) * (↑x : ℂ) ^ HSub.hSub (α := ℂ) (β := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) s : ℂ) (1 : ℂ) =
    (starRingEnd ℂ : (a : ℂ) → ℂ) ((↑(rexp (-x)) : ℂ) * (↑x : ℂ) ^ (s - 1))
have rw₂ : (↑(rexp (-x)) : ℂ) * cexp (log (↑x : ℂ) * HSub.hSub (α := ℂ) (β := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) s : ℂ) (1 : ℂ)) =
  HMul.hMul (β := ℂ) (↑(rexp (-x)) : ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) ((↑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]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Basic (goal)
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)) : ℂ)
⊢ (↑(rexp (-x)) : ℂ) * (↑x : ℂ) ^ HSub.hSub (α := ℂ) (β := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) s : ℂ) (1 : ℂ) =
    (starRingEnd ℂ : (a : ℂ) → ℂ) ((↑(rexp (-x)) : ℂ) * (↑x : ℂ) ^ (s - 1))
have rw₃ : (↑(rexp (-x)) : ℂ) * cexp (log (↑x : ℂ) * HSub.hSub (α := ℂ) (β := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) s : ℂ) (1 : ℂ)) =
  HMul.hMul (β := ℂ) (↑(rexp (-x)) : ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) (cexp (log (↑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]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Basic (goal)
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))) : ℂ)
⊢ (↑(rexp (-x)) : ℂ) * (↑x : ℂ) ^ HSub.hSub (α := ℂ) (β := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) s : ℂ) (1 : ℂ) =
    (starRingEnd ℂ : (a : ℂ) → ℂ) ((↑(rexp (-x)) : ℂ) * (↑x : ℂ) ^ (s - 1))
have rw₄ : (↑(rexp (-x)) : ℂ) * cexp (log (↑x : ℂ) * HSub.hSub (α := ℂ) (β := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) s : ℂ) (1 : ℂ)) =
  (↑(rexp (-x)) : ℂ) * cexp ((starRingEnd ℂ : (a : ℂ) → ℂ) (log (↑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]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Basic (goal)
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)))
⊢ (↑(rexp (-x)) : ℂ) * (↑x : ℂ) ^ HSub.hSub (α := ℂ) (β := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) s : ℂ) (1 : ℂ) =
    (starRingEnd ℂ : (a : ℂ) → ℂ) ((↑(rexp (-x)) : ℂ) * (↑x : ℂ) ^ (s - 1))
have 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) : ℂ))
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]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Basic (goal)
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) : ℂ))
⊢ (↑(rexp (-x)) : ℂ) * (↑x : ℂ) ^ HSub.hSub (α := ℂ) (β := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) s : ℂ) (1 : ℂ) =
    (starRingEnd ℂ : (a : ℂ) → ℂ) ((↑(rexp (-x)) : ℂ) * (↑x : ℂ) ^ (s - 1))
have 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) : ℂ))
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]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Basic (goal)
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) : ℂ))
⊢ (↑(rexp (-x)) : ℂ) * (↑x : ℂ) ^ HSub.hSub (α := ℂ) (β := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) s : ℂ) (1 : ℂ) =
    (starRingEnd ℂ : (a : ℂ) → ℂ) ((↑(rexp (-x)) : ℂ) * (↑x : ℂ) ^ (s - 1))
have 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) : ℂ))
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]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Basic (goal)
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) : ℂ))
⊢ (↑(rexp (-x)) : ℂ) * (↑x : ℂ) ^ HSub.hSub (α := ℂ) (β := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) s : ℂ) (1 : ℂ) =
    (starRingEnd ℂ : (a : ℂ) → ℂ) ((↑(rexp (-x)) : ℂ) * (↑x : ℂ) ^ (s - 1))
have 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 : ℂ))
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]