{v : Lean.Level} →
  {M : Q(Type v)} →
    (iM : Q(CommGroupWithZero «$M»)) →
      (l₁ l₂ : Mathlib.Tactic.FieldSimp.qNF M) →
        ({u : Lean.Level} → (type : Q(Sort u)) → Lean.MetaM Q(«$type»)) →
          (cond : Mathlib.Tactic.FieldSimp.DenomCondition q(inferInstance)) →
            Lean.MetaM
              ((L : Mathlib.Tactic.FieldSimp.qNF M) ×
                (l₁' : Mathlib.Tactic.FieldSimp.qNF M) ×
                  (l₂' : Mathlib.Tactic.FieldSimp.qNF M) ×
                    (have a := l₁.toNF;
                      have a_1 := l₁'.toNF;
                      have a_2 := L.toNF;
                      Q(«$a_2».eval * «$a_1».eval = «$a».eval)) ×
                      (have a := l₂.toNF;
                        have a_1 := l₂'.toNF;
                        have a_2 := L.toNF;
                        Q(«$a_2».eval * «$a_1».eval = «$a».eval)) ×
                        Mathlib.Tactic.FieldSimp.DenomCondition.proof L cond)