derangements formula (freek 88)

Stream: general

[Henry Swanson]

Hello! It took me quite a while, because I struggled a lot with equivalences, but I have a proof of the derangement formula! https://pastebin.com/Mvx1TE2Y

This is a super rough draft -- lemme know if there's anything else I should do prior to making a PR. I'm mostly just stoked to have a sorry-free proof finally. I plan to:

• rename a bunch of lemmas to be more Lean-conventional
• try to turn those apply equiv.trans sections into calc blocks
• look for more small lemmas to extract, some of these are pretty long
• figure out if equiv_rw can help me here

Also, @Johan Commelin I know you suggested a finset approach, but I couldn't get the proofs of nodup working right. I feel like nodup_perms_of_list is the right kind of thing to pattern off of, but that proof is a bit too dense for me.

[Johan Commelin]

@Henry Swanson congrats!

[Johan Commelin]

Your list of plans looks good. I would add three things before opening a PR:

• update the code to follow the style guide (you have lots of { and } on their own line, but mathlib compresses them like

begin
  split,
  { some_tactic,
    other_tactic },
  { yet_other tactic }

• add docstrings /-- I'm a docstring, I start with two dashes -/ above every definition
• add a module docstring /-! I'm a module doc. I start with dash-bang, and I'm usually > 10 lines long. -/ at the top of the file, explaining what's going on.

[Henry Swanson]

alrighty, that should be straightforward enough

btw, is there a linter? i didn't see one in the vscode extensions, but maybe there's a python script of some sort

[Rémy Degenne]

I you type #lint in the lean file, it will warn you about missing definitions and other issues for all statements in the file above the current line.

[Johan Commelin]

There isn't a style linter though

[Rémy Degenne]

It will not warn you about missing spaces or lone {

[Henry Swanson]

i'm following the instructions on how to contribute to mathlib; can i get permissions to add a new branch? my username is HenrySwanson

[Bryan Gin-ge Chen]

@Henry Swanson invite sent! https://github.com/leanprover-community/mathlib/invitations

[Henry Swanson]

submitted now, thanks! :D