{v : Lean.Level} →
  {M : Q(Type v)} →
    (iM : Q(CommGroupWithZero «$M»)) →
      (t : List ((ℤ × Q(«$M»)) × ℕ)) →
        (motive :
            ((l_n : Mathlib.Tactic.FieldSimp.qNF M) ×
                (l_d : Mathlib.Tactic.FieldSimp.qNF M) ×
                  let a := l_d.toNF;
                  let a_1 := l_n.toNF;
                  let a_2 := Mathlib.Tactic.FieldSimp.qNF.toNF t;
                  Q(Mathlib.Tactic.FieldSimp.NF.eval unknown_1 =
                      Mathlib.Tactic.FieldSimp.NF.eval unknown_2 / Mathlib.Tactic.FieldSimp.NF.eval unknown_3)) →
              Sort u_1) →
          (__discr :
              (l_n : Mathlib.Tactic.FieldSimp.qNF M) ×
                (l_d : Mathlib.Tactic.FieldSimp.qNF M) ×
                  let a := l_d.toNF;
                  let a_1 := l_n.toNF;
                  let a_2 := Mathlib.Tactic.FieldSimp.qNF.toNF t;
                  Q(Mathlib.Tactic.FieldSimp.NF.eval unknown_1 =
                      Mathlib.Tactic.FieldSimp.NF.eval unknown_2 / Mathlib.Tactic.FieldSimp.NF.eval unknown_3)) →
            ((t_n t_d : Mathlib.Tactic.FieldSimp.qNF M) →
                (pf :
                    let a := t_d.toNF;
                    let a_1 := t_n.toNF;
                    let a_2 := Mathlib.Tactic.FieldSimp.qNF.toNF t;
                    Q(Mathlib.Tactic.FieldSimp.NF.eval unknown_1 =
                        Mathlib.Tactic.FieldSimp.NF.eval unknown_2 / Mathlib.Tactic.FieldSimp.NF.eval unknown_3)) →
                  motive ⟨t_n, ⟨t_d, pf⟩⟩) →
              motive __discr