Using Set Tactics for Finsets

Stream: new members

[Dave Jones]

Using mathlib, I would like to prove a statement for finsets which I am able to establish for (finite) sets.
An illustration is shown here (the interval endpoints are simplified for illustration, but I intend to use expressions for the endpoints in an actual proof):

import tactic
import data.finset.basic

example (n : ℕ) (hn : n ≥ 2) :
(finset.Ico 1 2) ∪ (finset.Icc 2 n) = (finset.Icc 1 n)
:=
begin
  --Prove the statement for sets:
  have h1 : (set.Ico 1 2) ∪ (set.Icc 2 n) = (set.Icc 1 n),
  apply set.Ico_union_Icc_eq_Icc,
  exact one_le_two,
  exact hn,
  --QED

  --How to establish for finsets?
end

I'm not sure how to get from the statement involving set to the statement involving finset.

The motivation for wanting the result on finsets is so that I can go on to prove equalities between "big operator" sums (defined on finsets).

Thank you for any suggestions.

[Ruben Van de Velde]

Are you looking for a general solution or a proof for the interval union statement you mention?

[Ruben Van de Velde]

Because for the latter I'd try looking for similarly named finest lemmas, while the former is slightly harder

[Damiano Testa]

There is docs#finset.coe_inj, but then you still need to "push through" the coercion across your various operations.

[Damiano Testa]

E.g., this concludes your proof:

  refine finset.coe_inj.mp _,
  simp only [finset.coe_union, finset.coe_Icc, finset.coe_Ico, h1],

[Ruben Van de Velde]

Oh nice, I was thinking of set.finite.to_finset, but this is better

[Dave Jones]

@Damiano Testa Thank you so much for the suggestion!
I was trying to solve this through coercions somehow, but was having no luck.
A "push through" coercion solution was just the sort of thing I was expecting to have to do here (but all of my flailing wasn't working).

I'll review this and give this a go once I can get back in front of VS Code.
Thanks again!