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