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

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

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

State before:
b x : ℝ
⊢ b / sqrt π * rexp (-(b * x) ^ 2) = b * (sqrt π)⁻¹ * rexp (-(b * x) ^ 2)
Tactic:
rfl
State after:
no goals