feat: LRAT proof replay (#222)

This is based on a suggestion by @avigad. From the docs:
```lean
lrat_proof foo
  "p cnf 2 4  1 2 0  -1 2 0  1 -2 0  -1 -2 0"
  "5 -2 0 4 3 0  5 d 3 4 0  6 1 0 5 1 0  6 d 1 0  7 0 5 2 6 0"
```
produces the theorem:
```lean
foo : ∀ (a a_1 : Prop), (¬a ∧ ¬a_1 ∨ a ∧ ¬a_1) ∨ ¬a ∧ a_1 ∨ a ∧ a_1
```

There is still some design work to be done on how exactly to make this usable in practice; in particular the generated theorem is always written in DNF, while for a tactic we would generally want to infer the structure from the goal statement instead of the CNF file. The main aim of this implementation is to be as high performance as can be reasonably achieved while still being proof-object-based (there is some definitional unfolding but nothing too heavy). I haven't tried to give it any truly massive proofs yet (I will have to figure out how to run it compiled first), but it seems to hold up reasonably well even on proofs in the 10000 line range.

Author: digama0

Mathlib.lean

@@ -81,6 +81,7 @@ import Mathlib.Tactic.Rename
 import Mathlib.Tactic.Ring
 import Mathlib.Tactic.RunCmd
 import Mathlib.Tactic.RunTac
+import Mathlib.Tactic.Sat.FromLRAT
 import Mathlib.Tactic.ShowTerm
 import Mathlib.Tactic.SimpRw
 import Mathlib.Tactic.Simps