{v : Lean.Level} →
  {M : Q(Type v)} →
    (iM : Q(CommGroupWithZero «$M»)) →
      (e₂ : Q(«$M»)) →
        (motive :
            ((y : Q(«$M»)) ×
                ((g : Mathlib.Tactic.FieldSimp.Sign M) ×
                    have a := g.expr y;
                    Q(«$e₂» = «$a»)) ×
                  (l : Mathlib.Tactic.FieldSimp.qNF M) ×
                    have a := l.toNF;
                    Q(«$y» = «$a».eval)) →
              Sort u_1) →
          (__discr :
              (y : Q(«$M»)) ×
                ((g : Mathlib.Tactic.FieldSimp.Sign M) ×
                    have a := g.expr y;
                    Q(«$e₂» = «$a»)) ×
                  (l : Mathlib.Tactic.FieldSimp.qNF M) ×
                    have a := l.toNF;
                    Q(«$y» = «$a».eval)) →
            ((fst : Q(«$M»)) →
                (g₂ : Mathlib.Tactic.FieldSimp.Sign M) →
                  (pf_sgn₂ :
                      have a := g₂.expr fst;
                      Q(«$e₂» = «$a»)) →
                    (l₂ : Mathlib.Tactic.FieldSimp.qNF M) →
                      (pf_l₂ :
                          have a := l₂.toNF;
                          Q(«$fst» = «$a».eval)) →
                        motive ⟨fst, (⟨g₂, pf_sgn₂⟩, ⟨l₂, pf_l₂⟩)⟩) →
              motive __discr