# [isabelle] Cannot solve all subgoals

```Hi,

sometimes when I prove a lemma with multiple subgoals one after the
other, the number of subgoals does not shrink and in the end there are
unsolved subgoals that I don't understand.

The following is a minimal example of what happened:

theory Test imports Main begin
lemma foo:
assumes "R = {}"
shows "âx y. (x, y) â R â x = y" "âx y. (y, x) â R â (x, y) â R" proof-
show "âx y. (x, y) â R â x = y" sorry
show "âx y. (y, x) â R â (x, y) â R" sorry
(* 2 remaining subgoals at this point:
1. âx y. (x, y) â R â (y, x) â R
2. âx y. (y, x) â R â (x, y) â R
*)
qed
(*
Failed to finish proof:
goal (2 subgoals):
1. âx y. (x, y) â R â (y, x) â R
2. âx y. (y, x) â R â (x, y) â R
*)
end

In the lemma, after positioning the cursor in jedit behind proof-, it
shows me the two subgoals I expect.  After solving these two subgoals,
there are now still 2 goals remaining and the proof fails.

The last unsolved subgoal looks to me exactly like the one I proved
explicitly with the second show line, so I am somewhat puzzled as to why
it remains.

Where did I go wrong?  Is this the expected behavior?

(In case it is relevant, I work with Isabelle2015.)

Thanks,
Christoph

```

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.