-- 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) / (↑√π : ℂ)
rw₁₂ :
  (↑(Real.Gamma (2 * t)) : ℂ)⁻¹ * (↑(HPow.hPow (α := ℝ) 2 (1 - 2 * t)) : ℂ)⁻¹ * (↑√π : ℂ)⁻¹ =
    (↑(Real.Gamma (2 * t)) : ℂ)⁻¹ * HPow.hPow (α := ℂ) 2 ((↑(2 * t) : ℂ) - 1) / (↑√π : ℂ)
rw₁₃ :
  (↑(Real.Gamma (2 * t)) : ℂ)⁻¹ * ((↑2 : ℂ) ^ (↑(1 - 2 * t) : ℂ))⁻¹ * (↑√π : ℂ)⁻¹ =
    (↑(Real.Gamma (2 * t)) : ℂ)⁻¹ * HPow.hPow (α := ℂ) 2 ((↑(2 * t) : ℂ) - 1) / (↑√π : ℂ)
rw₁₄ :
  (↑(Real.Gamma (2 * t)) : ℂ)⁻¹ * (HPow.hPow (α := ℂ) 2 (↑(1 - 2 * t) : ℂ))⁻¹ * (↑√π : ℂ)⁻¹ =
    (↑(Real.Gamma (2 * t)) : ℂ)⁻¹ * HPow.hPow (α := ℂ) 2 ((↑(2 * t) : ℂ) - 1) / (↑√π : ℂ)
rw₁₅ :
  (↑(Real.Gamma (2 * t)) : ℂ)⁻¹ * HPow.hPow (α := ℂ) 2 (-(↑(1 - 2 * t) : ℂ)) * (↑√π : ℂ)⁻¹ =
    (↑(Real.Gamma (2 * t)) : ℂ)⁻¹ * HPow.hPow (α := ℂ) 2 ((↑(2 * t) : ℂ) - 1) / (↑√π : ℂ)
rw₁₆ :
  (↑(Real.Gamma (2 * t)) : ℂ)⁻¹ * HPow.hPow (α := ℂ) 2 (-((↑1 : ℂ) - (↑(2 * t) : ℂ))) * (↑√π : ℂ)⁻¹ =
    (↑(Real.Gamma (2 * t)) : ℂ)⁻¹ * HPow.hPow (α := ℂ) 2 ((↑(2 * t) : ℂ) - 1) / (↑√π : ℂ)
rw₁₇ :
  (↑(Real.Gamma (2 * t)) : ℂ)⁻¹ * HPow.hPow (α := ℂ) 2 (-(1 - (↑(2 * t) : ℂ))) * (↑√π : ℂ)⁻¹ =
    (↑(Real.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 ((↑(2 * t) : ℂ) - 1) * (↑√π : ℂ)⁻¹ =
  (↑(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]