Let tactic and replace

Stream: new members

[Julia Scheaffer]

Is there a way use the let tactic to make a declaration and then replace all instances of that expression in the context with the new name?
I have written a short example below.

example {a b i : Nat} (f : Nat -> Nat -> Nat) : f i a < f i b := by
  let g := f i
  -- I would like this to happen automatically in the goal and all context items
  change g a < g b

  sorry -- The rest of the proof doesn't matter

[Aaron Liu]

set g := f i

[Julia Scheaffer]

:woman_facepalming:

[Julia Scheaffer]

thank you

[Alfredo Moreira-Rosa]

and you can retain the proposition using with :

example {a b i : Nat} (f : Nat -> Nat -> Nat) : f i a < f i b := by
  set g := f i with hg
  sorry

[Robin Arnez]

Just going to note this but this is also in core under:

let (eq := hg) +generalize g := f i