How to avoid `ext`?

Stream: Is there code for X?

[Vasily Ilin]

Can I do this in one line, without ext?

import Mathlib.Probability.Distributions.Gaussian
example : (fun x => ↑(gaussianPDFReal 0 1 x).toNNReal) = fun x => gaussianPDFReal 0 1 x := by
  ext x
  exact coe_toNNReal (gaussianPDFReal 0 1 x) (gaussianPDFReal_nonneg 0 1 x)

A less minimal example of what I am after is the following:

import Mathlib.Probability.Distributions.Gaussian
example : (gaussianReal 0 1)[fun x => Real.exp (t * x)] = ∫ (x : ℝ), Real.exp (t * x) * (gaussianPDFReal 0 1 x) := by
        rw [gaussianReal_of_var_ne_zero 0 one_ne_zero, gaussianPDF_def]
        simp only [ENNReal.ofReal]
        rw [integral_withDensity_eq_integral_smul
        (Measurable.real_toNNReal (measurable_gaussianPDFReal 0 1))]
        have : (fun x => (gaussianPDFReal 0 1 x).toNNReal • Real.exp (t * x))
             = (fun x => Real.exp (t * x) * gaussianPDFReal 0 1 x) := by
            ext x
            rw [NNReal.smul_def, Real.coe_toNNReal (gaussianPDFReal 0 1 x) (gaussianPDFReal_nonneg 0 1 x), smul_eq_mul, mul_comm]
        simp only [this]

The proof essence is simple but what makes it look so messy is the have statement, which I cannot get rid of since I need to use the ext.

[Daniel Weber]

You can do

import Mathlib.Probability.Distributions.Gaussian
open Real ProbabilityTheory

example : (fun x => ↑(gaussianPDFReal 0 1 x).toNNReal) = fun x => gaussianPDFReal 0 1 x :=
  funext fun x ↦ coe_toNNReal (gaussianPDFReal 0 1 x) (gaussianPDFReal_nonneg 0 1 x)

[Vasily Ilin]

Daniel Weber said:

You can do

import Mathlib.Probability.Distributions.Gaussian
open Real ProbabilityTheory

example : (fun x => ↑(gaussianPDFReal 0 1 x).toNNReal) = fun x => gaussianPDFReal 0 1 x :=
  funext fun x ↦ coe_toNNReal (gaussianPDFReal 0 1 x) (gaussianPDFReal_nonneg 0 1 x)

Is there a way to apply these lemmas without explicitly introducing an x?

[Ruben Van de Velde]

simp can rewrite inside the lambda, though there may be issues if you need to pass a hypothesis

[Ruben Van de Velde]

Alternatively you might look at conv

[Jz Pan]

Maybe you can use congr and simp_rw:

import Mathlib.Probability.Distributions.Gaussian
open Real ProbabilityTheory

example : (gaussianReal 0 1)[fun x => Real.exp (t * x)] = ∫ (x : ℝ), Real.exp (t * x) * (gaussianPDFReal 0 1 x) := by
  rw [gaussianReal_of_var_ne_zero 0 one_ne_zero, gaussianPDF_def]
  simp only [ENNReal.ofReal]
  rw [integral_withDensity_eq_integral_smul (Measurable.real_toNNReal (measurable_gaussianPDFReal 0 1))]
  congr
  simp_rw [NNReal.smul_def, Real.coe_toNNReal _ (gaussianPDFReal_nonneg 0 1 _), smul_eq_mul, mul_comm]