-- Mathlib/Probability/Distributions/Gaussian.lean
lemma gaussianPDFReal_inv_mul {μ : ℝ} {v : ℝ≥0} {c : ℝ} (hc : c ≠ 0) (x : ℝ) :
    gaussianPDFReal μ v (c⁻¹ * x) = |c| * gaussianPDFReal (c * μ) (⟨c^2, sq_nonneg _⟩ * v) x

Proof state:
case refine_2.e_x
μ : ℝ
v : ℝ≥0
c : ℝ
hc : c ≠ 0
x : ℝ
⊢ -(x - c * μ) ^ 2 / (c ^ 2 * (2 * ↑v)) = -(x - c * μ) ^ 2 / (2 * (c ^ 2 * ↑v))

Tactic:
congr 1

Result:
case refine_2.e_x.e_a
μ : ℝ
v : ℝ≥0
c : ℝ
hc : c ≠ 0
x : ℝ
⊢ c ^ 2 * (2 * ↑v) = 2 * (c ^ 2 * ↑v)

Proof state:
case refine_2.e_x.e_a
μ : ℝ
v : ℝ≥0
c : ℝ
hc : c ≠ 0
x : ℝ
⊢ c ^ 2 * (2 * ↑v) = 2 * (c ^ 2 * ↑v)

Tactic:
ring

Result:
no goals

Proof state:
μ : ℝ
v : ℝ≥0
c : ℝ
hc : c ≠ 0
x : ℝ
⊢ (√↑v)⁻¹ * (√(2 * π))⁻¹ * rexp (-(c⁻¹ * x - μ) ^ 2 / (2 * ↑v)) =
    |c| * (√(2 * π * (c ^ 2 * ↑v)))⁻¹ * rexp (-(x - c * μ) ^ 2 / (2 * (c ^ 2 * ↑v)))

Tactic:
refine congr_arg₂ _ ?_ ?_

Result:
case refine_1
μ : ℝ
v : ℝ≥0
c : ℝ
hc : c ≠ 0
x : ℝ
⊢ (√↑v)⁻¹ * (√(2 * π))⁻¹ = |c| * (√(2 * π * (c ^ 2 * ↑v)))⁻¹

case refine_2
μ : ℝ
v : ℝ≥0
c : ℝ
hc : c ≠ 0
x : ℝ
⊢ rexp (-(c⁻¹ * x - μ) ^ 2 / (2 * ↑v)) = rexp (-(x - c * μ) ^ 2 / (2 * (c ^ 2 * ↑v)))

Proof state:
μ : ℝ
v : ℝ≥0
c : ℝ
hc : c ≠ 0
x : ℝ
⊢ (√↑v)⁻¹ * (√(2 * π))⁻¹ * rexp (-(c⁻¹ * x - μ) ^ 2 / (2 * ↑v)) =
    |c| * ((√(2 * π * (c ^ 2 * ↑v)))⁻¹ * rexp (-(x - c * μ) ^ 2 / (2 * (c ^ 2 * ↑v))))

Tactic:
rw [← mul_assoc]

Result:
μ : ℝ
v : ℝ≥0
c : ℝ
hc : c ≠ 0
x : ℝ
⊢ (√↑v)⁻¹ * (√(2 * π))⁻¹ * rexp (-(c⁻¹ * x - μ) ^ 2 / (2 * ↑v)) =
    |c| * (√(2 * π * (c ^ 2 * ↑v)))⁻¹ * rexp (-(x - c * μ) ^ 2 / (2 * (c ^ 2 * ↑v)))

Proof state:
case refine_2
μ : ℝ
v : ℝ≥0
c : ℝ
hc : c ≠ 0
x : ℝ
⊢ rexp (-(c⁻¹ * x - μ) ^ 2 / (2 * ↑v)) = rexp (-(x - c * μ) ^ 2 / (2 * (c ^ 2 * ↑v)))

Tactic:
congr 1

Result:
case refine_2.e_x
μ : ℝ
v : ℝ≥0
c : ℝ
hc : c ≠ 0
x : ℝ
⊢ -(c⁻¹ * x - μ) ^ 2 / (2 * ↑v) = -(x - c * μ) ^ 2 / (2 * (c ^ 2 * ↑v))

Proof state:
μ : ℝ
v : ℝ≥0
c : ℝ
hc : c ≠ 0
x : ℝ
⊢ (√↑v)⁻¹ * (√2)⁻¹ * (√π)⁻¹ * (|c| * |c|⁻¹) = (√↑v)⁻¹ * (√2)⁻¹ * (√π)⁻¹ * |c| * |c|⁻¹

Tactic:
ring

Result:
no goals

Proof state:
case refine_1
μ : ℝ
v : ℝ≥0
c : ℝ
hc : c ≠ 0
x : ℝ
⊢ (√↑v)⁻¹ * (√2)⁻¹ * (√π)⁻¹ = (√↑v)⁻¹ * (√2)⁻¹ * (√π)⁻¹ * |c| * |c|⁻¹

Tactic:
calc (Real.sqrt ↑v)⁻¹ * (Real.sqrt 2)⁻¹ * (Real.sqrt π)⁻¹
  = (Real.sqrt ↑v)⁻¹ * (Real.sqrt 2)⁻¹ * (Real.sqrt π)⁻¹ * (|c| * |c|⁻¹) := by
      rw [mul_inv_cancel₀, mul_one]
      simp only [ne_eq, abs_eq_zero, hc, not_false_eq_true]
_ = (Real.sqrt ↑v)⁻¹ * (Real.sqrt 2)⁻¹ * (Real.sqrt π)⁻¹ * |c| * |c|⁻¹ := by ring

Result:
no goals

Proof state:
case refine_2.e_x
μ : ℝ
v : ℝ≥0
c : ℝ
hc : c ≠ 0
x : ℝ
⊢ -(c⁻¹ * x - μ) ^ 2 / (2 * ↑v) = -(x - c * μ) ^ 2 / (2 * (c ^ 2 * ↑v))

Tactic:
field_simp

Result:
case refine_2.e_x
μ : ℝ
v : ℝ≥0
c : ℝ
hc : c ≠ 0
x : ℝ
⊢ -(x - c * μ) ^ 2 / (c ^ 2 * (2 * ↑v)) = -(x - c * μ) ^ 2 / (2 * (c ^ 2 * ↑v))

Proof state:
μ : ℝ
v : ℝ≥0
c : ℝ
hc : c ≠ 0
x : ℝ
⊢ |c| ≠ 0

Tactic:
simp only [ne_eq, abs_eq_zero, hc, not_false_eq_true]

Result:
no goals

Proof state:
μ : ℝ
v : ℝ≥0
c : ℝ
hc : c ≠ 0
x : ℝ
⊢ gaussianPDFReal μ v (c⁻¹ * x) = |c| * gaussianPDFReal (c * μ) (⟨c ^ 2, ⋯⟩ * v) x

Tactic:
simp only [gaussianPDFReal.eq_1, zero_lt_two, mul_nonneg_iff_of_pos_left, NNReal.zero_le_coe,
  Real.sqrt_mul', one_div, mul_inv_rev, NNReal.coe_mul, NNReal.coe_mk, NNReal.coe_pos]

Result:
μ : ℝ
v : ℝ≥0
c : ℝ
hc : c ≠ 0
x : ℝ
⊢ (√↑v)⁻¹ * (√(2 * π))⁻¹ * rexp (-(c⁻¹ * x - μ) ^ 2 / (2 * ↑v)) =
    |c| * ((√(2 * π * (c ^ 2 * ↑v)))⁻¹ * rexp (-(x - c * μ) ^ 2 / (2 * (c ^ 2 * ↑v))))

Proof state:
case refine_1
μ : ℝ
v : ℝ≥0
c : ℝ
hc : c ≠ 0
x : ℝ
⊢ 1 / (√↑v * (√2 * √π)) = |c| / (√2 * √π * (|c| * √↑v))

Tactic:
ring_nf

Result:
case refine_1
μ : ℝ
v : ℝ≥0
c : ℝ
hc : c ≠ 0
x : ℝ
⊢ (√↑v)⁻¹ * (√2)⁻¹ * (√π)⁻¹ = (√↑v)⁻¹ * (√2)⁻¹ * (√π)⁻¹ * |c| * |c|⁻¹

Proof state:
case refine_1
μ : ℝ
v : ℝ≥0
c : ℝ
hc : c ≠ 0
x : ℝ
⊢ (√↑v)⁻¹ * (√(2 * π))⁻¹ = |c| * (√(2 * π * (c ^ 2 * ↑v)))⁻¹

Tactic:
field_simp

Result:
case refine_1
μ : ℝ
v : ℝ≥0
c : ℝ
hc : c ≠ 0
x : ℝ
⊢ 1 / (√↑v * (√2 * √π)) = |c| / (√2 * √π * (√(c ^ 2) * √↑v))

Proof state:
μ : ℝ
v : ℝ≥0
c : ℝ
hc : c ≠ 0
x : ℝ
⊢ (√↑v)⁻¹ * (√2)⁻¹ * (√π)⁻¹ = (√↑v)⁻¹ * (√2)⁻¹ * (√π)⁻¹ * (|c| * |c|⁻¹)

Tactic:
rw [mul_inv_cancel₀, mul_one]

Result:
μ : ℝ
v : ℝ≥0
c : ℝ
hc : c ≠ 0
x : ℝ
⊢ |c| ≠ 0

Proof state:
case refine_1
μ : ℝ
v : ℝ≥0
c : ℝ
hc : c ≠ 0
x : ℝ
⊢ 1 / (√↑v * (√2 * √π)) = |c| / (√2 * √π * (√(c ^ 2) * √↑v))

Tactic:
rw [Real.sqrt_sq_eq_abs]

Result:
case refine_1
μ : ℝ
v : ℝ≥0
c : ℝ
hc : c ≠ 0
x : ℝ
⊢ 1 / (√↑v * (√2 * √π)) = |c| / (√2 * √π * (|c| * √↑v))