{v : Lean.Level} →
  {M : Q(Type v)} →
    (iM : Q(CommGroupWithZero «$M»)) →
      (l : Mathlib.Tactic.FieldSimp.qNF M) →
        Lean.MetaM
          ((e : Q(«$M»)) ×
            have a := l.toNF;
            Q(«$a».eval = «$e»))