exists.elim in tactic mode?

Stream: new members

[Abhimanyu Pallavi Sudhir]

Hi -- I've been trying to prove a certain relation is symmetric -- is there a way to use "exists.elim" in tactic mode? It always gives me errors.

[Johan Commelin]

Is that existsi?

[Edward Ayers]

cases h with x p will take an existential hypothesis and hit it with exists.elim

[Johan Commelin]

Aah, in that case, you might also be interested in rcases. It is cases on steroids.

[Edward Ayers]

example (P : α → Prop) (Q : Prop) (h₁ : ∃ x, P(x)) (h₂ : ∀ x, P(x) → Q) : Q :=
begin
    cases h₁ with x h₃, -- you can also omit the `with` and it will name them `h₁_w` and `h₁_h`
    apply h₂ _ h₃
end

[Abhimanyu Pallavi Sudhir]

Ok, that seems to work, thanks. It's quite natural to uses cases on ∃, certainly.

[Abhimanyu Pallavi Sudhir]

(deleted)

[Abhimanyu Pallavi Sudhir]

(deleted)

[Abhimanyu Pallavi Sudhir]

(deleted)

[Bryan Gin-ge Chen]

I've been writing exact exists.elim h (by { intro x hx, ... }), but maybe that's considered less elegant.

[Kenny Lau]

yes, that is considered less elegant

[Kevin Buzzard]

Elegance was never my strong point when it came to Lean code.

[Kevin Buzzard]

Lucky I might now have an MSc student who will elegantify my code :D