Zulip Chat Archive

Stream: general

Topic: how to eliminate a chain of exists

Anas Himmi (May 03 2020 at 15:40):

is there a way to apply the elimination rule quickly on a statement like this in term mode:

h :  a b c d, p

what i use to do is something like :

exists.elim h (λ a h₁,exists.elim h₁ (λ b h₂, exists.elim h₂ (λ c h₃, exists.elim h₃ (λ d hp,_))))

but it's too long and i get these unnecessary h₁ h₂ ...
i know i can do it with match h with |⟨a,b,c,d,hp⟩ := _ end but is it the only way?

Reid Barton (May 03 2020 at 15:42):

For term mode, let ⟨a,b,c,d,hp⟩ := h in _

Kenny Lau (May 03 2020 at 15:42):

for tactic mode, rcases h with \<a, b, c, d, hp\>

Anas Himmi (May 03 2020 at 15:42):

thank you!

Last updated: Aug 03 2023 at 10:10 UTC