# [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.
{"ft_lang_label":"__label__en","ft_lang_prob":0.8714441,"math_prob":0.8459386,"size":1276,"snap":"2020-24-2020-29","text_gpt3_token_len":416,"char_repetition_ratio":0.17610063,"word_repetition_ratio":0.25468165,"special_character_ratio":0.30564263,"punctuation_ratio":0.15161291,"nsfw_num_words":0,"has_unicode_error":false,"math_prob_llama3":0.99545866,"pos_list":[0],"im_url_duplicate_count":[null],"WARC_HEADER":"{\"WARC-Type\":\"response\",\"WARC-Date\":\"2020-05-26T22:04:18Z\",\"WARC-Record-ID\":\"<urn:uuid:95bac1c0-1388-4f97-9155-f1bb0d55e444>\",\"Content-Length\":\"5180\",\"Content-Type\":\"application/http; msgtype=response\",\"WARC-Warcinfo-ID\":\"<urn:uuid:643cd3dc-4724-4647-b3c5-c7364ee10d48>\",\"WARC-Concurrent-To\":\"<urn:uuid:67a4ce7c-1a94-4980-aff3-c41c5d7c4983>\",\"WARC-IP-Address\":\"131.111.8.15\",\"WARC-Target-URI\":\"https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2015-July/msg00015.html\",\"WARC-Payload-Digest\":\"sha1:4CGZ2LQ5AZPWJKG34FDHPSH2OMQLRBMU\",\"WARC-Block-Digest\":\"sha1:2NOKHQFXKDU446K2DDNGND7Y4F7LZM3A\",\"WARC-Identified-Payload-Type\":\"text/html\",\"warc_filename\":\"/cc_download/warc_2020/CC-MAIN-2020-24/CC-MAIN-2020-24_segments_1590347391309.4_warc_CC-MAIN-20200526191453-20200526221453-00340.warc.gz\"}"}