{v : Lean.Level} →
  {M : Q(Type v)} →
    (iM : Q(AddCommMonoid «$M»)) →
      (y : Q(«$M»)) →
        (motive :
            ((u : Lean.Level) ×
                (R : Q(Type u)) ×
                  (iR : Q(Semiring «$R»)) ×
                    (x : Q(Module «$R» «$M»)) ×
                      (l : Mathlib.Tactic.Module.qNF R M) ×
                        let a := l.toNF;
                        Q(«$y» = Mathlib.Tactic.Module.NF.eval unknown_1)) →
              Sort u_1) →
          (__discr :
              (u : Lean.Level) ×
                (R : Q(Type u)) ×
                  (iR : Q(Semiring «$R»)) ×
                    (x : Q(Module «$R» «$M»)) ×
                      (l : Mathlib.Tactic.Module.qNF R M) ×
                        let a := l.toNF;
                        Q(«$y» = Mathlib.Tactic.Module.NF.eval unknown_1)) →
            ((fst : Lean.Level) →
                (fst_1 : Q(Type fst)) →
                  (fst_2 : Q(Semiring «$fst_1»)) →
                    (iRM₀ : Q(Module «$fst_1» «$M»)) →
                      (l₀ : Mathlib.Tactic.Module.qNF fst_1 M) →
                        (pf₀ :
                            let a := l₀.toNF;
                            Q(«$y» = Mathlib.Tactic.Module.NF.eval unknown_1)) →
                          motive ⟨fst, ⟨fst_1, ⟨fst_2, ⟨iRM₀, ⟨l₀, pf₀⟩⟩⟩⟩⟩) →
              motive __discr