Zulip Chat Archive

Stream: new members

Topic: Multiple uses of existsi


view this post on Zulip Calle Sönne (Nov 20 2018 at 14:36):

I have the following goal:

 (s : ) (H : s  S),  (k : ), k  S  s  k

Now I have an element s which has all required properties to prove this goal. I would like to provide this s using existsi. Of course I also have to provide the fact that s is in S (my hypothesis Hs). However using existsi s Hs doesnt seem to work, and I need to call existsi two times. That is existsi s, existsi Hs. Is there anyway to make this into a one-liner?

view this post on Zulip Johan Commelin (Nov 20 2018 at 14:39):

refine \<s, Hs, _\>

view this post on Zulip Rob Lewis (Nov 20 2018 at 14:39):

existsi takes an expression or a list of expressions. Try existsi [s, Hs].

view this post on Zulip Calle Sönne (Nov 20 2018 at 14:53):

Thank you! Both methods worked fine :). What would be the pro of using refine instead of existsi? That its more general?

view this post on Zulip Johan Commelin (Nov 20 2018 at 14:56):

See also https://leanprover.zulipchat.com/#narrow/stream/113488-general/subject/.60existsi.60.20is.20so.20dumb

view this post on Zulip Calle Sönne (Nov 20 2018 at 15:03):

Thanks :)

view this post on Zulip Kevin Buzzard (Nov 21 2018 at 00:21):

theorem easy :  x : , x = x :=
begin
--  existsi 23, -- lean says "that's not an integer!"
    refine 23,_⟩, -- works fine
    refl
end

I have almost given up on existsi, it doesn't try hard enough.


Last updated: May 16 2021 at 05:21 UTC