awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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) / (↑√π : ℂ)
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₈ : (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) / (↑√π : ℂ)
rw₇ :
  ((↑(Real.Gamma (2 * t)) : ℂ) * (↑(HPow.hPow (α := ℝ) 2 (1 - 2 * t)) : ℂ) * (↑√π : ℂ))⁻¹ =
    (Gamma (2 * (↑t : ℂ)))⁻¹ * HPow.hPow (α := ℂ) 2 (2 * (↑t : ℂ) - 1) / (↑√π : ℂ)
rw₈ :
  (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₉ : (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) / (↑√π : ℂ)
rw₇ :
  ((↑(Real.Gamma (2 * t)) : ℂ) * (↑(HPow.hPow (α := ℝ) 2 (1 - 2 * t)) : ℂ) * (↑√π : ℂ))⁻¹ =
    (Gamma (2 * (↑t : ℂ)))⁻¹ * HPow.hPow (α := ℂ) 2 (2 * (↑t : ℂ) - 1) / (↑√π : ℂ)
rw₈ :
  (Gamma (↑(2 * t) : ℂ) * (↑(HPow.hPow (α := ℝ) 2 (1 - 2 * t)) : ℂ) * (↑√π : ℂ))⁻¹ =
    (Gamma (2 * (↑t : ℂ)))⁻¹ * HPow.hPow (α := ℂ) 2 (2 * (↑t : ℂ) - 1) / (↑√π : ℂ)
rw₉ :
  (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₁₀ : (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) / (↑√π : ℂ)
rw₇ :
  ((↑(Real.Gamma (2 * t)) : ℂ) * (↑(HPow.hPow (α := ℝ) 2 (1 - 2 * t)) : ℂ) * (↑√π : ℂ))⁻¹ =
    (Gamma (2 * (↑t : ℂ)))⁻¹ * HPow.hPow (α := ℂ) 2 (2 * (↑t : ℂ) - 1) / (↑√π : ℂ)
rw₈ :
  (Gamma (↑(2 * t) : ℂ) * (↑(HPow.hPow (α := ℝ) 2 (1 - 2 * t)) : ℂ) * (↑√π : ℂ))⁻¹ =
    (Gamma (2 * (↑t : ℂ)))⁻¹ * HPow.hPow (α := ℂ) 2 (2 * (↑t : ℂ) - 1) / (↑√π : ℂ)
rw₉ :
  (Gamma (↑(2 * t) : ℂ) * (↑(HPow.hPow (α := ℝ) 2 (1 - 2 * t)) : ℂ))⁻¹ * (↑√π : ℂ)⁻¹ =
    (Gamma (2 * (↑t : ℂ)))⁻¹ * HPow.hPow (α := ℂ) 2 (2 * (↑t : ℂ) - 1) / (↑√π : ℂ)
rw₁₀ :
  (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₁₁ : (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) / (↑√π : ℂ)
rw₇ :
  ((↑(Real.Gamma (2 * t)) : ℂ) * (↑(HPow.hPow (α := ℝ) 2 (1 - 2 * t)) : ℂ) * (↑√π : ℂ))⁻¹ =
    (Gamma (2 * (↑t : ℂ)))⁻¹ * HPow.hPow (α := ℂ) 2 (2 * (↑t : ℂ) - 1) / (↑√π : ℂ)
rw₈ :
  (Gamma (↑(2 * t) : ℂ) * (↑(HPow.hPow (α := ℝ) 2 (1 - 2 * t)) : ℂ) * (↑√π : ℂ))⁻¹ =
    (Gamma (2 * (↑t : ℂ)))⁻¹ * HPow.hPow (α := ℂ) 2 (2 * (↑t : ℂ) - 1) / (↑√π : ℂ)
rw₉ :
  (Gamma (↑(2 * t) : ℂ) * (↑(HPow.hPow (α := ℝ) 2 (1 - 2 * t)) : ℂ))⁻¹ * (↑√π : ℂ)⁻¹ =
    (Gamma (2 * (↑t : ℂ)))⁻¹ * HPow.hPow (α := ℂ) 2 (2 * (↑t : ℂ) - 1) / (↑√π : ℂ)
rw₁₀ :
  (Gamma (↑(2 * t) : ℂ))⁻¹ * (↑(HPow.hPow (α := ℝ) 2 (1 - 2 * t)) : ℂ)⁻¹ * (↑√π : ℂ)⁻¹ =
    (Gamma (2 * (↑t : ℂ)))⁻¹ * HPow.hPow (α := ℂ) 2 (2 * (↑t : ℂ) - 1) / (↑√π : ℂ)
rw₁₁ :
  (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)) : ℂ)⁻¹ * (↑√π : ℂ)⁻¹ =
  (↑(Real.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 : ℝ
⊢ Gamma s * Gamma (s + 1 / 2) = Gamma (2 * s) * HPow.hPow (α := ℝ) 2 (1 - 2 * s) * √π
have rw : (↑(Gamma s * Gamma (s + 1 / 2)) : ℂ) = (↑(Gamma (2 * s) * HPow.hPow (α := ℝ) 2 (1 - 2 * s) * √π) : ℂ)
Tactic: rw [← ofReal_inj]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup (hypothesis)
Goal:
s t a b : ℝ
hs : 0 < s
ht : 0 < t
ha : 0 < a
hb : 0 < b
hab : a + b = 1
f : ℝ → ℝ → ℝ → ℝ := fun (c u x : ℝ) ↦ rexp (-c * x) * x ^ (c * (u - 1))
⊢ Γ (a * s + b * t) ≤ Γ s ^ a * Γ t ^ b
have e : (1 / a).HolderConjugate (1 / b)
Tactic: have e : HolderConjugate (1 / a) (1 / b) := Real.holderConjugate_one_div ha hb hab
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup (goal)
Goal:
s t a b : ℝ
hs : 0 < s
ht : 0 < t
ha : 0 < a
hb : 0 < b
hab : a + b = 1
f : ℝ → ℝ → ℝ → ℝ := fun (c u x : ℝ) ↦ rexp (-c * x) * x ^ (c * (u - 1))
e : (1 / a).HolderConjugate (1 / b)
⊢ b = 1 - a
have linarith : b < 1 - a → -(a + b - 1) + (b - (1 - a)) = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup (goal)
Goal:
s t a b : ℝ
hs : 0 < s
ht : 0 < t
ha : 0 < a
hb : 0 < b
hab : a + b = 1
f : ℝ → ℝ → ℝ → ℝ := fun (c u x : ℝ) ↦ rexp (-c * x) * x ^ (c * (u - 1))
e : (1 / a).HolderConjugate (1 / b)
linarith : b < 1 - a → -(a + b - 1) + (b - (1 - a)) = 0
⊢ b = 1 - a
have linarith₁ : 1 - a < b → a + b - 1 + (1 - a - b) = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup (hypothesis)
Goal:
s t a b : ℝ
hs : 0 < s
ht : 0 < t
ha : 0 < a
hb : 0 < b
hab : a + b = 1
f : ℝ → ℝ → ℝ → ℝ := fun (c u x : ℝ) ↦ rexp (-c * x) * x ^ (c * (u - 1))
e : (1 / a).HolderConjugate (1 / b)
⊢ Γ (a * s + b * t) ≤ Γ s ^ a * Γ t ^ b
have hab' : b = 1 - a
Tactic: have hab' : b = 1 - a := by linarith
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup (hypothesis)
Goal:
s t a b : ℝ
hs : 0 < s
ht : 0 < t
ha : 0 < a
hb : 0 < b
hab : a + b = 1
f : ℝ → ℝ → ℝ → ℝ := fun (c u x : ℝ) ↦ rexp (-c * x) * x ^ (c * (u - 1))
e : (1 / a).HolderConjugate (1 / b)
hab' : b = 1 - a
⊢ Γ (a * s + b * t) ≤ Γ s ^ a * Γ t ^ b
have hst : 0 < a * s + b * t
Tactic: have hst : 0 < a * s + b * t := by positivity
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup (hypothesis)
Goal:
s t a b : ℝ
hs : 0 < s
ht : 0 < t
ha : 0 < a
hb : 0 < b
hab : a + b = 1
f : ℝ → ℝ → ℝ → ℝ := fun (c u x : ℝ) ↦ rexp (-c * x) * x ^ (c * (u - 1))
e : (1 / a).HolderConjugate (1 / b)
hab' : b = 1 - a
hst : 0 < a * s + b * t
⊢ Γ (a * s + b * t) ≤ Γ s ^ a * Γ t ^ b
have posf : ∀ (c u x : ℝ), Membership.mem (γ := Set ℝ) (Ioi 0) x → 0 ≤ f c u x
Tactic: have posf : ∀ c u x : ℝ, x ∈ Ioi (0 : ℝ) → 0 ≤ f c u x := fun c u x hx =>
    mul_nonneg (exp_pos _).le (rpow_pos_of_pos hx _).le
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup (hypothesis)
Goal:
s t a b : ℝ
hs : 0 < s
ht : 0 < t
ha : 0 < a
hb : 0 < b
hab : a + b = 1
f : ℝ → ℝ → ℝ → ℝ := fun (c u x : ℝ) ↦ rexp (-c * x) * x ^ (c * (u - 1))
e : (1 / a).HolderConjugate (1 / b)
hab' : b = 1 - a
hst : 0 < a * s + b * t
posf : ∀ (c u x : ℝ), Membership.mem (γ := Set ℝ) (Ioi 0) x → 0 ≤ f c u x
⊢ Γ (a * s + b * t) ≤ Γ s ^ a * Γ t ^ b
have posf' : ∀ (c u : ℝ), ∀ᵐ (x : ℝ) ∂Measure.restrict volume (Ioi 0), 0 ≤ f c u x
Tactic: have posf' : ∀ c u : ℝ, ∀ᵐ x : ℝ ∂volume.restrict (Ioi 0), 0 ≤ f c u x := fun c u =>
    (ae_restrict_iff' measurableSet_Ioi).mpr (ae_of_all _ (posf c u))
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup (goal)
Goal:
s t a b : ℝ
hs : 0 < s
ht : 0 < t
ha : 0 < a
hb : 0 < b
hab : a + b = 1
f : ℝ → ℝ → ℝ → ℝ := fun (c u x : ℝ) ↦ rexp (-c * x) * x ^ (c * (u - 1))
e : (1 / a).HolderConjugate (1 / b)
hab' : b = 1 - a
hst : 0 < a * s + b * t
posf : ∀ (c u x : ℝ), Membership.mem (γ := Set ℝ) (Ioi 0) x → 0 ≤ f c u x
posf' : ∀ (c u : ℝ), ∀ᵐ (x : ℝ) ∂Measure.restrict volume (Ioi 0), 0 ≤ f c u x
c x : ℝ
hc : 0 < c
u : ℝ
hx : 0 < x
⊢ rexp (-x) * x ^ (u - 1) = (rexp (-c * x) * x ^ (c * (u - 1))) ^ (1 / c)
have rw : rexp (-x) * x ^ (u - 1) = rexp (-c * x * (1 / c)) * x ^ (c * (u - 1) * (1 / c))
Tactic: rw [mul_rpow (exp_pos _).le ((rpow_nonneg hx.le) _), ← exp_mul, ← rpow_mul hx.le]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup (goal)
Goal:
s t a b : ℝ
hs : 0 < s
ht : 0 < t
ha : 0 < a
hb : 0 < b
hab : a + b = 1
f : ℝ → ℝ → ℝ → ℝ := fun (c u x : ℝ) ↦ rexp (-c * x) * x ^ (c * (u - 1))
e : (1 / a).HolderConjugate (1 / b)
hab' : b = 1 - a
hst : 0 < a * s + b * t
posf : ∀ (c u x : ℝ), Membership.mem (γ := Set ℝ) (Ioi 0) x → 0 ≤ f c u x
posf' : ∀ (c u : ℝ), ∀ᵐ (x : ℝ) ∂Measure.restrict volume (Ioi 0), 0 ≤ f c u x
c x : ℝ
hc : 0 < c
u : ℝ
hx : 0 < x
⊢ rexp (-x) * x ^ (u - 1) = rexp (-c * x * (1 / c)) * x ^ (c * (u - 1) * (1 / c))
have e_a : -x = -c * x * (1 / c)
Tactic: congr 2
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup (goal)
Goal:
s t a b : ℝ
hs : 0 < s
ht : 0 < t
ha : 0 < a
hb : 0 < b
hab : a + b = 1
f : ℝ → ℝ → ℝ → ℝ := fun (c u x : ℝ) ↦ rexp (-c * x) * x ^ (c * (u - 1))
e : (1 / a).HolderConjugate (1 / b)
hab' : b = 1 - a
hst : 0 < a * s + b * t
posf : ∀ (c u x : ℝ), Membership.mem (γ := Set ℝ) (Ioi 0) x → 0 ≤ f c u x
posf' : ∀ (c u : ℝ), ∀ᵐ (x : ℝ) ∂Measure.restrict volume (Ioi 0), 0 ≤ f c u x
c x : ℝ
hc : 0 < c
u : ℝ
hx : 0 < x
e_a : -x = -c * x * (1 / c)
⊢ rexp (-x) * x ^ (u - 1) = rexp (-c * x * (1 / c)) * x ^ (c * (u - 1) * (1 / c))
have e_a₁ : u - 1 = c * (u - 1) * (1 / c)
Tactic: congr 2
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup (hypothesis)
Goal:
s t a b : ℝ
hs : 0 < s
ht : 0 < t
ha : 0 < a
hb : 0 < b
hab : a + b = 1
f : ℝ → ℝ → ℝ → ℝ := fun (c u x : ℝ) ↦ rexp (-c * x) * x ^ (c * (u - 1))
e : (1 / a).HolderConjugate (1 / b)
hab' : b = 1 - a
hst : 0 < a * s + b * t
posf : ∀ (c u x : ℝ), Membership.mem (γ := Set ℝ) (Ioi 0) x → 0 ≤ f c u x
posf' : ∀ (c u : ℝ), ∀ᵐ (x : ℝ) ∂Measure.restrict volume (Ioi 0), 0 ≤ f c u x
⊢ Γ (a * s + b * t) ≤ Γ s ^ a * Γ t ^ b
have fpow : ∀ {c x : ℝ}, 0 < c → ∀ (u : ℝ), 0 < x → rexp (-x) * x ^ (u - 1) = f c u x ^ (1 / c)
Tactic: have fpow :
    ∀ {c x : ℝ} (_ : 0 < c) (u : ℝ) (_ : 0 < x), exp (-x) * x ^ (u - 1) = f c u x ^ (1 / c) := by
    intro c x hc u hx
    dsimp only [f]
    rw [mul_rpow (exp_pos _).le ((rpow_nonneg hx.le) _), ← exp_mul, ← rpow_mul hx.le]
    congr 2 <;> field
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup (goal)
Goal:
s t a b : ℝ
hs : 0 < s
ht : 0 < t
ha : 0 < a
hb : 0 < b
hab : a + b = 1
f : ℝ → ℝ → ℝ → ℝ := fun (c u x : ℝ) ↦ rexp (-c * x) * x ^ (c * (u - 1))
e : (1 / a).HolderConjugate (1 / b)
hab' : b = 1 - a
hst : 0 < a * s + b * t
posf : ∀ (c u x : ℝ), Membership.mem (γ := Set ℝ) (Ioi 0) x → 0 ≤ f c u x
posf' : ∀ (c u : ℝ), ∀ᵐ (x : ℝ) ∂Measure.restrict volume (Ioi 0), 0 ≤ f c u x
fpow : ∀ {c x : ℝ}, 0 < c → ∀ (u : ℝ), 0 < x → rexp (-x) * x ^ (u - 1) = f c u x ^ (1 / c)
c u : ℝ
hc : 0 < c
hu : 0 < u
⊢ ENNReal.ofReal (1 / c) ≠ 0
have rwa : ¬ENNReal.ofReal (1 / c) = 0
Tactic: rwa [Ne, ENNReal.ofReal_eq_zero, not_le, one_div_pos]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup (goal)
Goal:
s t a b : ℝ
hs : 0 < s
ht : 0 < t
ha : 0 < a
hb : 0 < b
hab : a + b = 1
f : ℝ → ℝ → ℝ → ℝ := fun (c u x : ℝ) ↦ rexp (-c * x) * x ^ (c * (u - 1))
e : (1 / a).HolderConjugate (1 / b)
hab' : b = 1 - a
hst : 0 < a * s + b * t
posf : ∀ (c u x : ℝ), Membership.mem (γ := Set ℝ) (Ioi 0) x → 0 ≤ f c u x
posf' : ∀ (c u : ℝ), ∀ᵐ (x : ℝ) ∂Measure.restrict volume (Ioi 0), 0 ≤ f c u x
fpow : ∀ {c x : ℝ}, 0 < c → ∀ (u : ℝ), 0 < x → rexp (-x) * x ^ (u - 1) = f c u x ^ (1 / c)
c u : ℝ
hc : 0 < c
hu : 0 < u
rwa : ¬ENNReal.ofReal (1 / c) = 0
⊢ ENNReal.ofReal (1 / c) ≠ 0
have rwa₁ : ¬1 / c ≤ 0
Tactic: rwa [Ne, ENNReal.ofReal_eq_zero, not_le, one_div_pos]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup (goal)
Goal:
s t a b : ℝ
hs : 0 < s
ht : 0 < t
ha : 0 < a
hb : 0 < b
hab : a + b = 1
f : ℝ → ℝ → ℝ → ℝ := fun (c u x : ℝ) ↦ rexp (-c * x) * x ^ (c * (u - 1))
e : (1 / a).HolderConjugate (1 / b)
hab' : b = 1 - a
hst : 0 < a * s + b * t
posf : ∀ (c u x : ℝ), Membership.mem (γ := Set ℝ) (Ioi 0) x → 0 ≤ f c u x
posf' : ∀ (c u : ℝ), ∀ᵐ (x : ℝ) ∂Measure.restrict volume (Ioi 0), 0 ≤ f c u x
fpow : ∀ {c x : ℝ}, 0 < c → ∀ (u : ℝ), 0 < x → rexp (-x) * x ^ (u - 1) = f c u x ^ (1 / c)
c u : ℝ
hc : 0 < c
hu : 0 < u
rwa : ¬ENNReal.ofReal (1 / c) = 0
rwa₁ : ¬1 / c ≤ 0
⊢ ENNReal.ofReal (1 / c) ≠ 0
have rwa₂ : 0 < 1 / c
Tactic: rwa [Ne, ENNReal.ofReal_eq_zero, not_le, one_div_pos]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup (hypothesis)
Goal:
s t a b : ℝ
hs : 0 < s
ht : 0 < t
ha : 0 < a
hb : 0 < b
hab : a + b = 1
f : ℝ → ℝ → ℝ → ℝ := fun (c u x : ℝ) ↦ rexp (-c * x) * x ^ (c * (u - 1))
e : (1 / a).HolderConjugate (1 / b)
hab' : b = 1 - a
hst : 0 < a * s + b * t
posf : ∀ (c u x : ℝ), Membership.mem (γ := Set ℝ) (Ioi 0) x → 0 ≤ f c u x
posf' : ∀ (c u : ℝ), ∀ᵐ (x : ℝ) ∂Measure.restrict volume (Ioi 0), 0 ≤ f c u x
fpow : ∀ {c x : ℝ}, 0 < c → ∀ (u : ℝ), 0 < x → rexp (-x) * x ^ (u - 1) = f c u x ^ (1 / c)
c u : ℝ
hc : 0 < c
hu : 0 < u
⊢ MemLp (m0 := MeasureSpace.toMeasurableSpace) (f c u) (ENNReal.ofReal (1 / c)) (Measure.restrict volume (Ioi 0))
have A : ENNReal.ofReal (1 / c) ≠ 0
Tactic: have A : ENNReal.ofReal (1 / c) ≠ 0 := by
      rwa [Ne, ENNReal.ofReal_eq_zero, not_le, one_div_pos]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup (hypothesis)
Goal:
s t a b : ℝ
hs : 0 < s
ht : 0 < t
ha : 0 < a
hb : 0 < b
hab : a + b = 1
f : ℝ → ℝ → ℝ → ℝ := fun (c u x : ℝ) ↦ rexp (-c * x) * x ^ (c * (u - 1))
e : (1 / a).HolderConjugate (1 / b)
hab' : b = 1 - a
hst : 0 < a * s + b * t
posf : ∀ (c u x : ℝ), Membership.mem (γ := Set ℝ) (Ioi 0) x → 0 ≤ f c u x
posf' : ∀ (c u : ℝ), ∀ᵐ (x : ℝ) ∂Measure.restrict volume (Ioi 0), 0 ≤ f c u x
fpow : ∀ {c x : ℝ}, 0 < c → ∀ (u : ℝ), 0 < x → rexp (-x) * x ^ (u - 1) = f c u x ^ (1 / c)
c u : ℝ
hc : 0 < c
hu : 0 < u
A : ENNReal.ofReal (1 / c) ≠ 0
⊢ MemLp (m0 := MeasureSpace.toMeasurableSpace) (f c u) (ENNReal.ofReal (1 / c)) (Measure.restrict volume (Ioi 0))
have B : ENNReal.ofReal (1 / c) ≠ ∞
Tactic: have B : ENNReal.ofReal (1 / c) ≠ ∞ := ENNReal.ofReal_ne_top