Lean4
/-- Given `l : qNF M`, obtain `l' : qNF M` by removing all `l`'s exponent-zero entries where the
corresponding atom can be proved nonzero, and construct a proof that their associated expressions
are equal. -/
def removeZeros (disch : ∀ {u : Level} (type : Q(Sort u)), MetaM Q($type)) (iM : Q(CommGroupWithZero $M)) (l : qNF M) :
MetaM <| Σ l' : qNF M, Q(NF.eval $(l.toNF) = NF.eval $(l'.toNF)) :=
match l with
| [] => return ⟨[], q(rfl)⟩
| ((r, x), i) :: t => do
let ⟨t', pf⟩ ← removeZeros disch iM t
let ⟨l', pf'⟩ ← tryClearZero disch iM r x i t'
let pf' : Q(NF.eval (($r, $x) ::ᵣ $(qNF.toNF t')) = NF.eval $(qNF.toNF l')) := pf'
let pf'' : Q(NF.eval (($r, $x) ::ᵣ $(qNF.toNF t)) = NF.eval $(qNF.toNF l')) :=
q(NF.eval_cons_eq_eval_of_eq_of_eq $r $x $pf $pf')
return ⟨l', pf''⟩
