## 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?

Thanks :)

#### 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