-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral (goal)
Goal:
b : ℂ
hb : 0 < b.re
x :
  HPow.hPow (α := ℂ) (β := ℕ)
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : ℝ) ↦ cexp (-b * HPow.hPow (β := ℕ) (↑x : ℂ) 2))
      2 =
    @integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (p : ℝ × ℝ) ↦
      cexp (-b * HPow.hPow (β := ℕ) (↑p.1 : ℂ) 2) * cexp (-b * HPow.hPow (β := ℕ) (↑p.2 : ℂ) 2)
x₁ :
  Eq (α := ℂ)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (p : ℝ × ℝ) ↦
      cexp (-b * HPow.hPow (β := ℕ) (↑p.1 : ℂ) 2) * cexp (-b * HPow.hPow (β := ℕ) (↑p.2 : ℂ) 2))
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (p : ℝ × ℝ) ↦
      cexp (-b * (HPow.hPow (β := ℕ) (↑p.1 : ℂ) 2 + HPow.hPow (β := ℕ) (↑p.2 : ℂ) 2)))
x₂ :
  Eq (α := ℂ)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (p : ℝ × ℝ) ↦
      cexp (-b * (HPow.hPow (β := ℕ) (↑p.1 : ℂ) 2 + HPow.hPow (β := ℕ) (↑p.2 : ℂ) 2)))
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume polarCoord.target) fun (p : ℝ × ℝ) ↦
      p.1 •
        cexp
          (-b *
            (HPow.hPow (β := ℕ) ((↑p.1 : ℂ) * Complex.cos (↑p.2 : ℂ)) 2 +
              HPow.hPow (β := ℕ) ((↑p.1 : ℂ) * Complex.sin (↑p.2 : ℂ)) 2)))
x₃ :
  (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume polarCoord.target) fun (p : ℝ × ℝ) ↦
      p.1 •
        cexp
          (-b *
            (HPow.hPow (β := ℕ) ((↑p.1 : ℂ) * Complex.cos (↑p.2 : ℂ)) 2 +
              HPow.hPow (β := ℕ) ((↑p.1 : ℂ) * Complex.sin (↑p.2 : ℂ)) 2))) =
    HMul.hMul (α := ℂ)
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (r : ℝ) ↦
        (↑r : ℂ) * cexp (-b * HPow.hPow (β := ℕ) (↑r : ℂ) 2))
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioo (-π) π)) fun (θ : ℝ) ↦ 1)
⊢ HPow.hPow (α := ℂ) (β := ℕ)
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : ℝ) ↦ cexp (-b * HPow.hPow (β := ℕ) (↑x : ℂ) 2))
      2 =
    (↑π : ℂ) / b
have x₄ : HMul.hMul (α := ℂ)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (r : ℝ) ↦
      (↑r : ℂ) * cexp (-b * HPow.hPow (β := ℕ) (↑r : ℂ) 2))
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioo (-π) π)) fun (θ : ℝ) ↦ 1) =
  (↑π : ℂ) / b
Tactic: calc
    (∫ x : ℝ, cexp (-b * (x : ℂ) ^ 2)) ^ 2 =
        ∫ p : ℝ × ℝ, cexp (-b * (p.1 : ℂ) ^ 2) * cexp (-b * (p.2 : ℂ) ^ 2) := by
      rw [pow_two, ← integral_prod_mul]; rfl
    _ = ∫ p : ℝ × ℝ, cexp (-b * ((p.1 : ℂ) ^ 2 + (p.2 : ℂ) ^ 2)) := by
      congr
      ext1 p
      rw [← Complex.exp_add, mul_add]
    _ = ∫ p in polarCoord.target, p.1 •
        cexp (-b * ((p.1 * Complex.cos p.2) ^ 2 + (p.1 * Complex.sin p.2) ^ 2)) := by
      rw [← integral_comp_polarCoord_symm]
      simp only [polarCoord_symm_apply, ofReal_mul, ofReal_cos, ofReal_sin]
    _ = (∫ r in Ioi (0 : ℝ), r * cexp (-b * (r : ℂ) ^ 2)) * ∫ θ in Ioo (-π) π, 1 := by
      rw [← setIntegral_prod_mul]
      congr with p : 1
      rw [mul_one]
      congr
      conv_rhs => rw [← one_mul ((p.1 : ℂ) ^ 2), ← sin_sq_add_cos_sq (p.2 : ℂ)]
      ring
    _ = ↑π / b := by
      simp only [integral_const, MeasurableSet.univ, measureReal_restrict_apply,
        univ_inter, real_smul, mul_one, integral_mul_cexp_neg_mul_sq hb]
      rw [volume_real_Ioo_of_le (by linarith [pi_nonneg])]
      simp
      ring