Even Better Parser

[lakesare]

Right now I'm just merging changes from this branch one-by-one using this diff:

https://github.com/Paper-Proof/paperproof/compare/main..even-better-parser

---

I was pushing this to main, but parser requires more care than that 😅

This PR:

• adds some other rwa/nth_rw/etc. rw rules handling
• adds line numbers to the parser output
• refactors the code (not in any meaningful way really, just to make it easier to work with for me - mostly educational refactors. does add some nice things too though!)

As it stands, the new parser sort of works, but doesn't handle rewrites well in this Carleson's lemma e.g.

lemma calculation_1 (s : ℤ) :
    4 * (D : ℝ) ^ (-2 : ℝ) * D ^ (s + 3) = 4 * D ^ (s + 1) := by
  have D_pos : (0 : ℝ) < D := defaultD_pos a
  calc 4 * (D : ℝ) ^ (-2 : ℝ) * D ^ (s + 3)
  _ = 4 * (D ^ (-2 : ℝ) * D ^ (s + 3)) := by
    ring
  _ = 4 * D ^ (-2 + (s + 3)) := by
    congr
    have pow_th := Real.rpow_add (x := (D : ℝ)) (y := (-2)) (z := (s + 3)) D_pos
    rw_mod_cast [pow_th]
  _ = 4 * D ^ (s + 1) := by
    ring_nf

The way to proceed with this PR is to make TEST.lean work, add many test cases, and make sure each of them works when we change stuff.