How to destruct pair equivalence in Coq?

Question

I'm trying to destruct a pair equivalence hypothesis in proof when using Coq. But I didn't find the tactic for me.

The case is:

a, b, a', b' : nat
H0 : (a, b) = (a', b')

I want to destruct the pairs in H0 to generate

H1 : a = a'
H2 : b = b'

How can I achieve this? Which tactic should I use? Or should I define lemma for destructing such pair?

Thank you!

Answer 1

You can also do it in one step with inversion H0.

Answer 2

Use injection H0 followed by intros as a first approximation.