awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Beta (goal)
Goal:
s : ℂ
⊢ Gamma s * Gamma (s + 1 / 2) = Gamma (2 * s) * HPow.hPow (α := ℂ) 2 (1 - 2 * s) * (↑√π : ℂ)
have suffices : Eq (α := (z : ℂ) → ℂ) (fun (z : ℂ) ↦ (Gamma z)⁻¹ * (Gamma (z + 1 / 2))⁻¹) fun (z : ℂ) ↦
  (Gamma (2 * z))⁻¹ * HPow.hPow (α := ℂ) 2 (2 * z - 1) / (↑√π : ℂ)
Tactic: suffices (fun z => (Gamma z)⁻¹ * (Gamma (z + 1 / 2))⁻¹) = fun z =>
      (Gamma (2 * z))⁻¹ * (2 : ℂ) ^ (2 * z - 1) / ↑(√π) by
    convert! congr_arg Inv.inv (congr_fun this s) using 1
    · rw [mul_inv, inv_inv, inv_inv]
    · 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 : ℂ
⊢ AnalyticOnNhd ℂ (F := ℂ) (fun (z : ℂ) ↦ (Gamma z)⁻¹ * (Gamma (z + 1 / 2))⁻¹) univ
have refine : DifferentiableOn ℂ (F := ℂ) (fun (z : ℂ) ↦ (Gamma z)⁻¹ * (Gamma (z + 1 / 2))⁻¹) univ
Tactic: refine DifferentiableOn.analyticOnNhd ?_ isOpen_univ
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Beta (goal)
Goal:
s : ℂ
⊢ DifferentiableOn ℂ (F := ℂ) (fun (z : ℂ) ↦ (Gamma z)⁻¹ * (Gamma (z + 1 / 2))⁻¹) univ
have refine : Differentiable ℂ (F := ℂ) fun (z : ℂ) ↦ (Gamma (z + 1 / 2))⁻¹
Tactic: refine (differentiable_one_div_Gamma.mul ?_).differentiableOn
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Beta (hypothesis)
Goal:
s : ℂ
⊢ Eq (α := (z : ℂ) → ℂ) (fun (z : ℂ) ↦ (Gamma z)⁻¹ * (Gamma (z + 1 / 2))⁻¹) fun (z : ℂ) ↦
    (Gamma (2 * z))⁻¹ * HPow.hPow (α := ℂ) 2 (2 * z - 1) / (↑√π : ℂ)
have h1 : AnalyticOnNhd ℂ (F := ℂ) (fun (z : ℂ) ↦ (Gamma z)⁻¹ * (Gamma (z + 1 / 2))⁻¹) univ
Tactic: have h1 : AnalyticOnNhd ℂ (fun z : ℂ => (Gamma z)⁻¹ * (Gamma (z + 1 / 2))⁻¹) univ := by
    refine DifferentiableOn.analyticOnNhd ?_ isOpen_univ
    refine (differentiable_one_div_Gamma.mul ?_).differentiableOn
    exact differentiable_one_div_Gamma.comp (differentiable_id.add (differentiable_const _))
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Beta (goal)
Goal:
s : ℂ
h1 : AnalyticOnNhd ℂ (F := ℂ) (fun (z : ℂ) ↦ (Gamma z)⁻¹ * (Gamma (z + 1 / 2))⁻¹) univ
⊢ AnalyticOnNhd ℂ (F := ℂ) (fun (z : ℂ) ↦ (Gamma (2 * z))⁻¹ * HPow.hPow (α := ℂ) 2 (2 * z - 1) / (↑√π : ℂ)) univ
have refine : DifferentiableOn ℂ (F := ℂ) (fun (z : ℂ) ↦ (Gamma (2 * z))⁻¹ * HPow.hPow (α := ℂ) 2 (2 * z - 1) / (↑√π : ℂ)) univ
Tactic: refine DifferentiableOn.analyticOnNhd ?_ isOpen_univ
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Beta (goal)
Goal:
s : ℂ
h1 : AnalyticOnNhd ℂ (F := ℂ) (fun (z : ℂ) ↦ (Gamma z)⁻¹ * (Gamma (z + 1 / 2))⁻¹) univ
⊢ DifferentiableOn ℂ (F := ℂ) (fun (z : ℂ) ↦ (Gamma (2 * z))⁻¹ * HPow.hPow (α := ℂ) 2 (2 * z - 1) / (↑√π : ℂ)) univ
have refine : Differentiable ℂ (F := ℂ) fun (z : ℂ) ↦ (Gamma (2 * z))⁻¹ * HPow.hPow (α := ℂ) 2 (2 * z - 1)
Tactic: refine (Differentiable.mul ?_ (differentiable_const _)).differentiableOn
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Beta (goal)
Goal:
s : ℂ
h1 : AnalyticOnNhd ℂ (F := ℂ) (fun (z : ℂ) ↦ (Gamma z)⁻¹ * (Gamma (z + 1 / 2))⁻¹) univ
⊢ Differentiable ℂ (F := ℂ) fun (z : ℂ) ↦ (Gamma (2 * z))⁻¹ * HPow.hPow (α := ℂ) 2 (2 * z - 1)
have ha : Differentiable ℂ (F := ℂ) fun (z : ℂ) ↦ (Gamma (2 * z))⁻¹
Tactic: apply Differentiable.mul
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Beta (goal)
Goal:
s : ℂ
h1 : AnalyticOnNhd ℂ (F := ℂ) (fun (z : ℂ) ↦ (Gamma z)⁻¹ * (Gamma (z + 1 / 2))⁻¹) univ
ha : Differentiable ℂ (F := ℂ) fun (z : ℂ) ↦ (Gamma (2 * z))⁻¹
⊢ Differentiable ℂ (F := ℂ) fun (z : ℂ) ↦ (Gamma (2 * z))⁻¹ * HPow.hPow (α := ℂ) 2 (2 * z - 1)
have hb : Differentiable ℂ (F := ℂ) fun (z : ℂ) ↦ HPow.hPow (α := ℂ) 2 (2 * z - 1)
Tactic: apply Differentiable.mul
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Beta (goal)
Goal:
s : ℂ
h1 : AnalyticOnNhd ℂ (F := ℂ) (fun (z : ℂ) ↦ (Gamma z)⁻¹ * (Gamma (z + 1 / 2))⁻¹) univ
⊢ Differentiable ℂ (F := ℂ) fun (z : ℂ) ↦ HPow.hPow (α := ℂ) 2 (2 * z - 1)
have hb : ∀ (t : ℂ), DifferentiableAt ℂ (F := ℂ) (fun (z : ℂ) ↦ 2 * z - 1) t
Tactic: refine fun t => DifferentiableAt.const_cpow ?_ (Or.inl two_ne_zero)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Beta (hypothesis)
Goal:
s : ℂ
h1 : AnalyticOnNhd ℂ (F := ℂ) (fun (z : ℂ) ↦ (Gamma z)⁻¹ * (Gamma (z + 1 / 2))⁻¹) univ
⊢ Eq (α := (z : ℂ) → ℂ) (fun (z : ℂ) ↦ (Gamma z)⁻¹ * (Gamma (z + 1 / 2))⁻¹) fun (z : ℂ) ↦
    (Gamma (2 * z))⁻¹ * HPow.hPow (α := ℂ) 2 (2 * z - 1) / (↑√π : ℂ)
have h2 : AnalyticOnNhd ℂ (F := ℂ) (fun (z : ℂ) ↦ (Gamma (2 * z))⁻¹ * HPow.hPow (α := ℂ) 2 (2 * z - 1) / (↑√π : ℂ)) univ
Tactic: have h2 : AnalyticOnNhd ℂ
      (fun z => (Gamma (2 * z))⁻¹ * (2 : ℂ) ^ (2 * z - 1) / ↑(√π)) univ := by
    refine DifferentiableOn.analyticOnNhd ?_ isOpen_univ
    refine (Differentiable.mul ?_ (differentiable_const _)).differentiableOn
    apply Differentiable.mul
    · exact differentiable_one_div_Gamma.comp (differentiable_id.const_mul _)
    · refine fun t => DifferentiableAt.const_cpow ?_ (Or.inl two_ne_zero)
      exact DifferentiableAt.sub_const (differentiableAt_id.const_mul _) _
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Beta (goal)
Goal:
s : ℂ
h1 : AnalyticOnNhd ℂ (F := ℂ) (fun (z : ℂ) ↦ (Gamma z)⁻¹ * (Gamma (z + 1 / 2))⁻¹) univ
h2 : AnalyticOnNhd ℂ (F := ℂ) (fun (z : ℂ) ↦ (Gamma (2 * z))⁻¹ * HPow.hPow (α := ℂ) 2 (2 * z - 1) / (↑√π : ℂ)) univ
⊢ Tendsto ofReal (𝓝[≠] 1) (𝓝[≠] 1)
have rw : Tendsto ofReal (𝓝[≠] 1) (𝓝 1) ∧ ∀ᶠ (n : ℝ) in 𝓝[≠] 1, Membership.mem (γ := Set ℂ) {1}ᶜ (↑n : ℂ)
Tactic: rw [tendsto_nhdsWithin_iff]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Beta (goal)
Goal:
s : ℂ
h1 : AnalyticOnNhd ℂ (F := ℂ) (fun (z : ℂ) ↦ (Gamma z)⁻¹ * (Gamma (z + 1 / 2))⁻¹) univ
h2 : AnalyticOnNhd ℂ (F := ℂ) (fun (z : ℂ) ↦ (Gamma (2 * z))⁻¹ * HPow.hPow (α := ℂ) 2 (2 * z - 1) / (↑√π : ℂ)) univ
⊢ Tendsto ofReal (𝓝[≠] 1) (𝓝 1) ∧ ∀ᶠ (n : ℝ) in 𝓝[≠] 1, Membership.mem (γ := Set ℂ) {1}ᶜ (↑n : ℂ)
have left : Tendsto ofReal (𝓝[≠] 1) (𝓝 1)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Beta (goal)
Goal:
s : ℂ
h1 : AnalyticOnNhd ℂ (F := ℂ) (fun (z : ℂ) ↦ (Gamma z)⁻¹ * (Gamma (z + 1 / 2))⁻¹) univ
h2 : AnalyticOnNhd ℂ (F := ℂ) (fun (z : ℂ) ↦ (Gamma (2 * z))⁻¹ * HPow.hPow (α := ℂ) 2 (2 * z - 1) / (↑√π : ℂ)) univ
left : Tendsto ofReal (𝓝[≠] 1) (𝓝 1)
⊢ Tendsto ofReal (𝓝[≠] 1) (𝓝 1) ∧ ∀ᶠ (n : ℝ) in 𝓝[≠] 1, Membership.mem (γ := Set ℂ) {1}ᶜ (↑n : ℂ)
have right : ∀ᶠ (n : ℝ) in 𝓝[≠] 1, Membership.mem (γ := Set ℂ) {1}ᶜ (↑n : ℂ)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Beta (hypothesis)
Goal:
s : ℂ
h1 : AnalyticOnNhd ℂ (F := ℂ) (fun (z : ℂ) ↦ (Gamma z)⁻¹ * (Gamma (z + 1 / 2))⁻¹) univ
h2 : AnalyticOnNhd ℂ (F := ℂ) (fun (z : ℂ) ↦ (Gamma (2 * z))⁻¹ * HPow.hPow (α := ℂ) 2 (2 * z - 1) / (↑√π : ℂ)) univ
⊢ Eq (α := (z : ℂ) → ℂ) (fun (z : ℂ) ↦ (Gamma z)⁻¹ * (Gamma (z + 1 / 2))⁻¹) fun (z : ℂ) ↦
    (Gamma (2 * z))⁻¹ * HPow.hPow (α := ℂ) 2 (2 * z - 1) / (↑√π : ℂ)
have h3 : Tendsto ofReal (𝓝[≠] 1) (𝓝[≠] 1)
Tactic: have h3 : Tendsto ((↑) : ℝ → ℂ) (𝓝[≠] 1) (𝓝[≠] 1) := by
    rw [tendsto_nhdsWithin_iff]; constructor
    · exact tendsto_nhdsWithin_of_tendsto_nhds continuous_ofReal.continuousAt
    · exact eventually_nhdsWithin_iff.mpr (Eventually.of_forall fun t ht => ofReal_ne_one.mpr ht)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Beta (goal)
Goal:
s : ℂ
h1 : AnalyticOnNhd ℂ (F := ℂ) (fun (z : ℂ) ↦ (Gamma z)⁻¹ * (Gamma (z + 1 / 2))⁻¹) univ
h2 : AnalyticOnNhd ℂ (F := ℂ) (fun (z : ℂ) ↦ (Gamma (2 * z))⁻¹ * HPow.hPow (α := ℂ) 2 (2 * z - 1) / (↑√π : ℂ)) univ
h3 : Tendsto ofReal (𝓝[≠] 1) (𝓝[≠] 1)
⊢ Eq (α := (z : ℂ) → ℂ) (fun (z : ℂ) ↦ (Gamma z)⁻¹ * (Gamma (z + 1 / 2))⁻¹) fun (z : ℂ) ↦
    (Gamma (2 * z))⁻¹ * HPow.hPow (α := ℂ) 2 (2 * z - 1) / (↑√π : ℂ)
have refine : ∃ᶠ (x : ℝ) in 𝓝[≠] 1,
  (Gamma (↑x : ℂ))⁻¹ * (Gamma ((↑x : ℂ) + 1 / 2))⁻¹ =
    (Gamma (2 * (↑x : ℂ)))⁻¹ * HPow.hPow (α := ℂ) 2 (2 * (↑x : ℂ) - 1) / (↑√π : ℂ)
Tactic: refine AnalyticOnNhd.eq_of_frequently_eq h1 h2 (h3.frequently ?_)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Beta (goal)
Goal:
s : ℂ
h1 : AnalyticOnNhd ℂ (F := ℂ) (fun (z : ℂ) ↦ (Gamma z)⁻¹ * (Gamma (z + 1 / 2))⁻¹) univ
h2 : AnalyticOnNhd ℂ (F := ℂ) (fun (z : ℂ) ↦ (Gamma (2 * z))⁻¹ * HPow.hPow (α := ℂ) 2 (2 * z - 1) / (↑√π : ℂ)) univ
h3 : Tendsto ofReal (𝓝[≠] 1) (𝓝[≠] 1)
⊢ ∃ᶠ (x : ℝ) in 𝓝[≠] 1,
    (Gamma (↑x : ℂ))⁻¹ * (Gamma ((↑x : ℂ) + 1 / 2))⁻¹ =
      (Gamma (2 * (↑x : ℂ)))⁻¹ * HPow.hPow (α := ℂ) 2 (2 * (↑x : ℂ) - 1) / (↑√π : ℂ)
have refine : ∀ᶠ (x : ℝ) in 𝓝 1,
  (Gamma (↑x : ℂ))⁻¹ * (Gamma ((↑x : ℂ) + 1 / 2))⁻¹ =
    (Gamma (2 * (↑x : ℂ)))⁻¹ * HPow.hPow (α := ℂ) 2 (2 * (↑x : ℂ) - 1) / (↑√π : ℂ)
Tactic: refine ((Eventually.filter_mono nhdsWithin_le_nhds) ?_).frequently
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Beta (goal)
Goal:
s : ℂ
h1 : AnalyticOnNhd ℂ (F := ℂ) (fun (z : ℂ) ↦ (Gamma z)⁻¹ * (Gamma (z + 1 / 2))⁻¹) univ
h2 : AnalyticOnNhd ℂ (F := ℂ) (fun (z : ℂ) ↦ (Gamma (2 * z))⁻¹ * HPow.hPow (α := ℂ) 2 (2 * z - 1) / (↑√π : ℂ)) univ
h3 : Tendsto ofReal (𝓝[≠] 1) (𝓝[≠] 1)
⊢ ∀ᶠ (x : ℝ) in 𝓝 1,
    (Gamma (↑x : ℂ))⁻¹ * (Gamma ((↑x : ℂ) + 1 / 2))⁻¹ =
      (Gamma (2 * (↑x : ℂ)))⁻¹ * HPow.hPow (α := ℂ) 2 (2 * (↑x : ℂ) - 1) / (↑√π : ℂ)
have refine : ∀ (t : ℝ) (ht : 0 < t),
  (Gamma (↑t : ℂ))⁻¹ * (Gamma ((↑t : ℂ) + 1 / 2))⁻¹ =
    (Gamma (2 * (↑t : ℂ)))⁻¹ * HPow.hPow (α := ℂ) 2 (2 * (↑t : ℂ) - 1) / (↑√π : ℂ)
Tactic: refine (eventually_gt_nhds zero_lt_one).mp (Eventually.of_forall fun t ht => ?_)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Beta (goal)
Goal:
s : ℂ
h1 : AnalyticOnNhd ℂ (F := ℂ) (fun (z : ℂ) ↦ (Gamma z)⁻¹ * (Gamma (z + 1 / 2))⁻¹) univ
h2 : AnalyticOnNhd ℂ (F := ℂ) (fun (z : ℂ) ↦ (Gamma (2 * z))⁻¹ * HPow.hPow (α := ℂ) 2 (2 * z - 1) / (↑√π : ℂ)) univ
h3 : Tendsto ofReal (𝓝[≠] 1) (𝓝[≠] 1)
t : ℝ
ht : 0 < t
⊢ (↑2 : ℂ) = 2
have norm_cast : Eq (α := ℕ) 2 2
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Beta (goal)
Goal:
s : ℂ
h1 : AnalyticOnNhd ℂ (F := ℂ) (fun (z : ℂ) ↦ (Gamma z)⁻¹ * (Gamma (z + 1 / 2))⁻¹) univ
h2 : AnalyticOnNhd ℂ (F := ℂ) (fun (z : ℂ) ↦ (Gamma (2 * z))⁻¹ * HPow.hPow (α := ℂ) 2 (2 * z - 1) / (↑√π : ℂ)) univ
h3 : Tendsto ofReal (𝓝[≠] 1) (𝓝[≠] 1)
t : ℝ
ht : 0 < t
⊢ (Gamma (↑t : ℂ))⁻¹ * (Gamma ((↑t : ℂ) + 1 / 2))⁻¹ =
    (Gamma (2 * (↑t : ℂ)))⁻¹ * HPow.hPow (α := ℂ) 2 (2 * (↑t : ℂ) - 1) / (↑√π : ℂ)
have rw : (Gamma (↑t : ℂ) * Gamma ((↑t : ℂ) + 1 / 2))⁻¹ =
  (Gamma (2 * (↑t : ℂ)))⁻¹ * HPow.hPow (α := ℂ) 2 (2 * (↑t : ℂ) - 1) / (↑√π : ℂ)
Tactic: rw [← mul_inv, Gamma_ofReal, (by simp : (t : ℂ) + 1 / 2 = ↑(t + 1 / 2)), Gamma_ofReal, ←
    ofReal_mul, Gamma_mul_Gamma_add_half_of_pos ht, ofReal_mul, ofReal_mul, ← Gamma_ofReal,
    mul_inv, mul_inv, (by simp : 2 * (t : ℂ) = ↑(2 * t)), Gamma_ofReal,
    ofReal_cpow zero_le_two, show (2 : ℝ) = (2 : ℂ) by norm_cast, ← cpow_neg, ofReal_sub,
    ofReal_one, neg_sub, ← div_eq_mul_inv]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Beta (goal)
Goal:
s : ℂ
h1 : AnalyticOnNhd ℂ (F := ℂ) (fun (z : ℂ) ↦ (Gamma z)⁻¹ * (Gamma (z + 1 / 2))⁻¹) univ
h2 : AnalyticOnNhd ℂ (F := ℂ) (fun (z : ℂ) ↦ (Gamma (2 * z))⁻¹ * HPow.hPow (α := ℂ) 2 (2 * z - 1) / (↑√π : ℂ)) univ
h3 : Tendsto ofReal (𝓝[≠] 1) (𝓝[≠] 1)
t : ℝ
ht : 0 < t
rw :
  (Gamma (↑t : ℂ) * Gamma ((↑t : ℂ) + 1 / 2))⁻¹ =
    (Gamma (2 * (↑t : ℂ)))⁻¹ * HPow.hPow (α := ℂ) 2 (2 * (↑t : ℂ) - 1) / (↑√π : ℂ)
⊢ (Gamma (↑t : ℂ))⁻¹ * (Gamma ((↑t : ℂ) + 1 / 2))⁻¹ =
    (Gamma (2 * (↑t : ℂ)))⁻¹ * HPow.hPow (α := ℂ) 2 (2 * (↑t : ℂ) - 1) / (↑√π : ℂ)
have rw₁ : ((↑(Real.Gamma t) : ℂ) * Gamma ((↑t : ℂ) + 1 / 2))⁻¹ =
  (Gamma (2 * (↑t : ℂ)))⁻¹ * HPow.hPow (α := ℂ) 2 (2 * (↑t : ℂ) - 1) / (↑√π : ℂ)
Tactic: rw [← mul_inv, Gamma_ofReal, (by simp : (t : ℂ) + 1 / 2 = ↑(t + 1 / 2)), Gamma_ofReal, ←
    ofReal_mul, Gamma_mul_Gamma_add_half_of_pos ht, ofReal_mul, ofReal_mul, ← Gamma_ofReal,
    mul_inv, mul_inv, (by simp : 2 * (t : ℂ) = ↑(2 * t)), Gamma_ofReal,
    ofReal_cpow zero_le_two, show (2 : ℝ) = (2 : ℂ) by norm_cast, ← cpow_neg, ofReal_sub,
    ofReal_one, neg_sub, ← div_eq_mul_inv]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Beta (goal)
Goal:
s : ℂ
h1 : AnalyticOnNhd ℂ (F := ℂ) (fun (z : ℂ) ↦ (Gamma z)⁻¹ * (Gamma (z + 1 / 2))⁻¹) univ
h2 : AnalyticOnNhd ℂ (F := ℂ) (fun (z : ℂ) ↦ (Gamma (2 * z))⁻¹ * HPow.hPow (α := ℂ) 2 (2 * z - 1) / (↑√π : ℂ)) univ
h3 : Tendsto ofReal (𝓝[≠] 1) (𝓝[≠] 1)
t : ℝ
ht : 0 < t
rw :
  (Gamma (↑t : ℂ) * Gamma ((↑t : ℂ) + 1 / 2))⁻¹ =
    (Gamma (2 * (↑t : ℂ)))⁻¹ * HPow.hPow (α := ℂ) 2 (2 * (↑t : ℂ) - 1) / (↑√π : ℂ)
rw₁ :
  ((↑(Real.Gamma t) : ℂ) * Gamma ((↑t : ℂ) + 1 / 2))⁻¹ =
    (Gamma (2 * (↑t : ℂ)))⁻¹ * HPow.hPow (α := ℂ) 2 (2 * (↑t : ℂ) - 1) / (↑√π : ℂ)
⊢ (Gamma (↑t : ℂ))⁻¹ * (Gamma ((↑t : ℂ) + 1 / 2))⁻¹ =
    (Gamma (2 * (↑t : ℂ)))⁻¹ * HPow.hPow (α := ℂ) 2 (2 * (↑t : ℂ) - 1) / (↑√π : ℂ)
have rw₂ : ((↑(Real.Gamma t) : ℂ) * Gamma (↑(t + 1 / 2) : ℂ))⁻¹ =
  (Gamma (2 * (↑t : ℂ)))⁻¹ * HPow.hPow (α := ℂ) 2 (2 * (↑t : ℂ) - 1) / (↑√π : ℂ)
Tactic: rw [← mul_inv, Gamma_ofReal, (by simp : (t : ℂ) + 1 / 2 = ↑(t + 1 / 2)), Gamma_ofReal, ←
    ofReal_mul, Gamma_mul_Gamma_add_half_of_pos ht, ofReal_mul, ofReal_mul, ← Gamma_ofReal,
    mul_inv, mul_inv, (by simp : 2 * (t : ℂ) = ↑(2 * t)), Gamma_ofReal,
    ofReal_cpow zero_le_two, show (2 : ℝ) = (2 : ℂ) by norm_cast, ← cpow_neg, ofReal_sub,
    ofReal_one, neg_sub, ← div_eq_mul_inv]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Beta (goal)
Goal:
s : ℂ
h1 : AnalyticOnNhd ℂ (F := ℂ) (fun (z : ℂ) ↦ (Gamma z)⁻¹ * (Gamma (z + 1 / 2))⁻¹) univ
h2 : AnalyticOnNhd ℂ (F := ℂ) (fun (z : ℂ) ↦ (Gamma (2 * z))⁻¹ * HPow.hPow (α := ℂ) 2 (2 * z - 1) / (↑√π : ℂ)) univ
h3 : Tendsto ofReal (𝓝[≠] 1) (𝓝[≠] 1)
t : ℝ
ht : 0 < t
rw :
  (Gamma (↑t : ℂ) * Gamma ((↑t : ℂ) + 1 / 2))⁻¹ =
    (Gamma (2 * (↑t : ℂ)))⁻¹ * HPow.hPow (α := ℂ) 2 (2 * (↑t : ℂ) - 1) / (↑√π : ℂ)
rw₁ :
  ((↑(Real.Gamma t) : ℂ) * Gamma ((↑t : ℂ) + 1 / 2))⁻¹ =
    (Gamma (2 * (↑t : ℂ)))⁻¹ * HPow.hPow (α := ℂ) 2 (2 * (↑t : ℂ) - 1) / (↑√π : ℂ)
rw₂ :
  ((↑(Real.Gamma t) : ℂ) * Gamma (↑(t + 1 / 2) : ℂ))⁻¹ =
    (Gamma (2 * (↑t : ℂ)))⁻¹ * HPow.hPow (α := ℂ) 2 (2 * (↑t : ℂ) - 1) / (↑√π : ℂ)
⊢ (Gamma (↑t : ℂ))⁻¹ * (Gamma ((↑t : ℂ) + 1 / 2))⁻¹ =
    (Gamma (2 * (↑t : ℂ)))⁻¹ * HPow.hPow (α := ℂ) 2 (2 * (↑t : ℂ) - 1) / (↑√π : ℂ)
have rw₃ : ((↑(Real.Gamma t) : ℂ) * (↑(Real.Gamma (t + 1 / 2)) : ℂ))⁻¹ =
  (Gamma (2 * (↑t : ℂ)))⁻¹ * HPow.hPow (α := ℂ) 2 (2 * (↑t : ℂ) - 1) / (↑√π : ℂ)
Tactic: rw [← mul_inv, Gamma_ofReal, (by simp : (t : ℂ) + 1 / 2 = ↑(t + 1 / 2)), Gamma_ofReal, ←
    ofReal_mul, Gamma_mul_Gamma_add_half_of_pos ht, ofReal_mul, ofReal_mul, ← Gamma_ofReal,
    mul_inv, mul_inv, (by simp : 2 * (t : ℂ) = ↑(2 * t)), Gamma_ofReal,
    ofReal_cpow zero_le_two, show (2 : ℝ) = (2 : ℂ) by norm_cast, ← cpow_neg, ofReal_sub,
    ofReal_one, neg_sub, ← div_eq_mul_inv]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Beta (goal)
Goal:
s : ℂ
h1 : AnalyticOnNhd ℂ (F := ℂ) (fun (z : ℂ) ↦ (Gamma z)⁻¹ * (Gamma (z + 1 / 2))⁻¹) univ
h2 : AnalyticOnNhd ℂ (F := ℂ) (fun (z : ℂ) ↦ (Gamma (2 * z))⁻¹ * HPow.hPow (α := ℂ) 2 (2 * z - 1) / (↑√π : ℂ)) univ
h3 : Tendsto ofReal (𝓝[≠] 1) (𝓝[≠] 1)
t : ℝ
ht : 0 < t
rw :
  (Gamma (↑t : ℂ) * Gamma ((↑t : ℂ) + 1 / 2))⁻¹ =
    (Gamma (2 * (↑t : ℂ)))⁻¹ * HPow.hPow (α := ℂ) 2 (2 * (↑t : ℂ) - 1) / (↑√π : ℂ)
rw₁ :
  ((↑(Real.Gamma t) : ℂ) * Gamma ((↑t : ℂ) + 1 / 2))⁻¹ =
    (Gamma (2 * (↑t : ℂ)))⁻¹ * HPow.hPow (α := ℂ) 2 (2 * (↑t : ℂ) - 1) / (↑√π : ℂ)
rw₂ :
  ((↑(Real.Gamma t) : ℂ) * Gamma (↑(t + 1 / 2) : ℂ))⁻¹ =
    (Gamma (2 * (↑t : ℂ)))⁻¹ * HPow.hPow (α := ℂ) 2 (2 * (↑t : ℂ) - 1) / (↑√π : ℂ)
rw₃ :
  ((↑(Real.Gamma t) : ℂ) * (↑(Real.Gamma (t + 1 / 2)) : ℂ))⁻¹ =
    (Gamma (2 * (↑t : ℂ)))⁻¹ * HPow.hPow (α := ℂ) 2 (2 * (↑t : ℂ) - 1) / (↑√π : ℂ)
⊢ (Gamma (↑t : ℂ))⁻¹ * (Gamma ((↑t : ℂ) + 1 / 2))⁻¹ =
    (Gamma (2 * (↑t : ℂ)))⁻¹ * HPow.hPow (α := ℂ) 2 (2 * (↑t : ℂ) - 1) / (↑√π : ℂ)
have rw₄ : (↑(Real.Gamma t * Real.Gamma (t + 1 / 2)) : ℂ)⁻¹ =
  (Gamma (2 * (↑t : ℂ)))⁻¹ * HPow.hPow (α := ℂ) 2 (2 * (↑t : ℂ) - 1) / (↑√π : ℂ)
Tactic: rw [← mul_inv, Gamma_ofReal, (by simp : (t : ℂ) + 1 / 2 = ↑(t + 1 / 2)), Gamma_ofReal, ←
    ofReal_mul, Gamma_mul_Gamma_add_half_of_pos ht, ofReal_mul, ofReal_mul, ← Gamma_ofReal,
    mul_inv, mul_inv, (by simp : 2 * (t : ℂ) = ↑(2 * t)), Gamma_ofReal,
    ofReal_cpow zero_le_two, show (2 : ℝ) = (2 : ℂ) by norm_cast, ← cpow_neg, ofReal_sub,
    ofReal_one, neg_sub, ← div_eq_mul_inv]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Beta (goal)
Goal:
s : ℂ
h1 : AnalyticOnNhd ℂ (F := ℂ) (fun (z : ℂ) ↦ (Gamma z)⁻¹ * (Gamma (z + 1 / 2))⁻¹) univ
h2 : AnalyticOnNhd ℂ (F := ℂ) (fun (z : ℂ) ↦ (Gamma (2 * z))⁻¹ * HPow.hPow (α := ℂ) 2 (2 * z - 1) / (↑√π : ℂ)) univ
h3 : Tendsto ofReal (𝓝[≠] 1) (𝓝[≠] 1)
t : ℝ
ht : 0 < t
rw :
  (Gamma (↑t : ℂ) * Gamma ((↑t : ℂ) + 1 / 2))⁻¹ =
    (Gamma (2 * (↑t : ℂ)))⁻¹ * HPow.hPow (α := ℂ) 2 (2 * (↑t : ℂ) - 1) / (↑√π : ℂ)
rw₁ :
  ((↑(Real.Gamma t) : ℂ) * Gamma ((↑t : ℂ) + 1 / 2))⁻¹ =
    (Gamma (2 * (↑t : ℂ)))⁻¹ * HPow.hPow (α := ℂ) 2 (2 * (↑t : ℂ) - 1) / (↑√π : ℂ)
rw₂ :
  ((↑(Real.Gamma t) : ℂ) * Gamma (↑(t + 1 / 2) : ℂ))⁻¹ =
    (Gamma (2 * (↑t : ℂ)))⁻¹ * HPow.hPow (α := ℂ) 2 (2 * (↑t : ℂ) - 1) / (↑√π : ℂ)
rw₃ :
  ((↑(Real.Gamma t) : ℂ) * (↑(Real.Gamma (t + 1 / 2)) : ℂ))⁻¹ =
    (Gamma (2 * (↑t : ℂ)))⁻¹ * HPow.hPow (α := ℂ) 2 (2 * (↑t : ℂ) - 1) / (↑√π : ℂ)
rw₄ :
  (↑(Real.Gamma t * Real.Gamma (t + 1 / 2)) : ℂ)⁻¹ =
    (Gamma (2 * (↑t : ℂ)))⁻¹ * HPow.hPow (α := ℂ) 2 (2 * (↑t : ℂ) - 1) / (↑√π : ℂ)
⊢ (Gamma (↑t : ℂ))⁻¹ * (Gamma ((↑t : ℂ) + 1 / 2))⁻¹ =
    (Gamma (2 * (↑t : ℂ)))⁻¹ * HPow.hPow (α := ℂ) 2 (2 * (↑t : ℂ) - 1) / (↑√π : ℂ)
have rw₅ : (↑(Real.Gamma (2 * t) * HPow.hPow (α := ℝ) 2 (1 - 2 * t) * √π) : ℂ)⁻¹ =
  (Gamma (2 * (↑t : ℂ)))⁻¹ * HPow.hPow (α := ℂ) 2 (2 * (↑t : ℂ) - 1) / (↑√π : ℂ)
Tactic: rw [← mul_inv, Gamma_ofReal, (by simp : (t : ℂ) + 1 / 2 = ↑(t + 1 / 2)), Gamma_ofReal, ←
    ofReal_mul, Gamma_mul_Gamma_add_half_of_pos ht, ofReal_mul, ofReal_mul, ← Gamma_ofReal,
    mul_inv, mul_inv, (by simp : 2 * (t : ℂ) = ↑(2 * t)), Gamma_ofReal,
    ofReal_cpow zero_le_two, show (2 : ℝ) = (2 : ℂ) by norm_cast, ← cpow_neg, ofReal_sub,
    ofReal_one, neg_sub, ← div_eq_mul_inv]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Beta (goal)
Goal:
s : ℂ
h1 : AnalyticOnNhd ℂ (F := ℂ) (fun (z : ℂ) ↦ (Gamma z)⁻¹ * (Gamma (z + 1 / 2))⁻¹) univ
h2 : AnalyticOnNhd ℂ (F := ℂ) (fun (z : ℂ) ↦ (Gamma (2 * z))⁻¹ * HPow.hPow (α := ℂ) 2 (2 * z - 1) / (↑√π : ℂ)) univ
h3 : Tendsto ofReal (𝓝[≠] 1) (𝓝[≠] 1)
t : ℝ
ht : 0 < t
rw :
  (Gamma (↑t : ℂ) * Gamma ((↑t : ℂ) + 1 / 2))⁻¹ =
    (Gamma (2 * (↑t : ℂ)))⁻¹ * HPow.hPow (α := ℂ) 2 (2 * (↑t : ℂ) - 1) / (↑√π : ℂ)
rw₁ :
  ((↑(Real.Gamma t) : ℂ) * Gamma ((↑t : ℂ) + 1 / 2))⁻¹ =
    (Gamma (2 * (↑t : ℂ)))⁻¹ * HPow.hPow (α := ℂ) 2 (2 * (↑t : ℂ) - 1) / (↑√π : ℂ)
rw₂ :
  ((↑(Real.Gamma t) : ℂ) * Gamma (↑(t + 1 / 2) : ℂ))⁻¹ =
    (Gamma (2 * (↑t : ℂ)))⁻¹ * HPow.hPow (α := ℂ) 2 (2 * (↑t : ℂ) - 1) / (↑√π : ℂ)
rw₃ :
  ((↑(Real.Gamma t) : ℂ) * (↑(Real.Gamma (t + 1 / 2)) : ℂ))⁻¹ =
    (Gamma (2 * (↑t : ℂ)))⁻¹ * HPow.hPow (α := ℂ) 2 (2 * (↑t : ℂ) - 1) / (↑√π : ℂ)
rw₄ :
  (↑(Real.Gamma t * Real.Gamma (t + 1 / 2)) : ℂ)⁻¹ =
    (Gamma (2 * (↑t : ℂ)))⁻¹ * HPow.hPow (α := ℂ) 2 (2 * (↑t : ℂ) - 1) / (↑√π : ℂ)
rw₅ :
  (↑(Real.Gamma (2 * t) * HPow.hPow (α := ℝ) 2 (1 - 2 * t) * √π) : ℂ)⁻¹ =
    (Gamma (2 * (↑t : ℂ)))⁻¹ * HPow.hPow (α := ℂ) 2 (2 * (↑t : ℂ) - 1) / (↑√π : ℂ)
⊢ (Gamma (↑t : ℂ))⁻¹ * (Gamma ((↑t : ℂ) + 1 / 2))⁻¹ =
    (Gamma (2 * (↑t : ℂ)))⁻¹ * HPow.hPow (α := ℂ) 2 (2 * (↑t : ℂ) - 1) / (↑√π : ℂ)
have rw₆ : ((↑(Real.Gamma (2 * t) * HPow.hPow (α := ℝ) 2 (1 - 2 * t)) : ℂ) * (↑√π : ℂ))⁻¹ =
  (Gamma (2 * (↑t : ℂ)))⁻¹ * HPow.hPow (α := ℂ) 2 (2 * (↑t : ℂ) - 1) / (↑√π : ℂ)
Tactic: rw [← mul_inv, Gamma_ofReal, (by simp : (t : ℂ) + 1 / 2 = ↑(t + 1 / 2)), Gamma_ofReal, ←
    ofReal_mul, Gamma_mul_Gamma_add_half_of_pos ht, ofReal_mul, ofReal_mul, ← Gamma_ofReal,
    mul_inv, mul_inv, (by simp : 2 * (t : ℂ) = ↑(2 * t)), Gamma_ofReal,
    ofReal_cpow zero_le_two, show (2 : ℝ) = (2 : ℂ) by norm_cast, ← cpow_neg, ofReal_sub,
    ofReal_one, neg_sub, ← div_eq_mul_inv]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.Beta (goal)
Goal:
s : ℂ
h1 : AnalyticOnNhd ℂ (F := ℂ) (fun (z : ℂ) ↦ (Gamma z)⁻¹ * (Gamma (z + 1 / 2))⁻¹) univ
h2 : AnalyticOnNhd ℂ (F := ℂ) (fun (z : ℂ) ↦ (Gamma (2 * z))⁻¹ * HPow.hPow (α := ℂ) 2 (2 * z - 1) / (↑√π : ℂ)) univ
h3 : Tendsto ofReal (𝓝[≠] 1) (𝓝[≠] 1)
t : ℝ
ht : 0 < t
rw :
  (Gamma (↑t : ℂ) * Gamma ((↑t : ℂ) + 1 / 2))⁻¹ =
    (Gamma (2 * (↑t : ℂ)))⁻¹ * HPow.hPow (α := ℂ) 2 (2 * (↑t : ℂ) - 1) / (↑√π : ℂ)
rw₁ :
  ((↑(Real.Gamma t) : ℂ) * Gamma ((↑t : ℂ) + 1 / 2))⁻¹ =
    (Gamma (2 * (↑t : ℂ)))⁻¹ * HPow.hPow (α := ℂ) 2 (2 * (↑t : ℂ) - 1) / (↑√π : ℂ)
rw₂ :
  ((↑(Real.Gamma t) : ℂ) * Gamma (↑(t + 1 / 2) : ℂ))⁻¹ =
    (Gamma (2 * (↑t : ℂ)))⁻¹ * HPow.hPow (α := ℂ) 2 (2 * (↑t : ℂ) - 1) / (↑√π : ℂ)
rw₃ :
  ((↑(Real.Gamma t) : ℂ) * (↑(Real.Gamma (t + 1 / 2)) : ℂ))⁻¹ =
    (Gamma (2 * (↑t : ℂ)))⁻¹ * HPow.hPow (α := ℂ) 2 (2 * (↑t : ℂ) - 1) / (↑√π : ℂ)
rw₄ :
  (↑(Real.Gamma t * Real.Gamma (t + 1 / 2)) : ℂ)⁻¹ =
    (Gamma (2 * (↑t : ℂ)))⁻¹ * HPow.hPow (α := ℂ) 2 (2 * (↑t : ℂ) - 1) / (↑√π : ℂ)
rw₅ :
  (↑(Real.Gamma (2 * t) * HPow.hPow (α := ℝ) 2 (1 - 2 * t) * √π) : ℂ)⁻¹ =
    (Gamma (2 * (↑t : ℂ)))⁻¹ * HPow.hPow (α := ℂ) 2 (2 * (↑t : ℂ) - 1) / (↑√π : ℂ)
rw₆ :
  ((↑(Real.Gamma (2 * t) * HPow.hPow (α := ℝ) 2 (1 - 2 * t)) : ℂ) * (↑√π : ℂ))⁻¹ =
    (Gamma (2 * (↑t : ℂ)))⁻¹ * HPow.hPow (α := ℂ) 2 (2 * (↑t : ℂ) - 1) / (↑√π : ℂ)
⊢ (Gamma (↑t : ℂ))⁻¹ * (Gamma ((↑t : ℂ) + 1 / 2))⁻¹ =
    (Gamma (2 * (↑t : ℂ)))⁻¹ * HPow.hPow (α := ℂ) 2 (2 * (↑t : ℂ) - 1) / (↑√π : ℂ)
have rw₇ : ((↑(Real.Gamma (2 * t)) : ℂ) * (↑(HPow.hPow (α := ℝ) 2 (1 - 2 * t)) : ℂ) * (↑√π : ℂ))⁻¹ =
  (Gamma (2 * (↑t : ℂ)))⁻¹ * HPow.hPow (α := ℂ) 2 (2 * (↑t : ℂ) - 1) / (↑√π : ℂ)
Tactic: rw [← mul_inv, Gamma_ofReal, (by simp : (t : ℂ) + 1 / 2 = ↑(t + 1 / 2)), Gamma_ofReal, ←
    ofReal_mul, Gamma_mul_Gamma_add_half_of_pos ht, ofReal_mul, ofReal_mul, ← Gamma_ofReal,
    mul_inv, mul_inv, (by simp : 2 * (t : ℂ) = ↑(2 * t)), Gamma_ofReal,
    ofReal_cpow zero_le_two, show (2 : ℝ) = (2 : ℂ) by norm_cast, ← cpow_neg, ofReal_sub,
    ofReal_one, neg_sub, ← div_eq_mul_inv]