Rewriting fin_cases

Stream: mathlib4

[Violeta Hernández]

Is there any tactic like fin_cases that allows rewriting? Specifically, I want to rewrite ∃ x : α, p x as p x₁ ∨ p x₂ ∨ ... within a larger expression.

[Daniel Weber]

There's docs#Fin.sum_univ_three, docs#Fin.sum_univ_four, docs#Fin.sum_univ_five, ..., perhaps you can do something similar for your type (with exists instead of sum)

[Violeta Hernández]

My type in question is Set Prop, which I don't think is quite common enough to justify this special casing