{"action":"created","issue":{"url":"https://api.github.com/repos/leanprover/tutorial/issues/100","labels_url":"https://api.github.com/repos/leanprover/tutorial/issues/100/labels{/name}","comments_url":"https://api.github.com/repos/leanprover/tutorial/issues/100/comments","events_url":"https://api.github.com/repos/leanprover/tutorial/issues/100/events","html_url":"https://github.com/leanprover/tutorial/issues/100","id":72564155,"number":100,"title":"exists.elim in tactics mode","user":{"login":"htzh","id":5956967,"avatar_url":"https://avatars.githubusercontent.com/u/5956967?v=3","gravatar_id":"","url":"https://api.github.com/users/htzh","html_url":"https://github.com/htzh","followers_url":"https://api.github.com/users/htzh/followers","following_url":"https://api.github.com/users/htzh/following{/other_user}","gists_url":"https://api.github.com/users/htzh/gists{/gist_id}","starred_url":"https://api.github.com/users/htzh/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/htzh/subscriptions","organizations_url":"https://api.github.com/users/htzh/orgs","repos_url":"https://api.github.com/users/htzh/repos","events_url":"https://api.github.com/users/htzh/events{/privacy}","received_events_url":"https://api.github.com/users/htzh/received_events","type":"User","site_admin":false},"labels":[],"state":"closed","locked":false,"assignee":null,"milestone":null,"comments":6,"created_at":"2015-05-02T01:33:07Z","updated_at":"2015-05-03T10:05:46Z","closed_at":"2015-05-02T15:02:33Z","body":"I can use ```obtain _ _, from _``` outside of tactics mode, but I can't figure out how to use it inside. If I don't use tactics I don't know how to force expansion of definitions. Also I have no feedback on what the current context and goal look like. Once inside tactics it seems really hard to introduce new intermediate facts into the context. The particular case I am stuck on is\r\n```\r\nimport data.set\r\nopen set\r\nnamespace set\r\nopen function\r\nvariables {A B C: Type}\r\nvariable {S : set A}\r\nlemma image_compose : ∀ (f : B → C) (g : A → B), f '[g '[S]] = (f ∘ g) '[S] :=\r\n      assume f, assume g,\r\n      setext (assume z,\r\n      iff.intro\r\n        (begin\r\n        rewrite [↑compose, ↑image, ↑set_of],\r\n        intro Hz,\r\n        --rewrite \r\n        end) _)\r\nend set\r\n```"},"comment":{"url":"https://api.github.com/repos/leanprover/tutorial/issues/comments/98461836","html_url":"https://github.com/leanprover/tutorial/issues/100#issuecomment-98461836","issue_url":"https://api.github.com/repos/leanprover/tutorial/issues/100","id":98461836,"user":{"login":"avigad","id":2783534,"avatar_url":"https://avatars.githubusercontent.com/u/2783534?v=3","gravatar_id":"","url":"https://api.github.com/users/avigad","html_url":"https://github.com/avigad","followers_url":"https://api.github.com/users/avigad/followers","following_url":"https://api.github.com/users/avigad/following{/other_user}","gists_url":"https://api.github.com/users/avigad/gists{/gist_id}","starred_url":"https://api.github.com/users/avigad/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/avigad/subscriptions","organizations_url":"https://api.github.com/users/avigad/orgs","repos_url":"https://api.github.com/users/avigad/repos","events_url":"https://api.github.com/users/avigad/events{/privacy}","received_events_url":"https://api.github.com/users/avigad/received_events","type":"User","site_admin":false},"created_at":"2015-05-03T10:05:46Z","updated_at":"2015-05-03T10:05:46Z","body":"Dear Haitao,\r\n\r\nThanks for the proof! I will add it to the library. I revised it a little to make it more readable:\r\n```lean\r\nimport data.set\r\nopen set function eq.ops\r\n\r\nvariables {A B C : Type} {S : set A}\r\n\r\ntheorem in_image {x : A} {y : B} {f : A → B} \r\n  (H1 : x ∈ S) (H2 : f x = y) : y ∈ f '[S] :=\r\nexists.intro x (and.intro H1 H2)\r\n\r\nlemma image_compose (f : B → C) (g : A → B) : f '[g '[S]] = (f ∘ g) '[S] :=\r\nsetext (take z,\r\n  iff.intro\r\n    (assume Hz : z ∈ f '[g '[S]],\r\n      obtain y (Hy : y ∈ g '[S] ∧ f y = z), from Hz,\r\n      obtain x (Hz : x ∈ S ∧ g x = y), from and.left Hy,\r\n      show z ∈ (f ∘ g) '[S], from in_image (and.left Hz) ((and.right Hz)⁻¹ ▸ (and.right Hy)))\r\n    (assume Hz : z ∈ (f ∘ g) '[S],\r\n      obtain x (Hx : x ∈ S ∧ f (g x) = z), from Hz,\r\n      have Hgx : g x ∈ g '[S], from in_image (and.left Hx) rfl,\r\n      show z ∈ f '[g '[S]], from in_image Hgx (and.right Hx)))\r\n```\r\n\r\nSome notes: \r\n\r\n- if you say ```namespace set``` then ```open set``` is not needed.\r\n- an equivalent form of ```rewrite [↑compose, ↑image, ↑set_of, ↑mem]``` is ```esimp [compose, image, set_of, mem]```\r\n- in fact, these are not needed in the proof above (the unifier unfolds the definitions)"}}