Split conjunction goal into subgoals

Question

Consider the following toy exercise:

Theorem swap_id : forall (m n : nat), m = n -> (m, n) = (n, m).forall m n : nat, m = n -> (m, n) = (n, m)
Proof.forall m n : nat, m = n -> (m, n) = (n, m)
  intros m n H.m, n: nat
H: m = n
(m, n) = (n, m)

At this point I have the following:

1 subgoal

  m, n : nat
  H : m = n
  ============================
  (m, n) = (n, m)

I would like to split the goal into two subgoals, m = n and n = m. Is there a tactic which does that?

Answer

Solve using the f_equal tactic:

Theorem test : forall (m n : nat), m = n -> (m, n) = (n, m).forall m n : nat, m = n -> (m, n) = (n, m)
Proof.forall m n : nat, m = n -> (m, n) = (n, m)
  intros m n H.m, n: nat
H: m = n
(m, n) = (n, m) f_equal.m, n: nat
H: m = n
m = n
m, n: nat
H: m = n
n = m

With state:

2 subgoals

  m, n : nat
  H : m = n
  ============================
  m = n

subgoal 2 is:
 n = m

A: A comment about the reason f_equal works: if we unfold some notations, we'll get from the goal (m, n) = (n, m) to pair m n = pair n m, where pair is the only constructor of the prod datatype. At this point it should be obvious why f_equal splits the goal into two subgoals.