Multiple uses of existsi

Stream: new members

[Calle Sönne]

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]

refine \<s, Hs, _\>

[Rob Lewis]

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

[Calle Sönne]

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

[Johan Commelin]

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

[Calle Sönne]

Thanks :)

[Kevin Buzzard]

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.