{v : Lean.Level} →
  {M : Q(Type v)} →
    {iM : Q(CommGroupWithZero «$M»)} →
      (motive : Mathlib.Tactic.FieldSimp.DenomCondition q(inferInstance) → Sort u_1) →
        (x : Mathlib.Tactic.FieldSimp.DenomCondition q(inferInstance)) →
          (Unit → motive Mathlib.Tactic.FieldSimp.DenomCondition.none) →
            (Unit → motive Mathlib.Tactic.FieldSimp.DenomCondition.nonzero) →
              ((iM' : Q(PartialOrder «$M»)) →
                  (iM'' : Q(PosMulStrictMono «$M»)) →
                    (iM''' : Q(PosMulReflectLT «$M»)) →
                      (iM'''' : Q(ZeroLEOneClass «$M»)) →
                        motive (Mathlib.Tactic.FieldSimp.DenomCondition.positive iM' iM'' iM''' iM'''')) →
                motive x