Extract Subexpression in Proof

Stream: new members

[Marcus Rossel]

Is it possible to give a name to specific subexpressions in a proof?
E.g. if the goal state is:

⊢(foo bar baz 1 2 3) + (foo bar baz 1 2 3) - (foo bar baz 1 2 3) = (foo bar baz 1 2 3)

... then can I change this somehow to: ?

e : nat
h_e : e = foo bar baz 1 2 3
⊢ e + e - e = e

[Kevin Buzzard]

generalize -- actually that's not quite what you want. How about just set e := foo bar baz 123 with h_e? I don't know if that changes the goal but you could just rw \l h_e or change the goal to e (set is definitional).

[Marcus Rossel]

The set e := ... with ... is exactly what I needed. Thanks :)

[Marcus Rossel]

set does change the goal automatically.

[Eric Wieser]

Doesn't generalize work here in exactly the same way?

[Kevin Buzzard]

I don't think it would give you h_e