Pattern `apply`, `rw`, `exact`

Stream: Is there code for X?

[Vasily Ilin]

I often find myself using the pattern

apply X
rw [Y]
exact Z

where X, Y and Z are some lemmas. If rw [Y] wasn't there then I could just do exact X Z instead. Is there a one-liner that I can use instead of the pattern above?

For an extremely contrived example, how to prove the following in one line without using trans?

lemma test (a b : ℕ) (h1 : a = b) (h2 : b = 0) : a = 0 := by
  rw [h1]
  exact h2

More realistic example: here

[Marco Campos]

I believe you can use rewrite on its own in the lemma you showed:

lemma test (a b : ℕ) (h1 : a = b) (h2 : b = 0) : a = 0 := by
rw [h1, h2]

[Vasily Ilin]

Okay, I think my contrived example is too contrived. Take a look at the realistic example I linked (also pasted below).

[Vasily Ilin]

Here it is

import Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral
import Mathlib.Probability.Moments

open Measurable Real

variable {Ω : Type*} {mΩ : MeasurableSpace Ω} {p : Measure Ω} {μ : ℝ} {v : ℝ≥0} {X : Ω → ℝ}

lemma mgf_dirac (hX : p.map X = .dirac μ) (t : ℝ) : mgf X p t = exp (μ * t) := by
  rw [← mgf_id_map, mgf, hX, integral_dirac, mul_comm]
  · rfl
  · apply AEMeasurable.of_map_ne_zero
    rw [hX]
    exact IsProbabilityMeasure.ne_zero (.dirac μ)

[Ruben Van de Velde]

Maybe with the triangle \t, but that's usually a sign you're condensing your code too much

[Yaël Dillies]

Do you know about simpa?

[Yaël Dillies]

Also I am pretty sure I suggested you a golf for those specific lines on the PR

[Vasily Ilin]

Yaël Dillies said:

Also I am pretty sure I suggested you a golf for those specific lines on the PR

I dont' think so. I have applied all suggestions you have given me so far. I think you suggested removing AEMeasurable and switching apply to refine but it's still 3 lines.

[Vasily Ilin]

Yaël Dillies said:

Do you know about simpa?

No, but I am looking it up now!

[Vasily Ilin]

I read the docstring of simpa but didn't really understand it.

[Yakov Pechersky]

simpa [my, lemmas, here] using term means apply the lemmas in the list to both the goal and the term such after some application, the term will solve the goal. So in your case, it'll be simpa [hx] using IsProbabilityMeasure.ne_zero (.dirac μ), perhaps

[Vasily Ilin]

Yakov Pechersky said:

simpa [my, lemmas, here] using term means apply the lemmas in the list to both the goal and the term such after some application, the term will solve the goal. So in your case, it'll be simpa [hx] using IsProbabilityMeasure.ne_zero (.dirac μ), perhaps

This does not work.