Tactic Notation "solve_by_inversion_aux" tactic(t) :=
match goal with
| H : _ |- _ => solve [ inversion H; subst++; t ]
end
|| fail "because the goal is not solvable by inversion.".
Tactic Notation "solve" "by" "inversion" "1" :=
solve_by_inversion_aux idtac.
Tactic Notation "solve" "by" "inversion" "2" :=
solve_by_inversion_aux (solve by inversion 1).
Tactic Notation "solve" "by" "inversion" "3" :=
solve_by_inversion_aux (solve by inversion 2).
Tactic Notation "solve" "by" "inversion" :=
solve by inversion 1.
solve by inversion n will attempt to solve the goal by n successive uses of inversion (where n may range between 1 and 3, given the above definitions). This tactic uses subst++ to maximize its effectiveness but could work almost as well replacing subst++ with subst.