Stream: new members
Topic: Multiple uses of existsi
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?
Johan Commelin (Nov 20 2018 at 14:39):
refine \<s, Hs, _\>
Rob Lewis (Nov 20 2018 at 14:39):
existsi takes an expression or a list of expressions. Try
existsi [s, Hs].
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?
Johan Commelin (Nov 20 2018 at 14:56):
Calle Sönne (Nov 20 2018 at 15:03):
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