Formalize refutations: 1692 -> 47, 1832, 2441, 3050, 3456, 4065

[Aaron1011]

This is based on this paper describing a proof strategy for the above non-implications:
https://leanprover.zulipchat.com/#narrow/stream/458659-Equational/topic/Proposed.20new.20target.3A.2063.20and.201692.20.28.22Dupont.20and.20Dupond.22.29/near/477252513

There's still quite a bit of room for cleanup (e.g. factoring out common code from several match branches). It's also very likely that there are simpler ways to prove some of the longer lemmas (e.g. partial_function), as I wasn't working off of the above paper for those proofs. However, this is now in a state where it's ready for review - I'm happy to spend more time minimizing this if it would be useful.

Closes #607

[teorth]

Wow, from two pages of human written notes to 3407 lines of Lean - but perhaps we don't have enough Mathlib support for trees and have to set up quite a bit of API. Given that this is a terminal point in the project (we don't need this machinery to prove anything else in the graph), probably there isn't a strong need to optimize it, so long as it compiles without running out of heartbeats (which has been our basic standard for whether a Lean proof is good enough for our codebase).

One could mention this PR in https://leanprover.zulipchat.com/#narrow/stream/458659-Equational/topic/Proposed.20new.20target.3A.2063.20and.201692.20.28.22Dupont.20and.20Dupond.22.29/near/477252513 to get a few more eyeballs on it.

[pitmonticone]

Thank you very much @Aaron1011 for your PR!

@teorth I believe it can be golfed quite a bit. I'll do it later today.