aliasing complex terms

Stream: lean4

[Rosie Baish]

Is there a way to alias a complex term with a shorthand
e.g. Rather than the pretty printer outputting "(func a b c d e f g)" it outputs "x", and whenever x appears in the proof it's replaced by the long version
It would be an exact replacement, not parameterised by anything.
The reason for this is that the proof I'm working on has loads of really long terms in that make reading and comprehending the output really hard

[Xubai Wang]

(deleted)

[Wojciech Nawrocki]

If you are in a tactic proof, you could do something like

example (f : α → α → α) (x y : α) : f (f x y) (f x y) = f x y := by
  let z := f x y
  have : f x y = z := rfl
  rw [this]
  ...

There might be a tactic for this, but I couldn't immediately find it.

[Ruben Van de Velde]

There's set in mathlib3

[Alex Keizer]

There's generalize, borrowing Wojciech example

example (f : α → α → α) (x y : α) : f (f x y) (f x y) = f x y := by
  generalize f x y = z;
  sorry

However, it "forgets" the concrete value of z and only replaces things in the goal.
We can use the generalize hz : f x y = z notation to add an hypothesis hz : f x y = z to the context, allowing us to unfold z again at a later point in the proof.

Eventually we should be able to write generalize hz : f x y = z at h |- to do the substitution at hypotheses as well, but until that is implemented we can work around it by reverting the hypotheses that mention f x y.

For example,

example (f : α → α → α) (x y w : α) (h : f x y = w)
  : f (f x y) (f x y) = f x y := by
  revert h;
  generalize hz : f x y = z;
  intro h;
  sorry

Result in the proof state

α : Sort ?u.7
f : α → α → α
x y w z : α
hz : f x y = z
h : z = w
⊢ f z z = z

Before the sorry