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

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

State before:
s a b : ℝ
⊢ s / sqrt π * ∫ (x : ℝ) in a..b, rexp (-(s * x) ^ 2) = (sqrt π)⁻¹ * ∫ (x : ℝ) in s * a..s * b, rexp (-x ^ 2)
Tactic:
rw [div_eq_inv_mul]
State after:
s a b : ℝ
⊢ (sqrt π)⁻¹ * s * ∫ (x : ℝ) in a..b, rexp (-(s * x) ^ 2) = (sqrt π)⁻¹ * ∫ (x : ℝ) in s * a..s * b, rexp (-x ^ 2)

State before:
s a b : ℝ
⊢ (sqrt π)⁻¹ * s * ∫ (x : ℝ) in a..b, rexp (-(s * x) ^ 2) = (sqrt π)⁻¹ * ∫ (x : ℝ) in s * a..s * b, rexp (-x ^ 2)
Tactic:
rw [mul_assoc]
State after:
s a b : ℝ
⊢ (sqrt π)⁻¹ * (s * ∫ (x : ℝ) in a..b, rexp (-(s * x) ^ 2)) = (sqrt π)⁻¹ * ∫ (x : ℝ) in s * a..s * b, rexp (-x ^ 2)

State before:
s a b : ℝ
⊢ (sqrt π)⁻¹ * (s * ∫ (x : ℝ) in a..b, rexp (-(s * x) ^ 2)) = (sqrt π)⁻¹ * ∫ (x : ℝ) in s * a..s * b, rexp (-x ^ 2)
Tactic:
rw [← intervalIntegral.mul_integral_comp_mul_left]
State after:
no goals