finset with two elements

Stream: maths

[Kevin Buzzard]

@Morenikeji Neri has proved det(AB)=det(A)det(B) modulo some lemma about switching two rows of a matrix making the sign change, which became a lemma about summing over a set of size 2, which has now been reduced to this:

import data.fintype

open finset

example (α : Type*) [fintype α] [decidable_eq α] (s t : α) (Hdiff : s ≠ t) :
filter (λ a, a = s ∨ a = t) univ = insert s (finset.singleton t) := sorry

This says (if I got it right) that if s and t are two distinct terms, then filtering over the predicate which says "I am s or t" gives me precisely the finset containing s and t (I built it using insert and singleton because there are lemmas like sum_insert and `sum_singleton).

I used to rant a lot about "easy in maths, hard in lean" stuff when I found it very frustrating that there was stuff which was easy in maths but which I found hard in Lean. As I get better at Lean I realise that I'm ranting less and just solving my own problems. But this one looks scary, because a finset is quite a complicated object for me -- I'm not sure I can steer nodup and I'm still quite an amateur when it comes to quotients.

This is about the third post I've written about this problem; the first two I've written, thought "actually I can make progress", and then deleted. But this one still looks scary. Can anyone suggest a way to progress on this?

[Kenny Lau]

import data.fintype

open finset

example (α : Type*) [fintype α] [decidable_eq α] (s t : α) (Hdiff : s ≠ t) :
  filter (λ a, a = s ∨ a = t) univ = insert s (finset.singleton t) :=
ext.2 $ by simp

[Kenny Lau]

import data.fintype

open finset

example (α : Type*) [fintype α] [decidable_eq α] (s t : α) (Hdiff : s ≠ t) :
  filter (λ a, a = s ∨ a = t) univ = insert s (finset.singleton t) :=
by ext; simp

[Kevin Buzzard]

:o

[Kevin Buzzard]

I didn't even think to try simp, because "this was obviously much too complicated for a stupid thing like simp"

[Kevin Buzzard]

Thanks Kenny!

[Kevin Buzzard]

My simp-fu is still very weak.

[Rob Lewis]

I think you don't even need the Hdiff argument!

[Kevin Buzzard]

You might be right -- I didn't check to see what insert did when it was already in.

[Kevin Buzzard]

multiset insert adds another one, I guess that was what scared me off.

[Mario Carneiro]

I would say the moral of the story here is the power of finset extensionality. Finsets are complicatedly defined, but it is not hard to show equalities between finsets because you can just reason about the set that they define

[Kevin Buzzard]

Yes -- it wasn't the simp that was the insight, it was the ext. The proof (of det AB = det A det B) is apparently complete now. Of course it's not remotely mathlib-ready...

[Kevin Buzzard]

By the way, the proof featured:

lemma sum_equiv_classes {α β : Type*} [add_comm_monoid α] [fintype β] (f : β → α)
  (h : setoid β) [decidable_rel h.r] [decidable_eq β] :
finset.sum (@finset.univ β _) f = finset.sum finset.univ
  (λ (x : quotient h), finset.sum (filter (λ b : β, ⟦b⟧ = x) finset.univ) f) :=

which I thought at the time was a good idea, but actually was a pain to apply because I didn't have an equivalence relation on a fintype, I had an equivalence relation on a finset, so there was a certain amount of inelegant scuffling around with ↥↑s at some point. Wouldn't surprise me if I was missing a trick.