awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Beta (hypothesis)
Goal:
s : ℂ
hs : ∀ (m : ℕ), s ≠ -(↑m : ℂ)
h_im : ¬s.im = 0
this : sin ((↑π : ℂ) * s) ≠ 0
⊢ Gamma s ≠ 0
have A : (↑π : ℂ) / sin ((↑π : ℂ) * s) ≠ 0
Tactic: have A := div_ne_zero (ofReal_ne_zero.mpr Real.pi_pos.ne') this
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Beta (hypothesis)
Goal:
s : ℂ
hs : ∀ (m : ℕ), s ≠ -(↑m : ℂ)
h_im : ¬s.im = 0
this : sin ((↑π : ℂ) * s) ≠ 0
A : (↑π : ℂ) / sin ((↑π : ℂ) * s) ≠ 0
⊢ Gamma s ≠ 0
have A₁ : Gamma s ≠ 0 ∧ Gamma (1 - s) ≠ 0
Tactic: rw [← Complex.Gamma_mul_Gamma_one_sub s, mul_ne_zero_iff] at A
Cleared hypotheses: A
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Beta (goal)
Goal:
s : ℂ
⊢ Gamma s = 0 ↔ ∃ (m : ℕ), s = -(↑m : ℂ)
have mp : Gamma s = 0 → ∃ (m : ℕ), s = -(↑m : ℂ)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Beta (goal)
Goal:
s : ℂ
mp : Gamma s = 0 → ∃ (m : ℕ), s = -(↑m : ℂ)
⊢ Gamma s = 0 ↔ ∃ (m : ℕ), s = -(↑m : ℂ)
have mpr : (∃ (m : ℕ), s = -(↑m : ℂ)) → Gamma s = 0
Tactic: constructor
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Beta (goal)
Goal:
s : ℂ
⊢ Gamma s = 0 → ∃ (m : ℕ), s = -(↑m : ℂ)
have mp : (∀ (m : ℕ), s ≠ -(↑m : ℂ)) → Gamma s ≠ 0
Tactic: contrapose!
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Beta (goal)
Goal:
s : ℂ
hs : 0 < s.re
⊢ Gamma s ≠ 0
have refine : ∀ (m : ℕ), s ≠ -(↑m : ℂ)
Tactic: refine Gamma_ne_zero fun m => ?_
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Beta (goal)
Goal:
s : ℂ
hs : 0 < s.re
m : ℕ
⊢ s ≠ -(↑m : ℂ)
have contrapose! : ∀ (hs : s = -(↑m : ℂ)), s.re ≤ 0
Tactic: contrapose! hs
Cleared hypotheses: hs
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Beta (goal)
Goal:
s : ℝ
⊢ Tendsto s.GammaSeq atTop (𝓝 (Gamma s))
have suffices : Tendsto (Complex.ofReal ∘ s.GammaSeq) atTop (𝓝 (Complex.Gamma (↑s : ℂ)))
Tactic: suffices Tendsto ((↑) ∘ GammaSeq s : ℕ → ℂ) atTop (𝓝 <| Complex.Gamma s) by
    exact (Complex.continuous_re.tendsto (Complex.Gamma ↑s)).comp this
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Beta (goal)
Goal:
s : ℝ
⊢ Tendsto (Complex.ofReal ∘ s.GammaSeq) atTop (𝓝 (Complex.Gamma (↑s : ℂ)))
have h : Complex.ofReal ∘ s.GammaSeq = (↑s : ℂ).GammaSeq
Tactic: convert! Complex.GammaSeq_tendsto_Gamma s
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Beta (goal)
Goal:
s : ℝ
⊢ Complex.ofReal ∘ s.GammaSeq = (↑s : ℂ).GammaSeq
have h : ∀ (n : ℕ), (Complex.ofReal ∘ s.GammaSeq) n = (↑s : ℂ).GammaSeq n
Tactic: ext1 n
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Beta (goal)
Goal:
s : ℝ
n : ℕ
⊢ (↑(HPow.hPow (α := ℝ) (↑n : ℝ) s * (↑n ! : ℝ) / ∏ j ∈ Finset.range (n + 1), (s + (↑j : ℝ))) : ℂ) =
    HPow.hPow (α := ℂ) (↑n : ℂ) (↑s : ℂ) * (↑n ! : ℂ) / ∏ j ∈ Finset.range (n + 1), ((↑s : ℂ) + (↑j : ℂ))
have h : (↑(HPow.hPow (α := ℝ) (↑n : ℝ) s) : ℂ) * (↑n ! : ℂ) / ∏ x ∈ Finset.range (n + 1), ((↑s : ℂ) + (↑x : ℂ)) =
  HPow.hPow (α := ℂ) (↑n : ℂ) (↑s : ℂ) * (↑n ! : ℂ) / ∏ x ∈ Finset.range (n + 1), ((↑s : ℂ) + (↑x : ℂ))
Tactic: push_cast
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Beta (goal)
Goal:
s : ℝ
n : ℕ
⊢ (↑(HPow.hPow (α := ℝ) (↑n : ℝ) s) : ℂ) * (↑n ! : ℂ) / ∏ x ∈ Finset.range (n + 1), ((↑s : ℂ) + (↑x : ℂ)) =
    HPow.hPow (α := ℂ) (↑n : ℂ) (↑s : ℂ) * (↑n ! : ℂ) / ∏ x ∈ Finset.range (n + 1), ((↑s : ℂ) + (↑x : ℂ))
have h : (↑(↑n : ℝ) : ℂ) ^ (↑s : ℂ) * (↑n ! : ℂ) / ∏ x ∈ Finset.range (n + 1), ((↑s : ℂ) + (↑x : ℂ)) =
  HPow.hPow (α := ℂ) (↑n : ℂ) (↑s : ℂ) * (↑n ! : ℂ) / ∏ x ∈ Finset.range (n + 1), ((↑s : ℂ) + (↑x : ℂ))
Tactic: rw [Complex.ofReal_cpow n.cast_nonneg, Complex.ofReal_natCast]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Beta (goal)
Goal:
s : ℝ
n : ℕ
h :
  (↑(↑n : ℝ) : ℂ) ^ (↑s : ℂ) * (↑n ! : ℂ) / ∏ x ∈ Finset.range (n + 1), ((↑s : ℂ) + (↑x : ℂ)) =
    HPow.hPow (α := ℂ) (↑n : ℂ) (↑s : ℂ) * (↑n ! : ℂ) / ∏ x ∈ Finset.range (n + 1), ((↑s : ℂ) + (↑x : ℂ))
⊢ (↑(HPow.hPow (α := ℝ) (↑n : ℝ) s) : ℂ) * (↑n ! : ℂ) / ∏ x ∈ Finset.range (n + 1), ((↑s : ℂ) + (↑x : ℂ)) =
    HPow.hPow (α := ℂ) (↑n : ℂ) (↑s : ℂ) * (↑n ! : ℂ) / ∏ x ∈ Finset.range (n + 1), ((↑s : ℂ) + (↑x : ℂ))
have h₁ : HPow.hPow (α := ℂ) (↑n : ℂ) (↑s : ℂ) * (↑n ! : ℂ) / ∏ x ∈ Finset.range (n + 1), ((↑s : ℂ) + (↑x : ℂ)) =
  HPow.hPow (α := ℂ) (↑n : ℂ) (↑s : ℂ) * (↑n ! : ℂ) / ∏ x ∈ Finset.range (n + 1), ((↑s : ℂ) + (↑x : ℂ))
Tactic: rw [Complex.ofReal_cpow n.cast_nonneg, Complex.ofReal_natCast]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Beta (goal)
Goal:
s : ℝ
⊢ Gamma s * Gamma (1 - s) = π / sin (π * s)
have simp_rw : Complex.Gamma (↑s : ℂ) * Complex.Gamma (1 - (↑s : ℂ)) = (↑π : ℂ) / Complex.sin ((↑π : ℂ) * (↑s : ℂ))
Tactic: simp_rw [← Complex.ofReal_inj, Complex.ofReal_div, Complex.ofReal_sin, Complex.ofReal_mul, ←
    Complex.Gamma_ofReal, Complex.ofReal_sub, Complex.ofReal_one]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Beta (goal)
Goal:
s : ℂ
⊢ (Gamma s)⁻¹ = s * (Gamma (s + 1))⁻¹
have inl : ∀ (h : s ≠ 0), (Gamma s)⁻¹ = s * (Gamma (s + 1))⁻¹
Tactic: rcases ne_or_eq s 0 with (h | rfl)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Beta (goal)
Goal:
s : ℂ
inl : ∀ (h : s ≠ 0), (Gamma s)⁻¹ = s * (Gamma (s + 1))⁻¹
⊢ (Gamma s)⁻¹ = s * (Gamma (s + 1))⁻¹
have inr : (Gamma 0)⁻¹ = 0 * (Gamma (HAdd.hAdd (α := ℂ) 0 1))⁻¹
Tactic: rcases ne_or_eq s 0 with (h | rfl)
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Beta (goal)
Goal:
s : ℂ
h : s ≠ 0
⊢ (Gamma s)⁻¹ = s * (Gamma (s + 1))⁻¹
have inl : (Gamma s)⁻¹ = s * (s * Gamma s)⁻¹
Tactic: rw [Gamma_add_one s h, mul_inv, mul_inv_cancel_left₀ h]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Beta (goal)
Goal:
s : ℂ
h : s ≠ 0
inl : (Gamma s)⁻¹ = s * (s * Gamma s)⁻¹
⊢ (Gamma s)⁻¹ = s * (Gamma (s + 1))⁻¹
have inl₁ : (Gamma s)⁻¹ = s * (s⁻¹ * (Gamma s)⁻¹)
Tactic: rw [Gamma_add_one s h, mul_inv, mul_inv_cancel_left₀ h]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Beta (goal)
Goal:
s : ℂ
h : s ≠ 0
inl : (Gamma s)⁻¹ = s * (s * Gamma s)⁻¹
inl₁ : (Gamma s)⁻¹ = s * (s⁻¹ * (Gamma s)⁻¹)
⊢ (Gamma s)⁻¹ = s * (Gamma (s + 1))⁻¹
have inl₂ : (Gamma s)⁻¹ = (Gamma s)⁻¹
Tactic: rw [Gamma_add_one s h, mul_inv, mul_inv_cancel_left₀ h]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Beta (goal)
Goal:
⊢ (Gamma 0)⁻¹ = 0 * (Gamma (HAdd.hAdd (α := ℂ) 0 1))⁻¹
have inr : (Gamma 0)⁻¹ = 0 * (Gamma 1)⁻¹
Tactic: rw [zero_add, Gamma_zero, inv_zero, zero_mul]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Beta (goal)
Goal:
inr : (Gamma 0)⁻¹ = 0 * (Gamma 1)⁻¹
⊢ (Gamma 0)⁻¹ = 0 * (Gamma (HAdd.hAdd (α := ℂ) 0 1))⁻¹
have inr₁ : 0⁻¹ = 0 * (Gamma 1)⁻¹
Tactic: rw [zero_add, Gamma_zero, inv_zero, zero_mul]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Beta (goal)
Goal:
inr : (Gamma 0)⁻¹ = 0 * (Gamma 1)⁻¹
inr₁ : 0⁻¹ = 0 * (Gamma 1)⁻¹
⊢ (Gamma 0)⁻¹ = 0 * (Gamma (HAdd.hAdd (α := ℂ) 0 1))⁻¹
have inr₂ : 0 = 0 * (Gamma 1)⁻¹
Tactic: rw [zero_add, Gamma_zero, inv_zero, zero_mul]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Beta (goal)
Goal:
inr : (Gamma 0)⁻¹ = 0 * (Gamma 1)⁻¹
inr₁ : 0⁻¹ = 0 * (Gamma 1)⁻¹
inr₂ : 0 = 0 * (Gamma 1)⁻¹
⊢ (Gamma 0)⁻¹ = 0 * (Gamma (HAdd.hAdd (α := ℂ) 0 1))⁻¹
have inr₃ : Eq (α := ℂ) 0 0
Tactic: rw [zero_add, Gamma_zero, inv_zero, zero_mul]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Beta (goal)
Goal:
s : ℂ
⊢ DifferentiableAt ℂ (F := ℂ) (fun (s : ℂ) ↦ (Gamma s)⁻¹) s
have rcases : ∀ (n : ℕ) (hs : -s.re < (↑n : ℝ)), DifferentiableAt ℂ (F := ℂ) (fun (s : ℂ) ↦ (Gamma s)⁻¹) s
Tactic: rcases exists_nat_gt (-s.re) with ⟨n, hs⟩
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Beta (hypothesis)
Goal:
s : ℂ
hs : -s.re < (↑0 : ℝ)
⊢ DifferentiableAt ℂ (F := ℂ) (fun (s : ℂ) ↦ (Gamma s)⁻¹) s
have hs₁ : 0 < s.re
Tactic: rw [Nat.cast_zero, neg_lt_zero] at hs
Cleared hypotheses: hs
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Beta (goal)
Goal:
s : ℂ
hs : 0 < s.re
⊢ DifferentiableAt ℂ (F := ℂ) (fun (s : ℂ) ↦ (Gamma s)⁻¹) s
have zero : ∀ (m : ℕ), s ≠ -(↑m : ℂ)
Tactic: suffices ∀ m : ℕ, s ≠ -↑m from (differentiableAt_Gamma _ this).inv (Gamma_ne_zero this)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Beta (goal)
Goal:
m : ℕ
hs : 0 < re (-(↑m : ℂ))
⊢ False
have zero : re (-(↑m : ℂ)) ≤ 0
Tactic: apply hs.not_ge
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Beta (goal)
Goal:
n : ℕ
ihn : ∀ (s : ℂ) (hs : -s.re < (↑n : ℝ)), DifferentiableAt ℂ (F := ℂ) (fun (s : ℂ) ↦ (Gamma s)⁻¹) s
s : ℂ
hs : -s.re < (↑(n + 1) : ℝ)
⊢ DifferentiableAt ℂ (F := ℂ) (fun (s : ℂ) ↦ (Gamma s)⁻¹) s
have succ : DifferentiableAt ℂ (F := ℂ) (fun (x : ℂ) ↦ x * (Gamma (x + 1))⁻¹) s
Tactic: rw [funext one_div_Gamma_eq_self_mul_one_div_Gamma_add_one]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Beta (goal)
Goal:
n : ℕ
ihn : ∀ (s : ℂ) (hs : -s.re < (↑n : ℝ)), DifferentiableAt ℂ (F := ℂ) (fun (s : ℂ) ↦ (Gamma s)⁻¹) s
s : ℂ
hs : -s.re < (↑(n + 1) : ℝ)
⊢ -(s + 1).re < (↑n : ℝ)
have rwa : -(s.re + re 1) < (↑n : ℝ)
Tactic: rwa [add_re, one_re, neg_add', sub_lt_iff_lt_add, ← Nat.cast_succ]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Beta (goal)
Goal:
n : ℕ
ihn : ∀ (s : ℂ) (hs : -s.re < (↑n : ℝ)), DifferentiableAt ℂ (F := ℂ) (fun (s : ℂ) ↦ (Gamma s)⁻¹) s
s : ℂ
hs : -s.re < (↑(n + 1) : ℝ)
rwa : -(s.re + re 1) < (↑n : ℝ)
⊢ -(s + 1).re < (↑n : ℝ)
have rwa₁ : -(s.re + 1) < (↑n : ℝ)
Tactic: rwa [add_re, one_re, neg_add', sub_lt_iff_lt_add, ← Nat.cast_succ]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Beta (goal)
Goal:
n : ℕ
ihn : ∀ (s : ℂ) (hs : -s.re < (↑n : ℝ)), DifferentiableAt ℂ (F := ℂ) (fun (s : ℂ) ↦ (Gamma s)⁻¹) s
s : ℂ
hs : -s.re < (↑(n + 1) : ℝ)
rwa : -(s.re + re 1) < (↑n : ℝ)
rwa₁ : -(s.re + 1) < (↑n : ℝ)
⊢ -(s + 1).re < (↑n : ℝ)
have rwa₂ : -s.re - 1 < (↑n : ℝ)
Tactic: rwa [add_re, one_re, neg_add', sub_lt_iff_lt_add, ← Nat.cast_succ]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Beta (goal)
Goal:
n : ℕ
ihn : ∀ (s : ℂ) (hs : -s.re < (↑n : ℝ)), DifferentiableAt ℂ (F := ℂ) (fun (s : ℂ) ↦ (Gamma s)⁻¹) s
s : ℂ
hs : -s.re < (↑(n + 1) : ℝ)
rwa : -(s.re + re 1) < (↑n : ℝ)
rwa₁ : -(s.re + 1) < (↑n : ℝ)
rwa₂ : -s.re - 1 < (↑n : ℝ)
⊢ -(s + 1).re < (↑n : ℝ)
have rwa₃ : -s.re < HAdd.hAdd (α := ℝ) (↑n : ℝ) 1
Tactic: rwa [add_re, one_re, neg_add', sub_lt_iff_lt_add, ← Nat.cast_succ]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Beta (hypothesis)
Goal:
n : ℕ
ihn : ∀ (s : ℂ) (hs : -s.re < (↑n : ℝ)), DifferentiableAt ℂ (F := ℂ) (fun (s : ℂ) ↦ (Gamma s)⁻¹) s
s : ℂ
hs : -s.re < (↑(n + 1) : ℝ)
⊢ DifferentiableAt ℂ (F := ℂ) (fun (x : ℂ) ↦ x * (Gamma (x + 1))⁻¹) s
have ihn₁ : DifferentiableAt ℂ (F := ℂ) (fun (s : ℂ) ↦ (Gamma s)⁻¹) (s + 1)
Tactic: specialize ihn (s + 1) (by rwa [add_re, one_re, neg_add', sub_lt_iff_lt_add, ← Nat.cast_succ])
Cleared hypotheses: ihn
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Beta (goal)
Goal:
s : ℂ
n : ℕ
hs : -s.re < (↑n : ℝ)
⊢ DifferentiableAt ℂ (F := ℂ) (fun (s : ℂ) ↦ (Gamma s)⁻¹) s
have zero : ∀ (s : ℂ) (hs : -s.re < (↑0 : ℝ)), DifferentiableAt ℂ (F := ℂ) (fun (s : ℂ) ↦ (Gamma s)⁻¹) s
Tactic: induction n generalizing s with
  | zero =>
    rw [Nat.cast_zero, neg_lt_zero] at hs
    suffices ∀ m : ℕ, s ≠ -↑m from (differentiableAt_Gamma _ this).inv (Gamma_ne_zero this)
    rintro m rfl
    apply hs.not_ge
    simp
  | succ n ihn =>
    rw [funext one_div_Gamma_eq_self_mul_one_div_Gamma_add_one]
    specialize ihn (s + 1) (by rwa [add_re, one_re, neg_add', sub_lt_iff_lt_add, ← Nat.cast_succ])
    exact differentiableAt_id.mul (ihn.comp s (f := fun s => s + 1) <|
      differentiableAt_id.add_const (1 : ℂ))
Cleared hypotheses: s, n, hs
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Beta (goal)
Goal:
s : ℂ
n : ℕ
hs : -s.re < (↑n : ℝ)
zero : ∀ (s : ℂ) (hs : -s.re < (↑0 : ℝ)), DifferentiableAt ℂ (F := ℂ) (fun (s : ℂ) ↦ (Gamma s)⁻¹) s
⊢ DifferentiableAt ℂ (F := ℂ) (fun (s : ℂ) ↦ (Gamma s)⁻¹) s
have succ : ∀ (n : ℕ) (ihn : ∀ (s : ℂ) (hs : -s.re < (↑n : ℝ)), DifferentiableAt ℂ (F := ℂ) (fun (s : ℂ) ↦ (Gamma s)⁻¹) s) (s : ℂ)
  (hs : -s.re < (↑(n + 1) : ℝ)), DifferentiableAt ℂ (F := ℂ) (fun (s : ℂ) ↦ (Gamma s)⁻¹) s
Tactic: induction n generalizing s with
  | zero =>
    rw [Nat.cast_zero, neg_lt_zero] at hs
    suffices ∀ m : ℕ, s ≠ -↑m from (differentiableAt_Gamma _ this).inv (Gamma_ne_zero this)
    rintro m rfl
    apply hs.not_ge
    simp
  | succ n ihn =>
    rw [funext one_div_Gamma_eq_self_mul_one_div_Gamma_add_one]
    specialize ihn (s + 1) (by rwa [add_re, one_re, neg_add', sub_lt_iff_lt_add, ← Nat.cast_succ])
    exact differentiableAt_id.mul (ihn.comp s (f := fun s => s + 1) <|
      differentiableAt_id.add_const (1 : ℂ))
Cleared hypotheses: s, n, hs
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Beta (goal)
Goal:
u v : ℂ
hu : 0 < u.re
hv : 0 < v.re
⊢ u.betaIntegral v = Gamma u * Gamma v / Gamma (u + v)
have rw : u.betaIntegral v = Gamma (u + v) * u.betaIntegral v / Gamma (u + v)
Tactic: rw [Gamma_mul_Gamma_eq_betaIntegral hu hv,
      mul_div_cancel_left₀ _ (Gamma_ne_zero_of_re_pos (add_pos hu hv))]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Beta (goal)
Goal:
u v : ℂ
hu : 0 < u.re
hv : 0 < v.re
rw : u.betaIntegral v = Gamma (u + v) * u.betaIntegral v / Gamma (u + v)
⊢ u.betaIntegral v = Gamma u * Gamma v / Gamma (u + v)
have rw₁ : u.betaIntegral v = u.betaIntegral v
Tactic: rw [Gamma_mul_Gamma_eq_betaIntegral hu hv,
      mul_div_cancel_left₀ _ (Gamma_ne_zero_of_re_pos (add_pos hu hv))]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Beta (goal)
Goal:
s : ℂ
this :
  Eq (α := (z : ℂ) → ℂ) (fun (z : ℂ) ↦ (Gamma z)⁻¹ * (Gamma (z + 1 / 2))⁻¹) fun (z : ℂ) ↦
    (Gamma (2 * z))⁻¹ * HPow.hPow (α := ℂ) 2 (2 * z - 1) / (↑√π : ℂ)
⊢ Gamma s * Gamma (s + 1 / 2) = Gamma (2 * s) * HPow.hPow (α := ℂ) 2 (1 - 2 * s) * (↑√π : ℂ)
have h : Gamma s * Gamma (s + 1 / 2) = ((Gamma s)⁻¹ * (Gamma (s + 1 / 2))⁻¹)⁻¹
Tactic: convert! congr_arg Inv.inv (congr_fun this s) using 1
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Beta (goal)
Goal:
s : ℂ
this :
  Eq (α := (z : ℂ) → ℂ) (fun (z : ℂ) ↦ (Gamma z)⁻¹ * (Gamma (z + 1 / 2))⁻¹) fun (z : ℂ) ↦
    (Gamma (2 * z))⁻¹ * HPow.hPow (α := ℂ) 2 (2 * z - 1) / (↑√π : ℂ)
h : Gamma s * Gamma (s + 1 / 2) = ((Gamma s)⁻¹ * (Gamma (s + 1 / 2))⁻¹)⁻¹
⊢ Gamma s * Gamma (s + 1 / 2) = Gamma (2 * s) * HPow.hPow (α := ℂ) 2 (1 - 2 * s) * (↑√π : ℂ)
have h₁ : Gamma (2 * s) * HPow.hPow (α := ℂ) 2 (1 - 2 * s) * (↑√π : ℂ) =
  ((Gamma (2 * s))⁻¹ * HPow.hPow (α := ℂ) 2 (2 * s - 1) / (↑√π : ℂ))⁻¹
Tactic: convert! congr_arg Inv.inv (congr_fun this s) using 1
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Beta (goal)
Goal:
s : ℂ
this :
  Eq (α := (z : ℂ) → ℂ) (fun (z : ℂ) ↦ (Gamma z)⁻¹ * (Gamma (z + 1 / 2))⁻¹) fun (z : ℂ) ↦
    (Gamma (2 * z))⁻¹ * HPow.hPow (α := ℂ) 2 (2 * z - 1) / (↑√π : ℂ)
⊢ Gamma s * Gamma (s + 1 / 2) = ((Gamma s)⁻¹ * (Gamma (s + 1 / 2))⁻¹)⁻¹
have h : Gamma s * Gamma (s + 1 / 2) = (Gamma s)⁻¹⁻¹ * (Gamma (s + 1 / 2))⁻¹⁻¹
Tactic: rw [mul_inv, inv_inv, inv_inv]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Beta (goal)
Goal:
s : ℂ
this :
  Eq (α := (z : ℂ) → ℂ) (fun (z : ℂ) ↦ (Gamma z)⁻¹ * (Gamma (z + 1 / 2))⁻¹) fun (z : ℂ) ↦
    (Gamma (2 * z))⁻¹ * HPow.hPow (α := ℂ) 2 (2 * z - 1) / (↑√π : ℂ)
h : Gamma s * Gamma (s + 1 / 2) = (Gamma s)⁻¹⁻¹ * (Gamma (s + 1 / 2))⁻¹⁻¹
⊢ Gamma s * Gamma (s + 1 / 2) = ((Gamma s)⁻¹ * (Gamma (s + 1 / 2))⁻¹)⁻¹
have h₁ : Gamma s * Gamma (s + 1 / 2) = Gamma s * (Gamma (s + 1 / 2))⁻¹⁻¹
Tactic: rw [mul_inv, inv_inv, inv_inv]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Beta (goal)
Goal:
s : ℂ
this :
  Eq (α := (z : ℂ) → ℂ) (fun (z : ℂ) ↦ (Gamma z)⁻¹ * (Gamma (z + 1 / 2))⁻¹) fun (z : ℂ) ↦
    (Gamma (2 * z))⁻¹ * HPow.hPow (α := ℂ) 2 (2 * z - 1) / (↑√π : ℂ)
h : Gamma s * Gamma (s + 1 / 2) = (Gamma s)⁻¹⁻¹ * (Gamma (s + 1 / 2))⁻¹⁻¹
h₁ : Gamma s * Gamma (s + 1 / 2) = Gamma s * (Gamma (s + 1 / 2))⁻¹⁻¹
⊢ Gamma s * Gamma (s + 1 / 2) = ((Gamma s)⁻¹ * (Gamma (s + 1 / 2))⁻¹)⁻¹
have h₂ : Gamma s * Gamma (s + 1 / 2) = Gamma s * Gamma (s + 1 / 2)
Tactic: rw [mul_inv, inv_inv, inv_inv]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Beta (goal)
Goal:
s : ℂ
this :
  Eq (α := (z : ℂ) → ℂ) (fun (z : ℂ) ↦ (Gamma z)⁻¹ * (Gamma (z + 1 / 2))⁻¹) fun (z : ℂ) ↦
    (Gamma (2 * z))⁻¹ * HPow.hPow (α := ℂ) 2 (2 * z - 1) / (↑√π : ℂ)
⊢ Gamma (2 * s) * HPow.hPow (α := ℂ) 2 (1 - 2 * s) * (↑√π : ℂ) =
    ((Gamma (2 * s))⁻¹ * HPow.hPow (α := ℂ) 2 (2 * s - 1) / (↑√π : ℂ))⁻¹
have h : Gamma (2 * s) * HPow.hPow (α := ℂ) 2 (1 - 2 * s) * (↑√π : ℂ) =
  ((Gamma (2 * s))⁻¹ * HPow.hPow (α := ℂ) 2 (2 * s - 1) * (↑√π : ℂ)⁻¹)⁻¹
Tactic: rw [div_eq_mul_inv, mul_inv, mul_inv, inv_inv, inv_inv, ← cpow_neg, neg_sub]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Beta (goal)
Goal:
s : ℂ
this :
  Eq (α := (z : ℂ) → ℂ) (fun (z : ℂ) ↦ (Gamma z)⁻¹ * (Gamma (z + 1 / 2))⁻¹) fun (z : ℂ) ↦
    (Gamma (2 * z))⁻¹ * HPow.hPow (α := ℂ) 2 (2 * z - 1) / (↑√π : ℂ)
h :
  Gamma (2 * s) * HPow.hPow (α := ℂ) 2 (1 - 2 * s) * (↑√π : ℂ) =
    ((Gamma (2 * s))⁻¹ * HPow.hPow (α := ℂ) 2 (2 * s - 1) * (↑√π : ℂ)⁻¹)⁻¹
⊢ Gamma (2 * s) * HPow.hPow (α := ℂ) 2 (1 - 2 * s) * (↑√π : ℂ) =
    ((Gamma (2 * s))⁻¹ * HPow.hPow (α := ℂ) 2 (2 * s - 1) / (↑√π : ℂ))⁻¹
have h₁ : Gamma (2 * s) * HPow.hPow (α := ℂ) 2 (1 - 2 * s) * (↑√π : ℂ) =
  ((Gamma (2 * s))⁻¹ * HPow.hPow (α := ℂ) 2 (2 * s - 1))⁻¹ * (↑√π : ℂ)⁻¹⁻¹
Tactic: rw [div_eq_mul_inv, mul_inv, mul_inv, inv_inv, inv_inv, ← cpow_neg, neg_sub]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Beta (goal)
Goal:
s : ℂ
this :
  Eq (α := (z : ℂ) → ℂ) (fun (z : ℂ) ↦ (Gamma z)⁻¹ * (Gamma (z + 1 / 2))⁻¹) fun (z : ℂ) ↦
    (Gamma (2 * z))⁻¹ * HPow.hPow (α := ℂ) 2 (2 * z - 1) / (↑√π : ℂ)
h :
  Gamma (2 * s) * HPow.hPow (α := ℂ) 2 (1 - 2 * s) * (↑√π : ℂ) =
    ((Gamma (2 * s))⁻¹ * HPow.hPow (α := ℂ) 2 (2 * s - 1) * (↑√π : ℂ)⁻¹)⁻¹
h₁ :
  Gamma (2 * s) * HPow.hPow (α := ℂ) 2 (1 - 2 * s) * (↑√π : ℂ) =
    ((Gamma (2 * s))⁻¹ * HPow.hPow (α := ℂ) 2 (2 * s - 1))⁻¹ * (↑√π : ℂ)⁻¹⁻¹
⊢ Gamma (2 * s) * HPow.hPow (α := ℂ) 2 (1 - 2 * s) * (↑√π : ℂ) =
    ((Gamma (2 * s))⁻¹ * HPow.hPow (α := ℂ) 2 (2 * s - 1) / (↑√π : ℂ))⁻¹
have h₂ : Gamma (2 * s) * HPow.hPow (α := ℂ) 2 (1 - 2 * s) * (↑√π : ℂ) =
  (Gamma (2 * s))⁻¹⁻¹ * (HPow.hPow (α := ℂ) 2 (2 * s - 1))⁻¹ * (↑√π : ℂ)⁻¹⁻¹
Tactic: rw [div_eq_mul_inv, mul_inv, mul_inv, inv_inv, inv_inv, ← cpow_neg, neg_sub]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Beta (goal)
Goal:
s : ℂ
this :
  Eq (α := (z : ℂ) → ℂ) (fun (z : ℂ) ↦ (Gamma z)⁻¹ * (Gamma (z + 1 / 2))⁻¹) fun (z : ℂ) ↦
    (Gamma (2 * z))⁻¹ * HPow.hPow (α := ℂ) 2 (2 * z - 1) / (↑√π : ℂ)
h :
  Gamma (2 * s) * HPow.hPow (α := ℂ) 2 (1 - 2 * s) * (↑√π : ℂ) =
    ((Gamma (2 * s))⁻¹ * HPow.hPow (α := ℂ) 2 (2 * s - 1) * (↑√π : ℂ)⁻¹)⁻¹
h₁ :
  Gamma (2 * s) * HPow.hPow (α := ℂ) 2 (1 - 2 * s) * (↑√π : ℂ) =
    ((Gamma (2 * s))⁻¹ * HPow.hPow (α := ℂ) 2 (2 * s - 1))⁻¹ * (↑√π : ℂ)⁻¹⁻¹
h₂ :
  Gamma (2 * s) * HPow.hPow (α := ℂ) 2 (1 - 2 * s) * (↑√π : ℂ) =
    (Gamma (2 * s))⁻¹⁻¹ * (HPow.hPow (α := ℂ) 2 (2 * s - 1))⁻¹ * (↑√π : ℂ)⁻¹⁻¹
⊢ Gamma (2 * s) * HPow.hPow (α := ℂ) 2 (1 - 2 * s) * (↑√π : ℂ) =
    ((Gamma (2 * s))⁻¹ * HPow.hPow (α := ℂ) 2 (2 * s - 1) / (↑√π : ℂ))⁻¹
have h₃ : Gamma (2 * s) * HPow.hPow (α := ℂ) 2 (1 - 2 * s) * (↑√π : ℂ) =
  Gamma (2 * s) * (HPow.hPow (α := ℂ) 2 (2 * s - 1))⁻¹ * (↑√π : ℂ)⁻¹⁻¹
Tactic: rw [div_eq_mul_inv, mul_inv, mul_inv, inv_inv, inv_inv, ← cpow_neg, neg_sub]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Beta (goal)
Goal:
s : ℂ
this :
  Eq (α := (z : ℂ) → ℂ) (fun (z : ℂ) ↦ (Gamma z)⁻¹ * (Gamma (z + 1 / 2))⁻¹) fun (z : ℂ) ↦
    (Gamma (2 * z))⁻¹ * HPow.hPow (α := ℂ) 2 (2 * z - 1) / (↑√π : ℂ)
h :
  Gamma (2 * s) * HPow.hPow (α := ℂ) 2 (1 - 2 * s) * (↑√π : ℂ) =
    ((Gamma (2 * s))⁻¹ * HPow.hPow (α := ℂ) 2 (2 * s - 1) * (↑√π : ℂ)⁻¹)⁻¹
h₁ :
  Gamma (2 * s) * HPow.hPow (α := ℂ) 2 (1 - 2 * s) * (↑√π : ℂ) =
    ((Gamma (2 * s))⁻¹ * HPow.hPow (α := ℂ) 2 (2 * s - 1))⁻¹ * (↑√π : ℂ)⁻¹⁻¹
h₂ :
  Gamma (2 * s) * HPow.hPow (α := ℂ) 2 (1 - 2 * s) * (↑√π : ℂ) =
    (Gamma (2 * s))⁻¹⁻¹ * (HPow.hPow (α := ℂ) 2 (2 * s - 1))⁻¹ * (↑√π : ℂ)⁻¹⁻¹
h₃ :
  Gamma (2 * s) * HPow.hPow (α := ℂ) 2 (1 - 2 * s) * (↑√π : ℂ) =
    Gamma (2 * s) * (HPow.hPow (α := ℂ) 2 (2 * s - 1))⁻¹ * (↑√π : ℂ)⁻¹⁻¹
⊢ Gamma (2 * s) * HPow.hPow (α := ℂ) 2 (1 - 2 * s) * (↑√π : ℂ) =
    ((Gamma (2 * s))⁻¹ * HPow.hPow (α := ℂ) 2 (2 * s - 1) / (↑√π : ℂ))⁻¹
have h₄ : Gamma (2 * s) * HPow.hPow (α := ℂ) 2 (1 - 2 * s) * (↑√π : ℂ) =
  Gamma (2 * s) * (HPow.hPow (α := ℂ) 2 (2 * s - 1))⁻¹ * (↑√π : ℂ)
Tactic: rw [div_eq_mul_inv, mul_inv, mul_inv, inv_inv, inv_inv, ← cpow_neg, neg_sub]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Beta (goal)
Goal:
s : ℂ
this :
  Eq (α := (z : ℂ) → ℂ) (fun (z : ℂ) ↦ (Gamma z)⁻¹ * (Gamma (z + 1 / 2))⁻¹) fun (z : ℂ) ↦
    (Gamma (2 * z))⁻¹ * HPow.hPow (α := ℂ) 2 (2 * z - 1) / (↑√π : ℂ)
h :
  Gamma (2 * s) * HPow.hPow (α := ℂ) 2 (1 - 2 * s) * (↑√π : ℂ) =
    ((Gamma (2 * s))⁻¹ * HPow.hPow (α := ℂ) 2 (2 * s - 1) * (↑√π : ℂ)⁻¹)⁻¹
h₁ :
  Gamma (2 * s) * HPow.hPow (α := ℂ) 2 (1 - 2 * s) * (↑√π : ℂ) =
    ((Gamma (2 * s))⁻¹ * HPow.hPow (α := ℂ) 2 (2 * s - 1))⁻¹ * (↑√π : ℂ)⁻¹⁻¹
h₂ :
  Gamma (2 * s) * HPow.hPow (α := ℂ) 2 (1 - 2 * s) * (↑√π : ℂ) =
    (Gamma (2 * s))⁻¹⁻¹ * (HPow.hPow (α := ℂ) 2 (2 * s - 1))⁻¹ * (↑√π : ℂ)⁻¹⁻¹
h₃ :
  Gamma (2 * s) * HPow.hPow (α := ℂ) 2 (1 - 2 * s) * (↑√π : ℂ) =
    Gamma (2 * s) * (HPow.hPow (α := ℂ) 2 (2 * s - 1))⁻¹ * (↑√π : ℂ)⁻¹⁻¹
h₄ :
  Gamma (2 * s) * HPow.hPow (α := ℂ) 2 (1 - 2 * s) * (↑√π : ℂ) =
    Gamma (2 * s) * (HPow.hPow (α := ℂ) 2 (2 * s - 1))⁻¹ * (↑√π : ℂ)
⊢ Gamma (2 * s) * HPow.hPow (α := ℂ) 2 (1 - 2 * s) * (↑√π : ℂ) =
    ((Gamma (2 * s))⁻¹ * HPow.hPow (α := ℂ) 2 (2 * s - 1) / (↑√π : ℂ))⁻¹
have h₅ : Gamma (2 * s) * HPow.hPow (α := ℂ) 2 (1 - 2 * s) * (↑√π : ℂ) =
  Gamma (2 * s) * HPow.hPow (α := ℂ) 2 (-(2 * s - 1)) * (↑√π : ℂ)
Tactic: rw [div_eq_mul_inv, mul_inv, mul_inv, inv_inv, inv_inv, ← cpow_neg, neg_sub]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Beta (goal)
Goal:
s : ℂ
this :
  Eq (α := (z : ℂ) → ℂ) (fun (z : ℂ) ↦ (Gamma z)⁻¹ * (Gamma (z + 1 / 2))⁻¹) fun (z : ℂ) ↦
    (Gamma (2 * z))⁻¹ * HPow.hPow (α := ℂ) 2 (2 * z - 1) / (↑√π : ℂ)
h :
  Gamma (2 * s) * HPow.hPow (α := ℂ) 2 (1 - 2 * s) * (↑√π : ℂ) =
    ((Gamma (2 * s))⁻¹ * HPow.hPow (α := ℂ) 2 (2 * s - 1) * (↑√π : ℂ)⁻¹)⁻¹
h₁ :
  Gamma (2 * s) * HPow.hPow (α := ℂ) 2 (1 - 2 * s) * (↑√π : ℂ) =
    ((Gamma (2 * s))⁻¹ * HPow.hPow (α := ℂ) 2 (2 * s - 1))⁻¹ * (↑√π : ℂ)⁻¹⁻¹
h₂ :
  Gamma (2 * s) * HPow.hPow (α := ℂ) 2 (1 - 2 * s) * (↑√π : ℂ) =
    (Gamma (2 * s))⁻¹⁻¹ * (HPow.hPow (α := ℂ) 2 (2 * s - 1))⁻¹ * (↑√π : ℂ)⁻¹⁻¹
h₃ :
  Gamma (2 * s) * HPow.hPow (α := ℂ) 2 (1 - 2 * s) * (↑√π : ℂ) =
    Gamma (2 * s) * (HPow.hPow (α := ℂ) 2 (2 * s - 1))⁻¹ * (↑√π : ℂ)⁻¹⁻¹
h₄ :
  Gamma (2 * s) * HPow.hPow (α := ℂ) 2 (1 - 2 * s) * (↑√π : ℂ) =
    Gamma (2 * s) * (HPow.hPow (α := ℂ) 2 (2 * s - 1))⁻¹ * (↑√π : ℂ)
h₅ :
  Gamma (2 * s) * HPow.hPow (α := ℂ) 2 (1 - 2 * s) * (↑√π : ℂ) =
    Gamma (2 * s) * HPow.hPow (α := ℂ) 2 (-(2 * s - 1)) * (↑√π : ℂ)
⊢ Gamma (2 * s) * HPow.hPow (α := ℂ) 2 (1 - 2 * s) * (↑√π : ℂ) =
    ((Gamma (2 * s))⁻¹ * HPow.hPow (α := ℂ) 2 (2 * s - 1) / (↑√π : ℂ))⁻¹
have h₆ : Gamma (2 * s) * HPow.hPow (α := ℂ) 2 (1 - 2 * s) * (↑√π : ℂ) =
  Gamma (2 * s) * HPow.hPow (α := ℂ) 2 (1 - 2 * s) * (↑√π : ℂ)
Tactic: rw [div_eq_mul_inv, mul_inv, mul_inv, inv_inv, inv_inv, ← cpow_neg, neg_sub]