Round trip, case by case: fractions, powers, cases

Lean module Esm.Document.Math.Cases8, formal/Esm/Document/Math/Cases8.lean at 184aa13d35e5
Imports Esm.Document.Math.Cases7

theorem pFracL_quot proved source

theorem pFracL_quot (c : Ctx) (a b : Json) (ha : M c a) (hb : M c b) (rest : List Tok) (f : Nat)
    (hf : need 1 (((pr c a).at c.sf 1).length + ((pr c b).at c.sf 1).length + 3) + 1 ≤ f) :
    pFracL c (f + 1) ((pr c a).at c.sf 1 ++ .kw .rb :: .kw .lb :: ((pr c b).at c.sf 1 ++ .kw .rb :: rest)) =
      some (node "/" [a, b], rest)

After \frac{: an ordinary quotient.

theorem M_pow_of proved source

theorem M_pow_of (c : Ctx) (a b : Json) (ha : M c a) (EX : List Tok)
    (hex : ∀ rest g, 30 * EX.length + 30 ≤ g → pExpo c g (EX ++ rest) = some (b, rest))
    (hpr : pr c (node "^" [a, b]) = mkOut c.sf 8 ((pr c a).at c.sf 9 ++ .kw .caret :: EX)) :
    M c (node "^" [a, b])

The power, once the exponent’s tokens EX are known to read back.

This module also proves 5 lemmas without doc comments; they are in the source.