how to alias something?

Stream: new members

[ShatteredLead]

How can I set a auxiliary variable, to give a whole part names, in order to simplify the proof? Thanks!

example (x: Nat) : x + 1 = x + 1 := by
  -- just example to show motivation:
  -- let x' := x + 1
  -- rw [← x'] -- it surely won't work
  -- exact (rfl x')

[Riccardo Brasca]

you can use set x := 1 with hx

[Zhuanhao Z Wu]

An alternative:

example (x: Nat) : x + 1 = x + 1 := by
  generalize h: x + 1 = x'
  rfl