awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gaussian.Real (goal)
Goal:
μ : ℝ
v : ℝ≥0
c : ℝ
hv : ¬v = 0
pos :
  ∀ (hc : c = 0),
    Measure.map (fun (x : ℝ) ↦ c * x) (gaussianReal μ v) =
      gaussianReal (c * μ) (NNReal.mk (HPow.hPow (β := ℕ) c 2) ⋯ * v)
⊢ Measure.map (fun (x : ℝ) ↦ c * x) (gaussianReal μ v) = gaussianReal (c * μ) (NNReal.mk (HPow.hPow (β := ℕ) c 2) ⋯ * v)
have neg : ∀ (hc : ¬c = 0),
  Measure.map (fun (x : ℝ) ↦ c * x) (gaussianReal μ v) = gaussianReal (c * μ) (NNReal.mk (HPow.hPow (β := ℕ) c 2) sorry * v)
Tactic: by_cases hc : c = 0
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gaussian.Real (goal)
Goal:
μ : ℝ
v : ℝ≥0
c : ℝ
hv : ¬v = 0
hc : ¬c = 0
e : ℝ ≃ᵐ ℝ := Homeomorph.toMeasurableEquiv (Homeomorph.symm (Homeomorph.mulLeft₀ c hc))
this : ∀ (x : ℝ), HasDerivAt (fun (x : ℝ) ↦ c⁻¹ * x) (c⁻¹ * 1) x
⊢ ∀ (x : ℝ), HasDerivAt (F := ℝ) (⇑e : (a : ℝ) → ℝ) ((fun (x : ℝ) ↦ c⁻¹) x) x
have rwa : ∀ (this : ∀ (x : ℝ), HasDerivAt (fun (x : ℝ) ↦ c⁻¹ * x) c⁻¹ x) (x : ℝ),
  HasDerivAt (F := ℝ) (⇑e : (a : ℝ) → ℝ) ((fun (x : ℝ) ↦ c⁻¹) x) x
Tactic: rwa [mul_one] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gaussian.Real (goal)
Goal:
μ : ℝ
v : ℝ≥0
c : ℝ
hv : ¬v = 0
hc : ¬c = 0
e : ℝ ≃ᵐ ℝ := Homeomorph.toMeasurableEquiv (Homeomorph.symm (Homeomorph.mulLeft₀ c hc))
⊢ ∀ (x : ℝ), HasDerivAt (F := ℝ) (⇑e : (a : ℝ) → ℝ) ((fun (x : ℝ) ↦ c⁻¹) x) x
have suffices : ∀ (x : ℝ), HasDerivAt (fun (x : ℝ) ↦ c⁻¹ * x) (c⁻¹ * 1) x
Tactic: suffices ∀ x, HasDerivAt (fun x => c⁻¹ * x) (c⁻¹ * 1) x by rwa [mul_one] at this
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gaussian.Real (hypothesis)
Goal:
μ : ℝ
v : ℝ≥0
c : ℝ
hv : ¬v = 0
hc : ¬c = 0
e : ℝ ≃ᵐ ℝ := Homeomorph.toMeasurableEquiv (Homeomorph.symm (Homeomorph.mulLeft₀ c hc))
⊢ Measure.map (fun (x : ℝ) ↦ c * x) (gaussianReal μ v) = gaussianReal (c * μ) (NNReal.mk (HPow.hPow (β := ℕ) c 2) ⋯ * v)
have he' : ∀ (x : ℝ), HasDerivAt (F := ℝ) (⇑e : (a : ℝ) → ℝ) ((fun (x : ℝ) ↦ c⁻¹) x) x
Tactic: have he' : ∀ x, HasDerivAt e ((fun _ ↦ c⁻¹) x) x := by
    suffices ∀ x, HasDerivAt (fun x => c⁻¹ * x) (c⁻¹ * 1) x by rwa [mul_one] at this
    exact fun _ ↦ HasDerivAt.const_mul _ (hasDerivAt_id _)
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gaussian.Real (goal)
Goal:
μ : ℝ
v : ℝ≥0
c : ℝ
hv : ¬v = 0
hc : ¬c = 0
e : ℝ ≃ᵐ ℝ := Homeomorph.toMeasurableEquiv (Homeomorph.symm (Homeomorph.mulLeft₀ c hc))
he' : ∀ (x : ℝ), HasDerivAt (F := ℝ) (⇑e : (a : ℝ) → ℝ) ((fun (x : ℝ) ↦ c⁻¹) x) x
⊢ Measure.map (fun (x : ℝ) ↦ c * x) (gaussianReal μ v) = gaussianReal (c * μ) (NNReal.mk (HPow.hPow (β := ℕ) c 2) ⋯ * v)
have neg : Measure.map (⇑e.symm : (a : ℝ) → ℝ) (gaussianReal μ v) = gaussianReal (c * μ) (NNReal.mk (HPow.hPow (β := ℕ) c 2) sorry * v)
Tactic: change (gaussianReal μ v).map e.symm = gaussianReal (c * μ) (.mk (c ^ 2) (sq_nonneg _) * v)
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gaussian.Real (goal)
Goal:
μ : ℝ
v : ℝ≥0
c : ℝ
hv : ¬v = 0
hc : ¬c = 0
e : ℝ ≃ᵐ ℝ := Homeomorph.toMeasurableEquiv (Homeomorph.symm (Homeomorph.mulLeft₀ c hc))
he' : ∀ (x : ℝ), HasDerivAt (F := ℝ) (⇑e : (a : ℝ) → ℝ) ((fun (x : ℝ) ↦ c⁻¹) x) x
⊢ Measure.map (⇑e.symm : (a : ℝ) → ℝ) (gaussianReal μ v) =
    gaussianReal (c * μ) (NNReal.mk (HPow.hPow (β := ℕ) c 2) ⋯ * v)
have neg : ∀ (s' : Set ℝ) (hs' : MeasurableSet s'),
  Eq (α := ℝ≥0∞) ((Measure.map (⇑e.symm : (a : ℝ) → ℝ) (gaussianReal μ v) : (a : Set ℝ) → ℝ≥0∞) s' : ℝ≥0∞)
    ((gaussianReal (c * μ) (NNReal.mk (HPow.hPow (β := ℕ) c 2) sorry * v) : (a : Set ℝ) → ℝ≥0∞) s' : ℝ≥0∞)
Tactic: ext s' hs'
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gaussian.Real (goal)
Goal:
μ : ℝ
v : ℝ≥0
c : ℝ
hv : ¬v = 0
hc : ¬c = 0
e : ℝ ≃ᵐ ℝ := Homeomorph.toMeasurableEquiv (Homeomorph.symm (Homeomorph.mulLeft₀ c hc))
he' : ∀ (x : ℝ), HasDerivAt (F := ℝ) (⇑e : (a : ℝ) → ℝ) ((fun (x : ℝ) ↦ c⁻¹) x) x
s' : Set ℝ
hs' : MeasurableSet s'
⊢ Eq (α := ℝ≥0∞) ((Measure.map (⇑e.symm : (a : ℝ) → ℝ) (gaussianReal μ v) : (a : Set ℝ) → ℝ≥0∞) s' : ℝ≥0∞)
    ((gaussianReal (c * μ) (NNReal.mk (HPow.hPow (β := ℕ) c 2) ⋯ * v) : (a : Set ℝ) → ℝ≥0∞) s' : ℝ≥0∞)
have neg : ENNReal.ofReal
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict ℙ s') fun (x : ℝ) ↦
      |c⁻¹| * gaussianPDFReal μ v ((e : (a : ℝ) → ℝ) x)) =
  ENNReal.ofReal
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict ℙ s') fun (x : ℝ) ↦
      gaussianPDFReal (c * μ) (NNReal.mk (HPow.hPow (β := ℕ) c 2) sorry * v) x)
Tactic: rw [MeasurableEquiv.gaussianReal_map_symm_apply hv e he' hs',
    gaussianReal_apply_eq_integral _ _ s']
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gaussian.Real (goal)
Goal:
μ : ℝ
v : ℝ≥0
c : ℝ
hv : ¬v = 0
hc : ¬c = 0
e : ℝ ≃ᵐ ℝ := Homeomorph.toMeasurableEquiv (Homeomorph.symm (Homeomorph.mulLeft₀ c hc))
he' : ∀ (x : ℝ), HasDerivAt (F := ℝ) (⇑e : (a : ℝ) → ℝ) ((fun (x : ℝ) ↦ c⁻¹) x) x
s' : Set ℝ
hs' : MeasurableSet s'
neg :
  ENNReal.ofReal
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict ℙ s') fun (x : ℝ) ↦
        |c⁻¹| * gaussianPDFReal μ v ((e : (a : ℝ) → ℝ) x)) =
    ENNReal.ofReal
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict ℙ s') fun (x : ℝ) ↦
        gaussianPDFReal (c * μ) (NNReal.mk (HPow.hPow (β := ℕ) c 2) ⋯ * v) x)
⊢ Eq (α := ℝ≥0∞) ((Measure.map (⇑e.symm : (a : ℝ) → ℝ) (gaussianReal μ v) : (a : Set ℝ) → ℝ≥0∞) s' : ℝ≥0∞)
    ((gaussianReal (c * μ) (NNReal.mk (HPow.hPow (β := ℕ) c 2) ⋯ * v) : (a : Set ℝ) → ℝ≥0∞) s' : ℝ≥0∞)
have rw : NNReal.mk (HPow.hPow (β := ℕ) c 2) sorry * v ≠ 0
Tactic: rw [MeasurableEquiv.gaussianReal_map_symm_apply hv e he' hs',
    gaussianReal_apply_eq_integral _ _ s']
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gaussian.Real (goal)
Goal:
μ : ℝ
v : ℝ≥0
c : ℝ
hv : ¬v = 0
hc : ¬c = 0
e : ℝ ≃ᵐ ℝ := Homeomorph.toMeasurableEquiv (Homeomorph.symm (Homeomorph.mulLeft₀ c hc))
he' : ∀ (x : ℝ), HasDerivAt (F := ℝ) (⇑e : (a : ℝ) → ℝ) ((fun (x : ℝ) ↦ c⁻¹) x) x
s' : Set ℝ
hs' : MeasurableSet s'
⊢ NNReal.mk (HPow.hPow (β := ℕ) c 2) ⋯ * v ≠ 0
have simp : ¬NNReal.mk (HPow.hPow (β := ℕ) c 2) sorry = 0
Tactic: simp only [ne_eq, mul_eq_zero, hv, or_false]
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gaussian.Real (goal)
Goal:
μ : ℝ
v : ℝ≥0
c : ℝ
hv : ¬v = 0
hc : ¬c = 0
e : ℝ ≃ᵐ ℝ := Homeomorph.toMeasurableEquiv (Homeomorph.symm (Homeomorph.mulLeft₀ c hc))
he' : ∀ (x : ℝ), HasDerivAt (F := ℝ) (⇑e : (a : ℝ) → ℝ) ((fun (x : ℝ) ↦ c⁻¹) x) x
s' : Set ℝ
hs' : MeasurableSet s'
⊢ ¬NNReal.mk (HPow.hPow (β := ℕ) c 2) ⋯ = 0
have rw : ¬(↑(NNReal.mk (HPow.hPow (β := ℕ) c 2) sorry) : ℝ) = (↑0 : ℝ)
Tactic: rw [← NNReal.coe_inj]
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gaussian.Real (goal)
Goal:
μ : ℝ
v : ℝ≥0
c : ℝ
hv : ¬v = 0
hc : ¬c = 0
e : ℝ ≃ᵐ ℝ := Homeomorph.toMeasurableEquiv (Homeomorph.symm (Homeomorph.mulLeft₀ c hc))
he' : ∀ (x : ℝ), HasDerivAt (F := ℝ) (⇑e : (a : ℝ) → ℝ) ((fun (x : ℝ) ↦ c⁻¹) x) x
s' : Set ℝ
hs' : MeasurableSet s'
⊢ ENNReal.ofReal
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict ℙ s') fun (x : ℝ) ↦
        |c⁻¹| * gaussianPDFReal μ v ((e : (a : ℝ) → ℝ) x)) =
    ENNReal.ofReal
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict ℙ s') fun (x : ℝ) ↦
        gaussianPDFReal (c * μ) (NNReal.mk (HPow.hPow (β := ℕ) c 2) ⋯ * v) x)
have neg : ENNReal.ofReal
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict ℙ s') fun (x : ℝ) ↦
      |c⁻¹| * (|c| * gaussianPDFReal (c * μ) (NNReal.mk (HPow.hPow (β := ℕ) c 2) sorry * v) x)) =
  ENNReal.ofReal
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict ℙ s') fun (x : ℝ) ↦
      gaussianPDFReal (c * μ) (NNReal.mk (HPow.hPow (β := ℕ) c 2) sorry * v) x)
Tactic: simp only [e, Homeomorph.mulLeft₀,
    Equiv.mulLeft₀_symm_apply, Homeomorph.toMeasurableEquiv_coe, Homeomorph.homeomorph_mk_coe_symm,
    gaussianPDFReal_inv_mul hc]
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gaussian.Real (goal)
Goal:
μ : ℝ
v : ℝ≥0
c : ℝ
hv : ¬v = 0
hc : ¬c = 0
e : ℝ ≃ᵐ ℝ := Homeomorph.toMeasurableEquiv (Homeomorph.symm (Homeomorph.mulLeft₀ c hc))
he' : ∀ (x : ℝ), HasDerivAt (F := ℝ) (⇑e : (a : ℝ) → ℝ) ((fun (x : ℝ) ↦ c⁻¹) x) x
s' : Set ℝ
hs' : MeasurableSet s'
⊢ ENNReal.ofReal
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict ℙ s') fun (x : ℝ) ↦
        |c⁻¹| * (|c| * gaussianPDFReal (c * μ) (NNReal.mk (HPow.hPow (β := ℕ) c 2) ⋯ * v) x)) =
    ENNReal.ofReal
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict ℙ s') fun (x : ℝ) ↦
        gaussianPDFReal (c * μ) (NNReal.mk (HPow.hPow (β := ℕ) c 2) ⋯ * v) x)
have neg : ∀ (x : ℝ),
  |c⁻¹| * (|c| * gaussianPDFReal (c * μ) (NNReal.mk (HPow.hPow (β := ℕ) c 2) sorry * v) x) =
    gaussianPDFReal (c * μ) (NNReal.mk (HPow.hPow (β := ℕ) c 2) sorry * v) x
Tactic: congr with x
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gaussian.Real (goal)
Goal:
μ : ℝ
v : ℝ≥0
c : ℝ
hv : ¬v = 0
hc : ¬c = 0
e : ℝ ≃ᵐ ℝ := Homeomorph.toMeasurableEquiv (Homeomorph.symm (Homeomorph.mulLeft₀ c hc))
he' : ∀ (x : ℝ), HasDerivAt (F := ℝ) (⇑e : (a : ℝ) → ℝ) ((fun (x : ℝ) ↦ c⁻¹) x) x
s' : Set ℝ
hs' : MeasurableSet s'
x : ℝ
this : |c⁻¹| * |c| = 1
⊢ |c⁻¹| * (|c| * gaussianPDFReal (c * μ) (NNReal.mk (HPow.hPow (β := ℕ) c 2) ⋯ * v) x) =
    gaussianPDFReal (c * μ) (NNReal.mk (HPow.hPow (β := ℕ) c 2) ⋯ * v) x
have rw : |c⁻¹| * |c| * gaussianPDFReal (c * μ) (NNReal.mk (HPow.hPow (β := ℕ) c 2) sorry * v) x =
  gaussianPDFReal (c * μ) (NNReal.mk (HPow.hPow (β := ℕ) c 2) sorry * v) x
Tactic: rw [← mul_assoc, this, one_mul]
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gaussian.Real (goal)
Goal:
μ : ℝ
v : ℝ≥0
c : ℝ
hv : ¬v = 0
hc : ¬c = 0
e : ℝ ≃ᵐ ℝ := Homeomorph.toMeasurableEquiv (Homeomorph.symm (Homeomorph.mulLeft₀ c hc))
he' : ∀ (x : ℝ), HasDerivAt (F := ℝ) (⇑e : (a : ℝ) → ℝ) ((fun (x : ℝ) ↦ c⁻¹) x) x
s' : Set ℝ
hs' : MeasurableSet s'
x : ℝ
this : |c⁻¹| * |c| = 1
rw :
  |c⁻¹| * |c| * gaussianPDFReal (c * μ) (NNReal.mk (HPow.hPow (β := ℕ) c 2) ⋯ * v) x =
    gaussianPDFReal (c * μ) (NNReal.mk (HPow.hPow (β := ℕ) c 2) ⋯ * v) x
⊢ |c⁻¹| * (|c| * gaussianPDFReal (c * μ) (NNReal.mk (HPow.hPow (β := ℕ) c 2) ⋯ * v) x) =
    gaussianPDFReal (c * μ) (NNReal.mk (HPow.hPow (β := ℕ) c 2) ⋯ * v) x
have rw₁ : 1 * gaussianPDFReal (c * μ) (NNReal.mk (HPow.hPow (β := ℕ) c 2) sorry * v) x =
  gaussianPDFReal (c * μ) (NNReal.mk (HPow.hPow (β := ℕ) c 2) sorry * v) x
Tactic: rw [← mul_assoc, this, one_mul]
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gaussian.Real (goal)
Goal:
μ : ℝ
v : ℝ≥0
c : ℝ
hv : ¬v = 0
hc : ¬c = 0
e : ℝ ≃ᵐ ℝ := Homeomorph.toMeasurableEquiv (Homeomorph.symm (Homeomorph.mulLeft₀ c hc))
he' : ∀ (x : ℝ), HasDerivAt (F := ℝ) (⇑e : (a : ℝ) → ℝ) ((fun (x : ℝ) ↦ c⁻¹) x) x
s' : Set ℝ
hs' : MeasurableSet s'
x : ℝ
this : |c⁻¹| * |c| = 1
rw :
  |c⁻¹| * |c| * gaussianPDFReal (c * μ) (NNReal.mk (HPow.hPow (β := ℕ) c 2) ⋯ * v) x =
    gaussianPDFReal (c * μ) (NNReal.mk (HPow.hPow (β := ℕ) c 2) ⋯ * v) x
rw₁ :
  1 * gaussianPDFReal (c * μ) (NNReal.mk (HPow.hPow (β := ℕ) c 2) ⋯ * v) x =
    gaussianPDFReal (c * μ) (NNReal.mk (HPow.hPow (β := ℕ) c 2) ⋯ * v) x
⊢ |c⁻¹| * (|c| * gaussianPDFReal (c * μ) (NNReal.mk (HPow.hPow (β := ℕ) c 2) ⋯ * v) x) =
    gaussianPDFReal (c * μ) (NNReal.mk (HPow.hPow (β := ℕ) c 2) ⋯ * v) x
have rw₂ : gaussianPDFReal (c * μ) (NNReal.mk (HPow.hPow (β := ℕ) c 2) sorry * v) x =
  gaussianPDFReal (c * μ) (NNReal.mk (HPow.hPow (β := ℕ) c 2) sorry * v) x
Tactic: rw [← mul_assoc, this, one_mul]
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gaussian.Real (goal)
Goal:
μ : ℝ
v : ℝ≥0
c : ℝ
hv : ¬v = 0
hc : ¬c = 0
e : ℝ ≃ᵐ ℝ := Homeomorph.toMeasurableEquiv (Homeomorph.symm (Homeomorph.mulLeft₀ c hc))
he' : ∀ (x : ℝ), HasDerivAt (F := ℝ) (⇑e : (a : ℝ) → ℝ) ((fun (x : ℝ) ↦ c⁻¹) x) x
s' : Set ℝ
hs' : MeasurableSet s'
x : ℝ
⊢ |c⁻¹| * (|c| * gaussianPDFReal (c * μ) (NNReal.mk (HPow.hPow (β := ℕ) c 2) ⋯ * v) x) =
    gaussianPDFReal (c * μ) (NNReal.mk (HPow.hPow (β := ℕ) c 2) ⋯ * v) x
have neg : |c⁻¹| * |c| = 1
Tactic: suffices |c⁻¹| * |c| = 1 by rw [← mul_assoc, this, one_mul]
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gaussian.Real (goal)
Goal:
μ : ℝ
v : ℝ≥0
c : ℝ
hv : ¬v = 0
hc : ¬c = 0
e : ℝ ≃ᵐ ℝ := Homeomorph.toMeasurableEquiv (Homeomorph.symm (Homeomorph.mulLeft₀ c hc))
he' : ∀ (x : ℝ), HasDerivAt (F := ℝ) (⇑e : (a : ℝ) → ℝ) ((fun (x : ℝ) ↦ c⁻¹) x) x
s' : Set ℝ
hs' : MeasurableSet s'
x : ℝ
⊢ |c⁻¹| * |c| = 1
have neg : |c| ≠ 0
Tactic: rw [abs_inv, inv_mul_cancel₀]
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gaussian.Real (goal)
Goal:
μ : ℝ
v : ℝ≥0
c : ℝ
hv : ¬v = 0
hc : ¬c = 0
e : ℝ ≃ᵐ ℝ := Homeomorph.toMeasurableEquiv (Homeomorph.symm (Homeomorph.mulLeft₀ c hc))
he' : ∀ (x : ℝ), HasDerivAt (F := ℝ) (⇑e : (a : ℝ) → ℝ) ((fun (x : ℝ) ↦ c⁻¹) x) x
s' : Set ℝ
hs' : MeasurableSet s'
x : ℝ
⊢ |c| ≠ 0
have neg : ¬|c| = 0
Tactic: rwa [ne_eq, abs_eq_zero]
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gaussian.Real (goal)
Goal:
μ : ℝ
v : ℝ≥0
c : ℝ
⊢ Measure.map (fun (x : ℝ) ↦ x * c) (gaussianReal μ v) = gaussianReal (c * μ) (NNReal.mk (HPow.hPow (β := ℕ) c 2) ⋯ * v)
have simp_rw : Measure.map (fun (x : ℝ) ↦ c * x) (gaussianReal μ v) = gaussianReal (c * μ) (NNReal.mk (HPow.hPow (β := ℕ) c 2) sorry * v)
Tactic: simp_rw [mul_comm _ c]
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gaussian.Real (goal)
Goal:
μ : ℝ
v : ℝ≥0
c : ℝ
⊢ Measure.map (fun (x : ℝ) ↦ x * c⁻¹) (gaussianReal μ v) =
    gaussianReal (μ * c⁻¹) (v * (NNReal.mk (HPow.hPow (β := ℕ) c 2) ⋯)⁻¹)
have h : μ * c⁻¹ = c⁻¹ * μ
Tactic: convert! gaussianReal_map_mul_const c⁻¹ using 2
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gaussian.Real (goal)
Goal:
μ : ℝ
v : ℝ≥0
c : ℝ
h : μ * c⁻¹ = c⁻¹ * μ
⊢ Measure.map (fun (x : ℝ) ↦ x * c⁻¹) (gaussianReal μ v) =
    gaussianReal (μ * c⁻¹) (v * (NNReal.mk (HPow.hPow (β := ℕ) c 2) ⋯)⁻¹)
have h₁ : v * (NNReal.mk (HPow.hPow (β := ℕ) c 2) sorry)⁻¹ = NNReal.mk (HPow.hPow (β := ℕ) c⁻¹ 2) sorry * v
Tactic: convert! gaussianReal_map_mul_const c⁻¹ using 2
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gaussian.Real (goal)
Goal:
μ : ℝ
v : ℝ≥0
c : ℝ
⊢ μ * c⁻¹ = c⁻¹ * μ
have h : c⁻¹ * μ = c⁻¹ * μ
Tactic: rw [mul_comm]
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gaussian.Real (goal)
Goal:
μ : ℝ
v : ℝ≥0
c : ℝ
⊢ v * (NNReal.mk (HPow.hPow (β := ℕ) c 2) ⋯)⁻¹ = NNReal.mk (HPow.hPow (β := ℕ) c⁻¹ 2) ⋯ * v
have h : (NNReal.mk (HPow.hPow (β := ℕ) c 2) sorry)⁻¹ * v = NNReal.mk (HPow.hPow (β := ℕ) c⁻¹ 2) sorry * v
Tactic: rw [mul_comm]
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gaussian.Real (goal)
Goal:
μ : ℝ
v : ℝ≥0
c : ℝ
⊢ (NNReal.mk (HPow.hPow (β := ℕ) c 2) ⋯)⁻¹ * v = NNReal.mk (HPow.hPow (β := ℕ) c⁻¹ 2) ⋯ * v
have h : (↑((NNReal.mk (HPow.hPow (β := ℕ) c 2) sorry)⁻¹ * v) : ℝ) = (↑(NNReal.mk (HPow.hPow (β := ℕ) c⁻¹ 2) sorry * v) : ℝ)
Tactic: ext
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gaussian.Real (goal)
Goal:
μ : ℝ
v : ℝ≥0
y : ℝ
⊢ Eq (α := (x : ℝ) → ℝ) (fun (x : ℝ) ↦ y + -x) ((fun (x : ℝ) ↦ y + x) ∘ fun (x : ℝ) ↦ -x)
have h : ∀ (x : ℝ), y + -x = ((fun (x : ℝ) ↦ y + x) ∘ fun (x : ℝ) ↦ -x) x
Tactic: ext
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gaussian.Real (hypothesis)
Goal:
μ : ℝ
v : ℝ≥0
y : ℝ
⊢ Measure.map (fun (x : ℝ) ↦ y + -x) (gaussianReal μ v) = gaussianReal (y + -μ) v
have this : Eq (α := (x : ℝ) → ℝ) (fun (x : ℝ) ↦ y + -x) ((fun (x : ℝ) ↦ y + x) ∘ fun (x : ℝ) ↦ -x)
Tactic: have : (fun x ↦ y + -x) = (fun x ↦ y + x) ∘ fun x ↦ -x := by ext; simp
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gaussian.Real (goal)
Goal:
μ : ℝ
v : ℝ≥0
y : ℝ
this : Eq (α := (x : ℝ) → ℝ) (fun (x : ℝ) ↦ y + -x) ((fun (x : ℝ) ↦ y + x) ∘ fun (x : ℝ) ↦ -x)
⊢ Measure.map (fun (x : ℝ) ↦ y + -x) (gaussianReal μ v) = gaussianReal (y + -μ) v
have rw : Measure.map ((fun (x : ℝ) ↦ y + x) ∘ fun (x : ℝ) ↦ -x) (gaussianReal μ v) = gaussianReal (y + -μ) v
Tactic: rw [this, ← Measure.map_map (by fun_prop) (by fun_prop), gaussianReal_map_neg,
    gaussianReal_map_const_add, add_comm]
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gaussian.Real (goal)
Goal:
μ : ℝ
v : ℝ≥0
y : ℝ
this : Eq (α := (x : ℝ) → ℝ) (fun (x : ℝ) ↦ y + -x) ((fun (x : ℝ) ↦ y + x) ∘ fun (x : ℝ) ↦ -x)
rw : Measure.map ((fun (x : ℝ) ↦ y + x) ∘ fun (x : ℝ) ↦ -x) (gaussianReal μ v) = gaussianReal (y + -μ) v
⊢ Measure.map (fun (x : ℝ) ↦ y + -x) (gaussianReal μ v) = gaussianReal (y + -μ) v
have rw₁ : Measure.map (fun (x : ℝ) ↦ y + x) (Measure.map (fun (x : ℝ) ↦ -x) (gaussianReal μ v)) = gaussianReal (y + -μ) v
Tactic: rw [this, ← Measure.map_map (by fun_prop) (by fun_prop), gaussianReal_map_neg,
    gaussianReal_map_const_add, add_comm]
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gaussian.Real (goal)
Goal:
μ : ℝ
v : ℝ≥0
y : ℝ
this : Eq (α := (x : ℝ) → ℝ) (fun (x : ℝ) ↦ y + -x) ((fun (x : ℝ) ↦ y + x) ∘ fun (x : ℝ) ↦ -x)
rw : Measure.map ((fun (x : ℝ) ↦ y + x) ∘ fun (x : ℝ) ↦ -x) (gaussianReal μ v) = gaussianReal (y + -μ) v
rw₁ : Measure.map (fun (x : ℝ) ↦ y + x) (Measure.map (fun (x : ℝ) ↦ -x) (gaussianReal μ v)) = gaussianReal (y + -μ) v
⊢ Measure.map (fun (x : ℝ) ↦ y + -x) (gaussianReal μ v) = gaussianReal (y + -μ) v
have rw₂ : Measure.map (fun (x : ℝ) ↦ y + x) (gaussianReal (-μ) v) = gaussianReal (y + -μ) v
Tactic: rw [this, ← Measure.map_map (by fun_prop) (by fun_prop), gaussianReal_map_neg,
    gaussianReal_map_const_add, add_comm]
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gaussian.Real (goal)
Goal:
μ : ℝ
v : ℝ≥0
y : ℝ
this : Eq (α := (x : ℝ) → ℝ) (fun (x : ℝ) ↦ y + -x) ((fun (x : ℝ) ↦ y + x) ∘ fun (x : ℝ) ↦ -x)
rw : Measure.map ((fun (x : ℝ) ↦ y + x) ∘ fun (x : ℝ) ↦ -x) (gaussianReal μ v) = gaussianReal (y + -μ) v
rw₁ : Measure.map (fun (x : ℝ) ↦ y + x) (Measure.map (fun (x : ℝ) ↦ -x) (gaussianReal μ v)) = gaussianReal (y + -μ) v
rw₂ : Measure.map (fun (x : ℝ) ↦ y + x) (gaussianReal (-μ) v) = gaussianReal (y + -μ) v
⊢ Measure.map (fun (x : ℝ) ↦ y + -x) (gaussianReal μ v) = gaussianReal (y + -μ) v
have rw₃ : gaussianReal (-μ + y) v = gaussianReal (y + -μ) v
Tactic: rw [this, ← Measure.map_map (by fun_prop) (by fun_prop), gaussianReal_map_neg,
    gaussianReal_map_const_add, add_comm]
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gaussian.Real (goal)
Goal:
μ : ℝ
v : ℝ≥0
y : ℝ
this : Eq (α := (x : ℝ) → ℝ) (fun (x : ℝ) ↦ y + -x) ((fun (x : ℝ) ↦ y + x) ∘ fun (x : ℝ) ↦ -x)
rw : Measure.map ((fun (x : ℝ) ↦ y + x) ∘ fun (x : ℝ) ↦ -x) (gaussianReal μ v) = gaussianReal (y + -μ) v
rw₁ : Measure.map (fun (x : ℝ) ↦ y + x) (Measure.map (fun (x : ℝ) ↦ -x) (gaussianReal μ v)) = gaussianReal (y + -μ) v
rw₂ : Measure.map (fun (x : ℝ) ↦ y + x) (gaussianReal (-μ) v) = gaussianReal (y + -μ) v
rw₃ : gaussianReal (-μ + y) v = gaussianReal (y + -μ) v
⊢ Measure.map (fun (x : ℝ) ↦ y + -x) (gaussianReal μ v) = gaussianReal (y + -μ) v
have rw₄ : gaussianReal (y + -μ) v = gaussianReal (y + -μ) v
Tactic: rw [this, ← Measure.map_map (by fun_prop) (by fun_prop), gaussianReal_map_neg,
    gaussianReal_map_const_add, add_comm]
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gaussian.Real (goal)
Goal:
μ : ℝ
v : ℝ≥0
z : ℂ
⊢ complexMGF id (gaussianReal μ v) z = cexp (z * (↑μ : ℂ) + (↑(↑v : ℝ) : ℂ) * HPow.hPow (β := ℕ) z 2 / 2)
have pos : ∀ (hv : v = 0), complexMGF id (gaussianReal μ v) z = cexp (z * (↑μ : ℂ) + (↑(↑v : ℝ) : ℂ) * HPow.hPow (β := ℕ) z 2 / 2)
Tactic: by_cases hv : v = 0
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gaussian.Real (goal)
Goal:
μ : ℝ
v : ℝ≥0
z : ℂ
pos :
  ∀ (hv : v = 0),
    complexMGF id (gaussianReal μ v) z = cexp (z * (↑μ : ℂ) + (↑(↑v : ℝ) : ℂ) * HPow.hPow (β := ℕ) z 2 / 2)
⊢ complexMGF id (gaussianReal μ v) z = cexp (z * (↑μ : ℂ) + (↑(↑v : ℝ) : ℂ) * HPow.hPow (β := ℕ) z 2 / 2)
have neg : ∀ (hv : ¬v = 0), complexMGF id (gaussianReal μ v) z = cexp (z * (↑μ : ℂ) + (↑(↑v : ℝ) : ℂ) * HPow.hPow (β := ℕ) z 2 / 2)
Tactic: by_cases hv : v = 0
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gaussian.Real (goal)
Goal:
μ : ℝ
v : ℝ≥0
z : ℂ
hv : ¬v = 0
⊢ Eq (α := ℂ) (∫ (x : ℝ), cexp (z * (↑x : ℂ)) ∂gaussianReal μ v)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace ℙ fun (x : ℝ) ↦
      (↑(gaussianPDFReal μ v x) : ℂ) * cexp (z * (↑x : ℂ)))
have simp_rw : Eq (α := ℂ)
  (@integral _ _ _ _ MeasureSpace.toMeasurableSpace ℙ fun (x : ℝ) ↦ gaussianPDFReal μ v x • cexp (z * (↑x : ℂ)))
  (@integral _ _ _ _ MeasureSpace.toMeasurableSpace ℙ fun (x : ℝ) ↦
    (↑(gaussianPDFReal μ v x) : ℂ) * cexp (z * (↑x : ℂ)))
Tactic: simp_rw [integral_gaussianReal_eq_integral_smul hv, Complex.real_smul]
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gaussian.Real (goal)
Goal:
μ : ℝ
v : ℝ≥0
z : ℂ
hv : ¬v = 0
⊢ (@integral _ _ _ _ MeasureSpace.toMeasurableSpace ℙ fun (x : ℝ) ↦
      (↑((√(2 * π * (↑v : ℝ)))⁻¹ * rexp (-HPow.hPow (β := ℕ) (x - μ) 2 / (2 * (↑v : ℝ)))) : ℂ) * cexp (z * (↑x : ℂ))) =
    (↑(√(2 * π * (↑v : ℝ)))⁻¹ : ℂ) *
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace ℙ fun (x : ℝ) ↦
        cexp
          (-(↑(↑(2 * v)⁻¹ : ℝ) : ℂ) * HPow.hPow (β := ℕ) (↑x : ℂ) 2 + (z + (↑μ : ℂ) / (↑(↑v : ℝ) : ℂ)) * (↑x : ℂ) +
            -HPow.hPow (β := ℕ) (↑μ : ℂ) 2 / (2 * (↑(↑v : ℝ) : ℂ)))
have push_cast : (@integral _ _ _ _ MeasureSpace.toMeasurableSpace ℙ fun (x : ℝ) ↦
    (↑√(2 * π * (↑v : ℝ)) : ℂ)⁻¹ * cexp (-HPow.hPow (β := ℕ) ((↑x : ℂ) - (↑μ : ℂ)) 2 / (2 * (↑(↑v : ℝ) : ℂ))) *
      cexp (z * (↑x : ℂ))) =
  (↑√(2 * π * (↑v : ℝ)) : ℂ)⁻¹ *
    @integral _ _ _ _ MeasureSpace.toMeasurableSpace ℙ fun (x : ℝ) ↦
      cexp
        (-(2 * (↑(↑v : ℝ) : ℂ))⁻¹ * HPow.hPow (β := ℕ) (↑x : ℂ) 2 + (z + (↑μ : ℂ) / (↑(↑v : ℝ) : ℂ)) * (↑x : ℂ) +
          -HPow.hPow (β := ℕ) (↑μ : ℂ) 2 / (2 * (↑(↑v : ℝ) : ℂ)))
Tactic: push_cast
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gaussian.Real (goal)
Goal:
μ : ℝ
v : ℝ≥0
z : ℂ
hv : ¬v = 0
⊢ (@integral _ _ _ _ MeasureSpace.toMeasurableSpace ℙ fun (x : ℝ) ↦
      (↑√(2 * π * (↑v : ℝ)) : ℂ)⁻¹ * cexp (-HPow.hPow (β := ℕ) ((↑x : ℂ) - (↑μ : ℂ)) 2 / (2 * (↑(↑v : ℝ) : ℂ))) *
        cexp (z * (↑x : ℂ))) =
    (↑√(2 * π * (↑v : ℝ)) : ℂ)⁻¹ *
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace ℙ fun (x : ℝ) ↦
        cexp
          (-(2 * (↑(↑v : ℝ) : ℂ))⁻¹ * HPow.hPow (β := ℕ) (↑x : ℂ) 2 + (z + (↑μ : ℂ) / (↑(↑v : ℝ) : ℂ)) * (↑x : ℂ) +
            -HPow.hPow (β := ℕ) (↑μ : ℂ) 2 / (2 * (↑(↑v : ℝ) : ℂ)))
have simp_rw : ((↑√(2 * (π * (↑v : ℝ))) : ℂ)⁻¹ *
    @integral _ _ _ _ MeasureSpace.toMeasurableSpace ℙ fun (a : ℝ) ↦
      cexp (-HPow.hPow (β := ℕ) ((↑a : ℂ) - (↑μ : ℂ)) 2 / (2 * (↑(↑v : ℝ) : ℂ)) + z * (↑a : ℂ))) =
  (↑√(2 * (π * (↑v : ℝ))) : ℂ)⁻¹ *
    @integral _ _ _ _ MeasureSpace.toMeasurableSpace ℙ fun (x : ℝ) ↦
      cexp
        (-(2 * (↑(↑v : ℝ) : ℂ))⁻¹ * HPow.hPow (β := ℕ) (↑x : ℂ) 2 + (z + (↑μ : ℂ) / (↑(↑v : ℝ) : ℂ)) * (↑x : ℂ) +
          -HPow.hPow (β := ℕ) (↑μ : ℂ) 2 / (2 * (↑(↑v : ℝ) : ℂ)))
Tactic: simp_rw [mul_assoc, integral_const_mul, ← Complex.exp_add]
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gaussian.Real (goal)
Goal:
μ : ℝ
v : ℝ≥0
z : ℂ
hv : ¬v = 0
⊢ ((↑√(2 * (π * (↑v : ℝ))) : ℂ)⁻¹ *
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace ℙ fun (a : ℝ) ↦
        cexp (-HPow.hPow (β := ℕ) ((↑a : ℂ) - (↑μ : ℂ)) 2 / (2 * (↑(↑v : ℝ) : ℂ)) + z * (↑a : ℂ))) =
    (↑√(2 * (π * (↑v : ℝ))) : ℂ)⁻¹ *
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace ℙ fun (x : ℝ) ↦
        cexp
          (-(2 * (↑(↑v : ℝ) : ℂ))⁻¹ * HPow.hPow (β := ℕ) (↑x : ℂ) 2 + (z + (↑μ : ℂ) / (↑(↑v : ℝ) : ℂ)) * (↑x : ℂ) +
            -HPow.hPow (β := ℕ) (↑μ : ℂ) 2 / (2 * (↑(↑v : ℝ) : ℂ)))
have e_a : ∀ (x : ℝ),
  cexp (-HPow.hPow (β := ℕ) ((↑x : ℂ) - (↑μ : ℂ)) 2 / (2 * (↑(↑v : ℝ) : ℂ)) + z * (↑x : ℂ)) =
    cexp
      (-(2 * (↑(↑v : ℝ) : ℂ))⁻¹ * HPow.hPow (β := ℕ) (↑x : ℂ) 2 + (z + (↑μ : ℂ) / (↑(↑v : ℝ) : ℂ)) * (↑x : ℂ) +
        -HPow.hPow (β := ℕ) (↑μ : ℂ) 2 / (2 * (↑(↑v : ℝ) : ℂ)))
Tactic: congr with x