-- Mathlib/Analysis/SpecialFunctions/Gaussian/GaussianIntegral.lean
theorem Real.Gamma_one_half_eq : Real.Gamma (1 / 2) = √π

Proof state:
case h.e'_2
x : ℝ
hx : x ∈ Ioi 0
this : (x ^ 2) ^ (1 / 2 - 1) = x⁻¹
⊢ 2 * x ^ (2 - 1) * rexp (-x ^ 2) = 2 * rexp (-x ^ 2) * x

Tactic:
norm_num

Result:
case h.e'_2
x : ℝ
hx : x ∈ Ioi 0
this : (x ^ 2) ^ (1 / 2 - 1) = x⁻¹
⊢ 2 * x * rexp (-x ^ 2) = 2 * rexp (-x ^ 2) * x

Proof state:
case h.e'_3

⊢ √π = 2 * (√(π / 1) / 2)

Tactic:
rw [div_one, ← mul_div_assoc, mul_comm, mul_div_cancel_right₀ _ (two_ne_zero' ℝ)]

Result:
no goals

Proof state:
case h.e'_2

⊢ ∫ (x : ℝ) in Ioi 0, (2 * x ^ (2 - 1)) • (rexp (-x ^ 2) * (x ^ 2) ^ (1 / 2 - 1)) =
    2 * ∫ (x : ℝ) in Ioi 0, rexp (-1 * x ^ 2)

Tactic:
rw [← integral_mul_left]

Result:
case h.e'_2

⊢ ∫ (x : ℝ) in Ioi 0, (2 * x ^ (2 - 1)) • (rexp (-x ^ 2) * (x ^ 2) ^ (1 / 2 - 1)) =
    ∫ (a : ℝ) in Ioi 0, 2 * rexp (-1 * a ^ 2)

Proof state:
x : ℝ
hx : x ∈ Ioi 0
⊢ (x ^ 2) ^ (1 / 2 - 1) = x⁻¹

Tactic:
rw [← rpow_mul (le_of_lt hx)]

Result:
x : ℝ
hx : x ∈ Ioi 0
⊢ x ^ (2 * (1 / 2 - 1)) = x⁻¹

Proof state:
case h.e'_2
x : ℝ
hx : x ∈ Ioi 0
this : (x ^ 2) ^ (1 / 2 - 1) = x⁻¹
⊢ (2 * x ^ (2 - 1)) • (rexp (-x ^ 2) * (x ^ 2) ^ (1 / 2 - 1)) = 2 * rexp (-1 * x ^ 2)

Tactic:
rw [smul_eq_mul, this]

Result:
case h.e'_2
x : ℝ
hx : x ∈ Ioi 0
this : (x ^ 2) ^ (1 / 2 - 1) = x⁻¹
⊢ 2 * x ^ (2 - 1) * (rexp (-x ^ 2) * x⁻¹) = 2 * rexp (-1 * x ^ 2)

Proof state:
⊢ ∫ (x : ℝ) in Ioi 0, (2 * x ^ (2 - 1)) • (rexp (-x ^ 2) * (x ^ 2) ^ (1 / 2 - 1)) = √π

Tactic:
convert congr_arg (fun x : ℝ => 2 * x) (integral_gaussian_Ioi 1) using 1

Result:
case h.e'_2

⊢ ∫ (x : ℝ) in Ioi 0, (2 * x ^ (2 - 1)) • (rexp (-x ^ 2) * (x ^ 2) ^ (1 / 2 - 1)) =
    2 * ∫ (x : ℝ) in Ioi 0, rexp (-1 * x ^ 2)

case h.e'_3

⊢ √π = 2 * (√(π / 1) / 2)

Proof state:
case h.e'_2
x : ℝ
hx : x ∈ Ioi 0
⊢ (2 * x ^ (2 - 1)) • (rexp (-x ^ 2) * (x ^ 2) ^ (1 / 2 - 1)) = 2 * rexp (-1 * x ^ 2)

Tactic:
have : (x ^ (2 : ℝ)) ^ (1 / (2 : ℝ) - 1) = x⁻¹ := by
  rw [← rpow_mul (le_of_lt hx)]
  norm_num
  rw [rpow_neg (le_of_lt hx), rpow_one]

Result:
case h.e'_2
x : ℝ
hx : x ∈ Ioi 0
this : (x ^ 2) ^ (1 / 2 - 1) = x⁻¹
⊢ (2 * x ^ (2 - 1)) • (rexp (-x ^ 2) * (x ^ 2) ^ (1 / 2 - 1)) = 2 * rexp (-1 * x ^ 2)

Proof state:
case h.e'_2
x : ℝ
hx : x ∈ Ioi 0
this : (x ^ 2) ^ (1 / 2 - 1) = x⁻¹
⊢ 2 * x ^ (2 - 1) * (rexp (-x ^ 2) * x⁻¹) = 2 * rexp (-1 * x ^ 2)

Tactic:
field_simp [(ne_of_lt (show 0 < x from hx)).symm]

Result:
case h.e'_2
x : ℝ
hx : x ∈ Ioi 0
this : (x ^ 2) ^ (1 / 2 - 1) = x⁻¹
⊢ 2 * x ^ (2 - 1) * rexp (-x ^ 2) = 2 * rexp (-x ^ 2) * x

Proof state:
⊢ Gamma (1 / 2) = √π

Tactic:
rw [Gamma_eq_integral one_half_pos, ← integral_comp_rpow_Ioi_of_pos zero_lt_two]

Result:
⊢ ∫ (x : ℝ) in Ioi 0, (2 * x ^ (2 - 1)) • (rexp (-x ^ 2) * (x ^ 2) ^ (1 / 2 - 1)) = √π

Proof state:
x : ℝ
hx : x ∈ Ioi 0
⊢ x ^ (-1) = x⁻¹

Tactic:
rw [rpow_neg (le_of_lt hx), rpow_one]

Result:
no goals

Proof state:
case h.e'_2
x : ℝ
hx : x ∈ Ioi 0
this : (x ^ 2) ^ (1 / 2 - 1) = x⁻¹
⊢ 2 * x * rexp (-x ^ 2) = 2 * rexp (-x ^ 2) * x

Tactic:
ring

Result:
no goals

Proof state:
x : ℝ
hx : x ∈ Ioi 0
⊢ x ^ (2 * (1 / 2 - 1)) = x⁻¹

Tactic:
norm_num

Result:
x : ℝ
hx : x ∈ Ioi 0
⊢ x ^ (-1) = x⁻¹

Proof state:
case h.e'_2

⊢ ∫ (x : ℝ) in Ioi 0, (2 * x ^ (2 - 1)) • (rexp (-x ^ 2) * (x ^ 2) ^ (1 / 2 - 1)) =
    ∫ (a : ℝ) in Ioi 0, 2 * rexp (-1 * a ^ 2)

Tactic:
refine setIntegral_congr_fun measurableSet_Ioi fun x hx => ?_

Result:
case h.e'_2
x : ℝ
hx : x ∈ Ioi 0
⊢ (2 * x ^ (2 - 1)) • (rexp (-x ^ 2) * (x ^ 2) ^ (1 / 2 - 1)) = 2 * rexp (-1 * x ^ 2)