How to replace `a : Int` with `-a`?

Stream: Is there code for X?

[Kim Morrison]

What is the most ergonomic way to replace a hypothesis a : Int with its negation?

One can jump through hoops with:

have h := Int.neg_neg a
generalize -a = b at h
subst h

but that feels pretty tedious, and ends up with a different name.

I guess we could write an appropriate XXX so we could write cases a using XXX, but it seems a lot of work to prepare such lemmas for all invertible operations.

[Yaël Dillies]

obtain ⟨a, rfl⟩ : ∃ b, -b = a := ⟨-a, a.neg_neg⟩?

[Kim Morrison]

(needs a .neg_neg.symm, but yes!)

[Yaël Dillies]

Edited to avoid the .symm!

[Eric Wieser]

revert a; rw [neg_involutive.surjective.forall]; intro a?

[Mitchell Lee]

Another option (in case you still want more options)

rewrite [← Int.neg_neg a] at *
set a := -a

[Mitchell Lee]

Eric Wieser said:

revert a; rw [neg_involutive.surjective.forall]; intro a?

This would also require re-introducing any other hypotheses that involve a.

[Eric Wieser]

That's perhaps an argument for "rewrite by a surjective function" being a tactic