awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral (hypothesis)
Goal:
b : ℂ
hb : 0 < b.re
hb' : b ≠ 0
A :
  ∀ (x : ℂ),
    HasDerivAt (fun (x : ℂ) ↦ -(2 * b)⁻¹ * cexp (-b * HPow.hPow (β := ℕ) x 2)) (x * cexp (-b * HPow.hPow (β := ℕ) x 2))
      x
⊢ (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (r : ℝ) ↦
      (↑r : ℂ) * cexp (-b * HPow.hPow (β := ℕ) (↑r : ℂ) 2)) =
    (2 * b)⁻¹
have B : Tendsto (fun (y : ℝ) ↦ -(2 * b)⁻¹ * cexp (-b * HPow.hPow (β := ℕ) (↑y : ℂ) 2)) atTop (𝓝 (-(2 * b)⁻¹ * 0))
Tactic: have B : Tendsto (fun y : ℝ ↦ -(2 * b)⁻¹ * cexp (-b * (y : ℂ) ^ 2))
    atTop (𝓝 (-(2 * b)⁻¹ * 0)) := by
    refine Tendsto.const_mul _ (tendsto_zero_iff_norm_tendsto_zero.mpr ?_)
    simp_rw [norm_cexp_neg_mul_sq b]
    exact tendsto_exp_atBot.comp
      ((tendsto_pow_atTop two_ne_zero).const_mul_atTop_of_neg (neg_lt_zero.2 hb))
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral (goal)
Goal:
b : ℂ
hb : 0 < b.re
hb' : b ≠ 0
A :
  ∀ (x : ℂ),
    HasDerivAt (fun (x : ℂ) ↦ -(2 * b)⁻¹ * cexp (-b * HPow.hPow (β := ℕ) x 2)) (x * cexp (-b * HPow.hPow (β := ℕ) x 2))
      x
B : Tendsto (fun (y : ℝ) ↦ -(2 * b)⁻¹ * cexp (-b * HPow.hPow (β := ℕ) (↑y : ℂ) 2)) atTop (𝓝 (-(2 * b)⁻¹ * 0))
⊢ (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (r : ℝ) ↦
      (↑r : ℂ) * cexp (-b * HPow.hPow (β := ℕ) (↑r : ℂ) 2)) =
    (2 * b)⁻¹
have h : (2 * b)⁻¹ = -(2 * b)⁻¹ * 0 - -(2 * b)⁻¹ * cexp (-b * HPow.hPow (β := ℕ) (↑0 : ℂ) 2)
Tactic: convert!
    integral_Ioi_of_hasDerivAt_of_tendsto' (fun x _ => (A ↑x).comp_ofReal)
      (integrable_mul_cexp_neg_mul_sq hb).integrableOn B using 1
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral (goal)
Goal:
b : ℂ
hb : 0 < b.re
⊢ 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)
have rw : Eq (α := ℂ)
  (@integral _ _ _ _ Prod.instMeasurableSpace (Measure.prod volume volume) fun (z : ℝ × ℝ) ↦
    cexp (-b * HPow.hPow (β := ℕ) (↑z.1 : ℂ) 2) * cexp (-b * HPow.hPow (β := ℕ) (↑z.2 : ℂ) 2))
  (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (p : ℝ × ℝ) ↦
    cexp (-b * HPow.hPow (β := ℕ) (↑p.1 : ℂ) 2) * cexp (-b * HPow.hPow (β := ℕ) (↑p.2 : ℂ) 2))
Tactic: rw [pow_two, ← integral_prod_mul]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral (goal)
Goal:
b : ℂ
hb : 0 < b.re
⊢ 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)))
have e_f : Eq (α := ℝ × ℝ → ℂ)
  (fun (p : ℝ × ℝ) ↦ cexp (-b * HPow.hPow (β := ℕ) (↑p.1 : ℂ) 2) * cexp (-b * HPow.hPow (β := ℕ) (↑p.2 : ℂ) 2))
  fun (p : ℝ × ℝ) ↦ cexp (-b * (HPow.hPow (β := ℕ) (↑p.1 : ℂ) 2 + HPow.hPow (β := ℕ) (↑p.2 : ℂ) 2))
Tactic: congr
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral (goal)
Goal:
b : ℂ
hb : 0 < b.re
⊢ Eq (α := ℝ × ℝ → ℂ)
    (fun (p : ℝ × ℝ) ↦ cexp (-b * HPow.hPow (β := ℕ) (↑p.1 : ℂ) 2) * cexp (-b * HPow.hPow (β := ℕ) (↑p.2 : ℂ) 2))
    fun (p : ℝ × ℝ) ↦ cexp (-b * (HPow.hPow (β := ℕ) (↑p.1 : ℂ) 2 + HPow.hPow (β := ℕ) (↑p.2 : ℂ) 2))
have e_f : ∀ (p : ℝ × ℝ),
  cexp (-b * HPow.hPow (β := ℕ) (↑p.1 : ℂ) 2) * cexp (-b * HPow.hPow (β := ℕ) (↑p.2 : ℂ) 2) =
    cexp (-b * (HPow.hPow (β := ℕ) (↑p.1 : ℂ) 2 + HPow.hPow (β := ℕ) (↑p.2 : ℂ) 2))
Tactic: ext1 p
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral (goal)
Goal:
b : ℂ
hb : 0 < b.re
p : ℝ × ℝ
⊢ cexp (-b * HPow.hPow (β := ℕ) (↑p.1 : ℂ) 2) * cexp (-b * HPow.hPow (β := ℕ) (↑p.2 : ℂ) 2) =
    cexp (-b * (HPow.hPow (β := ℕ) (↑p.1 : ℂ) 2 + HPow.hPow (β := ℕ) (↑p.2 : ℂ) 2))
have e_f : cexp (-b * HPow.hPow (β := ℕ) (↑p.1 : ℂ) 2 + -b * HPow.hPow (β := ℕ) (↑p.2 : ℂ) 2) =
  cexp (-b * (HPow.hPow (β := ℕ) (↑p.1 : ℂ) 2 + HPow.hPow (β := ℕ) (↑p.2 : ℂ) 2))
Tactic: rw [← Complex.exp_add, mul_add]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral (goal)
Goal:
b : ℂ
hb : 0 < b.re
p : ℝ × ℝ
e_f :
  cexp (-b * HPow.hPow (β := ℕ) (↑p.1 : ℂ) 2 + -b * HPow.hPow (β := ℕ) (↑p.2 : ℂ) 2) =
    cexp (-b * (HPow.hPow (β := ℕ) (↑p.1 : ℂ) 2 + HPow.hPow (β := ℕ) (↑p.2 : ℂ) 2))
⊢ cexp (-b * HPow.hPow (β := ℕ) (↑p.1 : ℂ) 2) * cexp (-b * HPow.hPow (β := ℕ) (↑p.2 : ℂ) 2) =
    cexp (-b * (HPow.hPow (β := ℕ) (↑p.1 : ℂ) 2 + HPow.hPow (β := ℕ) (↑p.2 : ℂ) 2))
have e_f₁ : cexp (-b * HPow.hPow (β := ℕ) (↑p.1 : ℂ) 2 + -b * HPow.hPow (β := ℕ) (↑p.2 : ℂ) 2) =
  cexp (-b * HPow.hPow (β := ℕ) (↑p.1 : ℂ) 2 + -b * HPow.hPow (β := ℕ) (↑p.2 : ℂ) 2)
Tactic: rw [← Complex.exp_add, mul_add]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral (goal)
Goal:
b : ℂ
hb : 0 < b.re
⊢ 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)))
have rw : Eq (α := ℂ)
  (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume polarCoord.target) fun (p : ℝ × ℝ) ↦
    p.1 •
      cexp
        (-b *
          (HPow.hPow (β := ℕ) (↑((↑polarCoord.symm : ℝ × ℝ → ℝ × ℝ) p).1 : ℂ) 2 +
            HPow.hPow (β := ℕ) (↑((↑polarCoord.symm : ℝ × ℝ → ℝ × ℝ) 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)))
Tactic: rw [← integral_comp_polarCoord_symm]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral (goal)
Goal:
b : ℂ
hb : 0 < b.re
⊢ (@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)
have rw : Eq (α := ℂ)
  (@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)))
  (@integral _ _ _ _ Prod.instMeasurableSpace
    (Measure.restrict (Measure.prod volume volume) (SProd.sprod (α := Set ℝ) (Ioi 0) (Ioo (-π) π))) fun (z : ℝ × ℝ) ↦
    (↑z.1 : ℂ) * cexp (-b * HPow.hPow (β := ℕ) (↑z.1 : ℂ) 2) * 1)
Tactic: rw [← setIntegral_prod_mul]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral (goal)
Goal:
b : ℂ
hb : 0 < b.re
⊢ Eq (α := ℂ)
    (@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)))
    (@integral _ _ _ _ Prod.instMeasurableSpace
      (Measure.restrict (Measure.prod volume volume) (SProd.sprod (α := Set ℝ) (Ioi 0) (Ioo (-π) π))) fun (z : ℝ × ℝ) ↦
      (↑z.1 : ℂ) * cexp (-b * HPow.hPow (β := ℕ) (↑z.1 : ℂ) 2) * 1)
have e_f : ∀ (p : ℝ × ℝ),
  p.1 •
      cexp
        (-b *
          (HPow.hPow (β := ℕ) ((↑p.1 : ℂ) * Complex.cos (↑p.2 : ℂ)) 2 +
            HPow.hPow (β := ℕ) ((↑p.1 : ℂ) * Complex.sin (↑p.2 : ℂ)) 2)) =
    (↑p.1 : ℂ) * cexp (-b * HPow.hPow (β := ℕ) (↑p.1 : ℂ) 2) * 1
Tactic: congr with p : 1
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral (goal)
Goal:
b : ℂ
hb : 0 < b.re
p : ℝ × ℝ
⊢ p.1 •
      cexp
        (-b *
          (HPow.hPow (β := ℕ) ((↑p.1 : ℂ) * Complex.cos (↑p.2 : ℂ)) 2 +
            HPow.hPow (β := ℕ) ((↑p.1 : ℂ) * Complex.sin (↑p.2 : ℂ)) 2)) =
    (↑p.1 : ℂ) * cexp (-b * HPow.hPow (β := ℕ) (↑p.1 : ℂ) 2) * 1
have e_f : p.1 •
    cexp
      (-b *
        (HPow.hPow (β := ℕ) ((↑p.1 : ℂ) * Complex.cos (↑p.2 : ℂ)) 2 +
          HPow.hPow (β := ℕ) ((↑p.1 : ℂ) * Complex.sin (↑p.2 : ℂ)) 2)) =
  (↑p.1 : ℂ) * cexp (-b * HPow.hPow (β := ℕ) (↑p.1 : ℂ) 2)
Tactic: rw [mul_one]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral (goal)
Goal:
b : ℂ
hb : 0 < b.re
p : ℝ × ℝ
⊢ p.1 •
      cexp
        (-b *
          (HPow.hPow (β := ℕ) ((↑p.1 : ℂ) * Complex.cos (↑p.2 : ℂ)) 2 +
            HPow.hPow (β := ℕ) ((↑p.1 : ℂ) * Complex.sin (↑p.2 : ℂ)) 2)) =
    (↑p.1 : ℂ) * cexp (-b * HPow.hPow (β := ℕ) (↑p.1 : ℂ) 2)
have e_f : HPow.hPow (β := ℕ) ((↑p.1 : ℂ) * Complex.cos (↑p.2 : ℂ)) 2 +
    HPow.hPow (β := ℕ) ((↑p.1 : ℂ) * Complex.sin (↑p.2 : ℂ)) 2 =
  HPow.hPow (β := ℕ) (↑p.1 : ℂ) 2
Tactic: congr
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral (goal)
Goal:
b : ℂ
hb : 0 < b.re
p : ℝ × ℝ
| HPow.hPow (β := ℕ) (↑p.1 : ℂ) 2
have rw : (HPow.hPow (β := ℕ) (Complex.sin (↑p.2 : ℂ)) 2 + HPow.hPow (β := ℕ) (Complex.cos (↑p.2 : ℂ)) 2) *
  HPow.hPow (β := ℕ) (↑p.1 : ℂ) 2
Tactic: rw [← one_mul ((p.1 : ℂ) ^ 2), ← sin_sq_add_cos_sq (p.2 : ℂ)]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral (goal)
Goal:
b : ℂ
hb : 0 < b.re
p : ℝ × ℝ
⊢ HPow.hPow (β := ℕ) ((↑p.1 : ℂ) * Complex.cos (↑p.2 : ℂ)) 2 +
      HPow.hPow (β := ℕ) ((↑p.1 : ℂ) * Complex.sin (↑p.2 : ℂ)) 2 =
    HPow.hPow (β := ℕ) (↑p.1 : ℂ) 2
have e_f : HPow.hPow (β := ℕ) ((↑p.1 : ℂ) * Complex.cos (↑p.2 : ℂ)) 2 +
    HPow.hPow (β := ℕ) ((↑p.1 : ℂ) * Complex.sin (↑p.2 : ℂ)) 2 =
  (HPow.hPow (β := ℕ) (Complex.sin (↑p.2 : ℂ)) 2 + HPow.hPow (β := ℕ) (Complex.cos (↑p.2 : ℂ)) 2) *
    HPow.hPow (β := ℕ) (↑p.1 : ℂ) 2
Tactic: conv_rhs => rw [← one_mul ((p.1 : ℂ) ^ 2), ← sin_sq_add_cos_sq (p.2 : ℂ)]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral (goal)
Goal:
b : ℂ
hb : 0 < b.re
⊢ 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
have simp : (2 * b)⁻¹ * (↑(Measure.real (m := MeasureSpace.toMeasurableSpace) volume (Ioo (-π) π)) : ℂ) = (↑π : ℂ) / b
Tactic: simp only [integral_const, MeasurableSet.univ, measureReal_restrict_apply,
        univ_inter, real_smul, mul_one, integral_mul_cexp_neg_mul_sq hb]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral (goal)
Goal:
b : ℂ
hb : 0 < b.re
⊢ -π ≤ π
have linarith : π < -π → π - -π + 2 * (0 - π) = 0
Tactic: linarith [pi_nonneg]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral (goal)
Goal:
b : ℂ
hb : 0 < b.re
linarith : π < -π → π - -π + 2 * (0 - π) = 0
⊢ -π ≤ π
have linarith₁ : π < -π → GT.gt (α := ℝ) 2 0
Tactic: linarith [pi_nonneg]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral (goal)
Goal:
b : ℂ
hb : 0 < b.re
⊢ (2 * b)⁻¹ * (↑(Measure.real (m := MeasureSpace.toMeasurableSpace) volume (Ioo (-π) π)) : ℂ) = (↑π : ℂ) / b
have rw : (2 * b)⁻¹ * (↑(π - -π) : ℂ) = (↑π : ℂ) / b
Tactic: rw [volume_real_Ioo_of_le (by linarith [pi_nonneg])]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral (goal)
Goal:
b : ℂ
hb : 0 < b.re
⊢ (2 * b)⁻¹ * (↑(π - -π) : ℂ) = (↑π : ℂ) / b
have simp : b⁻¹ * 2⁻¹ * ((↑π : ℂ) + (↑π : ℂ)) = (↑π : ℂ) / b
Tactic: simp
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral (goal)
Goal:
b : ℂ
hb : 0 < b.re
⊢ HPow.hPow (α := ℂ) (β := ℕ)
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : ℝ) ↦ cexp (-b * HPow.hPow (β := ℕ) (↑x : ℂ) 2))
      2 =
    (↑π : ℂ) / b
have 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)
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
-- 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)
⊢ HPow.hPow (α := ℂ) (β := ℕ)
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : ℝ) ↦ cexp (-b * HPow.hPow (β := ℕ) (↑x : ℂ) 2))
      2 =
    (↑π : ℂ) / b
have 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)))
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
-- 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)))
⊢ HPow.hPow (α := ℂ) (β := ℕ)
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : ℝ) ↦ cexp (-b * HPow.hPow (β := ℕ) (↑x : ℂ) 2))
      2 =
    (↑π : ℂ) / b
have 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)))
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
-- 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)))
⊢ HPow.hPow (α := ℂ) (β := ℕ)
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : ℝ) ↦ cexp (-b * HPow.hPow (β := ℕ) (↑x : ℂ) 2))
      2 =
    (↑π : ℂ) / b
have 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)
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
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral (goal)
Goal:
b : ℝ
⊢ (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : ℝ) ↦ rexp (-b * HPow.hPow (β := ℕ) x 2)) = √(π / b)
have inl : ∀ (hb : b ≤ 0),
  (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : ℝ) ↦ rexp (-b * HPow.hPow (β := ℕ) x 2)) = √(π / b)
Tactic: rcases le_or_gt b 0 with (hb | hb)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral (goal)
Goal:
b : ℝ
inl :
  ∀ (hb : b ≤ 0),
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : ℝ) ↦ rexp (-b * HPow.hPow (β := ℕ) x 2)) =
      √(π / b)
⊢ (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : ℝ) ↦ rexp (-b * HPow.hPow (β := ℕ) x 2)) = √(π / b)
have inr : ∀ (hb : 0 < b),
  (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : ℝ) ↦ rexp (-b * HPow.hPow (β := ℕ) x 2)) = √(π / b)
Tactic: rcases le_or_gt b 0 with (hb | hb)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral (goal)
Goal:
b : ℝ
hb : b ≤ 0
⊢ (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : ℝ) ↦ rexp (-b * HPow.hPow (β := ℕ) x 2)) = √(π / b)
have inl : π / b ≤ 0
Tactic: rw [integral_undef, sqrt_eq_zero_of_nonpos]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral (goal)
Goal:
b : ℝ
hb : b ≤ 0
inl : π / b ≤ 0
⊢ (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : ℝ) ↦ rexp (-b * HPow.hPow (β := ℕ) x 2)) = √(π / b)
have inl₁ : ¬@Integrable ℝ _ _ _ MeasureSpace.toMeasurableSpace (fun (x : ℝ) ↦ rexp (-b * HPow.hPow (β := ℕ) x 2)) volume
Tactic: rw [integral_undef, sqrt_eq_zero_of_nonpos]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral (goal)
Goal:
b : ℝ
hb : 0 < b
⊢ (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : ℝ) ↦ rexp (-b * HPow.hPow (β := ℕ) x 2)) = √(π / b)
have inr : HPow.hPow (α := ℝ) (β := ℕ)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : ℝ) ↦ rexp (-b * HPow.hPow (β := ℕ) x 2)) 2 =
  HPow.hPow (β := ℕ) (√(π / b)) 2
Tactic: refine (sq_eq_sq₀ (by positivity) (by positivity)).1 ?_