Theorem: DiracSeq.expNegSq (ForML/Dirac.lean)

State before:
x : ℝ
⊢ sqrt π * DiracSeq 1 x = rexp (-x ^ 2)
Tactic:
simp [DiracSeq]
State after:
x : ℝ
⊢ sqrt π * ((sqrt π)⁻¹ * rexp (-x ^ 2)) = rexp (-x ^ 2)

State before:
x : ℝ
⊢ sqrt π * ((sqrt π)⁻¹ * rexp (-x ^ 2)) = rexp (-x ^ 2)
Tactic:
rw [← mul_assoc]
State after:
x : ℝ
⊢ sqrt π * (sqrt π)⁻¹ * rexp (-x ^ 2) = rexp (-x ^ 2)

State before:
x : ℝ
⊢ sqrt π * (sqrt π)⁻¹ * rexp (-x ^ 2) = rexp (-x ^ 2)
Tactic:
rw [mul_inv_cancel sqrt_pi_pos.ne']
State after:
x : ℝ
⊢ 1 * rexp (-x ^ 2) = rexp (-x ^ 2)

State before:
x : ℝ
⊢ 1 * rexp (-x ^ 2) = rexp (-x ^ 2)
Tactic:
simp
State after:
no goals