convert Union on `finset` to finite union

Stream: new members

[Laurent Bartholdi]

I'm stuck trying to expand a Union parameterized by a finset; any suggestions ? I can do one direction, but it's very verbose, all hints welcome! A MNWE is

example (f : fin 3 → set ℕ) : (⋃(i : fin 3), f i) = f 0 ∪ f 1 ∪ f 2 := begin
  ext1,
  split,
{ intro h,
  rw set.mem_Union at h,
  rcases h with ⟨i,x_in_fi⟩,
  sorry },
{ intro h,
  rw [set.mem_union,set.mem_union] at h,
  rw set.mem_Union,
  cases h with h01 h2,
  cases h01 with h0 h1,
  exact ⟨0,h0⟩,
  exact ⟨1,h1⟩,
  exact ⟨2,h2⟩ }
end

[Laurent Bartholdi]

(the 5 lines in the second part can be golfed to exact or.elim h (λ h01, or.elim h01 (λ h, Exists.intro 0 h) (λ h, Exists.intro 1 h)) (λ h, Exists.intro 2 h), but I would hope that lean can do that expansion all by itself)

[Kyle Miller]

There ought to be a tactic for this, but it doesn't seem to have been written yet (it'd be like the ones in algebra/big_operators/norm_num)

Until then, here's a slightly shorter proof:

import tactic.fin_cases

example (f : fin 3 → set ℕ) : (⋃(i : fin 3), f i) = f 0 ∪ f 1 ∪ f 2 :=
begin
  ext,
  simp only [set.mem_Union, set.mem_union],
  split,
  { simp only [forall_exists_index],
    intro i,
    fin_cases i; simp {contextual := tt}, },
  { rintro ((h|h)|h); exact ⟨_, h⟩, },
end

[Jireh Loreaux]

I think there is an open PR for this which probably just needs reviewing.