Q: How to use rewrite on a subexpression of the current goal In coq, is it somehow possible to apply a lemma or hypothesis to a subexpression of the current goal?  For example I would like to apply the fact that plus is commutative in order to swap 3 and 4 in this example.
Require Import Coq.Arith.Plus.

Inductive foobar : nat -> Prop :=
 | foob : forall n:nat, foobar n.

Goal foob (3 + 4) = foob (4 + 3).
Proof.
apply plus_comm. (* or maybe rewrite plus_comm *)

gives:
Error: Impossible to unify "?199 + ?200 = ?200 + ?199" with
"foob (3 + 4) = foob (4 + 3)".

How can I tell coq where exactly in this goal to apply plus_comm?

A: Using the tactic simpl works, but don't ask me why rewrite plus_comm or rewrite (plus_comm 3 4) doesn't work. apply is for implications, not equations.

A: In this particular case, rewrite will work if you define the inductive type using a constructor parameter instead of an index:
Inductive foobar : Type :=
    | foob (n : nat).

Since there is only one constructor for this type, my understanding (from this answer) is that using an index does not provide any benefit but makes it harder for Coq to pattern-match.
In general, either of the following techniques can achieve the effect of a targeted rewrite:
assert
assert (H: 3 + 4 = 4 + 3). { rewrite <- plus_comm. reflexivity. }

rewrite
(* introduce a new sub-goal where you can prove that the replacement is OK *)
replace (3 + 4) with (4 + 3).
(* Coq orders the new goal last. I think it's clearer to tackle it first *)
Focus 2.
(* do the rewrite *)
rewrite <- plus_comm. reflexivity.

