two finsets of all of fin n are the same

Stream: new members

[Evan Lohn]

I wasn't sure how to prove the following:

import data.finset.basic

def rowindset : finset (fin 4) := list.to_finset [fin.of_nat 0, fin.of_nat 1, fin.of_nat 2, fin.of_nat 3]
example {r0 r1 r2 r3 : fin 4}
  (h1 : r0 ≠ r1)
  (h2 : r0 ≠ r2 ∧ r1 ≠ r2)
  (h3 : r0 ≠ r3 ∧ r1 ≠ r3 ∧ r2 ≠ r3) :
  rowindset = [r0, r1, r2, r3].to_finset :=
begin
  sorry,
end

essentially "four different elements of fin 4 are the same as the explicitly constructed set of the elements of fin 4". I'd be grateful if someone could point me to relevant lemmas and/or weirdness in my definition!

[Anne Baanen]

Since there are finitely many options and we can compute with fin, you can ask Lean to check all possibilities:

example : ∀ {r0 r1 r2 r3 : fin 4}
  (h1 : r0 ≠ r1)
  (h2 : r0 ≠ r2 ∧ r1 ≠ r2)
  (h3 : r0 ≠ r3 ∧ r1 ≠ r3 ∧ r2 ≠ r3),
  rowindset = [r0, r1, r2, r3].to_finset :=
by dec_trivial

[Anne Baanen]

Of course that doesn't scale to lots of fins :)

[Evan Lohn]

Thanks! Not sure if it's my version of Lean or mathlib that's causing this problem, but I had to use the exclam version dec_trivial! for some reason.

[Johan Commelin]

Note that Anne put all the assumptions in the goal (that is, right of the :)

[Johan Commelin]

dec_trivial! tries to do that for you.

[Anne Baanen]

I didn't even realize that dec_trivial! existed :grinning:

[Kevin Buzzard]

Whenever a tactic I try doesn't work, I always append an exclamation mark and try again ;-)